Replace WhereClauseAtom with WhereClause

Author: scalexm

chalk-parse/src/ast.rs

@@ -208,19 +208,27 @@ pub struct Identifier {
 
 pub enum WhereClause {
     Implemented { trait_ref: TraitRef },
-    Normalize { projection: ProjectionTy, ty: Ty },
     ProjectionEq { projection: ProjectionTy, ty: Ty },
-    TyWellFormed { ty: Ty },
+}
+
+pub enum DomainGoal {
+    Holds { where_clause: WhereClause },
+    Normalize { projection: ProjectionTy, ty: Ty },
     TraitRefWellFormed { trait_ref: TraitRef },
+    TyWellFormed { ty: Ty },
     TyFromEnv { ty: Ty },
     TraitRefFromEnv { trait_ref: TraitRef },
-    UnifyTys { a: Ty, b: Ty },
-    UnifyLifetimes { a: Lifetime, b: Lifetime },
     TraitInScope { trait_name: Identifier },
     Derefs { source: Ty, target: Ty },
     IsLocal { ty: Ty },
 }
 
+pub enum LeafGoal {
+    DomainGoal { goal: DomainGoal },
+    UnifyTys { a: Ty, b: Ty },
+    UnifyLifetimes { a: Lifetime, b: Lifetime },
+}
+
 pub struct QuantifiedWhereClause {
     pub parameter_kinds: Vec<ParameterKind>,
     pub where_clause: WhereClause,
@@ -235,7 +243,7 @@ pub struct Field {
 /// logic; it has no equivalent in Rust, but it's useful for testing.
 pub struct Clause {
     pub parameter_kinds: Vec<ParameterKind>,
-    pub consequence: WhereClause,
+    pub consequence: DomainGoal,
     pub conditions: Vec<Box<Goal>>,
 }
 
@@ -247,5 +255,5 @@ pub enum Goal {
     Not(Box<Goal>),
 
     // Additional kinds of goals:
-    Leaf(WhereClause),
+    Leaf(LeafGoal),
 }

chalk-parse/src/parser.lalrpop

@@ -29,9 +29,9 @@ pub Goal: Box<Goal> = {
 Goal1: Box<Goal> = {
     "forall" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::ForAll(p, g)),
     "exists" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::Exists(p, g)),
-    "if" "(" <w:SemiColon<InlineClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),
+    "if" "(" <h:SemiColon<InlineClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(h, g)),
     "not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
-    <w:WhereClause> => Box::new(Goal::Leaf(w)),
+    <leaf:LeafGoal> => Box::new(Goal::Leaf(leaf)),
     "(" <Goal> ")",
 };
 
