Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support const evaulation #596

Closed
wants to merge 17 commits into from
Closed

Support const evaulation #596

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
eea70d6
Basic support for unevaluated const expressions
hayashi-stl Aug 19, 2020
58fb4ff
Merge branch 'master' of https://github.com/josh65536/chalk
hayashi-stl Aug 19, 2020
e0748ad
Code formatting and unevaluated const formatting
hayashi-stl Aug 19, 2020
69623ba
Fixed tests
hayashi-stl Aug 19, 2020
b4684d0
Added newline, deleted unnecessary try_eval functions
hayashi-stl Aug 20, 2020
f4cd784
Added comments on tests
hayashi-stl Aug 21, 2020
f2ca1db
Moved UnevaluatedConstData to chalk-integration
hayashi-stl Aug 21, 2020
d767d7e
Removed const_eq for unevaluated consts. Rip reflexivity for now.
hayashi-stl Aug 28, 2020
6a6a68f
Merge branch 'master' of https://github.com/rust-lang/chalk
hayashi-stl Aug 30, 2020
3389719
Fixed tests
hayashi-stl Aug 19, 2020
bce9291
Added newline, deleted unnecessary try_eval functions
hayashi-stl Aug 20, 2020
0b603f9
Added comments on tests
hayashi-stl Aug 21, 2020
d4ee9a3
Moved UnevaluatedConstData to chalk-integration
hayashi-stl Aug 21, 2020
d05b66c
Removed const_eq for unevaluated consts. Rip reflexivity for now.
hayashi-stl Aug 28, 2020
60da39c
Disabled coherence in failing test and fixed comments in coherence tests
hayashi-stl Aug 30, 2020
1c38d7c
Oops, merge conflicts
hayashi-stl Aug 30, 2020
e048d93
Deduplicated some logic and fixed a test
hayashi-stl Aug 30, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,3 +12,4 @@ chalk-parse/src/parser.rs

## IDE files
/.idea/
/.vscode/
4 changes: 1 addition & 3 deletions chalk-engine/src/slg.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -505,9 +505,7 @@ impl<I: Interner> MayInvalidate<'_, I> {
}

