Recover from TooManyIterations when simplifying during rewriting (#3989)

Booster's rewriting algorithm, upon getting stuck (or aborting due to
`RuleApplicationUnclear`), will try so simplify the configuration once
and retry applying rules. When we cannot not finish simplifying the term
due to a `TooManyIterations`, we throw the partial result away and fail.

This PR handles the `TooManyIterations` exception and attempts applying
rewrite rules to the partially simplified term.

Author: geo2a

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -331,15 +331,14 @@ iterateEquations direction preference startTerm = do
             config <- getConfig
             currentCount <- countSteps
             when (coerce currentCount > config.maxIterations) $ do
-                withContext CtxAbort $ do
-                    logWarn $
-                        renderOneLineText $
-                            "Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
-                    withContext CtxDetail $
-                        getPrettyModifiers >>= \case
-                            ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
-                                logMessage . renderOneLineText $
-                                    "Final term:" <+> pretty' @mods currentTerm
+                logWarn $
+                    renderOneLineText $
+                        "Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
+                withContext CtxDetail $
+                    getPrettyModifiers >>= \case
+                        ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
+                            logMessage . renderOneLineText $
+                                "Final term:" <+> pretty' @mods currentTerm
                 throw $
                     TooManyIterations currentCount startTerm currentTerm
             pushTerm currentTerm
@@ -431,13 +430,24 @@ evaluatePattern' ::
     Pattern ->
     EquationT io Pattern
 evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
-    newTerm <- withTermContext term $ evaluateTerm' BottomUp term
+    newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults
     -- after evaluating the term, evaluate all (existing and
     -- newly-acquired) constraints, once
     traverse_ simplifyAssumedPredicate . predicates =<< getState
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
     pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
+  where
+    -- when TooManyIterations exception occurred while evaluating the top-level term,
+    -- i.e. not in a recursive evaluation of a side-condition,
+    -- it is safe to keep the partial result and ignore the exception.
+    -- Otherwise we would be throwing away useful work.
+    -- The exceptions thrown in recursion is caught in applyEquation.checkConstraint
+    keepTopLevelResults :: LoggerMIO io => EquationFailure -> EquationT io Term
+    keepTopLevelResults = \case
+        TooManyIterations _ _ partialResult ->
+            pure partialResult
+        err -> throw err
 
 -- evaluate the given predicate assuming all others
 simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io ()