diff options
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/infer/test.rs')
| -rw-r--r-- | vendor/chalk-solve-0.87.0/src/infer/test.rs | 422 |
1 files changed, 0 insertions, 422 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/infer/test.rs b/vendor/chalk-solve-0.87.0/src/infer/test.rs deleted file mode 100644 index 2ac35f027..000000000 --- a/vendor/chalk-solve-0.87.0/src/infer/test.rs +++ /dev/null @@ -1,422 +0,0 @@ -#![cfg(test)] - -use super::unify::RelationResult; -use super::*; -use chalk_integration::interner::ChalkIr; -use chalk_integration::{arg, lifetime, ty}; - -// We just use a vec of 20 `Invariant`, since this is zipped and no substs are -// longer than this -#[derive(Debug)] -struct TestDatabase; -impl UnificationDatabase<ChalkIr> for TestDatabase { - fn fn_def_variance(&self, _fn_def_id: FnDefId<ChalkIr>) -> Variances<ChalkIr> { - Variances::from_iter(ChalkIr, [Variance::Invariant; 20].iter().copied()) - } - - fn adt_variance(&self, _adt_id: AdtId<ChalkIr>) -> Variances<ChalkIr> { - Variances::from_iter(ChalkIr, [Variance::Invariant; 20].iter().copied()) - } -} - -#[test] -fn universe_error() { - // exists(A -> forall(X -> A = X)) ---> error - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(placeholder 1), - ) - .unwrap_err(); -} - -#[test] -fn cycle_error() { - // exists(A -> A = foo A) ---> error - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(apply (item 0) (expr a)), - ) - .unwrap_err(); - - // exists(A -> A = for<'a> A) - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(function 1 (infer 0)), - ) - .unwrap_err(); -} - -#[test] -fn cycle_indirect() { - // exists(A -> A = foo B, A = B) ---> error - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - let b = table.new_variable(U0).to_ty(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(apply (item 0) (expr b)), - ) - .unwrap(); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &b, - ) - .unwrap_err(); -} - -#[test] -fn universe_error_indirect_1() { - // exists(A -> forall(X -> exists(B -> B = X, A = B))) ---> error - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - let b = table.new_variable(U1).to_ty(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &b, - &ty!(placeholder 1), - ) - .unwrap(); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &b, - ) - .unwrap_err(); -} - -#[test] -fn universe_error_indirect_2() { - // exists(A -> forall(X -> exists(B -> B = A, B = X))) ---> error - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - let b = table.new_variable(U1).to_ty(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &b, - ) - .unwrap(); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &b, - &ty!(placeholder 1), - ) - .unwrap_err(); -} - -#[test] -fn universe_promote() { - // exists(A -> forall(X -> exists(B -> A = foo(B), A = foo(i32)))) ---> OK - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - let b = table.new_variable(U1).to_ty(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(apply (item 0) (expr b)), - ) - .unwrap(); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(apply (item 0) (apply (item 1))), - ) - .unwrap(); -} - -#[test] -fn universe_promote_bad() { - // exists(A -> forall(X -> exists(B -> A = foo(B), B = X))) ---> error - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - let b = table.new_variable(U1).to_ty(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(apply (item 0) (expr b)), - ) - .unwrap(); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &b, - &ty!(placeholder 1), - ) - .unwrap_err(); -} - -#[test] -fn projection_eq() { - // exists(A -> A = Item0<<A as Item1>::foo>) - // ^^^^^^^^^^^^ Can A repeat here? For now, - // we say no, but it's an interesting question. - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - - // expect an error ("cycle during unification") - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(apply (item 0) (projection (item 1) (expr a))), - ) - .unwrap_err(); -} - -const U0: UniverseIndex = UniverseIndex { counter: 0 }; -const U1: UniverseIndex = UniverseIndex { counter: 1 }; -const U2: UniverseIndex = UniverseIndex { counter: 2 }; - -fn make_table() -> InferenceTable<ChalkIr> { - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let _ = table.new_universe(); // U1 - let _ = table.new_universe(); // U2 - table -} - -#[test] -fn quantify_simple() { - let interner = ChalkIr; - let mut table = make_table(); - let _ = table.new_variable(U0); - let _ = table.new_variable(U1); - let _ = table.new_variable(U2); - - assert_eq!( - table - .canonicalize(interner, ty!(apply (item 0) (infer 2) (infer 1) (infer 0))) - .quantified, - Canonical { - value: ty!(apply (item 0) (bound 0) (bound 1) (bound 2)), - binders: CanonicalVarKinds::from_iter( - interner, - vec![ - CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U2), - CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U1), - CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0), - ] - ), - } - ); -} - -#[test] -fn quantify_bound() { - let interner = ChalkIr; - let mut table = make_table(); - let environment0 = Environment::new(interner); - - let v0 = table.new_variable(U0).to_ty(interner); - let v1 = table.new_variable(U1).to_ty(interner); - let v2a = table.new_variable(U2).to_ty(interner); - let v2b = table.new_variable(U2).to_ty(interner); - - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &v2b, - &ty!(apply (item 1) (expr v1) (expr v0)), - ) - .unwrap(); - - assert_eq!( - table - .canonicalize( - interner, - ty!(apply (item 0) (expr v2b) (expr v2a) (expr v1) (expr v0)) - ) - .quantified, - Canonical { - value: ty!(apply (item 0) (apply (item 1) (bound 0) (bound 1)) (bound 2) (bound 0) (bound 1)), - binders: CanonicalVarKinds::from_iter( - interner, - vec![ - CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U1), - CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0), - CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U2), - ] - ), - } - ); -} - -#[test] -fn quantify_ty_under_binder() { - let interner = ChalkIr; - let mut table = make_table(); - let v0 = table.new_variable(U0); - let v1 = table.new_variable(U0); - let _r2 = table.new_variable(U0); - - // Unify v0 and v1. - let environment0 = Environment::new(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &v0.to_ty(interner), - &v1.to_ty(interner), - ) - .unwrap(); - - // Here: the `function` introduces 3 binders, so in the result, - // `(bound 3)` references the first canonicalized inference - // variable. -- note that `infer 0` and `infer 1` have been - // unified above, as well. - assert_eq!( - table - .canonicalize( - interner, - ty!(function 3 (apply (item 0) (bound 1) (infer 0) (infer 1) (lifetime (infer 2)))) - ) - .quantified, - Canonical { - value: ty!(function 3 (apply (item 0) (bound 1) (bound 1 0) (bound 1 0) (lifetime (bound 1 1)))), - binders: CanonicalVarKinds::from_iter( - interner, - vec![ - CanonicalVarKind::new(VariableKind::Ty(TyVariableKind::General), U0), - CanonicalVarKind::new(VariableKind::Lifetime, U0) - ] - ), - } - ); -} - -#[test] -fn lifetime_constraint_indirect() { - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let _ = table.new_universe(); // U1 - - let _t_0 = table.new_variable(U0); - let _l_1 = table.new_variable(U1); - - let environment0 = Environment::new(interner); - - // Here, we unify '?1 (the lifetime variable in universe 1) with - // '!1. - let t_a = ty!(apply (item 0) (lifetime (placeholder 1))); - let t_b = ty!(apply (item 0) (lifetime (infer 1))); - let RelationResult { goals } = table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &t_a, - &t_b, - ) - .unwrap(); - assert!(goals.is_empty()); - - // Here, we try to unify `?0` (the type variable in universe 0) - // with something that involves `'?1`. Since `'?1` has been - // unified with `'!1`, and `'!1` is not visible from universe 0, - // we will replace `'!1` with a new variable `'?2` and introduce a - // (likely unsatisfiable) constraint relating them. - let t_c = ty!(infer 0); - let RelationResult { goals } = table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &t_c, - &t_b, - ) - .unwrap(); - assert_eq!(goals.len(), 2); - assert_eq!( - format!("{:?}", goals[0]), - "InEnvironment { environment: Env([]), goal: \'?2: \'!1_0 }", - ); - assert_eq!( - format!("{:?}", goals[1]), - "InEnvironment { environment: Env([]), goal: \'!1_0: \'?2 }", - ); -} |