@@ -199,29 +199,29 @@ Field: Field = {
 };
 
 Clause: Clause = {
-    "forall" <pk:Angle<ParameterKind>> "{" <wc:WhereClause> "if" <g:Comma<Goal1>> "}" => Clause {
+    "forall" <pk:Angle<ParameterKind>> "{" <dg:DomainGoal> "if" <g:Comma<Goal1>> "}" => Clause {
         parameter_kinds: pk,
-        consequence: wc,
+        consequence: dg,
         conditions: g,
     },
 
-    "forall" <pk:Angle<ParameterKind>> "{" <wc:WhereClause> "}" => Clause {
+    "forall" <pk:Angle<ParameterKind>> "{" <dg:DomainGoal> "}" => Clause {
         parameter_kinds: pk,
-        consequence: wc,
+        consequence: dg,
         conditions: vec![],
     },
 };
 
 InlineClause1: Clause = {
-    <wc:WhereClause> => Clause {
+    <dg:DomainGoal> => Clause {
         parameter_kinds: vec![],
-        consequence: wc,
+        consequence: dg,
         conditions: vec![],
     },
 
-    <wc:WhereClause> ":" "-" <g:Comma<Goal1>> => Clause {
+    <dg:DomainGoal> ":" "-" <g:Comma<Goal1>> => Clause {
         parameter_kinds: vec![],
-        consequence: wc,
+        consequence: dg,
         conditions: g,
     },
 };
@@ -236,29 +236,9 @@ InlineClause: Clause = {
     }
 };
 
-QuantifiedWhereClauses: Vec<QuantifiedWhereClause> = {
-    "where" <Comma<QuantifiedWhereClause>>,
-    () => vec![],
-};
-
 WhereClause: WhereClause = {
     <t:TraitRef<":">> => WhereClause::Implemented { trait_ref: t },
 
-    "WellFormed" "(" <t:Ty> ")" => WhereClause::TyWellFormed { ty: t },
-
-    "WellFormed" "(" <t:TraitRef<":">> ")" => WhereClause::TraitRefWellFormed { trait_ref: t },
-
-    "FromEnv" "(" <t:Ty> ")" => WhereClause::TyFromEnv { ty: t },
-
-    "FromEnv" "(" <t:TraitRef<":">> ")" => WhereClause::TraitRefFromEnv { trait_ref: t },
-
-    <a:Ty> "=" <b:Ty> => WhereClause::UnifyTys { a, b },
-
-    <a:Lifetime> "=" <b:Lifetime> => WhereClause::UnifyLifetimes { a, b },
-
-    // `<T as Foo>::U -> Bar` -- a normalization
-    "Normalize" "(" <s:ProjectionTy> "->" <t:Ty> ")" => WhereClause::Normalize { projection: s, ty: t },
-
     // `T: Foo<U = Bar>` -- projection equality
     <s:Ty> ":" <t:Id> "<" <a:(<Comma<Parameter>> ",")?> <name:Id> <a2:Angle<Parameter>>
         "=" <ty:Ty> ">" =>
@@ -269,11 +249,6 @@ WhereClause: WhereClause = {
         let projection = ProjectionTy { trait_ref, name, args: a2 };
         WhereClause::ProjectionEq { projection, ty }
     },
-
-    "InScope" "(" <t:Id> ")" => WhereClause::TraitInScope { trait_name: t },
-    "Derefs" "(" <source:Ty> "," <target:Ty> ")" => WhereClause::Derefs { source, target },
-
-    "IsLocal" "(" <ty:Ty> ")" => WhereClause::IsLocal { ty },
 };
 
 QuantifiedWhereClause: QuantifiedWhereClause = {
@@ -288,6 +263,40 @@ QuantifiedWhereClause: QuantifiedWhereClause = {
     },
 };
 
+QuantifiedWhereClauses: Vec<QuantifiedWhereClause> = {
+    "where" <Comma<QuantifiedWhereClause>>,
+    () => vec![],
+};
+
+DomainGoal: DomainGoal = {
+    <wc: WhereClause> => DomainGoal::Holds { where_clause: wc },
+
+    "WellFormed" "(" <t:Ty> ")" => DomainGoal::TyWellFormed { ty: t },
+
+    "WellFormed" "(" <t:TraitRef<":">> ")" => DomainGoal::TraitRefWellFormed { trait_ref: t },
+
+    "FromEnv" "(" <t:Ty> ")" => DomainGoal::TyFromEnv { ty: t },
+
+    "FromEnv" "(" <t:TraitRef<":">> ")" => DomainGoal::TraitRefFromEnv { trait_ref: t },
+
+    // `<T as Foo>::U -> Bar` -- a normalization
+    "Normalize" "(" <s:ProjectionTy> "->" <t:Ty> ")" => DomainGoal::Normalize { projection: s, ty: t },
+
+    "InScope" "(" <t:Id> ")" => DomainGoal::TraitInScope { trait_name: t },
+
+    "Derefs" "(" <source:Ty> "," <target:Ty> ")" => DomainGoal::Derefs { source, target },
+
+    "IsLocal" "(" <ty:Ty> ")" => DomainGoal::IsLocal { ty },
+};
+
+LeafGoal: LeafGoal = {
+    <dg: DomainGoal> => LeafGoal::DomainGoal { goal: dg },
+
+    <a:Ty> "=" <b:Ty> => LeafGoal::UnifyTys { a, b },
+
+    <a:Lifetime> "=" <b:Lifetime> => LeafGoal::UnifyLifetimes { a, b },
+};
+
 TraitRef<S>: TraitRef = {
     <s:Ty> S <t:Id> <a:Angle<Parameter>> => {
         let mut args = vec![Parameter::Ty(s)];

src/cast.rs

@@ -50,21 +50,21 @@ macro_rules! reflexive_impl {
 reflexive_impl!(TraitRef);
 reflexive_impl!(LeafGoal);
 reflexive_impl!(DomainGoal);
-reflexive_impl!(WhereClauseAtom);
+reflexive_impl!(WhereClause);
 
-impl Cast<WhereClauseAtom> for TraitRef {
-    fn cast(self) -> WhereClauseAtom {
-        WhereClauseAtom::Implemented(self)
+impl Cast<WhereClause> for TraitRef {
+    fn cast(self) -> WhereClause {
+        WhereClause::Implemented(self)
     }
 }
 
-impl Cast<WhereClauseAtom> for ProjectionEq {
-    fn cast(self) -> WhereClauseAtom {
-        WhereClauseAtom::ProjectionEq(self)
+impl Cast<WhereClause> for ProjectionEq {
+    fn cast(self) -> WhereClause {
+        WhereClause::ProjectionEq(self)
     }
 }
 
-impl<T> Cast<DomainGoal> for T where T: Cast<WhereClauseAtom> {
+impl<T> Cast<DomainGoal> for T where T: Cast<WhereClause> {
     fn cast(self) -> DomainGoal {
         DomainGoal::Holds(self.cast())
     }
@@ -94,13 +94,25 @@ impl Cast<DomainGoal> for UnselectedNormalize {
     }
 }
 
+impl Cast<DomainGoal> for WellFormed {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::WellFormed(self)
+    }
+}
+
+impl Cast<DomainGoal> for FromEnv {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::FromEnv(self)
+    }
+}
+
 impl Cast<LeafGoal> for EqGoal {
     fn cast(self) -> LeafGoal {
         LeafGoal::EqGoal(self)
     }
 }
 
-impl Cast<Goal> for QuantifiedDomainGoal {
+impl<T: Cast<Goal>> Cast<Goal> for Binders<T> {
     fn cast(self) -> Goal {
         if self.binders.is_empty() {
             self.value.cast()
@@ -113,21 +125,6 @@ impl Cast<Goal> for QuantifiedDomainGoal {
     }
 }
 
-impl Cast<ProgramClause> for QuantifiedDomainGoal {
-    fn cast(self) -> ProgramClause {
-        if self.binders.is_empty() {
-            self.value.cast()
-        } else {
-            ProgramClause::ForAll(
-                self.map(|bound| ProgramClauseImplication {
-                    consequence: bound,
-                    conditions: vec![],
-                })
-            )
-        }
-    }
-}
-
 impl Cast<Ty> for ApplicationTy {
     fn cast(self) -> Ty {
         Ty::Apply(self)
@@ -152,15 +149,30 @@ impl Cast<Parameter> for Lifetime {
     }
 }
 
-impl Cast<ProgramClause> for DomainGoal {
+impl<T> Cast<ProgramClause> for T where T: Cast<DomainGoal> {
     fn cast(self) -> ProgramClause {
         ProgramClause::Implies(ProgramClauseImplication {
-            consequence: self,
+            consequence: self.cast(),
             conditions: vec![],
         })
     }
 }
 
+impl<T: Cast<DomainGoal>> Cast<ProgramClause> for Binders<T> {
+    fn cast(self) -> ProgramClause {
+        if self.binders.is_empty() {
+           Cast::<ProgramClause>::cast(self.value)
+        } else {
+            ProgramClause::ForAll(
+                self.map(|bound| ProgramClauseImplication {
+                    consequence: bound.cast(),
+                    conditions: vec![],
+                })
+            )
+        }
+    }
+}
+
 impl Cast<ProgramClause> for ProgramClauseImplication {
     fn cast(self) -> ProgramClause {
         ProgramClause::Implies(self)

src/fold.rs

@@ -423,9 +423,11 @@ 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!(WhereClauseAtom[] { Implemented(a), ProjectionEq(a) });
+enum_fold!(WhereClause[] { Implemented(a), ProjectionEq(a) });
+enum_fold!(WellFormed[] { Trait(a), Ty(a) });
+enum_fold!(FromEnv[] { Trait(a), Ty(a) });
 enum_fold!(DomainGoal[] { Holds(a), WellFormed(a), FromEnv(a), Normalize(a), UnselectedNormalize(a),
-                          WellFormedTy(a), FromEnvTy(a), InScope(a), Derefs(a), IsLocal(a), LocalImplAllowed(a) });
+                          InScope(a), Derefs(a), IsLocal(a), LocalImplAllowed(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),