port truncator to use visitor

Author: basil-cow

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,9 @@ 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)),
+        match infer.goal_needs_truncation(context.interner(), subgoal) {
+            true => None,
+            false => Some(infer.fully_canonicalize_goal(context.interner(), subgoal)),
         }
     }
 
@@ -385,9 +385,9 @@ 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)),
+        match infer.goal_needs_truncation(context.interner(), &inverted_subgoal) {
+            true => None,
+            false => Some(infer.fully_canonicalize_goal(context.interner(), &inverted_subgoal)),
         }
     }
 }
@@ -1331,10 +1331,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

@@ -80,6 +80,7 @@ impl<I: Interner> InferenceTable<I> {
     }
 
     /// Current maximum universe -- one that can see all existing names.
+    #[allow(dead_code)]
     pub(crate) fn max_universe(&self) -> UniverseIndex {
         self.max_universe
     }

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;
@@ -348,38 +348,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)
     }
 }