convert formality-check and friends

(untested)

Author: nikomatsakis

Cargo.lock

@@ -10,6 +10,7 @@ formality-types = { path = "../formality-types" }
 formality-macros = { path = "../formality-macros" }
 formality-core = { path = "../formality-core" }
 formality-rust = { path = "../formality-rust" }
+formality-prove = { path = "../formality-prove" }
 tracing = "0.1"
 contracts = "0.6.3"
 anyhow = "1.0.66"

crates/formality-check/Cargo.toml

@@ -1,16 +1,10 @@
-use formality_decl::grammar::{Adt, AdtBoundData, AdtVariant, Field};
-use formality_types::{
-    cast::To,
-    grammar::{Fallible, Hypothesis},
-};
+use formality_prove::Env;
+use formality_rust::grammar::{Adt, AdtBoundData, Field, Variant};
+use formality_types::grammar::Fallible;
 
 impl super::Check<'_> {
     pub(super) fn check_adt(&self, adt: &Adt) -> Fallible<()> {
-        let Adt {
-            kind: _,
-            id: _,
-            binder,
-        } = adt;
+        let Adt { id: _, binder } = adt;
 
         let mut env = Env::default();
 
@@ -19,15 +13,13 @@ impl super::Check<'_> {
             variants,
         } = env.instantiate_universally(binder);
 
-        let assumptions: Vec<Hypothesis> = where_clauses.to();
-
-        self.prove_where_clauses_well_formed(&env, &assumptions, &where_clauses)?;
+        self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;
 
         // FIXME: check names are unique or integers from 0..n
 
