Merge pull request #487 from jackh726/recursive_refactor

Refactor the recursive solver a bit

Author: nikomatsakis

chalk-engine/src/context.rs

@@ -34,11 +34,6 @@ use std::fmt::Debug;
 /// FIXME: Clone and Debug bounds are just for easy derive, they are
 /// not actually necessary. But dang are they convenient.
 pub trait Context<I: Interner>: Clone + Debug {
-    /// A final solution that is passed back to the user. This is
-    /// completely opaque to the SLG solver; it is produced by
-    /// `make_solution`.
-    type Solution;
-
     /// Represents an inference table.
     type InferenceTable: InferenceTable<I, Self> + Clone;
 
@@ -47,9 +42,7 @@ pub trait Context<I: Interner>: Clone + Debug {
     fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize;
 }
 
-pub trait ContextOps<I: Interner, C: Context<I>>:
-    Sized + Clone + Debug + AggregateOps<I, C>
-{
+pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug {
     /// True if this is a coinductive goal -- e.g., proving an auto trait.
     fn is_coinductive(&self, goal: &UCanonical<InEnvironment<Goal<I>>>) -> bool;
 
@@ -147,16 +140,6 @@ pub trait ContextOps<I: Interner, C: Context<I>>:
     ) -> bool;
 }
 
-/// Methods for combining solutions to yield an aggregate solution.
-pub trait AggregateOps<I: Interner, C: Context<I>> {
-    fn make_solution(
-        &self,
-        root_goal: &UCanonical<InEnvironment<Goal<I>>>,
-        answers: impl AnswerStream<I>,
-        should_continue: impl Fn() -> bool,
-    ) -> Option<C::Solution>;
-}
-
 /// An "inference table" contains the state to support unification and
 /// other operations on terms.
 pub trait InferenceTable<I: Interner, C: Context<I>>:

chalk-engine/src/forest.rs

@@ -3,11 +3,10 @@ use crate::logic::RootSearchFail;
 use crate::table::AnswerIndex;
 use crate::tables::Tables;
 use crate::{TableIndex, TimeStamp};
-use std::fmt::Display;
 
 use chalk_ir::debug;
 use chalk_ir::interner::Interner;
-use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, Substitution, UCanonical};
+use chalk_ir::{Goal, InEnvironment, Substitution, UCanonical};
 
 pub struct Forest<I: Interner, C: Context<I>> {
     pub(crate) tables: Tables<I>,
@@ -39,7 +38,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
     /// iterator. Each time you invoke `next`, it will do the work to
     /// extract one more answer. These answers are cached in between
     /// invocations. Invoking `next` fewer times is preferable =)
-    fn iter_answers<'f>(
+    pub fn iter_answers<'f>(
         &'f mut self,
         context: &'f impl ContextOps<I, C>,
         goal: &UCanonical<InEnvironment<Goal<I>>>,
@@ -54,89 +53,6 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
             _context: std::marker::PhantomData::<C>,
         }
     }
-
-    /// Solves a given goal, producing the solution. This will do only
-    /// as much work towards `goal` as it has to (and that works is
-    /// cached for future attempts).
-    pub fn solve(
-        &mut self,
-        context: &impl ContextOps<I, C>,
-        goal: &UCanonical<InEnvironment<Goal<I>>>,
-        should_continue: impl Fn() -> bool,
-    ) -> Option<C::Solution> {
-        context.make_solution(&goal, self.iter_answers(context, goal), should_continue)
-    }
-
-    /// Solves a given goal, producing the solution. This will do only
-    /// as much work towards `goal` as it has to (and that works is
-    /// cached for future attempts). Calls provided function `f` to
-    /// iterate over multiple solutions until the function return `false`.
-    pub fn solve_multiple(
-        &mut self,
-        context: &impl ContextOps<I, C>,
-        goal: &UCanonical<InEnvironment<Goal<I>>>,
-        mut f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
-    ) -> bool {
-        let mut answers = self.iter_answers(context, goal);
-        loop {
-            let subst = match answers.next_answer(|| true) {
-                AnswerResult::Answer(answer) => {
-                    if !answer.ambiguous {
-                        SubstitutionResult::Definite(answer.subst)
-                    } else {
-                        if context.is_trivial_constrained_substitution(&answer.subst) {
-                            SubstitutionResult::Floundered
-                        } else {
-                            SubstitutionResult::Ambiguous(answer.subst)
-                        }
-                    }
-                }
-                AnswerResult::Floundered => SubstitutionResult::Floundered,
-                AnswerResult::NoMoreSolutions => {
-                    return true;
-                }
-                AnswerResult::QuantumExceeded => continue,
-            };
-
-            if !f(subst, !answers.peek_answer(|| true).is_no_more_solutions()) {
-                return false;
-            }
-        }
-    }
-}
-
-#[derive(Debug)]
-pub enum SubstitutionResult<S> {
-    Definite(S),
-    Ambiguous(S),
-    Floundered,
-}
-
-impl<S> SubstitutionResult<S> {
-    pub fn as_ref(&self) -> SubstitutionResult<&S> {
-        match self {
-            SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
-            SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
-            SubstitutionResult::Floundered => SubstitutionResult::Floundered,
-        }
-    }
-    pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
-        match self {
-            SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
-            SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
-            SubstitutionResult::Floundered => SubstitutionResult::Floundered,
-        }
-    }
-}
-
-impl<S: Display> Display for SubstitutionResult<S> {
-    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        match self {
-            SubstitutionResult::Definite(subst) => write!(fmt, "{}", subst),
-            SubstitutionResult::Ambiguous(subst) => write!(fmt, "Ambiguous({})", subst),
-            SubstitutionResult::Floundered => write!(fmt, "Floundered"),
-        }
-    }
 }
 
 struct ForestSolver<'me, I: Interner, C: Context<I>, CO: ContextOps<I, C>> {

chalk-integration/src/db.rs

@@ -6,7 +6,6 @@ use crate::{
     query::{Lowering, LoweringDatabase},
     tls,
 };
-use chalk_engine::forest::SubstitutionResult;
 use chalk_ir::{
     AdtId, AssocTypeId, Canonical, ConstrainedSubst, Environment, FnDefId, GenericArg, Goal,
     ImplId, InEnvironment, OpaqueTyId, ProgramClause, ProgramClauses, TraitId, Ty, UCanonical,
@@ -15,7 +14,7 @@ use chalk_solve::rust_ir::{
     AdtDatum, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, FnDefDatum, ImplDatum,
     OpaqueTyDatum, TraitDatum, WellKnownTrait,
 };
-use chalk_solve::{RustIrDatabase, Solution, SolverChoice};
+use chalk_solve::{RustIrDatabase, Solution, SolverChoice, SubstitutionResult};
 use salsa::Database;
 use std::sync::Arc;
 
@@ -58,6 +57,10 @@ impl ChalkDatabase {
         solution
     }
 
+    /// Solves a given goal, producing the solution. This will do only
+    /// as much work towards `goal` as it has to (and that works is
+    /// cached for future attempts). Calls provided function `f` to
+    /// iterate over multiple solutions until the function return `false`.
     pub fn solve_multiple(
         &self,
         goal: &UCanonical<InEnvironment<Goal<ChalkIr>>>,

chalk-solve/src/lib.rs

@@ -109,3 +109,4 @@ pub use solve::Guidance;
 pub use solve::Solution;
 pub use solve::Solver;
 pub use solve::SolverChoice;
+pub use solve::SubstitutionResult;