Merge pull request #93 from aatxe/issue-81

nikomatsakis · web-flow · commit 5e26056e8393 · 2018-04-02T17:48:38.000-04:00
Implement early stop for solver when no strands can invalidate the current substitution.
diff --git a/chalk-engine/src/context/mod.rs b/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.
@@ -157,7 +161,7 @@ pub trait AggregateOps<C: Context> {
     fn make_solution(
         &self,
         root_goal: &C::CanonicalGoalInEnvironment,
-        simplified_answers: impl IntoIterator<Item = SimplifiedAnswer<C>>,
+        simplified_answers: impl AnswerStream<C>,
     ) -> Option<C::Solution>;
 }
 
@@ -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 {
@@ -337,3 +349,15 @@ pub trait UnificationResult<C: Context, I: InferenceContext<C>> {
     /// Also add region constraints.
     fn into_ex_clause(self, ex_clause: &mut ExClause<C, I>);
 }
+
+pub trait AnswerStream<C: Context> {
+    fn peek_answer(&mut self) -> Option<SimplifiedAnswer<C>>;
+    fn next_answer(&mut self) -> Option<SimplifiedAnswer<C>>;
+
+    /// Invokes `test` with each possible future answer, returning true immediately
+    /// if we find any answer for which `test` returns true.
+    fn any_future_answer(
+        &mut self,
+        test: impl FnMut(&C::InferenceNormalizedSubst) -> bool,
+    ) -> bool;
+}
diff --git a/chalk-engine/src/context/prelude.rs b/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;
diff --git a/chalk-engine/src/forest.rs b/chalk-engine/src/forest.rs
@@ -1,5 +1,6 @@
 use crate::{DepthFirstNumber, SimplifiedAnswer, TableIndex};
 use crate::context::prelude::*;
+use crate::context::AnswerStream;
 use crate::logic::RootSearchFail;
 use crate::stack::{Stack, StackIndex};
 use crate::tables::Tables;
@@ -64,7 +65,7 @@ impl<C: Context> Forest<C> {
     fn iter_answers<'f>(
         &'f mut self,
         goal: &C::UCanonicalGoalInEnvironment,
-    ) -> impl Iterator<Item = SimplifiedAnswer<C>> + 'f {
+    ) -> impl AnswerStream<C> + 'f {
         let table = self.get_or_create_table_for_ucanonical_goal(goal.clone());
         let answer = AnswerIndex::ZERO;
         ForestSolver {
@@ -127,13 +128,11 @@ struct ForestSolver<'forest, C: Context + 'forest> {
     answer: AnswerIndex,
 }
 
-impl<'forest, C> Iterator for ForestSolver<'forest, C>
+impl<'forest, C> AnswerStream<C> for ForestSolver<'forest, C>
 where
     C: Context,
 {
-    type Item = SimplifiedAnswer<C>;
-
-    fn next(&mut self) -> Option<SimplifiedAnswer<C>> {
+    fn peek_answer(&mut self) -> Option<SimplifiedAnswer<C>> {
         loop {
             match self.forest.ensure_root_answer(self.table, self.answer) {
                 Ok(()) => {
@@ -154,8 +153,6 @@ where
                         ambiguous: !answer.delayed_literals.is_empty(),
                     };
 
-                    self.answer.increment();
-
                     return Some(simplified_answer);
                 }
 
@@ -167,4 +164,18 @@ where
             }
         }
     }
+
+    fn next_answer(&mut self) -> Option<SimplifiedAnswer<C>> {
+        self.peek_answer().map(|answer| {
+            self.answer.increment();
+            answer
+        })
+    }
+
+    fn any_future_answer(
+        &mut self,
+        test: impl FnMut(&C::InferenceNormalizedSubst) -> bool,
+    ) -> bool {
+        self.forest.any_future_answer(self.table, self.answer, test)
+    }
 }
diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs
@@ -103,6 +103,22 @@ impl<C: Context> Forest<C> {
         }
     }
 
