introduce prove function

add postcondition checking

Author: nikomatsakis

crates/formality-prove/src/prove.rs

@@ -9,4 +9,34 @@ mod prove_wc_list;
 mod subst;
 
 pub use constraints::Constraints;
-pub use prove_wc_list::prove_wc_list;
+use formality_types::{
+    cast::Upcast,
+    collections::Set,
+    grammar::{Binder, Wcs},
+    visit::Visit,
+};
+
+use crate::program::Program;
+
+use self::prove_wc_list::prove_wc_list;
+
+/// Top-level entry point for proving things; other rules recurse to this one.
+pub fn prove(
+    program: impl Upcast<Program>,
+    assumptions: impl Upcast<Wcs>,
+    goal: impl Upcast<Wcs>,
+) -> Set<Binder<Constraints>> {
+    let program: Program = program.upcast();
+    let assumptions: Wcs = assumptions.upcast();
+    let goal: Wcs = goal.upcast();
+
+    let fv_in = (&assumptions, &goal).free_variables();
+
+    let cs = prove_wc_list(program, assumptions, goal);
+
+    cs.free_variables()
+        .iter()
+        .for_each(|fv| assert!(fv_in.contains(&fv)));
+
+    cs
+}

crates/formality-prove/src/prove/prove_after.rs

@@ -5,7 +5,7 @@ use formality_types::{
 
 use crate::{
     program::Program,
-    prove::{constraints::merge_constraints, prove_wc_list::prove_wc_list},
+    prove::{constraints::merge_constraints, prove, prove_wc_list::prove_wc_list},
 };
 
 use super::{constraints::Constraints, subst::existential_substitution};
@@ -22,7 +22,7 @@ judgment_fn! {
             (let c1 = c1.instantiate_with(&existentials).unwrap())
             (let assumptions = c1.substitution().apply(&assumptions))
             (let goal = c1.substitution().apply(&goal))
-            (prove_wc_list(program, assumptions, goal) => c2)
+            (prove(program, assumptions, goal) => c2)
             --- ("prove_after")
             (prove_after(program, c1, assumptions, goal) => merge_constraints(&existentials, &c1, c2))
         )

crates/formality-prove/src/prove/prove_apr.rs

@@ -7,6 +7,7 @@ use crate::{
     program::Program,
     prove::{
         constraints::merge_constraints,
+        prove,
         prove_after::prove_after,
         prove_apr_via::prove_apr_via,
         prove_eq::{all_eq, prove_ty_eq},
@@ -36,7 +37,7 @@ judgment_fn! {
             (let i = i.binder.instantiate_with(&subst).unwrap())
             (let t = program.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
             (let assumptions_c = (&assumptions, trait_ref.is_implemented()))
-            (prove_wc_list(&program, &assumptions_c, all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c1)
+            (prove(&program, &assumptions_c, all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c1)
             (prove_after(&program, c1, &assumptions_c, (&i.where_clause, &t.where_clause)) => c2)
             ----------------------------- ("impl")
             (prove_apr(program, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => merge_constraints(&subst, (), c2))

crates/formality-prove/src/prove/prove_eq.rs

@@ -12,6 +12,7 @@ use crate::{
     program::Program,
     prove::{
         constraints::{constrain, merge_constraints, no_constraints, occurs_in},
+        prove,
         subst::existential_substitution,
     },
 };
@@ -44,7 +45,7 @@ pub fn prove_parameters_eq(
     let program = program.upcast();
     let assumptions = assumptions.upcast();
     let goals = all_eq(a, b);
-    prove_wc_list(program, assumptions, goals)
+    prove(program, assumptions, goals)
 }
 
 judgment_fn! {
@@ -112,7 +113,7 @@ judgment_fn! {
                 // Normalizing to a variable or alias: not productive
                 assumptions.clone()
             })
-            (prove_wc_list(&program, &assumptions1, (
+            (prove(&program, &assumptions1, (
                 all_eq(&a.parameters, &decl.alias.parameters),
                 eq(&b, &decl.ty),
                 decl.where_clause,

crates/formality-prove/src/test.rs

@@ -6,7 +6,7 @@ use formality_types::{
 
 use crate::{
     program::Program,
-    prove::{prove_wc_list, Constraints},
+    prove::{prove, Constraints},
 };
 
 mod eq_partial_eq;
@@ -22,5 +22,5 @@ mod universes;
 fn test_prove(program: Program, t: Binder<(Wcs, Wcs)>) -> Set<Binder<Constraints>> {
     let (assumptions, goals) =
         t.instantiate(|kind, var_index| InferenceVar { kind, var_index }.upcast());
-    prove_wc_list(program, assumptions, goals)
+    prove(program, assumptions, goals)
 }

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

@@ -5,7 +5,7 @@ use formality_types::{
     parse::term,
 };
 
-use crate::{program::Program, prove::prove_wc_list};
+use crate::{program::Program, prove::prove};
 
 /// Simple example program consisting only of two trait declarations.
 fn program() -> Program {
@@ -25,7 +25,7 @@ fn program() -> Program {
 fn eq_implies_partial_eq() {
     let assumptions: Wcs = Wcs::t();
     let goal: Wc = term("for<ty T> if {is_implemented(Eq(T))} is_implemented(PartialEq(T))");
-    let constraints = prove_wc_list(program(), assumptions, goal);
+    let constraints = prove(program(), assumptions, goal);
     expect![[r#"
         {
             <> Constraints { known_true: true, substitution: Substitution { map: {} } },
@@ -38,7 +38,7 @@ fn eq_implies_partial_eq() {
 fn not_partial_eq_implies_eq() {
     let assumptions: Wcs = Wcs::t();
     let goal: Wc = term("for<ty T> if {is_implemented(PartialEq(T))} is_implemented(Eq(T))");
-    let constraints = prove_wc_list(program(), assumptions, goal);
+    let constraints = prove(program(), assumptions, goal);
     expect![[r#"
         {}
     "#]]
@@ -49,7 +49,7 @@ fn not_partial_eq_implies_eq() {
 fn placeholders_not_eq() {
     let assumptions: Wcs = Wcs::t();
     let goal: Wc = term("for<ty T, ty U> if {is_implemented(Eq(T))} is_implemented(PartialEq(U))");
-    let constraints = prove_wc_list(program(), assumptions, goal);
+    let constraints = prove(program(), assumptions, goal);
     expect![[r#"
         {}
     "#]]

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

@@ -5,7 +5,7 @@ use formality_types::{
     parse::term,
 };
 
-use crate::{program::Program, prove::prove_wc_list};
+use crate::{program::Program, prove::prove};
 
 /// Simple example program consisting only of two trait declarations.
 fn program() -> Program {
@@ -25,7 +25,7 @@ fn program() -> Program {
 fn vec_u32_debug() {
     let assumptions: Wcs = Wcs::t();
     let goal: Wc = term("is_implemented(Debug(Vec<u32>))");
-    let constraints = prove_wc_list(program(), assumptions, goal);
+    let constraints = prove(program(), assumptions, goal);
     expect![[r#"
         {
             <> Constraints { known_true: true, substitution: Substitution { map: {} } },
@@ -38,7 +38,7 @@ fn vec_u32_debug() {
 fn vec_vec_u32_debug() {
     let assumptions: Wcs = Wcs::t();
     let goal: Wc = term("is_implemented(Debug(Vec<Vec<u32>>))");
-    let constraints = prove_wc_list(program(), assumptions, goal);
+    let constraints = prove(program(), assumptions, goal);
     expect![[r#"
         {
             <> Constraints { known_true: true, substitution: Substitution { map: {} } },