Merge pull request #389 from Areredify/truncator

port truncator to use visitor

Author: nikomatsakis

chalk-engine/src/context.rs

@@ -369,8 +369,7 @@ pub trait UnificationOps<C: Context> {
 /// refers to the act of modifying a goal or answer that has become
 /// too large in order to guarantee termination.
 ///
-/// The SLG solver doesn't care about the precise truncation function,
-/// so long as it's deterministic and so forth.
+/// Currently we don't perform truncation (but it might me readded later).
 ///
 /// Citations:
 ///
@@ -379,21 +378,15 @@ pub trait UnificationOps<C: Context> {
 /// - Radial Restraint
 ///   - Grosof and Swift; 2013
 pub trait TruncateOps<C: Context> {
-    /// If `subgoal` is too large, return a truncated variant (else
-    /// return `None`).
-    fn truncate_goal(
+    /// Check if `subgoal` is too large
+    fn goal_needs_truncation(
         &mut self,
         interner: &C::Interner,
         subgoal: &C::GoalInEnvironment,
-    ) -> Option<C::GoalInEnvironment>;
+    ) -> bool;
 
-    /// If `subst` is too large, return a truncated variant (else
-    /// return `None`).
-    fn truncate_answer(
-        &mut self,
-        interner: &C::Interner,
-        subst: &C::Substitution,
-    ) -> Option<C::Substitution>;
+    /// Check if `subst` is too large
+    fn answer_needs_truncation(&mut self, interner: &C::Interner, subst: &C::Substitution) -> bool;
 }
 
 pub trait ResolventOps<C: Context> {

chalk-engine/src/logic.rs

@@ -328,9 +328,10 @@ impl<C: Context> Forest<C> {
         infer: &mut dyn InferenceTable<C>,
         subgoal: &C::GoalInEnvironment,
     ) -> Option<(C::UCanonicalGoalInEnvironment, C::UniverseMap)> {
-        match infer.truncate_goal(context.interner(), subgoal) {
-            Some(_) => None,
-            None => Some(infer.fully_canonicalize_goal(context.interner(), subgoal)),
+        if infer.goal_needs_truncation(context.interner(), subgoal) {
+            None
+        } else {
+            Some(infer.fully_canonicalize_goal(context.interner(), subgoal))
         }
     }
 
@@ -385,9 +386,10 @@ impl<C: Context> Forest<C> {
         // affect completeness when it comes to subgoal abstraction.
         let inverted_subgoal = infer.invert_goal(context.interner(), subgoal)?;
 
-        match infer.truncate_goal(context.interner(), &inverted_subgoal) {
-            Some(_) => None,
-            None => Some(infer.fully_canonicalize_goal(context.interner(), &inverted_subgoal)),
+        if infer.goal_needs_truncation(context.interner(), &inverted_subgoal) {
+            None
+        } else {
+            Some(infer.fully_canonicalize_goal(context.interner(), &inverted_subgoal))
         }
     }
 }
@@ -1331,10 +1333,7 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
         // Ultimately, the current decision to flounder the entire table mostly boils
         // down to "it works as we expect for the current tests". And, we likely don't
         // even *need* the added complexity just for potentially more answers.
-        if infer
-            .truncate_answer(self.context.interner(), &subst)
-            .is_some()
-        {
+        if infer.answer_needs_truncation(self.context.interner(), &subst) {
             self.forest.tables[table].mark_floundered();
             return None;
         }

chalk-solve/src/infer.rs

@@ -79,11 +79,6 @@ impl<I: Interner> InferenceTable<I> {
         u
     }
 
-    /// Current maximum universe -- one that can see all existing names.
-    pub(crate) fn max_universe(&self) -> UniverseIndex {
-        self.max_universe
-    }
-
     /// Creates a new inference variable and returns its index. The
     /// kind of the variable should be known by the caller, but is not
     /// tracked directly by the inference table.

chalk-solve/src/solve/slg.rs

@@ -3,7 +3,7 @@ use crate::coinductive_goal::IsCoinductive;
 use crate::infer::ucanonicalize::{UCanonicalized, UniverseMap};
 use crate::infer::unify::UnificationResult;
 use crate::infer::InferenceTable;
-use crate::solve::truncate::{self, Truncated};
+use crate::solve::truncate;
 use crate::solve::Solution;
 use crate::RustIrDatabase;
 use chalk_derive::HasInterner;
@@ -347,38 +347,14 @@ impl<I: Interner> TruncatingInferenceTable<I> {
 }
 
 impl<I: Interner> context::TruncateOps<SlgContext<I>> for TruncatingInferenceTable<I> {
-    fn truncate_goal(
-        &mut self,
-        interner: &I,
-        subgoal: &InEnvironment<Goal<I>>,
-    ) -> Option<InEnvironment<Goal<I>>> {
-        // We only want to truncate the goal itself. We keep the environment intact.
+    fn goal_needs_truncation(&mut self, interner: &I, subgoal: &InEnvironment<Goal<I>>) -> bool {
+        // We only want to check the goal itself. We keep the environment intact.
         // See rust-lang/chalk#280
-        let InEnvironment { environment, goal } = subgoal;
-        let Truncated { overflow, value } =
-            truncate::truncate(interner, &mut self.infer, self.max_size, goal);
-        if overflow {
-            Some(InEnvironment {
-                environment: environment.clone(),
-                goal: value,
-            })
-        } else {
-            None
-        }
+        truncate::needs_truncation(interner, &mut self.infer, self.max_size, &subgoal.goal)
     }
 
-    fn truncate_answer(
-        &mut self,
-        interner: &I,
-        subst: &Substitution<I>,
-    ) -> Option<Substitution<I>> {
-        let Truncated { overflow, value } =
-            truncate::truncate(interner, &mut self.infer, self.max_size, subst);
-        if overflow {
-            Some(value)
-        } else {
-            None
-        }
+    fn answer_needs_truncation(&mut self, interner: &I, subst: &Substitution<I>) -> bool {
+        truncate::needs_truncation(interner, &mut self.infer, self.max_size, subst)
     }
 }