+    pub(super) fn any_future_answer(
+        &mut self,
+        table: TableIndex,
+        answer: AnswerIndex,
+        mut test: impl FnMut(&C::InferenceNormalizedSubst) -> bool,
+    ) -> bool {
+        if let Some(answer) = self.tables[table].answer(answer) {
+            info!("answer cached = {:?}", answer);
+            return test(answer.subst.inference_normalized_subst());
+        }
+
+        self.tables[table].strands_mut().any(|strand| {
+            test(strand.canonical_ex_clause.inference_normalized_subst())
+        })
+    }
+
     /// Ensures that answer with the given index is available from the
     /// given table. Returns `Ok` if there is an answer:
     ///
diff --git a/src/solve/slg/implementation/aggregate.rs b/src/solve/slg/implementation/aggregate.rs
@@ -15,18 +15,16 @@ impl context::AggregateOps<SlgContext> for SlgContext {
     fn make_solution(
         &self,
         root_goal: &Canonical<InEnvironment<Goal>>,
-        simplified_answers: impl IntoIterator<Item = SimplifiedAnswer<SlgContext>>,
+        mut simplified_answers: impl context::AnswerStream<SlgContext>,
     ) -> Option<Solution> {
-        let mut simplified_answers = simplified_answers.into_iter().peekable();
-
         // No answers at all?
-        if simplified_answers.peek().is_none() {
+        if simplified_answers.peek_answer().is_none() {
             return None;
         }
-        let SimplifiedAnswer { subst, ambiguous } = simplified_answers.next().unwrap();
+        let SimplifiedAnswer { subst, ambiguous } = simplified_answers.next_answer().unwrap();
 
         // Exactly 1 unconditional answer?
-        if simplified_answers.peek().is_none() && !ambiguous {
+        if simplified_answers.peek_answer().is_none() && !ambiguous {
             return Some(Solution::Unique(subst));
         }
 
@@ -57,7 +55,13 @@ impl context::AggregateOps<SlgContext> for SlgContext {
                 break Guidance::Unknown;
             }
 
-            match simplified_answers.next() {
+            if !simplified_answers.any_future_answer(|ref mut new_subst| {
+                new_subst.may_invalidate(&subst)
+            }) {
+                break Guidance::Definite(subst);
+            }
+
+            match simplified_answers.next_answer() {
                 Some(answer1) => {
                     subst = merge_into_guidance(root_goal, subst, &answer1.subst);
                 }
diff --git a/src/solve/slg/implementation/mod.rs b/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,6 +239,157 @@ impl context::Environment<SlgContext, SlgContext> for Arc<Environment> {
     }
 }
 
+impl Substitution {
+    fn may_invalidate(&self, subst: &Canonical<Substitution>) -> bool {
+        self.parameters
+            .iter()
+            .zip(&subst.value.parameters)
+            .any(|(new, current)| MayInvalidate.aggregate_parameters(new, current))
+    }
+}
+
+// This is a struct in case we need to add state at any point like in AntiUnifier
+struct MayInvalidate;
+
+impl MayInvalidate {
+    fn aggregate_parameters(&mut self, new: &Parameter, current: &Parameter) -> bool {
+        match (new, current) {
+            (ParameterKind::Ty(ty1), ParameterKind::Ty(ty2)) => {
+                self.aggregate_tys(ty1, ty2)
+            }
+            (ParameterKind::Lifetime(l1), ParameterKind::Lifetime(l2)) => {
+                self.aggregate_lifetimes(l1, l2)
+            }
+            (ParameterKind::Ty(_), _) | (ParameterKind::Lifetime(_), _) => {
+                panic!("mismatched parameter kinds: new={:?} current={:?}", new, current)
+            }
+        }
+    }
+
+    // Returns true if the two types could be unequal.
+    fn aggregate_tys(&mut self, new: &Ty, current: &Ty) -> bool {
+        match (new, current) {
+            (_, Ty::Var(_)) => {
+                // If the aggregate solution already has an inference variable here, then no matter
+                // what type we produce, the aggregate cannot get 'more generalized' than it already
+                // is. So return false, we cannot invalidate.
+                false
+            }
+
+            (Ty::Var(_), _) => {
+                // If we see a type variable in the potential future solution, we have to be
+                // conservative. We don't know what type variable will wind up being! Remember that
+                // the future solution could be any instantiation of `ty0` -- or it could leave this
+                // variable unbound, if the result is true for all types.
+                true
+            }
+
+            // Aggregating universally-quantified types seems hard according to Niko. ;)
+            // Since this is the case, we are conservative here and just say we may invalidate.
+            (Ty::ForAll(_), Ty::ForAll(_)) => true,
+
+            (Ty::Apply(apply1), Ty::Apply(apply2)) => {
+                self.aggregate_application_tys(apply1, apply2)
+            }
+
+            (Ty::Projection(apply1), Ty::Projection(apply2)) => {
+                self.aggregate_projection_tys(apply1, apply2)
+            }
+
+            (Ty::UnselectedProjection(apply1), Ty::UnselectedProjection(apply2)) => {
+                self.aggregate_unselected_projection_tys(apply1, apply2)
+            }
+
+            (Ty::ForAll(_), _)
+            | (Ty::Apply(_), _)
+            | (Ty::Projection(_), _)
+            | (Ty::UnselectedProjection(_), _) => true,
+        }
+    }
+
+    fn aggregate_lifetimes(&mut self, _: &Lifetime, _: &Lifetime) -> bool {
+        true
+    }
+
+    fn aggregate_application_tys(
+        &mut self,
+        new: &ApplicationTy,
+        current: &ApplicationTy
+    ) -> bool {
+        let ApplicationTy {
+            name: new_name,
+            parameters: new_parameters,
+        } = new;
+        let ApplicationTy {
+            name: current_name,
+            parameters: current_parameters,
+        } = current;
+
+        self.aggregate_name_and_substs(new_name, new_parameters, current_name, current_parameters)
+    }
+
+    fn aggregate_projection_tys(&mut self, new: &ProjectionTy, current: &ProjectionTy) -> bool {
+        let ProjectionTy {
+            associated_ty_id: new_name,
+            parameters: new_parameters,
+        } = new;
+        let ProjectionTy {
+            associated_ty_id: current_name,
+            parameters: current_parameters,
+        } = current;
+
+        self.aggregate_name_and_substs(new_name, new_parameters, current_name, current_parameters)
+    }
+
+    fn aggregate_unselected_projection_tys(
+        &mut self,
+        new: &UnselectedProjectionTy,
+        current: &UnselectedProjectionTy,
+    ) -> bool {
+        let UnselectedProjectionTy {
+            type_name: new_name,
+            parameters: new_parameters,
+        } = new;
+        let UnselectedProjectionTy {
+            type_name: current_name,
+            parameters: current_parameters,
+        } = current;
+
+        self.aggregate_name_and_substs(new_name, new_parameters, current_name, current_parameters)
+    }
+
+    fn aggregate_name_and_substs<N>(
+        &mut self,
+        new_name: N,
+        new_parameters: &[Parameter],
+        current_name: N,
+        current_parameters: &[Parameter],
+    ) -> bool
+    where
+        N: Copy + Eq + Debug,
+    {
+        if new_name != current_name {
+            return true;
+        }
+
+        let name = new_name;
+
+        assert_eq!(
+            new_parameters.len(),
+            current_parameters.len(),
+            "does {:?} take {} parameters or {}? can't both be right",
+            name,
+            new_parameters.len(),
+            current_parameters.len()
+        );
+
+       new_parameters 
+            .iter()
+            .zip(current_parameters)
+            .any(|(new, current)| self.aggregate_parameters(new, current))
+    }
+}
+
 impl context::UniverseMap<SlgContext> for ::crate::solve::infer::ucanonicalize::UniverseMap {
     fn map_goal_from_canonical(
         &self,
@@ -260,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
+    }
+}
+
 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
+    }
 }
 
 impl context::UCanonicalGoalInEnvironment<SlgContext> for UCanonical<InEnvironment<Goal>> {
diff --git a/src/solve/slg/test.rs b/src/solve/slg/test.rs
