put env/constraints together

Author: nikomatsakis

crates/formality-prove/src/prove.rs

@@ -23,7 +23,7 @@ pub fn prove(
     env: impl Upcast<Env>,
     assumptions: impl Upcast<Wcs>,
     goal: impl Upcast<Wcs>,
-) -> Set<(Env, Constraints)> {
+) -> Set<Constraints> {
     let program: Program = program.upcast();
     let env0: Env = env.upcast();
     let assumptions: Wcs = assumptions.upcast();
@@ -39,18 +39,15 @@ pub fn prove(
             term_in.size(),
             program.max_size
         );
-        return set![(env0, Constraints::default().ambiguous())];
+        return set![Constraints::none(env0).ambiguous()];
     }
 
     env0.assert_encloses(term_in);
 
     let result_set = prove_wc_list(program, &env0, assumptions, goal);
 
-    result_set.iter().for_each(|(env1, constraints1)| {
-        env1.assert_valid();
-        env1.assert_valid_extension_of(&env0);
-        env1.assert_encloses(&constraints1);
-        constraints1.assert_valid();
+    result_set.iter().for_each(|constraints1| {
+        constraints1.assert_valid_extension_of(&env0);
     });
 
     tracing::debug!(?result_set);

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

@@ -2,7 +2,6 @@ use formality_types::{
     cast::{Downcast, Upcast},
     cast_impl,
     derive_links::UpcastFrom,
-    fold::Fold,
     grammar::{InferenceVar, Parameter, Substitution, Variable},
     visit::Visit,
 };
@@ -11,51 +10,49 @@ use super::env::Env;
 
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)]
 pub struct Constraints {
+    env: Env,
     known_true: bool,
     substitution: Substitution,
 }
 
 cast_impl!(Constraints);
 
