rename placeholder to universal

Author: nikomatsakis

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

@@ -5,7 +5,7 @@ use formality_types::{
     collections::Set,
     fold::Fold,
     grammar::{
-        Binder, InferenceVar, ParameterKind, PlaceholderVar, VarIndex, VarSubstitution, Variable,
+        Binder, InferenceVar, ParameterKind, UniversalVar, VarIndex, VarSubstitution, Variable,
     },
     visit::Visit,
 };
@@ -59,7 +59,7 @@ impl Env {
             .variables
             .iter()
             .map(|v| match v {
-                Variable::PlaceholderVar(pv) => pv.var_index.index,
+                Variable::UniversalVar(pv) => pv.var_index.index,
                 Variable::InferenceVar(iv) => iv.var_index.index,
                 Variable::BoundVar(_) => panic!(),
             })
@@ -137,12 +137,12 @@ impl Env {
         vars
     }
 
-    pub fn universal_substitution<T>(&self, b: &Binder<T>) -> (Env, Vec<PlaceholderVar>)
+    pub fn universal_substitution<T>(&self, b: &Binder<T>) -> (Env, Vec<UniversalVar>)
     where
         T: Fold,
     {
         let mut env = self.clone();
-        let subst = env.fresh_substituion(b.kinds(), |kind, var_index| PlaceholderVar {
+        let subst = env.fresh_substituion(b.kinds(), |kind, var_index| UniversalVar {
             kind,
             var_index,
         });
@@ -153,7 +153,7 @@ impl Env {
     where
         T: Fold,
     {
-        let subst = self.fresh_substituion(b.kinds(), |kind, var_index| PlaceholderVar {
+        let subst = self.fresh_substituion(b.kinds(), |kind, var_index| UniversalVar {
             kind,
             var_index,
         });

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

@@ -2,7 +2,7 @@ use formality_types::{
     cast::{Downcast, Upcast},
     collections::Deduplicate,
     grammar::{
-        InferenceVar, Parameter, PlaceholderVar, Substitution, VarIndex, VarSubstitution, Variable,
+        InferenceVar, Parameter, Substitution, UniversalVar, VarIndex, VarSubstitution, Variable,
     },
     term::Term,
 };
@@ -24,7 +24,7 @@ pub fn minimize<T: Term>(env_max: Env, term: T) -> (Env, T, Minimization) {
         .iter()
         .zip(0..)
         .map(|(&fv, index)| match fv {
-            Variable::PlaceholderVar(PlaceholderVar { kind, var_index: _ }) => PlaceholderVar {
+            Variable::UniversalVar(UniversalVar { kind, var_index: _ }) => UniversalVar {
                 kind,
                 var_index: VarIndex { index },
             }

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, PlaceholderVar, Relation, RigidTy, Substitution, TyData,
+        AliasTy, InferenceVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar,
         Variable, Wcs,
     },
     judgment_fn, set,
@@ -103,7 +103,7 @@ judgment_fn! {
         (
             (if env.universe(p) < env.universe(v))
             ----------------------------- ("existential-placeholder")
-            (prove_existential_var_eq(_decls, env, _assumptions, v, Variable::PlaceholderVar(p)) => (env, (v, p)))
+            (prove_existential_var_eq(_decls, env, _assumptions, v, Variable::UniversalVar(p)) => (env, (v, p)))
         )
     }
 }
@@ -165,13 +165,13 @@ fn equate_variable(
             .chain(Some((x, universe_subst.apply(&p)).upcast())),
     );
 
-    // For each placeholder variable that we replaced with an inference variable
+    // For each universal variable that we replaced with an inference 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).
     let goals: Wcs = universe_subst
         .iter()
-        .filter(|(v, _)| v.is_a::<PlaceholderVar>())
+        .filter(|(v, _)| v.is_a::<UniversalVar>())
         .map(|(v, p)| eq(v, p))
         .upcasted()
         .collect();

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

@@ -1,5 +1,5 @@
 use formality_types::{
-    grammar::{Parameter, PlaceholderVar, RigidName, RigidTy, Wcs},
+    grammar::{Parameter, RigidName, RigidTy, UniversalVar, Wcs},
     judgment_fn,
 };
 
@@ -24,9 +24,9 @@ judgment_fn! {
             // are WF. An alternative would be to add explicit assumptions into the environment
             // for every universal variable. That just seems tedious.
             --- ("universal variables")
-            (prove_wf(_decls, env, _assumptions, PlaceholderVar { .. }) => Constraints::none(env))
+            (prove_wf(_decls, env, _assumptions, UniversalVar { .. }) => Constraints::none(env))
         )
- 
+
         (
             (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
             --- ("tuples")

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

@@ -49,7 +49,7 @@ fn not_partial_eq_implies_eq() {
 }
 
 #[test]
-fn placeholders_not_eq() {
+fn universals_not_eq() {
     let goal: Wc = term("for<ty T, ty U> if {Eq(T)} PartialEq(U)");
     let constraints = prove(decls(), (), (), goal);
     expect![[r#"

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

@@ -242,11 +242,11 @@ pub enum PredicateTy {
     ForAll(Binder<Ty>),
 }
 
-/// A *placeholder* is a dummy variable about which nothing is known except
+/// A *universal variable* is a dummy variable about which nothing is known except
 /// that which we see in the environment. When we want to prove something
-/// is true for all `T` (`∀T`), we replace `T` with a placeholder.
+/// is true for all `T` (`∀T`), we replace `T` with a universal variable.
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub struct PlaceholderVar {
+pub struct UniversalVar {
     pub kind: ParameterKind,
     pub var_index: VarIndex,
 }
@@ -406,7 +406,7 @@ impl Visit for LtData {
 
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum Variable {
-    PlaceholderVar(PlaceholderVar),
+    UniversalVar(UniversalVar),
     InferenceVar(InferenceVar),
     BoundVar(BoundVar),
 }
@@ -416,7 +416,7 @@ cast_impl!(Variable);
 impl Variable {
     pub fn kind(&self) -> ParameterKind {
         match self {
-            Variable::PlaceholderVar(v) => v.kind,
+            Variable::UniversalVar(v) => v.kind,
             Variable::InferenceVar(v) => v.kind,
             Variable::BoundVar(v) => v.kind,
         }
@@ -466,12 +466,12 @@ impl Variable {
     }
 
     /// A variable is *free* (i.e., not bound by any internal binder)
-    /// if it is an inference variable, a placeholder, or has a debruijn
+    /// if it is an inference 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::PlaceholderVar(_)
+            Variable::UniversalVar(_)
             | Variable::InferenceVar(_)
             | Variable::BoundVar(BoundVar {
                 debruijn: None,
@@ -489,7 +489,7 @@ impl Variable {
 
     pub fn is_universal(&self) -> bool {
         match self {
-            Variable::PlaceholderVar(_) => true,
+            Variable::UniversalVar(_) => true,
             Variable::InferenceVar(_) => false,
             Variable::BoundVar(_) => false,
         }
@@ -530,7 +530,7 @@ impl DowncastTo<Variable> for Parameter {
 cast_impl!(BoundVar);
 cast_impl!((InferenceVar) <: (Variable) <: (Parameter));
 cast_impl!((BoundVar) <: (Variable) <: (Parameter));
-cast_impl!((PlaceholderVar) <: (Variable) <: (Parameter));
+cast_impl!((UniversalVar) <: (Variable) <: (Parameter));
 
 /// Identifies a bound variable.
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
@@ -824,21 +824,21 @@ cast_impl!(TyData::AliasTy(AliasTy));
 cast_impl!(TyData::PredicateTy(PredicateTy));
 cast_impl!(TyData::Variable(Variable));
 cast_impl!((Variable) <: (TyData) <: (Ty));
-cast_impl!((PlaceholderVar) <: (Variable) <: (TyData));
+cast_impl!((UniversalVar) <: (Variable) <: (TyData));
 cast_impl!((InferenceVar) <: (Variable) <: (TyData));
 cast_impl!((BoundVar) <: (Variable) <: (TyData));
 cast_impl!((ScalarId) <: (RigidTy) <: (TyData));
-cast_impl!((PlaceholderVar) <: (Variable) <: (Ty));
+cast_impl!((UniversalVar) <: (Variable) <: (Ty));
 cast_impl!((InferenceVar) <: (Variable) <: (Ty));
 cast_impl!((BoundVar) <: (Variable) <: (Ty));
 cast_impl!(Lt);
 cast_impl!(LtData::Variable(Variable));
 cast_impl!((InferenceVar) <: (Variable) <: (LtData));
-cast_impl!((PlaceholderVar) <: (Variable) <: (LtData));
+cast_impl!((UniversalVar) <: (Variable) <: (LtData));
 cast_impl!((BoundVar) <: (Variable) <: (LtData));
-cast_impl!((PlaceholderVar) <: (LtData) <: (Lt));
+cast_impl!((UniversalVar) <: (LtData) <: (Lt));
 cast_impl!((InferenceVar) <: (LtData) <: (Lt));
 cast_impl!((BoundVar) <: (LtData) <: (Lt));
-cast_impl!(Variable::PlaceholderVar(PlaceholderVar));
+cast_impl!(Variable::UniversalVar(UniversalVar));
 cast_impl!(Variable::InferenceVar(InferenceVar));
 cast_impl!(Variable::BoundVar(BoundVar));

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

@@ -21,29 +21,23 @@ impl std::fmt::Debug for super::Lt {
 impl std::fmt::Debug for super::Variable {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
-            Self::PlaceholderVar(arg0) => write!(f, "{:?}", arg0),
+            Self::UniversalVar(arg0) => write!(f, "{:?}", arg0),
             Self::InferenceVar(arg0) => write!(f, "{:?}", arg0),
             Self::BoundVar(arg0) => write!(f, "{:?}", arg0),
         }
     }
 }
 
-impl std::fmt::Debug for super::PlaceholderVar {
+impl std::fmt::Debug for super::UniversalVar {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let super::PlaceholderVar {
-            var_index,
-            kind,
-        } = self;
+        let super::UniversalVar { var_index, kind } = self;
         write!(f, "!{:?}_{:?}", kind, var_index)
     }
 }
 
 impl std::fmt::Debug for super::InferenceVar {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let super::InferenceVar {
-            var_index,
-            kind,
-        } = self;
+        let super::InferenceVar { var_index, kind } = self;
         write!(f, "?{:?}_{:?}", kind, var_index)
     }
 }

crates/formality-types/src/visit.rs

@@ -26,15 +26,15 @@ pub trait Visit {
     /// This is to aid with fuzzing and bug detection.
     fn assert_valid(&self);
 
-    /// True if this term references only placeholder variables.
+    /// True if this term references only universal variables.
     /// This means that it contains no inference variables.
     /// If this is a goal, then when we prove it true, we don't expect any substitution.
     /// This is similar, but not *identical*, to the commonly used term "ground term",
     /// which in Prolog refers to a term that contains no variables. The difference here
     /// is that the term may contain variables, but only those instantiated universally (∀).
-    fn references_only_placeholder_variables(&self) -> bool {
+    fn references_only_universal_variables(&self) -> bool {
         self.free_variables().iter().all(|v| match v {
-            Variable::PlaceholderVar(_) => true,
+            Variable::UniversalVar(_) => true,
             Variable::InferenceVar(_) => false,
             Variable::BoundVar(_) => false,
         })