s/inference/existential/

Author: nikomatsakis

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

@@ -2,7 +2,7 @@ use formality_types::{
     cast::{Downcast, Upcast},
     cast_impl,
     derive_links::UpcastFrom,
-    grammar::{InferenceVar, Parameter, Substitution, Variable},
+    grammar::{ExistentialVar, Parameter, Substitution, Variable},
     visit::Visit,
 };
 
@@ -183,7 +183,7 @@ impl Visit for Constraints {
         // 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!(x.is_a::<ExistentialVar>());
 
             assert!(!occurs_in(x, &p));
 

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

@@ -5,7 +5,7 @@ use formality_types::{
     collections::Set,
     fold::Fold,
     grammar::{
-        Binder, InferenceVar, ParameterKind, UniversalVar, VarIndex, VarSubstitution, Variable,
+        Binder, ExistentialVar, ParameterKind, UniversalVar, VarIndex, VarSubstitution, Variable,
     },
     visit::Visit,
 };
@@ -60,7 +60,7 @@ impl Env {
             .iter()
             .map(|v| match v {
                 Variable::UniversalVar(pv) => pv.var_index.index,
-                Variable::InferenceVar(iv) => iv.var_index.index,
+                Variable::ExistentialVar(iv) => iv.var_index.index,
                 Variable::BoundVar(_) => panic!(),
             })
             .max()
@@ -71,16 +71,16 @@ impl Env {
         }
     }
 
-    pub fn fresh_existential(&mut self, kind: ParameterKind) -> InferenceVar {
+    pub fn fresh_existential(&mut self, kind: ParameterKind) -> ExistentialVar {
         let var_index = self.fresh_index();
-        let v = InferenceVar { kind, var_index };
+        let v = ExistentialVar { kind, var_index };
         self.variables.push(v.upcast());
         v
     }
 
-    pub fn insert_fresh_before(&mut self, kind: ParameterKind, rank: Universe) -> InferenceVar {
+    pub fn insert_fresh_before(&mut self, kind: ParameterKind, rank: Universe) -> ExistentialVar {
         let var_index = self.fresh_index();
-        let v = InferenceVar { kind, var_index };
+        let v = ExistentialVar { kind, var_index };
         self.variables.insert(rank.index, v.upcast());
         v
     }
@@ -160,12 +160,12 @@ impl Env {
         b.instantiate_with(&subst).unwrap()
     }
 
-    pub fn existential_substitution<T>(&self, b: &Binder<T>) -> (Env, Vec<InferenceVar>)
+    pub fn existential_substitution<T>(&self, b: &Binder<T>) -> (Env, Vec<ExistentialVar>)
     where
         T: Fold,
     {
         let mut env = self.clone();
-        let subst = env.fresh_substituion(b.kinds(), |kind, var_index| InferenceVar {
+        let subst = env.fresh_substituion(b.kinds(), |kind, var_index| ExistentialVar {
             kind,
             var_index,
         });

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

@@ -115,10 +115,10 @@ judgment_fn! {
         )
 
         (
-            // Inference variables *could* be inferred to downstream types; depends on the substitution
+            // existential variables *could* be inferred to downstream types; depends on the substitution
             // we ultimately have.
             --- ("type variable")
-            (not_downstream(_decls, env, _assumptions, TyData::Variable(Variable::InferenceVar(_))) => Constraints::none(env).ambiguous())
+            (not_downstream(_decls, env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => Constraints::none(env).ambiguous())
         )
     }
 }
@@ -159,10 +159,10 @@ judgment_fn! {
             (is_local_parameter(decls, env, _assumptions, RigidTy { name: RigidName::AdtId(a), parameters: _ }) => Constraints::none(env))
         )
 
-        // Inference variables might or might not be local, depending on how they are instantiated.
+        // existential variables might or might not be local, depending on how they are instantiated.
         (
             --- ("existential variable")
-            (is_local_parameter(_decls, env, _assumptions, TyData::Variable(Variable::InferenceVar(_))) => Constraints::none(env).ambiguous())
+            (is_local_parameter(_decls, env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => Constraints::none(env).ambiguous())
         )
     }
 }

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

@@ -2,7 +2,7 @@ use formality_types::{
     cast::{Downcast, Upcast},
     collections::Deduplicate,
     grammar::{
-        InferenceVar, Parameter, Substitution, UniversalVar, VarIndex, VarSubstitution, Variable,
+        ExistentialVar, Parameter, Substitution, UniversalVar, VarIndex, VarSubstitution, Variable,
     },
     term::Term,
 };
@@ -29,7 +29,7 @@ pub fn minimize<T: Term>(env_max: Env, term: T) -> (Env, T, Minimization) {
                 var_index: VarIndex { index },
             }
             .upcast(),
-            Variable::InferenceVar(InferenceVar { kind, var_index: _ }) => InferenceVar {
+            Variable::ExistentialVar(ExistentialVar { kind, var_index: _ }) => ExistentialVar {
                 kind,
                 var_index: VarIndex { index },
             }
@@ -83,7 +83,7 @@ impl Minimization {
 
         let mut env_out = self.env_max.clone();
 
-        let mut fresh_vars: Vec<InferenceVar> = vec![];
+        let mut fresh_vars: Vec<ExistentialVar> = vec![];
         let mut env2out_subst = self.min2max_subst.clone();
         for &var in constraints.env().variables() {
             if let Some(var_out) = env2out_subst.map_var(var) {
@@ -98,7 +98,7 @@ impl Minimization {
                 }
             } else {
                 // e.g., Z in the example above
-                let var: InferenceVar = var.downcast().unwrap(); // we only ever insert fresh existential variables
+                let var: ExistentialVar = var.downcast().unwrap(); // we only ever insert fresh existential variables
                 fresh_vars.push(var);
             }
         }

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

@@ -2,7 +2,7 @@ use formality_types::{
     cast::{Downcast, Upcast, Upcasted},
     collections::{Deduplicate, Set},
     grammar::{
-        AliasTy, InferenceVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar,
+        AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar,
         Variable, Wcs,
     },
     judgment_fn, set,
@@ -64,7 +64,7 @@ judgment_fn! {
         (
             (prove_existential_var_eq(decls, env, assumptions, v, r) => c)
             ----------------------------- ("existential-nonvar")
-            (prove_eq(decls, env, assumptions, Variable::InferenceVar(v), r) => c)
+            (prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c)
         )
 
         (
@@ -81,7 +81,7 @@ judgment_fn! {
         decls: Decls,
         env: Env,
         assumptions: Wcs,
-        v: InferenceVar,
+        v: ExistentialVar,
         b: Parameter,
     ) => Constraints {
         debug(v, b, assumptions, env, decls)
@@ -97,7 +97,7 @@ judgment_fn! {
             // Map the higher rank variable to the lower rank one.
             (let (a, b) = env.order_by_universe(l, r))
             ----------------------------- ("existential-existential")
-            (prove_existential_var_eq(_decls, env, _assumptions, l, Variable::InferenceVar(r)) => (env, (b, a)))
+            (prove_existential_var_eq(_decls, env, _assumptions, l, Variable::ExistentialVar(r)) => (env, (b, a)))
         )
 
         (
@@ -112,7 +112,7 @@ fn equate_variable(
     decls: Decls,
     mut env: Env,
     assumptions: Wcs,
-    x: InferenceVar,
+    x: ExistentialVar,
     p: impl Upcast<Parameter>,
 ) -> Set<Constraints> {
     let p: Parameter = p.upcast();
@@ -161,11 +161,11 @@ fn equate_variable(
         env,
         universe_subst
             .iter()
-            .filter(|(v, _)| v.is_a::<InferenceVar>())
+            .filter(|(v, _)| v.is_a::<ExistentialVar>())
             .chain(Some((x, universe_subst.apply(&p)).upcast())),
     );
 
-    // For each universal variable that we replaced with an inference variable
+    // For each universal variable that we replaced with an existential variable
     // above, we now have to prove that goal. e.g., if we had `X = Vec<!Y>`, we would replace `!Y` with `?Z`
     // (where `?Z` is in a lower universe than `X`), but now we must prove that `!Y = ?Z`
     // (this may be posible due to assumptions).

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

@@ -1,15 +1,16 @@
 use formality_types::{
     cast::Downcast,
     grammar::{
-        AliasTy, InferenceVar, Parameter, Relation, RigidTy, TyData, Variable, Wc, WcData, Wcs,
+        AliasTy, ExistentialVar, Parameter, Relation, RigidTy, TyData, Variable, Wc, WcData, Wcs,
     },
     judgment_fn,
 };
 
 use crate::{
     decls::{AliasEqDeclBoundData, Decls},
     prove::{
-        env::Env, prove, prove_after::prove_after, prove_eq::prove_existential_var_eq, combinators::zip,
+        combinators::zip, env::Env, prove, prove_after::prove_after,
+        prove_eq::prove_existential_var_eq,
     },
 };
 
@@ -58,36 +59,36 @@ judgment_fn! {
     ) => (Constraints, Parameter) {
         debug(goal, via, assumptions, env, decls)
 
-        // The following 2 rules handle normalization of inference variables. We look specifically for
+        // The following 2 rules handle normalization of existential variables. We look specifically for
         // the case of a assumption `?X = Y`, which lets us normalize `?X` to `Y`, and ignore
         // everything else. In principle, we could allow the more general normalization rules
         // below handle this case too, but that generates a LOT of false paths, and I *believe*
         // it is unnecessary (FIXME: prove this).
 
         (
-            (if let Some(Variable::InferenceVar(v_a)) = a.downcast())
+            (if let Some(Variable::ExistentialVar(v_a)) = a.downcast())
             (if v_goal == v_a)
             ----------------------------- ("var-axiom-l")
-            (prove_normalize_via(_decls, env, _assumptions, Relation::Equals(a, b), Variable::InferenceVar(v_goal)) => (Constraints::none(env), b))
+            (prove_normalize_via(_decls, env, _assumptions, Relation::Equals(a, b), Variable::ExistentialVar(v_goal)) => (Constraints::none(env), b))
         )
 
         (
-            (if let Some(Variable::InferenceVar(v_a)) = a.downcast())
+            (if let Some(Variable::ExistentialVar(v_a)) = a.downcast())
             (if v_goal == v_a)
             ----------------------------- ("var-axiom-r")
-            (prove_normalize_via(_decls, env, _assumptions, Relation::Equals(b, a), Variable::InferenceVar(v_goal)) => (Constraints::none(env), b))
+            (prove_normalize_via(_decls, env, _assumptions, Relation::Equals(b, a), Variable::ExistentialVar(v_goal)) => (Constraints::none(env), b))
         )
 
         // The following 2 rules handle normalization of a type `X` given an assumption `X = Y`.
-        // We can't just check for `goal == a` though because we sometimes need to bind inference
+        // We can't just check for `goal == a` though because we sometimes need to bind existential
         // variables. Consider normalizing `R<?X>` given an assumption `R<u32> = Y`: this can be
         // normalized to `Y` given the constraint `?X = u32`.
         //
-        // We don't use these rules to normalize an inference variable `?X` because such a goal
+        // We don't use these rules to normalize an existential variable `?X` because such a goal
         // could be equated to everything, and thus generates a ton of spurious paths.
 
         (
-            (if let None = goal.downcast::<InferenceVar>())
+            (if let None = goal.downcast::<ExistentialVar>())
             (if goal != b)
             (prove_syntactically_eq(decls, env, assumptions, a, goal) => c)
             (let b = c.substitution().apply(&b))
@@ -96,7 +97,7 @@ judgment_fn! {
         )
 
         (
-            (if let None = goal.downcast::<InferenceVar>())
+            (if let None = goal.downcast::<ExistentialVar>())
             (if goal != b)
             (prove_syntactically_eq(decls, env, assumptions, a, goal) => c)
             (let b = c.substitution().apply(&b))
@@ -165,7 +166,7 @@ judgment_fn! {
         (
             (prove_existential_var_eq(decls, env, assumptions, v, t) => c)
             ----------------------------- ("existential-nonvar")
-            (prove_syntactically_eq(decls, env, assumptions, Variable::InferenceVar(v), t) => c)
+            (prove_syntactically_eq(decls, env, assumptions, Variable::ExistentialVar(v), t) => c)
         )
     }
 }

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

@@ -76,7 +76,7 @@ fn test_normalize_assoc_ty() {
 }
 
 #[test]
-fn test_normalize_assoc_ty_inference0() {
+fn test_normalize_assoc_ty_existential0() {
     let constraints = test_prove(
         Decls::empty(),
         term("exists<ty A> {} => {for<ty T> if { <T as Iterator>::Item = u32 } <A as Iterator>::Item = u32}"),
@@ -88,7 +88,7 @@ fn test_normalize_assoc_ty_inference0() {
 }
 
 #[test]
-fn test_normalize_assoc_ty_inference1() {
+fn test_normalize_assoc_ty_existential1() {
     let constraints = test_prove(
         Decls::empty(),
         term(

crates/formality-types/src/grammar/ty.rs

@@ -114,14 +114,14 @@ impl UpcastFrom<Ty> for TyData {
 }
 
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub struct InferenceVar {
+pub struct ExistentialVar {
     pub kind: ParameterKind,
     pub var_index: VarIndex,
 }
 
-cast_impl!(InferenceVar);
+cast_impl!(ExistentialVar);
 
-impl Visit for InferenceVar {
+impl Visit for ExistentialVar {
     fn free_variables(&self) -> Vec<Variable> {
         vec![self.upcast()]
     }
@@ -407,7 +407,7 @@ impl Visit for LtData {
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum Variable {
     UniversalVar(UniversalVar),
-    InferenceVar(InferenceVar),
+    ExistentialVar(ExistentialVar),
     BoundVar(BoundVar),
 }
 
@@ -417,7 +417,7 @@ impl Variable {
     pub fn kind(&self) -> ParameterKind {
         match self {
             Variable::UniversalVar(v) => v.kind,
-            Variable::InferenceVar(v) => v.kind,
+            Variable::ExistentialVar(v) => v.kind,
             Variable::BoundVar(v) => v.kind,
         }
     }
@@ -466,13 +466,13 @@ impl Variable {
     }
 
     /// A variable is *free* (i.e., not bound by any internal binder)
-    /// if it is an inference variable, a universal, or has a debruijn
+    /// if it is an existential variable, a universal, or has a debruijn
     /// index of `None`. The latter occurs when you `open` a binder (and before
     /// you close it back up again).
     pub fn is_free(&self) -> bool {
         match self {
             Variable::UniversalVar(_)
-            | Variable::InferenceVar(_)
+            | Variable::ExistentialVar(_)
             | Variable::BoundVar(BoundVar {
                 debruijn: None,
                 var_index: _,
@@ -490,7 +490,7 @@ impl Variable {
     pub fn is_universal(&self) -> bool {
         match self {
             Variable::UniversalVar(_) => true,
-            Variable::InferenceVar(_) => false,
+            Variable::ExistentialVar(_) => false,
             Variable::BoundVar(_) => false,
         }
     }
@@ -528,7 +528,7 @@ impl DowncastTo<Variable> for Parameter {
 }
 
 cast_impl!(BoundVar);
-cast_impl!((InferenceVar) <: (Variable) <: (Parameter));
+cast_impl!((ExistentialVar) <: (Variable) <: (Parameter));
 cast_impl!((BoundVar) <: (Variable) <: (Parameter));
 cast_impl!((UniversalVar) <: (Variable) <: (Parameter));
 
@@ -825,20 +825,20 @@ cast_impl!(TyData::PredicateTy(PredicateTy));
 cast_impl!(TyData::Variable(Variable));
 cast_impl!((Variable) <: (TyData) <: (Ty));
 cast_impl!((UniversalVar) <: (Variable) <: (TyData));
-cast_impl!((InferenceVar) <: (Variable) <: (TyData));
+cast_impl!((ExistentialVar) <: (Variable) <: (TyData));
 cast_impl!((BoundVar) <: (Variable) <: (TyData));
 cast_impl!((ScalarId) <: (RigidTy) <: (TyData));
 cast_impl!((UniversalVar) <: (Variable) <: (Ty));
-cast_impl!((InferenceVar) <: (Variable) <: (Ty));
+cast_impl!((ExistentialVar) <: (Variable) <: (Ty));
 cast_impl!((BoundVar) <: (Variable) <: (Ty));
 cast_impl!(Lt);
 cast_impl!(LtData::Variable(Variable));
-cast_impl!((InferenceVar) <: (Variable) <: (LtData));
+cast_impl!((ExistentialVar) <: (Variable) <: (LtData));
 cast_impl!((UniversalVar) <: (Variable) <: (LtData));
 cast_impl!((BoundVar) <: (Variable) <: (LtData));
 cast_impl!((UniversalVar) <: (LtData) <: (Lt));
-cast_impl!((InferenceVar) <: (LtData) <: (Lt));
+cast_impl!((ExistentialVar) <: (LtData) <: (Lt));
 cast_impl!((BoundVar) <: (LtData) <: (Lt));
 cast_impl!(Variable::UniversalVar(UniversalVar));
-cast_impl!(Variable::InferenceVar(InferenceVar));
+cast_impl!(Variable::ExistentialVar(ExistentialVar));
 cast_impl!(Variable::BoundVar(BoundVar));