wip wip

Author: nikomatsakis

crates/formality-logic/src/env.rs

@@ -110,6 +110,7 @@ impl Env {
         });
         InferenceVar {
             var_index: VarIndex { index },
+            universe: universe,
             kind,
         }
     }
@@ -121,6 +122,7 @@ impl Env {
             .zip(0..)
             .map(|(id, index)| InferenceVar {
                 var_index: VarIndex { index },
+                universe: id.universe,
                 kind: id.kind,
             })
             .collect()
@@ -307,6 +309,7 @@ impl Env {
             .flat_map(|(data, index)| {
                 self.inference_var_relations(InferenceVar {
                     var_index: VarIndex { index },
+                    universe: data.universe,
                     kind: data.kind,
                 })
             })

crates/formality-prove/src/prove.rs

@@ -4,6 +4,7 @@ mod prove_after;
 mod prove_apr;
 mod prove_apr_via;
 mod prove_eq;
+mod prove_normalize;
 mod prove_wc;
 mod prove_wc_list;
 mod subst;

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

@@ -4,16 +4,20 @@ use formality_types::{
     derive_links::UpcastFrom,
     fold::Fold,
     grammar::{Binder, InferenceVar, Parameter, Substitution, Variable},
+    term::Term,
     visit::Visit,
 };
 
+use super::subst::existential_substitution;
+
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)]
-pub struct Constraints {
+pub struct Constraints<R: Term = ()> {
+    result: R,
     known_true: bool,
     substitution: Substitution,
 }
 
-cast_impl!(Constraints);
+cast_impl!(impl(R: Term) Constraints<R>);
 
 impl<A, B> UpcastFrom<(A, B)> for Constraints
 where
@@ -24,38 +28,100 @@ where
         Constraints {
             substitution: term.upcast(),
             known_true: true,
+            result: (),
         }
     }
 }
 
+impl<A, B> FromIterator<(A, B)> for Constraints
+where
+    A: Upcast<Variable>,
+    B: Upcast<Parameter>,
+{
+    fn from_iter<T: IntoIterator<Item = (A, B)>>(iter: T) -> Self {
+        let substitution = iter.into_iter().collect();
+        let c = Constraints {
+            substitution,
+            known_true: true,
+            result: (),
+        };
+        c.assert_valid();
+        c
+    }
+}
+
 impl Default for Constraints {
     fn default() -> Self {
         Self {
+            result: (),
             known_true: true,
             substitution: Default::default(),
         }
     }
 }
 