(ConstValue::Unevaluated(u1), ConstValue::Unevaluated(u2)) => {
if u1.const_eq(new_ty, u2, interner) {
false
} else if let (Ok(c1), Ok(c2)) = (
if let (Ok(c1), Ok(c2)) = (
u1.try_eval(new_ty, interner),
u2.try_eval(current_ty, interner),
) {
Expand Down
26 changes: 13 additions & 13 deletions chalk-engine/src/slg/aggregate.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -502,22 +502,22 @@ impl<I: Interner> AntiUnifier<'_, '_, I> {
}

(ConstValue::Unevaluated(u1), ConstValue::Unevaluated(u2)) => {
if u1.const_eq(&ty, u2, interner) {
c1.clone()
} else if let (Ok(e1), Ok(e2)) =
(u1.try_eval(&ty, interner), u2.try_eval(&ty, interner))
{
if e1.const_eq(&ty, &e2, interner) {
ConstData {
ty: ty.clone(),
value: ConstValue::Concrete(e1),
match (u1.try_eval(&ty, interner), u2.try_eval(&ty, interner)) {
(Ok(e1), Ok(e2)) => {
if e1.const_eq(&ty, &e2, interner) {
ConstData {
ty: ty.clone(),
value: ConstValue::Concrete(e1),
}
.intern(interner)
} else {
self.new_const_variable(ty)
}
.intern(interner)
} else {
}

(Err(ConstEvalError::TooGeneric), _) | (_, Err(ConstEvalError::TooGeneric)) => {
self.new_const_variable(ty)
}
} else {
self.new_const_variable(ty)
}
}

Expand Down
27 changes: 11 additions & 16 deletions chalk-engine/src/slg/resolvent.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ use tracing::{debug, instrument};
//
// Then:
//
// S(A :- D | L1...Li-1, L1'...L'm, Li+1...Ln)
// S(A :- D | L1...Li-1, L'1...L'm, Li+1...Ln)
//
// is the SLG resolvent of G with C.

Expand Down Expand Up @@ -521,25 +521,20 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
}

(ConstValue::Unevaluated(u1), ConstValue::Unevaluated(u2)) => {
if u1.const_eq(answer_ty, u2, interner) {
Ok(())
} else {
match (
u1.try_eval(answer_ty, interner),
u2.try_eval(answer_ty, interner),
) {
(Ok(ev1), Ok(ev2)) => {
assert!(ev1.const_eq(answer_ty, &ev2, interner));
Ok(())
}

(Err(ConstEvalError::TooGeneric), _)
| (_, Err(ConstEvalError::TooGeneric)) => panic!(
match (
u1.try_eval(answer_ty, interner),
u2.try_eval(answer_ty, interner),
) {
(Ok(c1), Ok(c2)) => assert!(c1.const_eq(answer_ty, &c2, interner)),

(Err(ConstEvalError::TooGeneric), _) | (_, Err(ConstEvalError::TooGeneric)) => {
panic!(
"structural mismatch between answer `{:?}` and pending goal `{:?}`",
answer, pending,
),
)
}
}
Ok(())
}

(ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => panic!(
Expand Down
9 changes: 0 additions & 9 deletions chalk-integration/src/interner.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -258,15 +258,6 @@ impl Interner for ChalkIr {
c1 == c2
}

fn unevaluated_const_eq(
&self,
_ty: &Arc<TyData<ChalkIr>>,
c1: &UnevaluatedConstData,
c2: &UnevaluatedConstData,
) -> bool {
c1 == c2
}

fn try_eval_const(
&self,
_ty: &Arc<TyData<ChalkIr>>,
Expand Down
8 changes: 0 additions & 8 deletions chalk-ir/src/interner.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -473,14 +473,6 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
c2: &Self::InternedConcreteConst,
) -> bool;

/// Determine whether two unevaluated const expressions are equal.
fn unevaluated_const_eq(
&self,
ty: &Self::InternedType,
c1: &Self::InternedUnevaluatedConst,
c2: &Self::InternedUnevaluatedConst,
) -> bool;

/// Attempt to evaluate a const to a concrete const.
fn try_eval_const(
&self,
Expand Down
5 changes: 0 additions & 5 deletions chalk-ir/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1004,11 +1004,6 @@ impl<I: Interner> UnevaluatedConst<I> {
interned: interner.try_eval_const(&ty.interned, &self.interned)?,
})
}

/// Checks whether two unevaluated constants are equal.
pub fn const_eq(&self, ty: &Ty<I>, other: &UnevaluatedConst<I>, interner: &I) -> bool {
interner.unevaluated_const_eq(&ty.interned, &self.interned, &other.interned)
}
}

/// An error that can occur when evaluating a const expression.
Expand Down
27 changes: 12 additions & 15 deletions chalk-solve/src/infer/unify.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -464,25 +464,22 @@ impl<'t, I: Interner> Unifier<'t, I> {
}

(&ConstValue::Unevaluated(ref expr1), &ConstValue::Unevaluated(ref expr2)) => {
hayashi-stl marked this conversation as resolved.
Show resolved Hide resolved
if expr1.const_eq(a_ty, expr2, interner) {
Ok(())
} else {
match (expr1.try_eval(a_ty, interner), expr2.try_eval(b_ty, interner)) {
(Ok(ev1), Ok(ev2)) if ev1.const_eq(a_ty, &ev2, interner) => Ok(()),
(Ok(_), Ok(_)) => Err(NoSolution),
(Err(ConstEvalError::TooGeneric), _) | (_, Err(ConstEvalError::TooGeneric)) => Ok(
self.goals.push(InEnvironment::new(
self.environment,
GoalData::CannotProve.intern(interner)
))
)
}
match (expr1.try_eval(a_ty, interner), expr2.try_eval(b_ty, interner)) {
(Ok(ev1), Ok(ev2)) if ev1.const_eq(a_ty, &ev2, interner) => Ok(()),
(Ok(_), Ok(_)) => Err(NoSolution),
(Err(ConstEvalError::TooGeneric), _) | (_, Err(ConstEvalError::TooGeneric)) => Ok(
self.goals.push(InEnvironment::new(
self.environment,
GoalData::CannotProve.intern(interner)
))
)
}
}

(&ConstValue::Concrete(_), &ConstValue::Placeholder(_))
| (&ConstValue::Placeholder(_), &ConstValue::Concrete(_))
| (&ConstValue::Unevaluated(_), &ConstValue::Placeholder(_))
| (&ConstValue::Placeholder(_), &ConstValue::Concrete(_)) => Err(NoSolution),

(&ConstValue::Unevaluated(_), &ConstValue::Placeholder(_))
| (&ConstValue::Placeholder(_), &ConstValue::Unevaluated(_)) => Err(NoSolution),

(ConstValue::BoundVar(_), _) | (_, ConstValue::BoundVar(_)) => panic!(
Expand Down
85 changes: 48 additions & 37 deletions tests/test/coherence.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -517,17 +517,22 @@ fn orphan_check() {
}
}

#[test]
fn unevaluated_const_unknown() {
lowering_success! {
program {
trait Foo<const N> {}
struct Baz {}

impl Foo<?> for Baz {}
}
}
}
// FIXME: The following test fails by violation of the orphan rules.
// This is because right now, unevaluated const expressions have a
// temporary reflexivity hole, where ? != ?,
// which messes with the SLG resolvent.
// The test should be uncommented when the reflexivity hole is fixed.
hayashi-stl marked this conversation as resolved.
Show resolved Hide resolved
//#[test]
//fn unevaluated_const_unknown() {
// lowering_success! {
// program {
// trait Foo<const N> {}
// struct Baz {}
//
// impl Foo<?> for Baz {}
// }
// }
//}

#[test]
fn unevaluated_const_no_intersect() {
Expand Down Expand Up @@ -579,29 +584,35 @@ fn unevaluated_const_intersect() {
}
}

#[test]
fn unevaluated_const_too_generic() {
lowering_error! {
program {
trait Foo<const N> { }
struct Baz { }

impl Foo<3> for Baz {}
impl Foo<?> for Baz {}
} error_msg {
"overlapping impls of trait `Foo`"
}
}

lowering_error! {
program {
trait Foo<const N> { }
struct Baz { }

impl Foo<3?> for Baz {}
impl Foo<?> for Baz {}
} error_msg {
"overlapping impls of trait `Foo`"
}
}
}
// FIXME: The following test fails by violation of the orphan rules.
// This is because right now, unevaluated const expressions have a
// temporary reflexivity hole, where ? != ?,
// which messes with the SLG resolvent.
// The test should be uncommented when the reflexivity hole is fixed.
// It is supposed to fail because of overlapping impls.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See above. What error do we get here if we leave these uncommented? With these, we actually don't know that these are overlapping impls (could impl Foo<3> and impl Foo<4>). But this still shouldn't lower successfully.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right now it's structural mismatch between answer '?' and pending goal '?'. Is the resolvent allowed to create a CannotProve goal? Also, in the case where chalk can't prove that impls don't overlap, it assumes that they do.

//#[test]
//fn unevaluated_const_too_generic() {
// lowering_error! {
// program {
// trait Foo<const N> { }
// struct Baz { }
//
// impl Foo<3> for Baz {}
// impl Foo<?> for Baz {}
// } error_msg {
// "overlapping impls of trait `Foo`"
// }
// }
//
// lowering_error! {
// program {
// trait Foo<const N> { }
// struct Baz { }
//
// impl Foo<3?> for Baz {}
// impl Foo<?> for Baz {}
// } error_msg {
// "overlapping impls of trait `Foo`"
// }
// }
//}
84 changes: 49 additions & 35 deletions tests/test/constants.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -188,41 +188,55 @@ fn unevaluated_impl() {
}
}

#[test]
fn unevaluated_impl_generic() {
test! {
program {
struct S<const N> {}

trait Trait {}

impl Trait for S<?> {}
}

// Tests unification of unknown unevaluated const and evaluated const
goal {
S<0>: Trait
} yields {
"Ambiguous; no inference guidance"
}

// Tests unification of two unknown unevaluated consts
goal {
S<?>: Trait
} yields {
"Unique"
}

// Tests unification of unknown unevaluated const and placeholder const
goal {
exists<const N> {
S<N>: Trait
}
} yields {
"Unique; substitution [?0 := ?], lifetime constraints []"
}
}
}
// FIXME: This won't even lower
// because `impl Trait for S<?>` fails the orphan rules
// because `LocalImplAllowed(S<?>: Trait)` can't be proven
// because `?` != `?`.
hayashi-stl marked this conversation as resolved.
Show resolved Hide resolved
//#[test]
//fn unevaluated_impl_generic() {
// test! {
// program {
// struct S<const N> {}
//
// trait Trait {}
//
// impl Trait for S<?> {}
// }
//
// // Tests unification of unknown unevaluated const and evaluated const
// goal {
// S<0>: Trait
// } yields {
// "Ambiguous; no inference guidance"
// }
//
// // Tests unification of two unknown unevaluated consts
// goal {
// S<?>: Trait
// } yields {
// "Ambiguous; no inference guidance"
// }
//
// // Tests unification of unknown unevaluated const and inference var
// // We don't know if ? evaluates to a valid const, so even this is ambiguous
// goal {
// exists<const N> {
// S<N>: Trait
// }
// } yields {
// "Ambiguous; no inference guidance"
// }
//
// // Tests unification of unknown unevaluated const and placeholder const
// goal {
// forall<const N> {
// S<N>: Trait
// }
// } yields {
// "No possible solution"
// }
// }
//}

#[test]
fn placeholders_eq() {
Expand Down