rework universes big time, most tests pass

Author: nikomatsakis

crates/formality-logic/src/env/query/extract_query_result.rs

@@ -107,7 +107,6 @@ fn close_over(
     let to_bound_variables: VarSubstitution = new_inference_variables
         .iter()
         .zip(&fresh_bound_variables)
-        .upcasted()
         .collect();
 
     let bound_data = QueryResultBoundData {

crates/formality-logic/src/env/query/querify.rs

@@ -60,7 +60,7 @@ pub fn querify(
     let mut universe_counters: Map<Universe, VarIndex> = Map::default();
     let var_substitution: VarSubstitution = source_free_vars
         .iter()
-        .map(|&source_free_var| {
+        .map(|&source_free_var| -> (Variable, Variable) {
             (
                 source_free_var,
                 match source_free_var {

crates/formality-prove/src/prove.rs

@@ -1,60 +1,59 @@
 mod constraints;
-mod forall;
+mod env;
 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;
 
 pub use constraints::Constraints;
-use formality_types::{
-    cast::Upcast,
-    collections::Set,
-    grammar::{Binder, Wcs},
-    set,
-    visit::Visit,
-};
+use formality_types::{cast::Upcast, collections::Set, grammar::Wcs, set, visit::Visit};
 use tracing::Level;
 
 use crate::program::Program;
 
+pub use self::env::Env;
 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>,
+    env: impl Upcast<Env>,
     assumptions: impl Upcast<Wcs>,
     goal: impl Upcast<Wcs>,
-) -> Set<Binder<Constraints>> {
+) -> Set<(Env, Constraints)> {
     let program: Program = program.upcast();
+    let env0: Env = env.upcast();
     let assumptions: Wcs = assumptions.upcast();
     let goal: Wcs = goal.upcast();
 
     let span = tracing::span!(Level::DEBUG, "prove", ?goal, ?assumptions);
     let _guard = span.enter();
 
     let term_in = (&assumptions, &goal);
-    let fv_in = term_in.free_variables();
     if term_in.size() > program.max_size {
         tracing::debug!(
             "term has size {} which exceeds max size of {}",
             term_in.size(),
             program.max_size
         );
-        return set![Binder::dummy(Constraints::default().ambiguous())];
+        return set![(env0, Constraints::default().ambiguous())];
     }
 
-    let cs = prove_wc_list(program, assumptions, goal);
+    env0.assert_encloses(term_in);
 
-    cs.assert_valid();
-    cs.free_variables()
-        .iter()
-        .for_each(|fv| assert!(fv_in.contains(&fv)));
+    let result_set = prove_wc_list(program, &env0, assumptions, goal);
 
-    tracing::debug!(?cs);
+    result_set.iter().for_each(|(env1, constraints1)| {
+        env1.assert_valid();
+        env1.assert_valid_extension_of(&env0);
+        env1.assert_encloses(&constraints1);
+        constraints1.assert_valid();
+    });
 
-    cs
+    tracing::debug!(?result_set);
+
+    result_set
 }

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

@@ -3,12 +3,12 @@ use formality_types::{
     cast_impl,
     derive_links::UpcastFrom,
     fold::Fold,
-    grammar::{Binder, InferenceVar, Parameter, Substitution, Variable},
+    grammar::{Parameter, Substitution, Variable},
     term::Term,
     visit::Visit,
 };
 
-use super::subst::existential_substitution;
+use super::env::Env;
 
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)]
 pub struct Constraints<R: Term = ()> {
@@ -40,13 +40,13 @@ where
 {
     fn from_iter<T: IntoIterator<Item = (A, B)>>(iter: T) -> Self {
         let substitution = iter.into_iter().collect();
-        let c = Constraints {
+        let c2 = Constraints {
             substitution,
             known_true: true,
             result: (),
         };
-        c.assert_valid();
-        c
+        c2.assert_valid();
+        c2
     }
 }
 
@@ -72,110 +72,88 @@ impl<R: Term> Constraints<R> {
         }
     }
 
-    pub fn map<S: Term>(self, op: impl FnOnce(R) -> S) -> Constraints<S> {
-        let Constraints {
-            result,
-            known_true,
-            substitution,
-        } = self;
-        let result = op(result);
+    /// Given constraings from solving the subparts of `(A /\ B)`, yield combined constraints.
+    ///
+    /// # Parameters
+    ///
+    /// * `self` -- the constraints from solving `A`
+    /// * `c2` -- the constraints from solving `B` (after applying substitution from `self` to `B`)
+    pub fn seq<R2: Term>(&self, c2: impl Upcast<Constraints<R2>>) -> Constraints<R2>
+    where
+        R: CombineResults<R2>,
+    {
+        let c2: Constraints<R2> = c2.upcast();
+
+        self.assert_valid();
+        c2.assert_valid();
+
+        // This substitution should have already been applied to produce
+        // `c2`, therefore we don't expect any bindings for *our* variables.
+        assert!(self
+            .substitution
+            .domain()
+            .is_disjoint(&c2.substitution.domain()));
+
+        // Similarly, we don't expect any references to variables that we have
+        // defined.
+        assert!(self
+            .substitution
+            .domain()
+            .iter()
+            .all(|v| !occurs_in(v, &c2.substitution)));
+
+        // Apply c2's substitution to our substitution (since it may have bound
+        // existential variables that we reference)
+        let c1_substitution = c2.substitution.apply(&self.substitution);
+
         Constraints {
-            known_true,
-            substitution,
-            result,
+            known_true: self.known_true && c2.known_true,
+            result: R::combine(&self.result, c2.result),
+            substitution: c1_substitution.into_iter().chain(c2.substitution).collect(),
         }
     }
 
-    pub fn split_result(self) -> (R, Constraints) {
-        let Constraints {
-            result,
-            known_true,
-            substitution,
-        } = self;
-        (
-            result,
-            Constraints {
-                known_true,
-                substitution,
-                result: (),
-            },
-        )
-    }
-}
+    pub fn assert_valid_in(&self, env: &Env) {
+        self.assert_valid();
 
-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)
-}
+        // Each variable `x` is only bound to a term of strictly lower universe.
+        // This implies that `x` does not appear in `p`.
+        for (x, p) in self.substitution.iter() {
+            let fvs = p.free_variables();
+            fvs.iter()
+                .for_each(|fv| assert!(env.universe(fv) < env.universe(x)));
+        }
+    }
 
-pub fn merge_constraints<R0: Term, R1: Term>(
-    existentials: impl Upcast<Vec<Variable>>,
-    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();
-    c1.assert_valid();
-
-    assert!(c0
-        .substitution
-        .domain()
-        .is_disjoint(&c1.substitution.domain()));
-    assert!(!c0
-        .substitution
-        .domain()
-        .iter()
-        .any(|v| occurs_in(v, &c1.substitution)));
-
-    let existentials: Vec<Variable> = existentials.upcast();
-
-    let c0 = c1.substitution.apply(&c0);
-
-    // Drop any bindings `X := P` from the subst that appear in the `variables` set;
-    // those are existentials that we temporarily introduced and no longer need.
-    let substitution = c0
-        .substitution
-        .into_iter()
-        .chain(c1.substitution)
-        .filter(|(v, _)| !existentials.contains(&v.upcast()))
-        .collect();
+    pub fn pop_subst<V>(mut self, mut env: Env, v: &[V]) -> (Env, Constraints<R>)
+    where
+        V: Upcast<Variable> + Copy,
+    {
+        self.assert_valid_in(&env);
 
-    let known_true = c0.known_true && c1.known_true;
+        if v.len() == 0 {
+            return (env, self);
+        }
 
-    let result = R0::combine(c0.result, c1.result);
+        let vars = env.pop_vars(v);
+        self.substitution -= vars;
 
-    Binder::mentioned(
-        (c1_bound_vars, existentials),
-        Constraints {
-            known_true,
-            substitution,
-            result,
-        },
-    )
+        (env, self)
+    }
 }
 
 impl<R: Term> Fold for Constraints<R> {
     fn substitute(&self, substitution_fn: formality_types::fold::SubstitutionFn<'_>) -> Self {
-        let c = Constraints {
+        let c2 = 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
-        c.assert_valid();
+        c2.assert_valid();
 
-        c
+        c2
     }
 }
 
@@ -244,33 +222,27 @@ pub fn is_valid_binding(v: impl Upcast<Variable>, t: &impl Visit) -> bool {
         .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<R: Term>(result: R) -> Binder<Constraints<R>> {
-    Binder::dummy(Constraints {
-        result,
+pub fn no_constraints() -> Constraints {
+    Constraints {
+        result: (),
         known_true: true,
         substitution: Substitution::default(),
-    })
+    }
 }
 
 pub trait CombineResults<R> {
-    fn combine(r0: Self, r1: R) -> R;
+    fn combine(r0: &Self, r1: R) -> R;
 }
 
 impl<R> CombineResults<R> for () {
-    fn combine((): (), r1: R) -> R {
+    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);
+    fn combine(r0: &Self, mut r1: Vec<Parameter>) -> Vec<Parameter> {
+        r1.push(r0.clone());
         r1
     }
 }