Change WellFormed/FromEnv::Normalize to WellFormed/FromEnv::ProjectionEq

Author: scalexm

src/fold/mod.rs

@@ -405,8 +405,8 @@ macro_rules! enum_fold {
 enum_fold!(PolarizedTraitRef[] { Positive(a), Negative(a) });
 enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);
 enum_fold!(DomainGoal[] { Implemented(a), ProjectionEq(a), Normalize(a), UnselectedNormalize(a), WellFormed(a), FromEnv(a), InScope(a) });
-enum_fold!(WellFormed[] { Ty(a), TraitRef(a), Normalize(a) });
-enum_fold!(FromEnv[] { Ty(a), TraitRef(a), Normalize(a) });
+enum_fold!(WellFormed[] { Ty(a), TraitRef(a), ProjectionEq(a) });
+enum_fold!(FromEnv[] { Ty(a), TraitRef(a), ProjectionEq(a) });
 enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });
 enum_fold!(Constraint[] { LifetimeEq(a, b) });
 enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), Leaf(wc),

src/ir/debug.rs

@@ -202,7 +202,7 @@ impl Debug for WellFormed {
         let value: &Debug = match *self {
             WellFormed::Ty(ref t) => t,
             WellFormed::TraitRef(ref t) => t,
-            WellFormed::Normalize(ref t) => t,
+            WellFormed::ProjectionEq(ref t) => t,
         };
         write!(fmt, "WellFormed({:?})", value)
     }
@@ -213,7 +213,7 @@ impl Debug for FromEnv {
         let value: &Debug = match *self {
             FromEnv::Ty(ref t) => t,
             FromEnv::TraitRef(ref t) => t,
-            FromEnv::Normalize(ref t) => t,
+            FromEnv::ProjectionEq(ref t) => t,
         };
         write!(fmt, "FromEnv({:?})", value)
     }

src/ir/mod.rs

@@ -476,7 +476,7 @@ impl DomainGoal {
     crate fn into_well_formed_clause(self) -> DomainGoal {
         match self {
             DomainGoal::Implemented(tr) => DomainGoal::WellFormed(WellFormed::TraitRef(tr)),
-            DomainGoal::Normalize(n) => DomainGoal::WellFormed(WellFormed::Normalize(n)),
+            DomainGoal::ProjectionEq(n) => DomainGoal::WellFormed(WellFormed::ProjectionEq(n)),
             goal => goal,
         }
     }
@@ -485,7 +485,7 @@ impl DomainGoal {
     crate fn into_from_env_clause(self) -> DomainGoal {
         match self {
             DomainGoal::Implemented(tr) => DomainGoal::FromEnv(FromEnv::TraitRef(tr)),
-            DomainGoal::Normalize(n) => DomainGoal::FromEnv(FromEnv::Normalize(n)),
+            DomainGoal::ProjectionEq(n) => DomainGoal::FromEnv(FromEnv::ProjectionEq(n)),
             goal => goal,
         }
     }
@@ -521,7 +521,7 @@ pub struct EqGoal {
 pub enum WellFormed {
     Ty(Ty),
     TraitRef(TraitRef),
-    Normalize(Normalize),
+    ProjectionEq(ProjectionEq),
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
@@ -547,7 +547,7 @@ pub enum WellFormed {
 pub enum FromEnv {
     Ty(Ty),
     TraitRef(TraitRef),
-    Normalize(Normalize),
+    ProjectionEq(ProjectionEq),
 }
 
 /// Proves that the given projection **normalizes** to the given

src/lower/mod.rs

@@ -1468,6 +1468,9 @@ impl ir::AssociatedTyDatum {
         // `Normalize(<T as Foo>::Assoc -> U)`
         let normalize = ir::Normalize { projection: projection.clone(), ty: ty.clone() };
 
+        // `ProjectionEq(<T as Foo>::Assoc = U)`
+        let projection_eq = ir::ProjectionEq { projection: projection.clone(), ty };
+
         //    forall<T> {
         //        ProjectionEq(<T as Foo>::Assoc = U) :-
         //            Normalize(<T as Foo>::Assoc -> U)
@@ -1476,10 +1479,7 @@ impl ir::AssociatedTyDatum {
             implication: ir::Binders {
                 binders: binders.clone(),
                 value: ir::ProgramClauseImplication {
-                    consequence: ir::ProjectionEq {
-                        projection: projection.clone(),
-                        ty,
-                    }.cast(),
+                    consequence: projection_eq.clone().cast(),
                     conditions: vec![normalize.clone().cast()],
                 },
             },
@@ -1492,16 +1492,16 @@ impl ir::AssociatedTyDatum {
         //
         //    forall<T> {
         //        WellFormed(T: Foo<Assoc = U>) :-
-        //            WellFormed(T: Foo), Normalize(<T as Foo>::Assoc -> U)
+        //            WellFormed(T: Foo), ProjectionEq(<T as Foo>::Assoc = U)
         //    }
         clauses.push(ir::ProgramClause {
             implication: ir::Binders {
                 binders: binders.clone(),
                 value: ir::ProgramClauseImplication {
-                    consequence: ir::WellFormed::Normalize(normalize.clone()).cast(),
+                    consequence: ir::WellFormed::ProjectionEq(projection_eq.clone()).cast(),
                     conditions: vec![
-                        normalize.clone().cast(),
-                        ir::WellFormed::TraitRef(trait_ref.clone()).cast()
+                        ir::WellFormed::TraitRef(trait_ref.clone()).cast(),
+                        projection_eq.clone().cast()
                     ],
                 }
             }
@@ -1517,22 +1517,22 @@ impl ir::AssociatedTyDatum {
                 binders: binders.clone(),
                 value: ir::ProgramClauseImplication {
                     consequence: ir::FromEnv::TraitRef(trait_ref).cast(),
-                    conditions: vec![ir::FromEnv::Normalize(normalize.clone()).cast()],
+                    conditions: vec![ir::FromEnv::ProjectionEq(projection_eq.clone()).cast()],
                 },
             }
         });
 
         // And the other one being:
         //
         //    forall<T> {
-        //        Normalize(<T as Foo>::Assoc -> U) :- FromEnv(T: Foo<Assoc = U>)
+        //        ProjectionEq(<T as Foo>::Assoc = U) :- FromEnv(T: Foo<Assoc = U>)
         //    }
         clauses.push(ir::ProgramClause {
             implication: ir::Binders {
                 binders: binders,
                 value: ir::ProgramClauseImplication {
-                    consequence: normalize.clone().cast(),
-                    conditions: vec![ir::FromEnv::Normalize(normalize).cast()],
+                    consequence: projection_eq.clone().cast(),
+                    conditions: vec![ir::FromEnv::ProjectionEq(projection_eq).cast()],
                 },
             }
         });

src/zip.rs

@@ -224,8 +224,8 @@ enum_zip!(DomainGoal {
     InScope,
 });
 enum_zip!(LeafGoal { DomainGoal, EqGoal });
-enum_zip!(WellFormed { Ty, TraitRef, Normalize });
-enum_zip!(FromEnv { Ty, TraitRef, Normalize });
+enum_zip!(WellFormed { Ty, TraitRef, ProjectionEq });
+enum_zip!(FromEnv { Ty, TraitRef, ProjectionEq });
 
 // Annoyingly, Goal cannot use `enum_zip` because some variants have
 // two parameters, and I'm too lazy to make the macro account for the