-        for AdtVariant { name: _, fields } in &variants {
+        for Variant { name: _, fields } in &variants {
             for Field { name: _, ty } in fields {
-                self.prove_goal(&env, &assumptions, ty.well_formed())?;
+                self.prove_goal(&env, &where_clauses, ty.well_formed())?;
             }
         }
 

crates/formality-check/src/adts.rs

@@ -1,5 +1,5 @@
 use anyhow::bail;
-use formality_decl::grammar::{Crate, TraitImpl};
+use formality_rust::grammar::{Crate, TraitImpl};
 use formality_types::{cast::Downcasted, grammar::Fallible};
 use itertools::Itertools;
 

crates/formality-check/src/coherence.rs

@@ -1,9 +1,6 @@
-use formality_decl::grammar::{Fn, FnBoundData};
-use formality_logic::Env;
-use formality_types::{
-    cast::Upcast,
-    grammar::{Fallible, Hypothesis},
-};
+use formality_prove::Env;
+use formality_rust::grammar::{Fn, FnBoundData, WhereClause};
+use formality_types::{cast::Upcast, grammar::Fallible};
 
 use crate::Check;
 
@@ -15,7 +12,7 @@ impl Check<'_> {
     pub(crate) fn check_fn(
         &self,
         in_env: &Env,
-        in_assumptions: &[Hypothesis],
+        in_assumptions: &[WhereClause],
         f: &Fn,
     ) -> Fallible<()> {
         let mut env = in_env.clone();
@@ -26,9 +23,10 @@ impl Check<'_> {
             input_tys,
             output_ty,
             where_clauses,
+            body: _,
         } = env.instantiate_universally(binder);
 
-        let assumptions: Vec<Hypothesis> = (in_assumptions, &where_clauses).upcast();
+        let assumptions: Vec<WhereClause> = (in_assumptions, &where_clauses).upcast();
 
         self.prove_where_clauses_well_formed(&env, &assumptions, &where_clauses)?;
 

crates/formality-check/src/fns.rs

@@ -1,14 +1,14 @@
 use anyhow::bail;
 use contracts::requires;
 use fn_error_context::context;
-use formality_decl::grammar::{
+use formality_prove::Env;
+use formality_rust::grammar::{
     AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Fn,
-    FnBoundData, ImplItem, TraitBoundData, TraitImpl, TraitImplBoundData, TraitItem,
+    FnBoundData, ImplItem, TraitBoundData, TraitImpl, TraitImplBoundData, TraitItem, WhereClause,
 };
-use formality_logic::Env;
 use formality_types::{
-    cast::{Downcasted, To},
-    grammar::{Binder, Fallible, Goal, Hypothesis, Substitution},
+    cast::Downcasted,
+    grammar::{AtomicRelation, Binder, Fallible, Substitution, Wcs},
     term::Term,
     visit::Visit,
 };
@@ -21,16 +21,18 @@ impl super::Check<'_> {
         let mut env = Env::default();
 
         let TraitImplBoundData {
-            trait_ref,
+            trait_id,
+            self_ty,
+            trait_parameters,
             where_clauses,
             impl_items,
         } = env.instantiate_universally(binder);
 
-        let assumptions: Vec<Hypothesis> = where_clauses.to();
+        let trait_ref = trait_id.with(self_ty, trait_parameters);
 
-        self.prove_where_clauses_well_formed(&env, &assumptions, &where_clauses)?;
+        self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;
 
-        self.prove_goal(&env, &assumptions, trait_ref.is_implemented())?;
+        self.prove_goal(&env, &where_clauses, trait_ref.is_implemented())?;
 
         let trait_decl = self.program.trait_named(&trait_ref.trait_id)?;
         let TraitBoundData {
@@ -39,7 +41,7 @@ impl super::Check<'_> {
         } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?;
 
         for impl_item in &impl_items {
-            self.check_trait_impl_item(&env, &assumptions, &trait_items, impl_item)?;
+            self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?;
         }
 
         Ok(())
@@ -49,7 +51,7 @@ impl super::Check<'_> {
     fn check_trait_impl_item(
         &self,
         env: &Env,
-        assumptions: &[Hypothesis],
+        assumptions: &[WhereClause],
         trait_items: &[TraitItem],
         impl_item: &ImplItem,
     ) -> Fallible<()> {
@@ -61,15 +63,17 @@ impl super::Check<'_> {
         }
     }
 
-    #[context("check_fn_in_impl")]
-    #[requires(impl_assumptions.iter().all(|a| a.references_only_placeholder_variables()))]
     fn check_fn_in_impl(
         &self,
         env: &Env,
-        impl_assumptions: &[Hypothesis],
+        impl_assumptions: &[WhereClause],
         trait_items: &[TraitItem],
         ii_fn: &Fn,
     ) -> Fallible<()> {
+        assert!(
+            env.only_universal_variables() && env.encloses((impl_assumptions, trait_items, ii_fn))
+        );
+
         // Find the corresponding function from the trait:
         let ti_fn = match trait_items
             .iter()
@@ -90,18 +94,20 @@ impl super::Check<'_> {
                 input_tys: ii_input_tys,
                 output_ty: ii_output_ty,
                 where_clauses: ii_where_clauses,
+                body: _,
             },
             FnBoundData {
                 input_tys: ti_input_tys,
                 output_ty: ti_output_ty,
                 where_clauses: ti_where_clauses,
+                body: _,
             },
         ) = env.instantiate_universally(&self.merge_binders(&ii_fn.binder, &ti_fn.binder)?);
 
         self.prove_goal(
             &env,
             (impl_assumptions, &ti_where_clauses),
-            Goal::all(&ii_where_clauses),
+            &ii_where_clauses,
         )?;
 
         if ii_input_tys.len() != ti_input_tys.len() {
@@ -116,14 +122,14 @@ impl super::Check<'_> {
             self.prove_goal(
                 &env,
                 (impl_assumptions, &ii_where_clauses),
-                Goal::sub(ti_input_ty, ii_input_ty),
+                AtomicRelation::sub(ti_input_ty, ii_input_ty),
             )?;
         }
 
         self.prove_goal(
             &env,
             (impl_assumptions, &ii_where_clauses),
-            Goal::sub(ii_output_ty, ti_output_ty),
+            AtomicRelation::sub(ii_output_ty, ti_output_ty),
         )?;
 
         Ok(())
