add ability to test where-clause, test mirror norm

nikomatsakis · nikomatsakis · commit d3ac31574611 · 2023-03-20T05:53:28.000-04:00
Whoops, we aren't adding the required WF predicates.
Gotta deal with implied bounds.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -14,12 +14,14 @@ expect-test = "1.4.0"
 formality-macros = { version = "0.1.0", path = "crates/formality-macros" }
 formality-core = { version = "0.1.0", path = "crates/formality-core" }
 
+
 [dependencies]
 anyhow = "1"
 clap = { version = "4.0.9", features = ["derive"] }
 formality-rust = { version = "0.1.0", path = "crates/formality-rust" }
 formality-types = { version = "0.1.0", path = "crates/formality-types" }
 formality-check = { version = "0.1.0", path = "crates/formality-check" }
+formality-prove = { version = "0.1.0", path = "crates/formality-prove" }
 
 [workspace]
 members = [
diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
@@ -157,6 +157,7 @@ impl super::Check<'_> {
         Ok(())
     }
 
+    #[context("check_associated_ty_value({impl_value:?})")]
     fn check_associated_ty_value(
         &self,
         impl_env: &Env,
diff --git a/crates/formality-prove/src/lib.rs b/crates/formality-prove/src/lib.rs
@@ -6,7 +6,10 @@ mod prove;
 
 pub use decls::*;
 pub use prove::prove;
+pub use prove::Constraints;
 pub use prove::Env;
 
 #[cfg(test)]
 mod test;
+
+pub mod test_util;
diff --git a/crates/formality-prove/src/test.rs b/crates/formality-prove/src/test.rs
@@ -1,16 +1,3 @@
-use std::sync::Arc;
-
-use formality_macros::term;
-use formality_types::{
-    collections::Set,
-    grammar::{Binder, Wcs},
-};
-
-use crate::{
-    decls::Decls,
-    prove::{prove, Constraints, Env},
-};
-
 mod eq_assumptions;
 mod eq_partial_eq;
 mod exists_constraints;
@@ -20,50 +7,3 @@ mod magic_copy;
 mod occurs_check;
 mod simple_impl;
 mod universes;
-
-#[term]
-enum TestAssertion {
-    #[grammar(coherence_mode $v0)]
-    CoherenceMode(Arc<TestAssertion>),
-    #[grammar(forall $v0)]
-    ForAll(Binder<Arc<TestAssertion>>),
-    #[grammar(exists $v0)]
-    Exists(Binder<Arc<TestAssertion>>),
-    #[grammar($v0 => $v1)]
-    Prove(Wcs, Wcs),
-}
-
-/// `t` represents some set of existential bindings combined with (assumptions, goals).
-/// Returns the constraints that result from proving assumptions/goals. These will reference
-/// existential variables created for the bindings, so they're really just suitable for
-/// using with expect.
-fn test_prove(decls: Decls, mut assertion: Arc<TestAssertion>) -> Set<Constraints> {
-    let mut env = Env::default();
-
-    loop {
-        match &*assertion {
-            TestAssertion::ForAll(binder) => {
-                let (env1, subst) = env.universal_substitution(binder);
-                let assertion1 = binder.instantiate_with(&subst).unwrap();
-                env = env1;
-                assertion = assertion1;
-            }
-
-            TestAssertion::Exists(binder) => {
-                let (env1, subst) = env.existential_substitution(binder);
-                let assertion1 = binder.instantiate_with(&subst).unwrap();
-                env = env1;
-                assertion = assertion1;
-            }
-
-            TestAssertion::Prove(assumptions, goals) => {
-                return prove(decls, env, assumptions, goals);
-            }
-
-            TestAssertion::CoherenceMode(assertion1) => {
-                env = env.with_coherence_mode(true);
-                assertion = assertion1.clone();
-            }
-        }
-    }
-}
diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs
@@ -4,7 +4,7 @@ use formality_types::parse::term;
 
 use crate::decls::Decls;
 
-use super::test_prove;
+use crate::test_util::test_prove;
 
 #[test]
 fn test_a() {
diff --git a/crates/formality-prove/src/test/exists_constraints.rs b/crates/formality-prove/src/test/exists_constraints.rs
@@ -4,7 +4,7 @@ use formality_types::parse::term;
 
 use crate::decls::Decls;
 
-use super::test_prove;
+use crate::test_util::test_prove;
 
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
diff --git a/crates/formality-prove/src/test/expanding.rs b/crates/formality-prove/src/test/expanding.rs
@@ -2,7 +2,7 @@ use expect_test::expect;
 use formality_macros::test;
 use formality_types::parse::term;
 
-use crate::decls::Decls;
+use crate::{test_util::test_prove, Decls};
 
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
@@ -17,7 +17,7 @@ fn decls() -> Decls {
 /// There is no U that is equal to all T.
 #[test]
 fn expanding() {
-    let constraints = super::test_prove(decls(), term("exists<ty T> {} => {Debug(T)}"));
+    let constraints = test_prove(decls(), term("exists<ty T> {} => {Debug(T)}"));
     expect![[r#"
         {
             Constraints {
diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs
@@ -4,7 +4,7 @@ use formality_types::parse::term;
 
 use crate::decls::Decls;
 
-use super::test_prove;
+use crate::test_util::test_prove;
 
 #[test]
 fn test_forall_not_local() {
diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs
@@ -4,7 +4,7 @@ use formality_types::parse::term;
 
 use crate::decls::Decls;
 
-use super::test_prove;
+use crate::test_util::test_prove;
 
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs
@@ -4,7 +4,7 @@ use formality_types::parse::term;
 
 use crate::decls::Decls;
 
-use super::test_prove;
+use crate::test_util::test_prove;
 
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs
@@ -4,11 +4,13 @@ use formality_types::parse::term;
 
 use crate::decls::Decls;
 
+use crate::test_util::test_prove;
+
 /// There is no U that is equal to all T.
 #[test]
 fn exists_u_for_t() {
     let decls = Decls::empty();
-    let constraints = super::test_prove(decls, term("exists<ty U> {} => {for<ty T> T = U}"));
+    let constraints = test_prove(decls, term("exists<ty U> {} => {for<ty T> T = U}"));
     expect![[r#"
             {}
         "#]]
@@ -24,7 +26,7 @@ fn for_t_exists_u() {
         ..Decls::empty()
     };
 
-    let constraints = super::test_prove(decls, term("{} => {for<ty T> Test(T, T)}"));
+    let constraints = test_prove(decls, term("{} => {for<ty T> Test(T, T)}"));
     expect![[r#"
         {
             Constraints {
diff --git a/crates/formality-prove/src/test_util.rs b/crates/formality-prove/src/test_util.rs
@@ -0,0 +1,60 @@
+use std::sync::Arc;
+
+use formality_macros::term;
+use formality_types::{
+    collections::Set,
+    grammar::{Binder, Wcs},
+};
+
+use crate::{
+    decls::Decls,
+    prove::{prove, Constraints, Env},
+};
+
+/// Useful assertions for use in tests.
+#[term]
+pub enum TestAssertion {
+    #[grammar(coherence_mode $v0)]
+    CoherenceMode(Arc<TestAssertion>),
+    #[grammar(forall $v0)]
+    ForAll(Binder<Arc<TestAssertion>>),
+    #[grammar(exists $v0)]
+    Exists(Binder<Arc<TestAssertion>>),
+    #[grammar($v0 => $v1)]
+    Prove(Wcs, Wcs),
+}
+
+/// `t` represents some set of existential bindings combined with (assumptions, goals).
+/// Returns the constraints that result from proving assumptions/goals. These will reference
+/// existential variables created for the bindings, so they're really just suitable for
+/// using with expect.
+pub fn test_prove(decls: Decls, mut assertion: Arc<TestAssertion>) -> Set<Constraints> {
+    let mut env = Env::default();
+
+    loop {
+        match &*assertion {
+            TestAssertion::ForAll(binder) => {
+                let (env1, subst) = env.universal_substitution(binder);
+                let assertion1 = binder.instantiate_with(&subst).unwrap();
+                env = env1;
+                assertion = assertion1;
+            }
+
+            TestAssertion::Exists(binder) => {
+                let (env1, subst) = env.existential_substitution(binder);
+                let assertion1 = binder.instantiate_with(&subst).unwrap();
+                env = env1;
+                assertion = assertion1;
+            }
+
+            TestAssertion::Prove(assumptions, goals) => {
+                return prove(decls, env, assumptions, goals);
+            }
+
+            TestAssertion::CoherenceMode(assertion1) => {
+                env = env.with_coherence_mode(true);
+                assertion = assertion1.clone();
+            }
+        }
+    }
+}
diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs
@@ -227,7 +227,7 @@ pub enum FnBody {
     MirFnBody(MirFnBody),
 }
 
-#[term(type $id $binder)]
+#[term(type $id $binder ;)]
 pub struct AssociatedTy {
     pub id: AssociatedItemId,
     pub binder: Binder<AssociatedTyBoundData>,
@@ -283,13 +283,13 @@ pub enum ImplItem {
     AssociatedTyValue(AssociatedTyValue),
 }
 
-#[term(type $id $binder)]
+#[term(type $id $binder ;)]
 pub struct AssociatedTyValue {
     pub id: AssociatedItemId,
     pub binder: Binder<AssociatedTyValueBoundData>,
 }
 
-#[term(where $where_clauses = $ty)]
+#[term(= $ty where $where_clauses)]
 pub struct AssociatedTyValueBoundData {
     pub where_clauses: Vec<WhereClause>,
     pub ty: Ty,
diff --git a/src/lib.rs b/src/lib.rs
@@ -1,7 +1,10 @@
+use std::sync::Arc;
+
 use clap::Parser;
 use formality_check::check_all_crates;
+use formality_prove::{test_util::TestAssertion, Constraints};
 use formality_rust::grammar::Program;
-use formality_types::parse::term;
+use formality_types::{collections::Set, parse::term};
 
 #[derive(Parser, Debug)]
 #[command(author, version, about, long_about = None)]
@@ -28,3 +31,11 @@ pub fn test_program_ok(input: &str) -> anyhow::Result<()> {
     let program: Program = term(&input);
     check_all_crates(&program)
 }
+
+pub fn test_where_clause(program: &str, assertion: &str) -> anyhow::Result<Set<Constraints>> {
+    let program: Program = term(&program);
+    check_all_crates(&program)?;
+    let assertion: Arc<TestAssertion> = term(assertion);
+    let decls = program.to_prove_decls();
+    Ok(formality_prove::test_util::test_prove(decls, assertion))
+}
diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs
@@ -0,0 +1,33 @@
+use formality::test_where_clause;
+
+#[test]
+fn test_mirror_normalizes_u32_to_u32() {
+    // Variant of test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait
+    // where there is a negative impl, so it is accepted.
+
+    expect_test::expect![[r#"
+        Err(
+            Error {
+                context: "check_trait_impl(impl <ty> Mirror < > for ^ty0_0 where [] { type Assoc <> = ^ty1_0 where [] ; })",
+                source: Error {
+                    context: "check_associated_ty_value(type Assoc <> = !ty_1 where [] ;)",
+                    source: "failed to prove {@ wf(!ty_1)} given {}, got {}",
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        "[
+            crate core {
+                trait Mirror<> where [] {
+                    type Assoc<> : [] where [];
+                }
+
+                impl<ty T> Mirror<> for T where [] {
+                    type Assoc<> = T where [];
+                }
+            }
+        ]",
+        "exists<ty T> {} => {<u32 as Mirror>::Assoc<> = T}",
+    ));
+}

Original file line number	Diff line number	Diff line change
`@@ -157,6 +157,7 @@ impl super::Check<'_> {`
`157`	`157`	`Ok(())`
`158`	`158`	`}`
`159`	`159`
	`160`	`+ #[context("check_associated_ty_value({impl_value:?})")]`
`160`	`161`	`fn check_associated_ty_value(`
`161`	`162`	`&self,`
`162`	`163`	`impl_env: &Env,`