Implement a tabling strategy for handling cycles

src/bin/chalki.rs

@@ -11,7 +11,7 @@ use std::sync::Arc;
 
 use chalk::ir;
 use chalk::lower::*;
-use chalk::solve::solver::Solver;
+use chalk::solve::solver::{Solver, CycleStrategy};
 
 use rustyline::error::ReadlineError;
 
@@ -118,8 +118,7 @@ fn read_program(rl: &mut rustyline::Editor<()>) -> Result<String> {
 
 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);
+    let mut solver = Solver::new(&prog.env, CycleStrategy::Tabling);
     let goal = ir::InEnvironment::new(&ir::Environment::new(), *goal);
     match solver.solve_closed_goal(goal) {
         Ok(v) => println!("{}\n", v),

src/overlap.rs

@@ -4,11 +4,11 @@ use itertools::Itertools;
 
 use errors::*;
 use ir::*;
-use solve::solver::Solver;
+use solve::solver::{Solver, CycleStrategy};
 
 impl Program {
     pub fn check_overlapping_impls(&self) -> Result<()> {
-        let mut solver = Solver::new(&Arc::new(self.environment()), 10);
+        let mut solver = Solver::new(&Arc::new(self.environment()), CycleStrategy::Tabling);
 
         // Create a vector of references to impl datums, sorted by trait ref
         let impl_data = self.impl_data.values().sorted_by(|lhs, rhs| {
@@ -80,7 +80,7 @@ fn intersection_of(lhs: &ImplDatum, rhs: &ImplDatum) -> InEnvironment<Goal> {
 
     let lhs_len = lhs.binders.len();
 
-    // Join the two impls' binders together 
+    // Join the two impls' binders together
     let mut binders = lhs.binders.binders.clone();
     binders.extend(rhs.binders.binders.clone());
 
@@ -100,7 +100,7 @@ fn intersection_of(lhs: &ImplDatum, rhs: &ImplDatum) -> InEnvironment<Goal> {
     // Create a goal for each clause in both where clauses
     let wc_goals = lhs_where_clauses.chain(rhs_where_clauses)
                 .map(|wc| Goal::Leaf(LeafGoal::DomainGoal(wc)));
- 
+
     // Join all the goals we've created together with And, then quantify them
     // over the joined binders. This is our query.
     let goal = params_goals.chain(wc_goals)

src/solve/solver.rs

@@ -4,16 +4,33 @@ use std::sync::Arc;
 use super::*;
 use solve::fulfill::Fulfill;
 
+/// We use a stack for detecting cycles. Each stack slot contains:
+/// - a goal which is being processed
+/// - a flag indicating the presence of a cycle during the processing of this goal
+/// - in case a cycle has been found, the latest previous answer to the same goal
+#[derive(Debug)]
+struct StackSlot {
+    goal: FullyReducedGoal,
+    cycle: bool,
+    answer: Option<Solution>,
+}
+
+/// For debugging purpose only: choose whether to apply a tabling strategy for cycles or
+/// treat them as hard errors (the latter can possibly reduce debug output)
+pub enum CycleStrategy {
+    Tabling,
+    Error,
+}
+
 /// A Solver is the basic context in which you can propose goals for a given
 /// program. **All questions posed to the solver are in canonical, closed form,
 /// so that each question is answered with effectively a "clean slate"**. This
 /// allows for better caching, and simplifies management of the inference
-/// context. Solvers do, however, maintain a stack of questions being posed, so
-/// as to avoid unbounded search.
+/// context.
 pub struct Solver {
     pub(super) program: Arc<ProgramEnvironment>,
-    overflow_depth: usize,
-    stack: Vec<FullyReducedGoal>,
+    stack: Vec<StackSlot>,
+    cycle_strategy: CycleStrategy,
 }
 
 /// An extension trait for merging `Result`s
@@ -35,11 +52,11 @@ impl<T> MergeWith<T> for Result<T> {
 }
 
 impl Solver {
-    pub fn new(program: &Arc<ProgramEnvironment>, overflow_depth: usize) -> Self {
+    pub fn new(program: &Arc<ProgramEnvironment>, cycle_strategy: CycleStrategy) -> Self {
         Solver {
             program: program.clone(),
             stack: vec![],
-            overflow_depth,
+            cycle_strategy,
         }
     }
 
@@ -88,67 +105,94 @@ impl Solver {
     pub fn solve_reduced_goal(&mut self, goal: FullyReducedGoal) -> Result<Solution> {
         debug_heading!("Solver::solve({:?})", goal);
 
-        // First we cut off runaway recursion
-        if self.stack.contains(&goal) || self.stack.len() > self.overflow_depth {
-            // Recursive invocation or overflow
-            debug!(
-                "solve: {:?} already on the stack or overflowed max depth",
-                goal
-            );
-            return Ok(Solution::Ambig(Guidance::Unknown));
+        // If the goal is already on the stack, we found a cycle and indicate it by setting
+        // `slot.cycle = true`. If there is no cached answer, we can't make any more progress
+        // and return `Err`. If there is one, use this answer.
+        if let Some(slot) = self.stack.iter_mut().find(|s| { s.goal == goal }) {
+            slot.cycle = true;
+            debug!("cycle detected: previous solution {:?}", slot.answer);
+            return slot.answer.clone().ok_or("cycle".into());
         }
-        self.stack.push(goal.clone());
 
-        let result = match goal {
-            FullyReducedGoal::EqGoal(g) => {
-                // Equality goals are understood "natively" by the logic, via unification:
-                self.solve_via_unification(g)
-            }
-            FullyReducedGoal::DomainGoal(Canonical { value, binders }) => {
-                // "Domain" goals (i.e., leaf goals that are Rust-specific) are
-                // always solved via some form of implication. We can either
-                // apply assumptions from our environment (i.e. where clauses),
-                // or from the lowered program, which includes fallback
-                // clauses. We try each approach in turn:
-
-                let env_clauses = value
-                    .environment
-                    .elaborated_clauses(&self.program)
-                    .map(DomainGoal::into_program_clause);
-                let env_solution = self.solve_from_clauses(&binders, &value, env_clauses);
-
-                let prog_clauses: Vec<_> = self.program.program_clauses.iter()
-                    .cloned()
-                    .filter(|clause| !clause.fallback_clause)
-                    .collect();
-                let prog_solution = self.solve_from_clauses(&binders, &value, prog_clauses);
-
-                // These fallback clauses are used when we're sure we'll never
-                // reach Unique via another route
-                let fallback: Vec<_> = self.program.program_clauses.iter()
-                    .cloned()
-                    .filter(|clause| clause.fallback_clause)
-                    .collect();
-                let fallback_solution = self.solve_from_clauses(&binders, &value, fallback);
-
-                // Now that we have all the outcomes, we attempt to combine
-                // them. Here, we apply a heuristic (also found in rustc): if we
-                // have possible solutions via both the environment *and* the
-                // program, we favor the environment; this only impacts type
-                // inference. The idea is that the assumptions you've explicitly
-                // made in a given context are more likely to be relevant than
-                // general `impl`s.
-
-                env_solution
-                    .merge_with(prog_solution, |env, prog| env.favor_over(prog))
-                    .merge_with(fallback_solution, |merged, fallback| merged.fallback_to(fallback))
-            }
-        };
+        // We start with `answer = None` and try to solve the goal. At the end of the iteration,
+        // `answer` will be updated with the result of the solving process. If we detect a cycle
+        // during the solving process, we cache `answer` and try to solve the goal again. We repeat
+        // until we reach a fixed point for `answer`.
+        // Considering the partial order:
+        // - None < Some(Unique) < Some(Ambiguous)
+        // - None < Some(CannotProve)
+        // the function which maps the loop iteration to `answer` is a nondecreasing function
+        // so this function will eventually be constant and the loop terminates.
+        let mut answer = None;
+        loop {
+            self.stack.push(StackSlot {
+                goal: goal.clone(),
+                cycle: false,
+                answer: answer.clone(),
+            });
 
-        self.stack.pop().unwrap();
+            debug!("Solver::solve: new loop iteration");
+            let result = match goal.clone() {
+                FullyReducedGoal::EqGoal(g) => {
+                    // Equality goals are understood "natively" by the logic, via unification:
+                    self.solve_via_unification(g)
+                }
+                FullyReducedGoal::DomainGoal(Canonical { value, binders }) => {
+                    // "Domain" goals (i.e., leaf goals that are Rust-specific) are
+                    // always solved via some form of implication. We can either
+                    // apply assumptions from our environment (i.e. where clauses),
+                    // or from the lowered program, which includes fallback
+                    // clauses. We try each approach in turn:
 
-        debug!("Solver::solve: result={:?}", result);
-        result
+                    let env_clauses = value
+                        .environment
+                        .elaborated_clauses(&self.program)
+                        .map(DomainGoal::into_program_clause);
+                    let env_solution = self.solve_from_clauses(&binders, &value, env_clauses);
+
+                    let prog_clauses: Vec<_> = self.program.program_clauses.iter()
+                        .cloned()
+                        .filter(|clause| !clause.fallback_clause)
+                        .collect();
+                    let prog_solution = self.solve_from_clauses(&binders, &value, prog_clauses);
+
+                    // These fallback clauses are used when we're sure we'll never
+                    // reach Unique via another route
+                    let fallback: Vec<_> = self.program.program_clauses.iter()
+                        .cloned()
+                        .filter(|clause| clause.fallback_clause)
+                        .collect();
+                    let fallback_solution = self.solve_from_clauses(&binders, &value, fallback);
+
+                    // Now that we have all the outcomes, we attempt to combine
+                    // them. Here, we apply a heuristic (also found in rustc): if we
+                    // have possible solutions via both the environment *and* the
+                    // program, we favor the environment; this only impacts type
+                    // inference. The idea is that the assumptions you've explicitly
+                    // made in a given context are more likely to be relevant than
+                    // general `impl`s.
+
+                    env_solution
+                        .merge_with(prog_solution, |env, prog| env.favor_over(prog))
+                        .merge_with(fallback_solution, |merged, fallback| merged.fallback_to(fallback))
+                }
+            };
+            debug!("Solver::solve: loop iteration result = {:?}", result);
+
+            let slot = self.stack.pop().unwrap();
+            match self.cycle_strategy {
+                CycleStrategy::Tabling if slot.cycle => {
+                    let actual_answer = result.as_ref().ok().map(|s| s.clone());
+                    if actual_answer == answer {
+                        // Fixed point: break
+                        return result;
+                    } else {
+                        answer = actual_answer;
+                    }
+                }
+                _ => return result,
+            };
+        }
     }
 
     fn solve_via_unification(

src/solve/test.rs

@@ -2,7 +2,7 @@ use chalk_parse;
 use errors::*;
 use ir;
 use lower::*;
-use solve::solver::Solver;
+use solve::solver::{Solver, CycleStrategy};
 use std::sync::Arc;
 
 fn parse_and_lower_program(text: &str) -> Result<ir::Program> {
@@ -35,11 +35,7 @@ fn solve_goal(program_text: &str,
             assert!(goal_text.ends_with("}"));
             let goal = parse_and_lower_goal(&program, &goal_text[1..goal_text.len()-1]).unwrap();
 
-            // Pick a low overflow depth just because the existing
-            // tests don't require a higher one.
-            let overflow_depth = 3;
-
-            let mut solver = Solver::new(&env, overflow_depth);
+            let mut solver = Solver::new(&env, CycleStrategy::Tabling);
             let goal = ir::InEnvironment::new(&ir::Environment::new(), *goal);
             let result = match solver.solve_closed_goal(goal) {
                 Ok(v) => format!("{}", v),
@@ -136,6 +132,8 @@ fn prove_forall() {
             impl<T> Marker for Vec<T> { }
 
             trait Clone { }
+            impl Clone for Foo { }
+
             impl<T> Clone for Vec<T> where T: Clone { }
         }
 
@@ -158,7 +156,7 @@ fn prove_forall() {
             "Unique; substitution [], lifetime constraints []"
         }
 
-        // We don't have know to anything about `T` to know that
+        // We don't have to know anything about `T` to know that
         // `Vec<T>: Marker`.
         goal {
             forall<T> { Vec<T>: Marker }
@@ -229,28 +227,66 @@ fn ordering() {
     }
 }
 
-/// This test forces the solver into an overflow scenario: `Foo` is
-/// only implemented for `S<S<S<...>>>` ad infinitum. So when asked to
-/// compute the type for which `Foo` is implemented, we wind up
-/// recursing for a while before we overflow. You can see that our
-/// final result is "Maybe" (i.e., either multiple proof trees or an
-/// infinite proof tree) and that we do conclude that, if a definite
-/// proof tree exists, it must begin with `S<S<S<S<...>>>>`.
 #[test]
-fn max_depth() {
+fn cycle_no_solution() {
+    test! {
+        program {
+            trait Foo { }
+            struct S<T> { }
+            impl<T> Foo for S<T> where T: Foo { }
+        }
+
+        // only solution: infinite type S<S<S<...
+        goal {
+            exists<T> {
+                T: Foo
+            }
+        } yields {
+            "No possible solution: no applicable candidates"
+        }
+    }
+}
+
+#[test]
+fn cycle_many_solutions() {
     test! {
         program {
             trait Foo { }
             struct S<T> { }
+            struct i32 { }
             impl<T> Foo for S<T> where T: Foo { }
+            impl Foo for i32 { }
+        }
+
+        // infinite family of solutions: {i32, S<i32>, S<S<i32>>, ... }
+        goal {
+            exists<T> {
+                T: Foo
+            }
+        } yields {
+            "Ambiguous; no inference guidance"
+        }
+    }
+}
+
+#[test]
+fn cycle_unique_solution() {
+    test! {
+        program {
+            trait Foo { }
+            trait Bar { }
+            struct S<T> { }
+            struct i32 { }
+            impl<T> Foo for S<T> where T: Foo, T: Bar { }
+            impl Foo for i32 { }
         }
 
         goal {
             exists<T> {
                 T: Foo
             }
         } yields {
-            "Ambiguous; definite substitution [?0 := S<S<S<S<?0>>>>]"
+            "Unique; substitution [?0 := i32]"
         }
     }
 }