@@ -132,7 +138,7 @@ impl super::Check<'_> {
     fn check_associated_ty_value(
         &self,
         impl_env: &Env,
-        impl_assumptions: &[Hypothesis],
+        impl_assumptions: &[WhereClause],
         trait_items: &[TraitItem],
         impl_value: &AssociatedTyValue,
     ) -> Fallible<()> {
@@ -169,7 +175,7 @@ impl super::Check<'_> {
         self.prove_goal(
             &env,
             (impl_assumptions, &ti_where_clauses),
-            Goal::all(&ii_where_clauses),
+            &ii_where_clauses,
         )?;
 
         self.prove_goal(
@@ -178,12 +184,8 @@ impl super::Check<'_> {
             ii_ty.well_formed(),
         )?;
 
-        let ensures = ti_ensures.instantiate_with(&[ii_ty])?;
-        self.prove_goal(
-            &env,
-            (impl_assumptions, &ii_where_clauses),
-            Goal::all(ensures),
-        )?;
+        let ensures: Wcs = ti_ensures.iter().map(|e| e.to_wc(&ii_ty)).collect();
+        self.prove_goal(&env, (impl_assumptions, &ii_where_clauses), ensures)?;
 
         Ok(())
     }

crates/formality-check/src/impls.rs

@@ -1,18 +1,16 @@
 #![allow(dead_code)]
-#![cfg(FIXME)]
 
 use std::collections::VecDeque;
 
 use anyhow::bail;
-use contracts::requires;
-use formality_decl::grammar::{Crate, CrateItem, Program};
-use formality_logic::Db;
-use formality_logic::Env;
-use formality_logic::{prove_universal_goal, UniversalGoalResult};
+use formality_prove::{Decls, Env};
+use formality_rust::{
+    grammar::{Crate, CrateItem, Program, WhereClause},
+    prove::ToWcs,
+};
 use formality_types::{
     cast::Upcast,
-    grammar::{Fallible, Goal, Hypothesis},
-    term::Term,
+    grammar::{Fallible, Wcs},
 };
 
 /// Check all crates in the program. The crates must be in dependency order
@@ -44,7 +42,7 @@ mod where_clauses;
 
 struct Check<'p> {
     program: &'p Program,
-    db: Db,
+    decls: &'p Decls,
 }
 
 impl Check<'_> {
@@ -77,28 +75,31 @@ impl Check<'_> {
 
     fn check_crate_item(&self, c: &CrateItem) -> Fallible<()> {
         match c {
-            CrateItem::Adt(v) => self.check_adt(v),
             CrateItem::Trait(v) => self.check_trait(v),
             CrateItem::TraitImpl(v) => self.check_trait_impl(v),
-            CrateItem::Fn(v) => self.check_free_fn(v),
+            CrateItem::Struct(s) => self.check_adt(&s.to_adt()),
+            CrateItem::Enum(e) => self.check_adt(&e.to_adt()),
+            CrateItem::Fn(f) => self.check_free_fn(f),
         }
     }
 
-    #[requires(goal.references_only_placeholder_variables())]
     fn prove_goal(
         &self,
         env: &Env,
-        assumptions: impl Upcast<Vec<Hypothesis>>,
-        goal: impl Term + Upcast<Goal>,
+        assumptions: impl Upcast<Vec<WhereClause>>,
+        goal: impl ToWcs,
     ) -> Fallible<()> {
-        let goal: Goal = goal.upcast();
-        let assumptions = assumptions.upcast();
-        match prove_universal_goal(&self.db, env, &assumptions, &goal) {
-            UniversalGoalResult::Yes => Ok(()),
-            UniversalGoalResult::No => bail!("could not prove `{goal:?}` given `{assumptions:#?}`"),
-            UniversalGoalResult::Maybe => {
-                bail!("could not prove `{goal:?}` (ambiguous) given `{assumptions:#?}`")
-            }
+        let goal: Wcs = goal.to_wcs();
+        let assumptions: Vec<WhereClause> = assumptions.upcast();
+
+        assert!(env.only_universal_variables());
+        assert!(env.encloses((&assumptions, &goal)));
+
+        let cs = formality_prove::prove(self.decls, env, assumptions.to_wcs(), &goal);
+        if cs.iter().any(|c| c.unconditionally_true()) {
+            return Ok(());
         }
+
+        bail!("failed to prove {goal:?} from {assumptions:?}, got {cs:?}")
     }
 }