-impl<A, B> UpcastFrom<(A, B)> for Constraints
+impl<A, B> UpcastFrom<(Env, (A, B))> for Constraints
 where
     A: Upcast<Variable>,
     B: Upcast<Parameter>,
 {
-    fn upcast_from(term: (A, B)) -> Self {
-        Constraints {
-            substitution: term.upcast(),
-            known_true: true,
-        }
+    fn upcast_from((env, pair): (Env, (A, B))) -> Self {
+        Constraints::from(env, std::iter::once(pair))
     }
 }
 
-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();
+impl Constraints {
+    pub fn none(env: Env) -> Self {
+        let v: Vec<(Variable, Parameter)> = vec![];
+        Self::from(env, v)
+    }
+
+    pub fn from(
+        env: Env,
+        iter: impl IntoIterator<Item = (impl Upcast<Variable>, impl Upcast<Parameter>)>,
+    ) -> Self {
+        let substitution: Substitution = iter.into_iter().collect();
+        env.assert_encloses(substitution.range());
+        env.assert_encloses(substitution.domain());
         let c2 = Constraints {
+            env,
             substitution,
             known_true: true,
         };
         c2.assert_valid();
         c2
     }
-}
 
-impl Default for Constraints {
-    fn default() -> Self {
-        Self {
-            known_true: true,
-            substitution: Default::default(),
-        }
+    pub fn env(&self) -> &Env {
+        &self.env
     }
-}
 
-impl Constraints {
     pub fn substitution(&self) -> &Substitution {
         &self.substitution
     }
@@ -78,6 +75,7 @@ impl Constraints {
 
         self.assert_valid();
         c2.assert_valid();
+        c2.assert_valid_extension_of(&self.env);
 
         // This substitution should have already been applied to produce
         // `c2`, therefore we don't expect any bindings for *our* variables.
@@ -99,114 +97,93 @@ impl Constraints {
         let c1_substitution = c2.substitution.apply(&self.substitution);
 
         Constraints {
+            env: c2.env,
             known_true: self.known_true && c2.known_true,
             substitution: c1_substitution.into_iter().chain(c2.substitution).collect(),
         }
     }
 
-    pub fn assert_valid_in(&self, env: &Env) {
-        self.assert_valid();
-
-        // 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 pop_subst<V>(mut self, mut env: Env, v: &[V]) -> (Env, Self)
+    pub fn pop_subst<V>(mut self, v: &[V]) -> Self
     where
         V: Upcast<Variable> + Copy,
     {
-        self.assert_valid_in(&env);
-
         if v.len() == 0 {
-            return (env, self);
+            return self;
         }
 
-        let vars = env.pop_vars(v);
+        let vars = self.env.pop_vars(v);
         self.substitution -= vars;
 
-        (env, self)
+        self
     }
-}
-
-impl Fold for Constraints {
-    fn substitute(&self, substitution_fn: formality_types::fold::SubstitutionFn<'_>) -> Self {
-        let c2 = Constraints {
-            known_true: self.known_true,
-            substitution: self.substitution.substitute(substitution_fn),
-        };
 
-        // not all substitutions preserve the constraint set invariant
-        c2.assert_valid();
-
-        c2
+    pub fn assert_valid_extension_of(&self, env0: &Env) {
+        self.env.assert_valid_extension_of(env0)
     }
 }
 
 impl Visit for Constraints {
     fn free_variables(&self) -> Vec<Variable> {
         let Constraints {
+            env,
             known_true: _,
             substitution,
         } = self;
 
-        substitution.free_variables().into_iter().collect()
+        // Debatable if `env.free_variables()` should be considered
+        // free here, env kind of acts as a binder. Don't think it matters.
+
+        env.free_variables()
+            .into_iter()
+            .chain(substitution.free_variables())
+            .collect()
     }
 
     fn size(&self) -> usize {
         let Constraints {
+            env,
             known_true: _,
             substitution,
         } = self;
-        substitution.size()
+        env.size() + substitution.size()
     }
 
     fn assert_valid(&self) {
         let Constraints {
+            env,
             known_true: _,
             substitution,
         } = self;
 
         let domain = substitution.domain();
+        let range = substitution.range();
 
-        for &v in &domain {
-            assert!(v.downcast::<InferenceVar>().is_some());
-            assert!(v.is_free());
-            assert!(is_valid_binding(v, &substitution[v]));
-        }
+        env.assert_encloses(&domain);
+        env.assert_encloses(&range);
 
-        let range = substitution.range();
+        // No variable in the domain appears in any part of the range;
+        // this prevents the obvious occurs check violations like `X = Vec<X>`
+        // but also indirect ones like `X = Vec<Y>, Y = X`; it also implies that
+        // the substitution has been fully applied, so we don't have `X = Vec<Y>, Y = u32`.
         range
             .iter()
-            .for_each(|t| assert!(domain.iter().all(|&v| !occurs_in(v, t))));
+            .for_each(|p| assert!(domain.iter().all(|&v| !occurs_in(v, p))));
+
+        // 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 substitution.iter() {
+            assert!(x.is_a::<InferenceVar>());
+
+            assert!(!occurs_in(x, &p));
+
+            let fvs = p.free_variables();
+            fvs.iter()
+                .for_each(|fv| assert!(env.universe(fv) < env.universe(x)));
+        }
     }
 }
 
 pub fn occurs_in(v: impl Upcast<Variable>, t: &impl Visit) -> bool {
     let v: Variable = v.upcast();
     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 no_constraints() -> Constraints {
-    Constraints {
-        known_true: true,
-        substitution: Substitution::default(),
-    }
-}

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

@@ -1,25 +1,21 @@
 use formality_types::{grammar::Wcs, judgment_fn};
 
-use crate::{
-    program::Program,
-    prove::{env::Env, prove},
-};
+use crate::{program::Program, prove::prove};
 
 use super::constraints::Constraints;
 
 judgment_fn! {
     pub fn prove_after(
         program: Program,
-        env: Env,
         constraints: Constraints,
         assumptions: Wcs,
         goal: Wcs,
-    ) => (Env, Constraints) {
+    ) => Constraints {
         (
             (let (assumptions, goal) = c1.substitution().apply(&(assumptions, goal)))
-            (prove(program, env, assumptions, goal) => (env, c2))
+            (prove(program, c1.env(), assumptions, goal) => c2)
             --- ("prove_after")
-            (prove_after(program, env, c1, assumptions, goal) => (env, c1.seq(c2)))
+            (prove_after(program, c1, assumptions, goal) => c1.seq(c2))
         )
     }
 }

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

@@ -22,7 +22,7 @@ judgment_fn! {
         env: Env,
         assumptions: Wcs,
         goal: APR,
-    ) => (Env, Constraints) {
+    ) => Constraints {
         (
             (&assumptions => a)
             (prove_apr_via(&program, &env, &assumptions, a, &goal) => c)
@@ -36,22 +36,20 @@ 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))
-            (prove(&program, env, &assumptions_c, all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => (env, c))
-            (prove_after(&program, env, c, &assumptions_c, (&i.where_clause, &t.where_clause)) => (env, c))
-            (let (env, c) = c.pop_subst(env, &subst))
+            (prove(&program, env, &assumptions_c, all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
+            (prove_after(&program, c, &assumptions_c, (&i.where_clause, &t.where_clause)) => c)
             ----------------------------- ("impl")
-            (prove_apr(program, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => (env, c))
+            (prove_apr(program, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
         )
 
         (
             (program.trait_invariants() => ti)
             (let (env, subst) = env.existential_substitution(&ti.binder))
             (let ti = ti.binder.instantiate_with(&subst).unwrap())
-            (prove_apr_via(&program, env, &assumptions, &ti.where_clause, &trait_ref) => (env, c))
-            (prove_after(&program, env, c, &assumptions, &ti.trait_ref) => (env, c))
-            (let (env, c) = c.pop_subst(env, &subst))
+            (prove_apr_via(&program, env, &assumptions, &ti.where_clause, &trait_ref) => c)
+            (prove_after(&program, c, &assumptions, &ti.trait_ref) => c)
             ----------------------------- ("trait implied bound")
-            (prove_apr(program, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => (env, c))
+            (prove_apr(program, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
         )
 
         (