Refactor WhereClauseAtom into WhereClause.

chalk-parse/src/ast.rs

@@ -1,7 +1,7 @@
 use lalrpop_intern::InternedString;
 use std::fmt;
 
-#[derive(Copy, Clone, Debug, PartialEq, Eq)]
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
 pub struct Span {
     pub lo: usize,
     pub hi: usize,
@@ -13,17 +13,20 @@ impl Span {
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct Program {
     pub items: Vec<Item>
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub enum Item {
     StructDefn(StructDefn),
     TraitDefn(TraitDefn),
     Impl(Impl),
     Clause(Clause),
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct StructDefn {
     pub name: Identifier,
     pub parameter_kinds: Vec<ParameterKind>,
@@ -32,11 +35,13 @@ pub struct StructDefn {
     pub flags: StructFlags,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct StructFlags {
     pub external: bool,
     pub fundamental: bool,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct TraitDefn {
     pub name: Identifier,
     pub parameter_kinds: Vec<ParameterKind>,
@@ -45,43 +50,50 @@ pub struct TraitDefn {
     pub flags: TraitFlags,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct TraitFlags {
     pub auto: bool,
     pub marker: bool,
     pub external: bool,
     pub deref: bool,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct AssocTyDefn {
     pub name: Identifier,
     pub parameter_kinds: Vec<ParameterKind>,
     pub bounds: Vec<InlineBound>,
     pub where_clauses: Vec<QuantifiedWhereClause>,
 }
 
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
 pub enum ParameterKind {
     Ty(Identifier),
     Lifetime(Identifier),
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub enum Parameter {
     Ty(Ty),
     Lifetime(Lifetime),
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 /// An inline bound, e.g. `: Foo<K>` in `impl<K, T: Foo<K>> SomeType<T>`.
 pub enum InlineBound {
     TraitBound(TraitBound),
     ProjectionEqBound(ProjectionEqBound),
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 /// Represents a trait bound on e.g. a type or type parameter.
 /// Does not know anything about what it's binding.
 pub struct TraitBound {
     pub trait_name: Identifier,
     pub args_no_self: Vec<Parameter>,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 /// Represents a projection equality bound on e.g. a type or type parameter.
 /// Does not know anything about what it's binding.
 pub struct ProjectionEqBound {
@@ -91,7 +103,7 @@ pub struct ProjectionEqBound {
     pub value: Ty,
 }
 
-#[derive(Copy, Clone, Debug, Eq, PartialEq)]
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
 pub enum Kind {
     Ty,
     Lifetime,
@@ -130,19 +142,22 @@ impl Kinded for Parameter {
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct Impl {
     pub parameter_kinds: Vec<ParameterKind>,
     pub trait_ref: PolarizedTraitRef,
     pub where_clauses: Vec<QuantifiedWhereClause>,
     pub assoc_ty_values: Vec<AssocTyValue>,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct AssocTyValue {
     pub name: Identifier,
     pub parameter_kinds: Vec<ParameterKind>,
     pub value: Ty,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub enum Ty {
     Id {
         name: Identifier,
@@ -163,28 +178,33 @@ pub enum Ty {
     }
 }
 
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
 pub enum Lifetime {
     Id {
         name: Identifier,
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct ProjectionTy {
     pub trait_ref: TraitRef,
     pub name: Identifier,
     pub args: Vec<Parameter>,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct UnselectedProjectionTy {
     pub name: Identifier,
     pub args: Vec<Parameter>,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct TraitRef {
     pub trait_name: Identifier,
     pub args: Vec<Parameter>,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub enum PolarizedTraitRef {
     Positive(TraitRef),
     Negative(TraitRef),
@@ -200,45 +220,60 @@ impl PolarizedTraitRef {
     }
 }
 
-#[derive(Copy, Clone, Debug)]
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
 pub struct Identifier {
     pub str: InternedString,
     pub span: Span,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub enum WhereClause {
     Implemented { trait_ref: TraitRef },
-    Normalize { projection: ProjectionTy, ty: Ty },
     ProjectionEq { projection: ProjectionTy, ty: Ty },
-    TyWellFormed { ty: Ty },
+}
+
+#[derive(Clone, PartialEq, Eq, Debug)]
+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 },
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub enum LeafGoal {
+    DomainGoal { goal: DomainGoal },
+    UnifyTys { a: Ty, b: Ty },
+    UnifyLifetimes { a: Lifetime, b: Lifetime },
+}
+
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct QuantifiedWhereClause {
     pub parameter_kinds: Vec<ParameterKind>,
     pub where_clause: WhereClause,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct Field {
     pub name: Identifier,
     pub ty: Ty,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 /// This allows users to add arbitrary `A :- B` clauses into the
 /// 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>>,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub enum Goal {
     ForAll(Vec<ParameterKind>, Box<Goal>),
     Exists(Vec<ParameterKind>, Box<Goal>),
@@ -247,5 +282,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),

src/ir.rs

@@ -6,6 +6,7 @@ use lalrpop_intern::InternedString;
 use std::collections::{BTreeMap, BTreeSet};
 use std::sync::Arc;
 use std::iter;
+use cast::Cast;
 
 #[macro_use]
 mod macros;
@@ -205,7 +206,7 @@ pub struct ImplDatum {
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct ImplDatumBound {
     crate trait_ref: PolarizedTraitRef,
-    crate where_clauses: Vec<QuantifiedDomainGoal>,
+    crate where_clauses: Vec<QuantifiedWhereClause>,
     crate associated_ty_values: Vec<AssociatedTyValue>,
     crate specialization_priority: usize,
 }
@@ -230,7 +231,7 @@ pub struct StructDatum {
 pub struct StructDatumBound {
     crate self_ty: ApplicationTy,
     crate fields: Vec<Ty>,
-    crate where_clauses: Vec<QuantifiedDomainGoal>,
+    crate where_clauses: Vec<QuantifiedWhereClause>,
     crate flags: StructFlags,
 }
 
@@ -248,7 +249,7 @@ pub struct TraitDatum {
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct TraitDatumBound {
     crate trait_ref: TraitRef,
-    crate where_clauses: Vec<QuantifiedDomainGoal>,
+    crate where_clauses: Vec<QuantifiedWhereClause>,
     crate flags: TraitFlags,
 }
 
@@ -272,10 +273,10 @@ impl InlineBound {
     ///
     /// Because an `InlineBound` does not know anything about what it's binding,
     /// you must provide that type as `self_ty`.
-    crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
+    crate fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
         match self {
-            InlineBound::TraitBound(b) => b.lower_with_self(self_ty),
-            InlineBound::ProjectionEqBound(b) => b.lower_with_self(self_ty),
+            InlineBound::TraitBound(b) => b.into_where_clauses(self_ty),
+            InlineBound::ProjectionEqBound(b) => b.into_where_clauses(self_ty),
         }
     }
 }
@@ -289,12 +290,12 @@ pub struct TraitBound {
 }
 
 impl TraitBound {
-    crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
+    crate fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
         let trait_ref = self.as_trait_ref(self_ty);
-        vec![DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref))]
+        vec![WhereClause::Implemented(trait_ref)]
     }
 
-    fn as_trait_ref(&self, self_ty: Ty) -> TraitRef {
+    crate fn as_trait_ref(&self, self_ty: Ty) -> TraitRef {
         let self_ty = ParameterKind::Ty(self_ty);
         TraitRef {
             trait_id: self.trait_id,
@@ -315,21 +316,21 @@ pub struct ProjectionEqBound {
 }
 
 impl ProjectionEqBound {
-    crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
+    crate fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
         let trait_ref = self.trait_bound.as_trait_ref(self_ty);
 
         let mut parameters = self.parameters.clone();
         parameters.extend(trait_ref.parameters.clone());
 
         vec![
-            DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref)),
-            DomainGoal::Holds(WhereClauseAtom::ProjectionEq(ProjectionEq {
+            WhereClause::Implemented(trait_ref),
+            WhereClause::ProjectionEq(ProjectionEq {
                 projection: ProjectionTy {
                     associated_ty_id: self.associated_ty_id,
                     parameters: parameters,
                 },
                 ty: self.value.clone(),
-            }))
+            }),
         ]
     }
 }
@@ -356,7 +357,7 @@ pub struct AssociatedTyDatum {
     crate bounds: Vec<InlineBound>,
 
     /// Where clauses that must hold for the projection to be well-formed.
-    crate where_clauses: Vec<QuantifiedDomainGoal>,
+    crate where_clauses: Vec<QuantifiedWhereClause>,
 }
 
 impl AssociatedTyDatum {
@@ -365,7 +366,7 @@ impl AssociatedTyDatum {
     /// ```notrust
     /// Implemented(<?0 as Foo>::Item<?1>: Sized)
     /// ```
-    crate fn bounds_on_self(&self) -> Vec<DomainGoal> {
+    crate fn bounds_on_self(&self) -> Vec<WhereClause> {
         let parameters = self.parameter_kinds
                              .anonymize()
                              .iter()
@@ -376,7 +377,7 @@ impl AssociatedTyDatum {
             associated_ty_id: self.id,
             parameters
         });
-        self.bounds.iter().flat_map(|b| b.lower_with_self(self_ty.clone())).collect()
+        self.bounds.iter().flat_map(|b| b.into_where_clauses(self_ty.clone())).collect()
     }
 }
 
@@ -605,9 +606,9 @@ impl PolarizedTraitRef {
     }
 }
 
-/// "Basic" where clauses which have a WF/FromEnv version of themselves.
+/// Where clauses that can be written by a Rust programmer.
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-pub enum WhereClauseAtom {
+pub enum WhereClause {
     Implemented(TraitRef),
     ProjectionEq(ProjectionEq),
 }
@@ -618,13 +619,8 @@ pub struct Derefs {
     pub target: Ty,
 }
 
-/// A "domain goal" is a goal that is directly about Rust, rather than a pure
-/// logical statement. As much as possible, the Chalk solver should avoid
-/// decomposing this enum, and instead treat its values opaquely.
-#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-pub enum DomainGoal {
-    Holds(WhereClauseAtom),
-
+#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
+pub enum WellFormed {
     /// A predicate which is true is some trait ref is well-formed.
     /// For example, given the following trait definitions:
     ///
@@ -635,8 +631,23 @@ pub enum DomainGoal {
     ///
     /// then we have the following rule:
     /// `WellFormed(?Self: Copy) :- ?Self: Copy, WellFormed(?Self: Clone)`.
-    WellFormed(WhereClauseAtom),
+    Trait(TraitRef),
+
+    /// A predicate which is true is some type is well-formed.
+    /// For example, given the following type definition:
+    ///
+    /// ```notrust
+    /// struct Set<K> where K: Hash {
+    ///     ...
+    /// }
+    /// ```
+    ///
+    /// then we have the following rule: `WellFormedTy(Set<K>) :- Implemented(K: Hash)`.
+    Ty(Ty),
+}
 
+#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
+pub enum FromEnv {
     /// A predicate which enables deriving everything which should be true if we *know* that
     /// some trait ref is well-formed. For example given the above trait definitions, we can use
     /// `FromEnv(T: Copy)` to derive that `T: Clone`, like in:
@@ -648,23 +659,7 @@ pub enum DomainGoal {
     ///     }
     /// }
     /// ```
-    FromEnv(WhereClauseAtom),
-
-
-    Normalize(Normalize),
-    UnselectedNormalize(UnselectedNormalize),
-
-    /// A predicate which is true is some type is well-formed.
-    /// For example, given the following type definition:
-    ///
-    /// ```notrust
-    /// struct Set<K> where K: Hash {
-    ///     ...
-    /// }
-    /// ```
-    ///
-    /// then we have the following rule: `WellFormedTy(Set<K>) :- Implemented(K: Hash)`.
-    WellFormedTy(Ty),
+    Trait(TraitRef),
 
     /// A predicate which enables deriving everything which should be true if we *know* that
     /// some type is well-formed. For example given the above type definition, we can use
@@ -677,7 +672,21 @@ pub enum DomainGoal {
     ///     }
     /// }
     /// ```
-    FromEnvTy(Ty),
+    Ty(Ty),
+}
+
+/// A "domain goal" is a goal that is directly about Rust, rather than a pure
+/// logical statement. As much as possible, the Chalk solver should avoid
+/// decomposing this enum, and instead treat its values opaquely.
+#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
+pub enum DomainGoal {
+    Holds(WhereClause),
+    WellFormed(WellFormed),
+    FromEnv(FromEnv),
+
+
+    Normalize(Normalize),
+    UnselectedNormalize(UnselectedNormalize),
 
     InScope(ItemId),
 
@@ -703,26 +712,33 @@ pub enum DomainGoal {
     LocalImplAllowed(TraitRef),
 }
 
-pub type QuantifiedDomainGoal = Binders<DomainGoal>;
+pub type QuantifiedWhereClause = Binders<WhereClause>;
 
-impl DomainGoal {
+impl WhereClause {
     /// Turn a where clause into the WF version of it i.e.:
     /// * `Implemented(T: Trait)` maps to `WellFormed(T: Trait)`
     /// * `ProjectionEq(<T as Trait>::Item = Foo)` maps to `WellFormed(<T as Trait>::Item = Foo)`
     /// * any other clause maps to itself
     crate fn into_well_formed_goal(self) -> DomainGoal {
         match self {
-            DomainGoal::Holds(wca) => DomainGoal::WellFormed(wca),
-            goal => goal,
+            WhereClause::Implemented(trait_ref) => WellFormed::Trait(trait_ref).cast(),
+            wc => wc.cast(),
         }
     }
 
     /// Same as `into_well_formed_goal` but with the `FromEnv` predicate instead of `WellFormed`.
     crate fn into_from_env_goal(self) -> DomainGoal {
         match self {
-            DomainGoal::Holds(wca @ WhereClauseAtom::Implemented(..)) => {
-                DomainGoal::FromEnv(wca)
-            }
+            WhereClause::Implemented(trait_ref) => FromEnv::Trait(trait_ref).cast(),
+            wc => wc.cast(),
+        }
+    }
+}
+
+impl DomainGoal {
+    crate fn into_from_env_goal(self) -> DomainGoal {
+        match self {
+            DomainGoal::Holds(wc) => wc.into_from_env_goal(),
             goal => goal,
         }
     }
@@ -1055,14 +1071,14 @@ impl Goal {
         match self {
             Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Holds(wca))) => {
                 match wca {
-                    WhereClauseAtom::Implemented(tr) => {
+                    WhereClause::Implemented(tr) => {
                         let trait_datum = &program.trait_data[&tr.trait_id];
                         trait_datum.binders.value.flags.auto
                     }
-                    WhereClauseAtom::ProjectionEq(..) => false,
+                    WhereClause::ProjectionEq(..) => false,
                 }
             }
-            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(..))) => {
+            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..)))) => {
                 true
             }
             Goal::Quantified(QuantifierKind::ForAll, goal) => goal.value.is_coinductive(program),

src/ir/debug.rs

@@ -169,41 +169,29 @@ impl Debug for UnselectedNormalize {
     }
 }
 
-impl Debug for WhereClauseAtom {
+impl Debug for WhereClause {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match self {
-            WhereClauseAtom::Implemented(tr) => write!(
+            WhereClause::Implemented(tr) => write!(
                 fmt,
                 "Implemented({:?}: {:?}{:?})",
                 tr.parameters[0],
                 tr.trait_id,
                 Angle(&tr.parameters[1..])
             ),
-            WhereClauseAtom::ProjectionEq(p) => write!(fmt, "{:?}", p),
+            WhereClause::ProjectionEq(p) => write!(fmt, "{:?}", p),
         }
     }
 }
 
 impl Debug for DomainGoal {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match self {
-            DomainGoal::Holds(wca) => write!(fmt, "{:?}", wca),
-            DomainGoal::WellFormed(WhereClauseAtom::Implemented(tr)) => {
-                write!(fmt, "WellFormed({:?})", tr)
-            }
-            DomainGoal::WellFormed(WhereClauseAtom::ProjectionEq(p)) => {
-                write!(fmt, "WellFormed({:?})", p)
-            }
-            DomainGoal::FromEnv(WhereClauseAtom::Implemented(tr)) => {
-                write!(fmt, "FromEnv({:?})", tr)
-            }
-            DomainGoal::FromEnv(WhereClauseAtom::ProjectionEq(p)) => {
-                write!(fmt, "FromEnv({:?})", p)
-            }
+            DomainGoal::Holds(n) => write!(fmt, "{:?}", n),
+            DomainGoal::WellFormed(n) => write!(fmt, "{:?}", n),
+            DomainGoal::FromEnv(n) => write!(fmt, "{:?}", n),
             DomainGoal::Normalize(n) => write!(fmt, "{:?}", n),
             DomainGoal::UnselectedNormalize(n) => write!(fmt, "{:?}", n),
-            DomainGoal::WellFormedTy(t) => write!(fmt, "WellFormed({:?})", t),
-            DomainGoal::FromEnvTy(t) => write!(fmt, "FromEnv({:?})", t),
             DomainGoal::InScope(n) => write!(fmt, "InScope({:?})", n),
             DomainGoal::Derefs(n) => write!(fmt, "Derefs({:?})", n),
             DomainGoal::IsLocal(n) => write!(fmt, "IsLocal({:?})", n),

src/rules/wf.rs

@@ -109,45 +109,11 @@ impl FoldInputTypes for ProjectionEq {
     }
 }
 
-impl FoldInputTypes for WhereClauseAtom {
+impl FoldInputTypes for WhereClause {
     fn fold(&self, accumulator: &mut Vec<Ty>) {
         match self {
-            WhereClauseAtom::Implemented(tr) => tr.fold(accumulator),
-            WhereClauseAtom::ProjectionEq(p) => p.fold(accumulator),
-        }
-    }
-}
-
-impl FoldInputTypes for Normalize {
-    fn fold(&self, accumulator: &mut Vec<Ty>) {
-        self.projection.parameters.fold(accumulator);
-        self.ty.fold(accumulator);
-    }
-}
-
-impl FoldInputTypes for UnselectedNormalize {
-    fn fold(&self, accumulator: &mut Vec<Ty>) {
-        self.projection.parameters.fold(accumulator);
-        self.ty.fold(accumulator);
-    }
-}
-
-impl FoldInputTypes for DomainGoal {
-    fn fold(&self, accumulator: &mut Vec<Ty>) {
-        match self {
-            DomainGoal::Holds(wca) => wca.fold(accumulator),
-            DomainGoal::Normalize(n) => n.fold(accumulator),
-            DomainGoal::UnselectedNormalize(n) => n.fold(accumulator),
-
-            DomainGoal::WellFormed(..) |
-            DomainGoal::FromEnv(..) |
-            DomainGoal::WellFormedTy(..) |
-            DomainGoal::FromEnvTy(..) |
-            DomainGoal::IsLocal(..) |
-            DomainGoal::LocalImplAllowed(..) |
-            DomainGoal::Derefs(..) => panic!("unexpected where clause"),
-
-            DomainGoal::InScope(..) => (),
+            WhereClause::Implemented(tr) => tr.fold(accumulator),
+            WhereClause::ProjectionEq(p) => p.fold(accumulator),
         }
     }
 }
@@ -169,7 +135,9 @@ impl WfSolver {
             return true;
         }
 
-        let goals = input_types.into_iter().map(|ty| DomainGoal::WellFormedTy(ty).cast());
+        let goals = input_types.into_iter()
+                               .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)))
+                               .casted();
         let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
                         .expect("at least one goal");
 
@@ -248,7 +216,7 @@ impl WfSolver {
 
             let wf_goals =
                 input_types.into_iter()
-                           .map(|ty| DomainGoal::WellFormedTy(ty));
+                           .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)));
 
             let trait_ref = trait_ref.up_shift(assoc_ty.value.binders.len());
 
@@ -264,7 +232,7 @@ impl WfSolver {
             let bound_goals =
                 bounds.iter()
                       .map(|b| Subst::apply(&all_parameters, b))
-                      .flat_map(|b| b.lower_with_self(assoc_ty.value.value.ty.clone()))
+                      .flat_map(|b| b.into_where_clauses(assoc_ty.value.value.ty.clone()))
                       .map(|g| g.into_well_formed_goal());
 
             let goals = wf_goals.chain(bound_goals).casted();
@@ -301,11 +269,11 @@ impl WfSolver {
         // Things to prove well-formed: input types of the where-clauses, projection types
         // appearing in the header, associated type values, and of course the trait ref.
         let trait_ref_wf = DomainGoal::WellFormed(
-            WhereClauseAtom::Implemented(trait_ref.clone())
+            WellFormed::Trait(trait_ref.clone())
         );
         let goals =
             input_types.into_iter()
-                       .map(|ty| DomainGoal::WellFormedTy(ty).cast())
+                       .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)).cast())
                        .chain(assoc_ty_goals)
                        .chain(Some(trait_ref_wf).cast());
 
@@ -323,7 +291,11 @@ impl WfSolver {
                       .cloned()
                       .map(|wc| wc.map(|bound| bound.into_from_env_goal()))
                       .casted()
-                      .chain(header_input_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast()))
+                      .chain(
+                          header_input_types.into_iter()
+                                            .map(|ty| DomainGoal::FromEnv(FromEnv::Ty(ty)))
+                                            .casted()
+                      )
                       .collect();
 
         let goal = Goal::Implies(hypotheses, Box::new(goal))

src/rules/wf/test.rs

@@ -206,7 +206,7 @@ fn wf_requiremements_for_projection() {
 }
 
 #[test]
-fn projection_type_in_header() {
+fn ill_formed_type_in_header() {
     lowering_error! {
         program {
             trait Foo {
@@ -215,8 +215,8 @@ fn projection_type_in_header() {
 
             trait Bar { }
 
-            // Projection types in an impl header are not assumed to be well-formed,
-            // an explicit where clause is needed (see below).
+            // Types in where clauses are not assumed to be well-formed,
+            // an explicit where clause would be needed (see below).
             impl<T> Bar for T where <T as Foo>::Value: Bar { }
         } error_msg {
             "trait impl for \"Bar\" does not meet well-formedness requirements"

src/zip.rs

@@ -216,15 +216,15 @@ macro_rules! enum_zip {
 /// variant, then zips each field of the variant in turn. Only works
 /// if all variants have a single parenthesized value right now.
 enum_zip!(PolarizedTraitRef { Positive, Negative });
-enum_zip!(WhereClauseAtom { Implemented, ProjectionEq });
+enum_zip!(WhereClause { Implemented, ProjectionEq });
+enum_zip!(WellFormed { Trait, Ty });
+enum_zip!(FromEnv { Trait, Ty });
 enum_zip!(DomainGoal {
     Holds,
     WellFormed,
     FromEnv,
     Normalize,
     UnselectedNormalize,
-    WellFormedTy,
-    FromEnvTy,
     InScope,
     Derefs,
     IsLocal,