Only check top-level symbol when deciding to skip sort predicate rules (#4134)

The previous fix #4133 checked `isEvaluated` on the term in a sort
predicate before applying rules. This is correct but leads to too many
fall-backs which slow down symbolic execution when sort predicates are
used in rewrite side conditions. The only case that matters is when an
_unevaluated function_ is at the _head_ of the term in the sort
predicate. This is now matched directly.

Author: jberthold

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -873,18 +873,20 @@ applyEquation ::
     EquationT
         io
         (Either ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) Term)
-applyEquation (FunctionApplication _sym [] [Term term _]) rule
+applyEquation (FunctionApplication _sym [] [term]) rule
     | isSortPredicate rule
-    , not term.isEvaluated =
+    , KSeq _ (FunctionApplication _ _ _) <- term =
         -- sort predicates only match on a sort injection, unevaluated
         -- function applications may create false negatives
-        getPrettyModifiers >>= \case
-            ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do
-                pure $
-                    Left
-                        ( \ctxt -> ctxt $ logWarn "Refusing to apply sort predicate rule to an unevaluated term"
-                        , IndeterminateMatch
-                        )
+        pure $
+            Left
+                ( \ctxt ->
+                    ctxt $
+                        withTermContext term $
+                            withContext CtxWarn $
+                                logMessage ("Refusing to apply sort predicate rule to an unevaluated term" :: Text)
+                , IndeterminateMatch
+                )
 applyEquation term rule =
     runExceptT $
         getPrettyModifiers >>= \case