Elaborate where clauses in Implies goals

Author: scalexm

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,7 +28,8 @@ 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)),
+    "if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, true)),
+    "if_raw" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, false)),
     "not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
     <w:WhereClause> => Box::new(Goal::Leaf(w)),
 };

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

@@ -225,6 +225,9 @@ pub struct AssociatedTyDatum {
     /// Parameters on this associated type, beginning with those from the trait,
     /// but possibly including more.
     pub parameter_kinds: Vec<ParameterKind<Identifier>>,
+
+    /// Where clauses that must hold for the projection be well-formed.
+    pub where_clauses: Vec<DomainGoal>,
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -367,7 +370,7 @@ impl DomainGoal {
     }
 
     /// 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>), (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 {
@@ -380,7 +383,6 @@ impl DomainGoal {
                     trait_id: associated_ty_data.trait_id,
                     parameters: trait_params.to_owned()
                 };
-                expanded.push(trait_ref.clone().cast());
                 expanded.push(WellFormed::TraitRef(trait_ref).cast());
             }
             _ => ()

src/lower/mod.rs

@@ -3,7 +3,7 @@ use std::collections::HashMap;
 use chalk_parse::ast::*;
 use lalrpop_intern::intern;
 
-use cast::Cast;
+use cast::{Cast, Caster};
 use errors::*;
 use ir;
 
@@ -167,6 +167,7 @@ impl LowerProgram for Program {
                             id: info.id,
                             name: defn.name.str,
                             parameter_kinds: parameter_kinds,
+                            where_clauses: vec![],
                         });
                     }
                 }
@@ -725,8 +726,19 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
                 g.lower_quantified(env, ir::QuantifierKind::ForAll, ids),
             Goal::Exists(ref ids, ref g) =>
                 g.lower_quantified(env, ir::QuantifierKind::Exists, ids),
-            Goal::Implies(ref wc, ref g) =>
-                Ok(Box::new(ir::Goal::Implies(wc.lower(env)?, g.lower(env)?))),
+            Goal::Implies(ref wc, ref g, elaborate) => {
+                let mut where_clauses = wc.lower(env)?;
+                if elaborate {
+                    where_clauses = ir::with_current_program(|program| {
+                        let program = program.expect("cannot elaborate without a program");
+                        where_clauses.into_iter()
+                                     .flat_map(|wc| wc.expanded(program))
+                                     .casted()
+                                     .collect()
+                    });
+                }
+                Ok(Box::new(ir::Goal::Implies(where_clauses, g.lower(env)?)))
+            }
             Goal::And(ref g1, ref g2) =>
                 Ok(Box::new(ir::Goal::And(g1.lower(env)?, g2.lower(env)?))),
             Goal::Not(ref g) =>
@@ -803,7 +815,7 @@ impl ir::ImplDatum {
                                      .iter()
                                      .cloned()
                                      .flat_map(|wc| wc.expanded(program))
-                                     .map(|wc| wc.cast())
+                                     .casted()
                                      .collect(),
                 }
             }),
@@ -935,12 +947,13 @@ impl ir::StructDatum {
                                              .iter()
                                              .filter_map(|pk| pk.as_ref().ty())
                                              .cloned()
-                                             .map(|ty| ir::WellFormed::Ty(ty).cast());
+                                             .map(|ty| ir::WellFormed::Ty(ty))
+                                             .casted();
 
                         let where_clauses = bound_datum.where_clauses.iter()
                                                        .cloned()
                                                        .flat_map(|wc| wc.expanded(program))
-                                                       .map(|wc| wc.cast());
+                                                       .casted();
 
                         tys.chain(where_clauses).collect()
                     }
@@ -987,9 +1000,10 @@ impl ir::TraitDatum {
                                                  .iter()
                                                  .filter_map(|pk| pk.as_ref().ty())
                                                  .cloned()
-                                                 .map(|ty| ir::WellFormed::Ty(ty).cast());
+                                                 .map(|ty| ir::WellFormed::Ty(ty))
+                                                 .casted();
 
-                        tys.chain(where_clauses.iter().cloned().map(|wc| wc.cast())).collect()
+                        tys.chain(where_clauses.iter().cloned().casted()).collect()
                     }
                 }
             }),

src/solve/test.rs

@@ -175,13 +175,23 @@ fn prove_forall() {
         // Here, we do know that `T: Clone`, so we can.
         goal {
             forall<T> {
-                if (WellFormed(T: Clone), T: Clone) {
+                if (T: Clone) {
                     Vec<T>: Clone
                 }
             }
         } yields {
             "Unique; substitution [], lifetime constraints []"
         }
+
+        goal {
+            forall<T> {
+                if_raw (T: Clone) {
+                    Vec<T>: Clone
+                }
+            }
+        } yields {
+            "CannotProve"
+        }
     }
 }
 
@@ -546,7 +556,7 @@ fn elaborate_eq() {
 
         goal {
             forall<T> {
-                if (WellFormed(T: Eq)) {
+                if (T: Eq) {
                     T: PartialEq
                 }
             }
@@ -567,7 +577,7 @@ fn elaborate_transitive() {
 
         goal {
             forall<T> {
-                if (WellFormed(T: StrictEq)) {
+                if (T: StrictEq) {
                     T: PartialEq
                 }
             }
@@ -596,7 +606,7 @@ fn elaborate_normalize() {
 
         goal {
             forall<T, U> {
-                if (WellFormed(T: Item), T: Item<Out = U>) {
+                if (T: Item<Out = U>) {
                     U: Eq
                 }
             }
@@ -753,6 +763,8 @@ fn trait_wf() {
 
             impl Ord<Int> for Int { }
             impl<T> Ord<Vec<T>> for Vec<T> where T: Ord<T> { }
+
+            impl<T> Ord<Slice<T>> for Slice<T> { }
         }
 
         goal {
@@ -779,13 +791,19 @@ fn trait_wf() {
             "Unique; substitution [], lifetime constraints []"
         }
 
+        goal {
+            Slice<Int>: Ord<Slice<Int>>
+        } yields {
+            "Unique"
+        }
+
         goal {
             Slice<Int>: Eq<Slice<Int>>
         } yields {
             "No possible solution"
         }
 
-        // not WF because previous equation doesn't hold
+        // not WF because previous equation doesn't hold, despite Slice<Int> having an impl for Ord<Int> 
         goal {
             WellFormed(Slice<Int>: Ord<Slice<Int>>)
         } yields {