add more tests, rewrite equals notation

Author: nikomatsakis

crates/formality-prove/src/program.rs

@@ -55,6 +55,16 @@ impl Program {
             .flat_map(|td| td.trait_invariants())
             .collect()
     }
+
+    pub fn empty() -> Self {
+        Self {
+            max_size: Program::DEFAULT_MAX_SIZE,
+            trait_decls: vec![],
+            impl_decls: vec![],
+            alias_eq_decls: vec![],
+            alias_bound_decls: vec![],
+        }
+    }
 }
 
 #[term(impl $binder)]

crates/formality-prove/src/test/occurs_check.rs

@@ -20,20 +20,41 @@ fn program() -> Program {
 /// Test that `X = Vec<X>` cannot be solved
 #[test]
 fn direct_cycle() {
-    let constraints = test_prove(program(), term("<ty A> ({}, {equals(A, Vec<A>)})"));
+    let constraints = test_prove(program(), term("<ty A> ({}, {A = Vec<A>})"));
     expect![[r#"
         {}
     "#]]
     .assert_debug_eq(&constraints);
 }
 
+/// Test that `X = Vec<Y>` can be solved
+#[test]
+fn eq_variable_to_rigid() {
+    let constraints = test_prove(program(), term("<ty X, ty Y> ({}, {X = Vec<Y>})"));
+    expect![[r#"
+        {
+            <> Constraints { known_true: true, substitution: Substitution { map: {?ty_0: (rigid (adt Vec) ?ty_1)} } },
+        }
+    "#]]
+    .assert_debug_eq(&constraints);
+}
+
+/// Test that `Vec<Y> = X` can be solved
+#[test]
+fn eq_rigid_to_variable() {
+    let constraints = test_prove(program(), term("<ty X, ty Y> ({}, {Vec<Y> = X})"));
+    expect![[r#"
+        {
+            <> Constraints { known_true: true, substitution: Substitution { map: {?ty_0: (rigid (adt Vec) ?ty_1)} } },
+        }
+    "#]]
+    .assert_debug_eq(&constraints);
+}
+
 /// Test that `X = Vec<X>` cannot be solved (when constructed over several steps)
 #[test]
 fn indirect_cycle_1() {
-    let constraints = test_prove(
-        program(),
-        term("<ty A, ty B> ({}, {equals(A, Vec<B>), equals(B, A)})"),
-    );
+    let constraints = test_prove(program(), term("<ty A, ty B> ({}, {A = Vec<B>, B = A})"));
     expect![[r#"
         {}
     "#]]
@@ -43,10 +64,7 @@ fn indirect_cycle_1() {
 /// Test that `X = Vec<X>` cannot be solved (when constructed over several steps)
 #[test]
 fn indirect_cycle_2() {
-    let constraints = test_prove(
-        program(),
-        term("<ty A, ty B> ({}, {equals(B, A), equals(A, Vec<B>)})"),
-    );
+    let constraints = test_prove(program(), term("<ty A, ty B> ({}, {B = A, A = Vec<B>})"));
     expect![[r#"
         {}
     "#]]

crates/formality-prove/src/test/universes.rs

@@ -4,23 +4,33 @@ use formality_types::parse::term;
 
 use crate::program::Program;
 
-/// Simple example program consisting only of two trait declarations.
-fn program() -> Program {
-    Program {
-        max_size: Program::DEFAULT_MAX_SIZE,
-        trait_decls: vec![],
-        impl_decls: vec![],
-        alias_eq_decls: vec![],
-        alias_bound_decls: vec![],
-    }
-}
-
 /// There is no U that is equal to all T.
 #[test]
 fn exists_u_for_t() {
-    let constraints = super::test_prove(program(), term("<ty U> ({}, {for<ty T> equals(T, U)})"));
+    let program = Program::empty();
+    let constraints = super::test_prove(program, term("<ty U> ({}, {for<ty T> T = U})"));
     expect![[r#"
             {}
         "#]]
     .assert_debug_eq(&constraints);
 }
+
+/// There is U that is equal to some T.
+#[test]
+fn for_t_exists_u() {
+    let program = Program {
+        max_size: Program::DEFAULT_MAX_SIZE,
+        trait_decls: vec![term("trait Test<ty Self, ty T> where {}")],
+        impl_decls: vec![term("impl<ty X, ty Y> Test(X, Y) where {X = Y}")],
+        alias_eq_decls: vec![],
+        alias_bound_decls: vec![],
+    };
+
+    let constraints = super::test_prove(program, term("<> ({}, {for<ty T> Test(T, T)})"));
+    expect![[r#"
+        {
+            <> Constraints { known_true: true, substitution: Substitution { map: {} } },
+        }
+    "#]]
+    .assert_debug_eq(&constraints);
+}

crates/formality-types/src/grammar/formulas.rs

@@ -189,19 +189,15 @@ impl AdtId {
 /// Relations are built-in goals which are implemented in custom Rust logic.
 #[term]
 pub enum AtomicRelation {
-    /// `T1 == T2` etc
-    #[grammar($v0 == $v1)]
+    #[grammar($v0 = $v1)]
     Equals(Parameter, Parameter),
 
-    /// `T1 <: T2` or `L1 <: L2`
     #[grammar($v0 <: $v1)]
     Sub(Parameter, Parameter),
 
-    /// `P : P`
     #[grammar($v0 : $v1)]
     Outlives(Parameter, Parameter),
 
-    /// `WF(Parameter)`
     #[grammar(@wf($v0))]
     WellFormed(Parameter),
 }