-impl Constraints {
+impl<R: Term> Constraints<R> {
     pub fn substitution(&self) -> &Substitution {
         &self.substitution
     }
 
-    pub fn ambiguous(self) -> Constraints {
+    pub fn ambiguous(self) -> Constraints<R> {
         Self {
             known_true: false,
             ..self
         }
     }
+
+    pub fn map<S: Term>(self, op: impl FnOnce(R) -> S) -> Constraints<S> {
+        let Constraints {
+            result,
+            known_true,
+            substitution,
+        } = self;
+        let result = op(result);
+        Constraints {
+            known_true,
+            substitution,
+            result,
+        }
+    }
+
+    pub fn split_result(self) -> (R, Constraints) {
+        let Constraints {
+            result,
+            known_true,
+            substitution,
+        } = self;
+        (
+            result,
+            Constraints {
+                known_true,
+                substitution,
+                result: (),
+            },
+        )
+    }
 }
 
-pub fn merge_constraints(
+pub fn instantiate_and_apply_constraints<T: Term, R: Term>(
+    c: Binder<Constraints<R>>,
+    term: T,
+) -> (Vec<InferenceVar>, Constraints<R>, T) {
+    let existentials = existential_substitution(&c, &term);
+    let c = c.instantiate_with(&existentials).unwrap();
+    let term = c.substitution().apply(&term);
+    (existentials, c, term)
+}
+
+pub fn merge_constraints<R0: Term, R1: Term>(
     existentials: impl Upcast<Vec<Variable>>,
-    c0: impl Upcast<Constraints>,
-    c1: Binder<Constraints>,
-) -> Binder<Constraints> {
-    let c0: Constraints = c0.upcast();
+    c0: impl Upcast<Constraints<R0>>,
+    c1: Binder<Constraints<R1>>,
+) -> Binder<Constraints<R1>>
+where
+    R0: CombineResults<R1>,
+{
+    let c0: Constraints<R0> = c0.upcast();
     c0.assert_valid();
 
     let (c1_bound_vars, c1) = c1.open();
@@ -85,20 +151,25 @@ pub fn merge_constraints(
         .collect();
 
     let known_true = c0.known_true && c1.known_true;
+
+    let result = R0::combine(c0.result, c1.result);
+
     Binder::mentioned(
         (c1_bound_vars, existentials),
         Constraints {
             known_true,
             substitution,
+            result,
         },
     )
 }
 
-impl Fold for Constraints {
+impl<R: Term> Fold for Constraints<R> {
     fn substitute(&self, substitution_fn: formality_types::fold::SubstitutionFn<'_>) -> Self {
         let c = Constraints {
             known_true: self.known_true,
             substitution: self.substitution.substitute(substitution_fn),
+            result: self.result.substitute(substitution_fn),
         };
 
         // not all substitutions preserve the constraint set invariant
@@ -108,29 +179,50 @@ impl Fold for Constraints {
     }
 }
 
-impl Visit for Constraints {
+impl<R: Term> Visit for Constraints<R> {
     fn free_variables(&self) -> Vec<Variable> {
         let Constraints {
             known_true: _,
             substitution,
+            result,
         } = self;
-        substitution.free_variables()
+
+        substitution
+            .free_variables()
+            .into_iter()
+            .chain(result.free_variables())
+            .collect()
     }
 
     fn size(&self) -> usize {
         let Constraints {
             known_true: _,
             substitution,
+            result,
         } = self;
-        substitution.size()
+        substitution.size() + result.size()
     }
 
     fn assert_valid(&self) {
-        let domain = self.substitution.domain();
-        let range = self.substitution.range();
+        let Constraints {
+            known_true: _,
+            substitution,
+            result,
+        } = self;
+
+        let domain = substitution.domain();
+
+        for &v in &domain {
+            assert!(v.is_free());
+            assert!(is_valid_binding(v, &substitution[v]));
+        }
+
+        let range = substitution.range();
         range
             .iter()
             .for_each(|t| assert!(domain.iter().all(|&v| !occurs_in(v, t))));
+
+        result.assert_valid();
     }
 }
 
@@ -139,12 +231,46 @@ pub fn occurs_in(v: impl Upcast<Variable>, t: &impl Visit) -> bool {
     t.free_variables().contains(&v)
 }
 
+/// True if `t` would be a valid binding for `v`, meaning...
+/// * `v` does not appear in `t`; and,
+/// * all free variables in `t` are within the universe of `v`
+pub fn is_valid_binding(v: impl Upcast<Variable>, t: &impl Visit) -> bool {
+    let v: Variable = v.upcast();
+    assert!(v.is_free());
+
+    let v_universe = v.max_universe();
+    t.free_variables()
+        .into_iter()
+        .all(|fv| fv != v && fv.max_universe() <= v_universe)
+}
+
 pub fn constrain(v: impl Upcast<InferenceVar>, p: impl Upcast<Parameter>) -> Binder<Constraints> {
     let v: InferenceVar = v.upcast();
     let p: Parameter = p.upcast();
     Binder::dummy((v, p).upcast())
 }
 
-pub fn no_constraints() -> Binder<Constraints> {
-    Binder::dummy(().upcast())
+pub fn no_constraints<R: Term>(result: R) -> Binder<Constraints<R>> {
+    Binder::dummy(Constraints {
+        result,
+        known_true: true,
+        substitution: Substitution::default(),
+    })
+}
+
+pub trait CombineResults<R> {
+    fn combine(r0: Self, r1: R) -> R;
+}
+
+impl<R> CombineResults<R> for () {
+    fn combine((): (), r1: R) -> R {
+        r1
+    }
+}
+
+impl CombineResults<Vec<Parameter>> for Parameter {
+    fn combine(r0: Self, mut r1: Vec<Parameter>) -> Vec<Parameter> {
+        r1.push(r0);
+        r1
+    }
 }

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

@@ -5,10 +5,13 @@ use formality_types::{
 
 use crate::{
     program::Program,
-    prove::{constraints::merge_constraints, prove},
+    prove::{
+        constraints::{instantiate_and_apply_constraints, merge_constraints},
+        prove,
+    },
 };
 
-use super::{constraints::Constraints, subst::existential_substitution};
+use super::constraints::Constraints;
 
 judgment_fn! {
     pub fn prove_after(
@@ -18,10 +21,7 @@ judgment_fn! {
         goal: Wcs,
     ) => Binder<Constraints> {
         (
-            (let existentials = existential_substitution(&c1, (&assumptions, &goal)))
-            (let c1 = c1.instantiate_with(&existentials).unwrap())
-            (let assumptions = c1.substitution().apply(&assumptions))
-            (let goal = c1.substitution().apply(&goal))
+            (let (existentials, c1, (assumptions, goal)) = instantiate_and_apply_constraints(c1, (assumptions, goal)))
             (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_via.rs

@@ -6,9 +6,10 @@ use formality_types::{
 use crate::{
     program::Program,
     prove::{
-        constraints::{merge_constraints, Constraints},
+        constraints::{merge_constraints, no_constraints, Constraints},
+        prove,
         prove_after::prove_after,
-        prove_eq::prove_parameters_eq,
+        prove_eq::all_eq,
         subst::existential_substitution,
     },
 };
@@ -21,12 +22,21 @@ judgment_fn! {
         goal: APR,
     ) => Binder<Constraints> {
         (
-            (let (skel_c, parameters_c) = clause.debone())
+            (let (skel_c, parameters_c) = predicate.debone())
             (let (skel_g, parameters_g) = goal.debone())
             (if skel_c == skel_g)
-            (prove_parameters_eq(program, assumptions, parameters_c, parameters_g) => c)
-            ----------------------------- ("axiom")
-            (prove_apr_via(program, assumptions, WcData::Atomic(clause), goal) => c)
+            (prove(program, assumptions, all_eq(parameters_c, parameters_g)) => c)
+            ----------------------------- ("predicate-congruence-axiom")
+            (prove_apr_via(program, assumptions, APR::AtomicPredicate(predicate), goal) => c)
+        )
+
+        (
+            (let (skel_c, parameters_c) = relation.debone())
+            (let (skel_g, parameters_g) = goal.debone())
+            (if skel_c == skel_g)
+            (if parameters_c == parameters_g) // for relations, we require 100% match
+            ----------------------------- ("relation-axiom")
+            (prove_apr_via(_program, _assumptions, APR::AtomicRelation(relation), goal) => no_constraints(()))
         )
 
         (
@@ -43,5 +53,5 @@ judgment_fn! {
             ----------------------------- ("implies")
             (prove_apr_via(program, assumptions, WcData::Implies(wc_condition, wc_consequence), goal) => c2)
         )
-}
+    }
 }