Changed Forest::any_future_answer to take an answer index.

This allows us to replace an ad-hoc and probably wrong special case with
something that is actually very sensible.

Author: aatxe

chalk-engine/src/context/mod.rs

@@ -8,7 +8,7 @@ crate mod prelude;
 
 /// The "context" in which the SLG solver operates.
 pub trait Context: Sized + Clone + Debug + ContextOps<Self> + AggregateOps<Self> {
-    type CanonicalExClause: Debug;
+    type CanonicalExClause: CanonicalExClause<Self>;
 
     /// A map between universes. These are produced when
     /// u-canonicalizing something; they map canonical results back to
@@ -21,6 +21,10 @@ pub trait Context: Sized + Clone + Debug + ContextOps<Self> + AggregateOps<Self>
     /// [the rustc-guide]: https://rust-lang-nursery.github.io/rustc-guide/traits-canonicalization.html#canonicalizing-the-query-result
     type CanonicalConstrainedSubst: CanonicalConstrainedSubst<Self>;
 
+    /// Extracted from a canonicalized substitution or canonicalized ex clause, this is the type of
+    /// substitution that is fully normalized with respect to inference variables.
+    type InferenceNormalizedSubst: Debug;
+
     /// A canonicalized `GoalInEnvironment` -- that is, one where all
     /// free inference variables have been bound into the canonical
     /// binder. See [the rustc-guide] for more information.
@@ -285,9 +289,17 @@ pub trait Environment<C: Context, I: InferenceContext<C>>: Debug + Clone {
     fn add_clauses(&self, clauses: impl IntoIterator<Item = I::ProgramClause>) -> Self;
 }
 
+pub trait CanonicalExClause<C: Context>: Debug {
+    /// Extracts the inner normalized substitution.
+    fn inference_normalized_subst(&self) -> C::InferenceNormalizedSubst;
+}
+
 pub trait CanonicalConstrainedSubst<C: Context>: Clone + Debug + Eq + Hash + Ord {
     /// True if this solution has no region constraints.
     fn empty_constraints(&self) -> bool;
+
+    /// Extracts the inner normalized substitution.
+    fn inference_normalized_subst(&self) -> C::InferenceNormalizedSubst;
 }
 
 pub trait DomainGoal<C: Context, I: InferenceContext<C>>: Debug {
@@ -346,6 +358,6 @@ pub trait AnswerStream<C: Context> {
     /// if we find any answer for which `test` returns true.
     fn any_future_answer(
         &mut self,
-        test: impl FnMut(&mut C::CanonicalExClause) -> bool,
+        test: impl FnMut(&mut C::InferenceNormalizedSubst) -> bool,
     ) -> bool;
 }

chalk-engine/src/context/prelude.rs

@@ -11,6 +11,7 @@ crate use super::UnificationResult;
 crate use super::GoalInEnvironment;
 crate use super::UCanonicalGoalInEnvironment;
 crate use super::UniverseMap;
+crate use super::CanonicalExClause;
 crate use super::CanonicalConstrainedSubst;
 crate use super::Goal;
 crate use super::DomainGoal;

chalk-engine/src/forest.rs

@@ -174,8 +174,8 @@ where
 
     fn any_future_answer(
         &mut self,
-        test: impl FnMut(&mut C::CanonicalExClause) -> bool,
+        test: impl FnMut(&mut C::InferenceNormalizedSubst) -> bool,
     ) -> bool {
-        self.forest.any_future_answer(self.table, test)
+        self.forest.any_future_answer(self.table, self.answer, test)
     }
 }

chalk-engine/src/logic.rs

@@ -106,20 +106,17 @@ impl<C: Context> Forest<C> {
     pub(super) fn any_future_answer(
         &mut self,
         table: TableIndex,
-        mut test: impl FnMut(&mut C::CanonicalExClause) -> bool,
+        answer: AnswerIndex,
+        mut test: impl FnMut(&mut C::InferenceNormalizedSubst) -> bool,
     ) -> bool {
-        let mut strands = self.tables[table].strands_mut();
-
-        // If we don't have any strands at all, then we are
-        // intentionally conservative and say it may_invalidate.
-        match strands.next() {
-            None => return true,
-            Some(strand) => if test(&mut strand.canonical_ex_clause) {
-                return true
-            },
+        if let Some(answer) = self.tables[table].answer(answer) {
+            info!("answer cached = {:?}", answer);
+            return test(&mut answer.subst.inference_normalized_subst());
         }
 
-        strands.any(|strand| test(&mut strand.canonical_ex_clause))
+        self.tables[table].strands_mut().any(|strand| {
+            test(&mut strand.canonical_ex_clause.inference_normalized_subst())
+        })
     }
 
     /// Ensures that answer with the given index is available from the

src/solve/slg/implementation/mod.rs

@@ -55,6 +55,7 @@ impl context::Context for SlgContext {
     type UCanonicalGoalInEnvironment = UCanonical<InEnvironment<Goal>>;
     type UniverseMap = UniverseMap;
     type CanonicalConstrainedSubst = Canonical<ConstrainedSubst>;
+    type InferenceNormalizedSubst = Substitution;
     type Solution = Solution;
 }
 
@@ -238,11 +239,9 @@ impl context::Environment<SlgContext, SlgContext> for Arc<Environment> {
     }
 }
 
-impl Canonical<ExClause<SlgContext, SlgContext>> {
+impl Substitution {
     fn may_invalidate(&mut self, subst: &Canonical<Substitution>) -> bool {
-        self.value
-            .subst
-            .parameters
+        self.parameters
             .iter()
             .zip(&subst.value.parameters)
             .any(|(new, current)| MayInvalidate.aggregate_parameters(new, current))
@@ -413,10 +412,20 @@ impl context::DomainGoal<SlgContext, SlgContext> for DomainGoal {
     }
 }
 
+impl context::CanonicalExClause<SlgContext> for Canonical<ExClause<SlgContext, SlgContext>> {
+    fn inference_normalized_subst(&self) -> Substitution {
+        self.value.subst.clone()
+    }
+}
+
 impl context::CanonicalConstrainedSubst<SlgContext> for Canonical<ConstrainedSubst> {
     fn empty_constraints(&self) -> bool {
         self.value.constraints.is_empty()
     }
+
+    fn inference_normalized_subst(&self) -> Substitution {
+        self.value.subst.clone()
+    }
 }
 
 impl context::UCanonicalGoalInEnvironment<SlgContext> for UCanonical<InEnvironment<Goal>> {