Merge pull request #36 from aturon/maybe-subst

Use substitutions and suggestions in Solution; implement negation

Author: nikomatsakis

chalk-parse/src/ast.rs

@@ -164,6 +164,7 @@ pub enum Goal {
     Exists(Vec<ParameterKind>, Box<Goal>),
     Implies(Vec<WhereClause>, Box<Goal>),
     And(Box<Goal>, Box<Goal>),
+    Not(Box<Goal>),
 
     // Additional kinds of goals:
     Leaf(WhereClause),

chalk-parse/src/parser.lalrpop

@@ -29,6 +29,7 @@ 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)),
+    "not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
     <w:WhereClause> => Box::new(Goal::Leaf(w)),
 };
 

chalk-parse/src/parser.rs

@@ -11,7 +11,6 @@ use std::sync::Arc;
 
 use chalk::ir;
 use chalk::lower::*;
-use chalk::solve::prove::Prove;
 use chalk::solve::solver::Solver;
 
 use rustyline::error::ReadlineError;
@@ -121,9 +120,13 @@ fn goal(text: &str, prog: &Program) -> Result<()> {
     let goal = chalk_parse::parse_goal(text)?.lower(&*prog.ir)?;
     let overflow_depth = 10;
     let mut solver = Solver::new(&prog.env, overflow_depth);
-    match Prove::new(&mut solver, goal).solve() {
-        Ok(v) => println!("{:#?}", v),
-        Err(e) => println!("{}", e),
+    let goal = ir::Canonical {
+        value: ir::InEnvironment::new(&ir::Environment::new(), *goal),
+        binders: vec![],
+    };
+    match solver.solve_goal(goal) {
+        Ok(v) => println!("{}\n", v),
+        Err(e) => println!("No possible solution: {}\n", e),
     }
     Ok(())
 }

src/bin/repl.rs

@@ -1,5 +1,4 @@
 use ir::*;
-use solve::Solution;
 
 pub trait Cast<T>: Sized {
     fn cast(self) -> T;
@@ -23,59 +22,62 @@ macro_rules! reflexive_impl {
 }
 
 reflexive_impl!(TraitRef);
-reflexive_impl!(WhereClause);
-reflexive_impl!(WhereClauseGoal);
+reflexive_impl!(LeafGoal);
+reflexive_impl!(DomainGoal);
 
-impl Cast<WhereClause> for TraitRef {
-    fn cast(self) -> WhereClause {
-        WhereClause::Implemented(self)
+impl Cast<DomainGoal> for TraitRef {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::Implemented(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for TraitRef {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::Implemented(self)
+impl Cast<LeafGoal> for TraitRef {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self.cast())
     }
 }
 
-impl Cast<WhereClause> for Normalize {
-    fn cast(self) -> WhereClause {
-        WhereClause::Normalize(self)
+impl Cast<DomainGoal> for Normalize {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::Normalize(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for Normalize {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::Normalize(self)
+impl Cast<LeafGoal> for Normalize {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self.cast())
     }
 }
 
-impl Cast<WhereClauseGoal> for WellFormed {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::WellFormed(self)
+impl Cast<DomainGoal> for WellFormed {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::WellFormed(self)
+    }
+}
+
+impl Cast<LeafGoal> for WellFormed {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self.cast())
     }
 }
 
 impl Cast<Goal> for WellFormed {
     fn cast(self) -> Goal {
-        let wcg: WhereClauseGoal = self.cast();
+        let wcg: LeafGoal = self.cast();
         wcg.cast()
     }
 }
 
 impl Cast<Goal> for Normalize {
     fn cast(self) -> Goal {
-        let wcg: WhereClauseGoal = self.cast();
+        let wcg: LeafGoal = self.cast();
         wcg.cast()
     }
 }
 
-impl Cast<WhereClauseGoal> for WhereClause {
-    fn cast(self) -> WhereClauseGoal {
-        match self {
-            WhereClause::Implemented(a) => a.cast(),
-            WhereClause::Normalize(a) => a.cast(),
-        }
+impl Cast<LeafGoal> for DomainGoal {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self)
     }
 }
 
@@ -85,27 +87,21 @@ impl Cast<Goal> for TraitRef {
     }
 }
 
-impl Cast<Goal> for WhereClause {
+impl Cast<Goal> for DomainGoal {
     fn cast(self) -> Goal {
         Goal::Leaf(self.cast())
     }
 }
 
-impl Cast<Goal> for WhereClauseGoal {
+impl Cast<Goal> for LeafGoal {
     fn cast(self) -> Goal {
         Goal::Leaf(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for Unify<Ty> {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::UnifyTys(self)
-    }
-}
-
-impl Cast<WhereClauseGoal> for Unify<Lifetime> {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::UnifyLifetimes(self)
+impl Cast<LeafGoal> for EqGoal {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::EqGoal(self)
     }
 }
 
@@ -126,10 +122,8 @@ macro_rules! map_impl {
 }
 
 map_impl!(impl[T: Cast<U>, U] Cast<Option<U>> for Option<T>);
-map_impl!(impl[T: Cast<U>, U] Cast<Query<U>> for Query<T>);
-map_impl!(impl[T: Cast<U>, U] Cast<Solution<U>> for Solution<T>);
+map_impl!(impl[T: Cast<U>, U] Cast<Canonical<U>> for Canonical<T>);
 map_impl!(impl[T: Cast<U>, U] Cast<InEnvironment<U>> for InEnvironment<T>);
-map_impl!(impl[T: Cast<U>, U] Cast<Constrained<U>> for Constrained<T>);
 map_impl!(impl[T: Cast<U>, U, E] Cast<Result<U, E>> for Result<T, E>);
 
 impl<T, U> Cast<Vec<U>> for Vec<T>

src/cast.rs

@@ -2,6 +2,7 @@ use errors::*;
 use ir::*;
 use std::fmt::Debug;
 use std::sync::Arc;
+use std::collections::BTreeMap;
 
 mod instantiate;
 mod shifted;
@@ -139,6 +140,23 @@ impl Fold for Lifetime {
     }
 }
 
+impl Fold for Substitution {
+    type Result = Substitution;
+    fn fold_with(&self, folder: &mut Folder, binders: usize) -> Result<Self::Result> {
+        let mut tys = BTreeMap::new();
+        let mut lifetimes = BTreeMap::new();
+
+        for (var, ty) in &self.tys {
+            tys.insert(*var, ty.fold_with(folder, binders)?);
+        }
+        for (var, lt) in &self.lifetimes {
+            lifetimes.insert(*var, lt.fold_with(folder, binders)?);
+        }
+
+        Ok(Substitution { tys, lifetimes })
+    }
+}
+
 macro_rules! copy_fold {
     ($t:ty) => {
         impl Fold for $t {
@@ -178,12 +196,11 @@ macro_rules! enum_fold {
 }
 
 enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);
-enum_fold!(WhereClause[] { Implemented(a), Normalize(a) });
+enum_fold!(DomainGoal[] { Implemented(a), RawNormalize(a), Normalize(a), WellFormed(a) });
 enum_fold!(WellFormed[] { Ty(a), TraitRef(a) });
-enum_fold!(WhereClauseGoal[] { Implemented(a), Normalize(a), UnifyTys(a),
-                               UnifyLifetimes(a), WellFormed(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), Leaf(wc) });
+enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), Leaf(wc) });
 
 macro_rules! struct_fold {
     ($s:ident $([$($n:ident),*])* { $($name:ident),* } $($w:tt)*) => {
@@ -206,6 +223,6 @@ struct_fold!(AssociatedTyValue { associated_ty_id, value });
 struct_fold!(AssociatedTyValueBound { ty, where_clauses });
 struct_fold!(Environment { universe, clauses });
 struct_fold!(InEnvironment[F] { environment, goal } where F: Fold);
-struct_fold!(Unify[T] { a, b } where T: Fold);
-struct_fold!(Constrained[F] { value, constraints } where F: Fold);
+struct_fold!(EqGoal { a, b });
 struct_fold!(ProgramClauseImplication { consequence, conditions });
+struct_fold!(ConstrainedSubst { subst, constraints });

src/fold/mod.rs

@@ -34,6 +34,7 @@ up_shift_method!(Ty);
 up_shift_method!(Parameter);
 up_shift_method!(Lifetime);
 up_shift_method!(TraitRef);
+up_shift_method!(ProjectionTy);
 
 impl Folder for Shifter {
     fn fold_free_var(&mut self, depth: usize, binders: usize) -> Result<Ty> {

src/fold/shifter.rs

@@ -145,35 +145,28 @@ impl Debug for Normalize {
     }
 }
 
-impl Debug for WhereClause {
+impl Debug for DomainGoal {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match *self {
-            WhereClause::Normalize(ref n) => write!(fmt, "{:?}", n),
-            WhereClause::Implemented(ref n) => {
+            DomainGoal::Normalize(ref n) => write!(fmt, "{:?}", n),
+            DomainGoal::RawNormalize(ref n) => write!(fmt, "raw {{ {:?} }}", n),
+            DomainGoal::Implemented(ref n) => {
                 write!(fmt,
                        "{:?}: {:?}{:?}",
                        n.parameters[0],
                        n.trait_id,
                        Angle(&n.parameters[1..]))
             }
+            DomainGoal::WellFormed(ref n) => write!(fmt, "{:?}", n),
         }
     }
 }
 
-impl Debug for WhereClauseGoal {
+impl Debug for LeafGoal {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match *self {
-            WhereClauseGoal::Normalize(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::Implemented(ref n) => {
-                write!(fmt,
-                       "{:?}: {:?}{:?}",
-                       n.parameters[0],
-                       n.trait_id,
-                       Angle(&n.parameters[1..]))
-            }
-            WhereClauseGoal::UnifyTys(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::UnifyLifetimes(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::WellFormed(ref n) => write!(fmt, "{:?}", n),
+            LeafGoal::EqGoal(ref eq) => write!(fmt, "{:?}", eq),
+            LeafGoal::DomainGoal(ref dom) => write!(fmt, "{:?}", dom),
         }
     }
 }
@@ -188,7 +181,7 @@ impl Debug for WellFormed {
     }
 }
 
-impl<T: Debug> Debug for Unify<T> {
+impl Debug for EqGoal {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         write!(fmt, "({:?} = {:?})", self.a, self.b)
     }
@@ -212,6 +205,7 @@ impl Debug for Goal {
             }
             Goal::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
             Goal::And(ref g1, ref g2) => write!(fmt, "({:?}, {:?})", g1, g2),
+            Goal::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
             Goal::Leaf(ref wc) => write!(fmt, "{:?}", wc),
         }
     }