Elaborating where clauses directly in the logic

chalk-parse/src/ast.rs

@@ -162,7 +162,10 @@ pub struct Field {
 pub enum Goal {
     ForAll(Vec<ParameterKind>, Box<Goal>),
     Exists(Vec<ParameterKind>, Box<Goal>),
-    Implies(Vec<WhereClause>, Box<Goal>),
+
+    // The `bool` flag indicates whether we should elaborate where clauses or not
+    Implies(Vec<WhereClause>, Box<Goal>, bool),
+
     And(Box<Goal>, Box<Goal>),
     Not(Box<Goal>),
 

chalk-parse/src/parser.lalrpop

@@ -28,11 +28,16 @@ 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:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),
+    <i:IfKeyword> "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, i)),
     "not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
     <w:WhereClause> => Box::new(Goal::Leaf(w)),
 };
 
+IfKeyword: bool = {
+    "if" => true,
+    "if_raw" => false,
+};
+
 StructDefn: StructDefn = {
     "struct" <n:Id><p:Angle<ParameterKind>> <w:WhereClauses> "{" <f:Fields> "}" => StructDefn {
         name: n,

src/cast.rs

@@ -1,4 +1,5 @@
 use ir::*;
+use std::marker::PhantomData;
 
 pub trait Cast<T>: Sized {
     fn cast(self) -> T;
@@ -130,7 +131,7 @@ impl<T, U> Cast<Vec<U>> for Vec<T>
     where T: Cast<U>
 {
     fn cast(self) -> Vec<U> {
-        self.into_iter().map(|v| v.cast()).collect()
+        self.into_iter().casted().collect()
     }
 }
 
@@ -145,3 +146,33 @@ impl Cast<Parameter> for Lifetime {
         ParameterKind::Lifetime(self)
     }
 }
+
+pub struct Casted<I, U> {
+    iterator: I,
+    _cast: PhantomData<U>,
+}
+
+impl<I: Iterator, U> Iterator for Casted<I, U> where I::Item: Cast<U> {
+    type Item = U;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        self.iterator.next().map(|item| item.cast())
+    }
+
+    fn size_hint(&self) -> (usize, Option<usize>) {
+        self.iterator.size_hint()
+    }
+}
+
+pub trait Caster<U>: Sized {
+    fn casted(self) -> Casted<Self, U>;
+}
+
+impl<I: Iterator, U> Caster<U> for I {
+    fn casted(self) -> Casted<Self, U> {
+        Casted {
+            iterator: self,
+            _cast: PhantomData,
+        }
+    }
+}

src/ir/mod.rs

@@ -1,9 +1,8 @@
 use cast::Cast;
 use chalk_parse::ast;
-use fold::Subst;
 use lalrpop_intern::InternedString;
 use solve::infer::{TyInferenceVariable, LifetimeInferenceVariable};
-use std::collections::{HashSet, HashMap, BTreeMap};
+use std::collections::{HashMap, BTreeMap};
 use std::sync::Arc;
 
 pub type Identifier = InternedString;
@@ -95,58 +94,6 @@ impl Environment {
         env.universe = UniverseIndex { counter: self.universe.counter + 1 };
         Arc::new(env)
     }
-
-    /// Generate the full set of clauses that are "syntactically implied" by the
-    /// clauses in this environment. Currently this consists of two kinds of expansions:
-    ///
-    /// - Supertraits are added, so `T: Ord` would expand to `T: Ord, T: PartialOrd`
-    /// - Projections imply that a trait is implemented, to `T: Iterator<Item=Foo>` expands to
-    ///   `T: Iterator, T: Iterator<Item=Foo>`
-    pub fn elaborated_clauses(&self, program: &ProgramEnvironment) -> impl Iterator<Item = DomainGoal> {
-        let mut set = HashSet::new();
-        set.extend(self.clauses.iter().cloned());
-
-        let mut stack: Vec<_> = set.iter().cloned().collect();
-
-        while let Some(clause) = stack.pop() {
-            let mut push_clause = |clause: DomainGoal| {
-                if !set.contains(&clause) {
-                    set.insert(clause.clone());
-                    stack.push(clause);
-                }
-            };
-
-            match clause {
-                DomainGoal::Implemented(ref trait_ref) => {
-                    // trait Foo<A> where Self: Bar<A> { }
-                    // T: Foo<U>
-                    // ----------------------------------------------------------
-                    // T: Bar<U>
-
-                    let trait_datum = &program.trait_data[&trait_ref.trait_id];
-                    for where_clause in &trait_datum.binders.value.where_clauses {
-                        let where_clause = Subst::apply(&trait_ref.parameters, where_clause);
-                        push_clause(where_clause);
-                    }
-                }
-                DomainGoal::Normalize(Normalize { ref projection, ty: _ }) => {
-                    // <T as Trait<U>>::Foo ===> V
-                    // ----------------------------------------------------------
-                    // T: Trait<U>
-
-                    let (associated_ty_data, trait_params, _) = program.split_projection(projection);
-                    let trait_ref = TraitRef {
-                        trait_id: associated_ty_data.trait_id,
-                        parameters: trait_params.to_owned()
-                    };
-                    push_clause(trait_ref.cast());
-                }
-                _ => {}
-            }
-        }
-
-        set.into_iter()
-    }
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
@@ -249,6 +196,7 @@ pub struct StructDatum {
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct StructDatumBound {
     pub self_ty: ApplicationTy,
+    pub fields: Vec<Ty>,
     pub where_clauses: Vec<DomainGoal>,
 }
 
@@ -420,6 +368,28 @@ impl DomainGoal {
             fallback_clause: false,
         }
     }
+
+    /// A clause of the form (T: Foo) expands to (T: Foo), WF(T: Foo).
+    /// A clause of the form (T: Foo<Item = U>) expands to (T: Foo<Item = U>), WF(T: Foo).
+    pub fn expanded(self, program: &Program) -> impl Iterator<Item = DomainGoal> {
+        let mut expanded = vec![];
+        match self {
+            DomainGoal::Implemented(ref trait_ref) => {
+                expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast());
+            }
+            DomainGoal::Normalize(Normalize { ref projection, .. }) => {
+                let (associated_ty_data, trait_params, _) = program.split_projection(&projection);
+                let trait_ref = TraitRef {
+                    trait_id: associated_ty_data.trait_id,
+                    parameters: trait_params.to_owned()
+                };
+                expanded.push(WellFormed::TraitRef(trait_ref).cast());
+            }
+            _ => ()
+        };
+        expanded.push(self.cast());
+        expanded.into_iter()
+    }
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]