Hotfix indeterminate match for supersort function under injection (#4135)

Improves #4117  and removes temporary workaround #4133

The injection matcher was biased towards variable matching before, and
returned a `Fail` prematurely if this failed.
The new preference is to check for unevaluated functions that return a
supersort first (to return indeterminate), before trying to match a rule
variable with supersort. If the source sorts are unrelated, the match
can immediately fail.

Author: jberthold

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -844,27 +844,6 @@ applyEquations theory handler term = do
                     )
                     err
 
-{- | A sort predicate equation is characterised by the following:
-  * Its lhs is a function application (of a symbol starting with 'Lblis', not checked)
-  * function argument is a singleton K sequence
-  * containing an injection of a Variable into the 'KItem' sort
-  * rhs is a boolean
-  * requires and ensures are both empty (i.e., plain "true" DVs)
-  * the rule has no location information
--}
-isSortPredicate :: RewriteRule tag -> Bool
-isSortPredicate rule
-    | SymbolApplication _funSym [] [arg] <- rule.lhs
-    , KSeq sort (Var v) <- arg -- implicitly: Injection sort KItem (Var v)
-    , v.variableSort == sort
-    , (rule.rhs == TrueBool || rule.rhs == FalseBool)
-    , [Predicate TrueBool] <- rule.requires -- , null rule.requires
-    , [Predicate TrueBool] <- rule.ensures -- , null rule.ensures
-    , UNKNOWN <- sourceRef rule.attributes =
-        True
-    | otherwise =
-        False
-
 applyEquation ::
     forall io tag.
     LoggerMIO io =>
@@ -873,20 +852,6 @@ applyEquation ::
     EquationT
         io
         (Either ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) Term)
-applyEquation (FunctionApplication _sym [] [term]) rule
-    | isSortPredicate rule
-    , KSeq _ (FunctionApplication _ _ _) <- term =
-        -- sort predicates only match on a sort injection, unevaluated
-        -- function applications may create false negatives
-        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

booster/library/Booster/Pattern/Match.hs

@@ -330,7 +330,7 @@ matchInj ::
     Term ->
     StateT MatchState (Except MatchResult) ()
 matchInj
-    matchType
+    _matchType
     source1
     target1
     trm1
@@ -341,28 +341,44 @@ matchInj
             failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2))
         | source1 == source2 = do
             enqueueRegularProblem trm1 trm2
-        | Var v <- trm1 = do
-            -- variable in pattern, check source sorts and bind
+matchInj
+    matchType
+    source1
+    target1
+    trm1
+    source2
+    target2
+    trm2 =
+        do
             subsorts <- gets mSubsorts
-            isSubsort <-
+            s1IsSubsort <-
+                lift . withExcept (MatchFailed . SubsortingError) $
+                    checkSubsort subsorts source1 source2
+            s2IsSubsort <-
                 lift . withExcept (MatchFailed . SubsortingError) $
                     checkSubsort subsorts source2 source1
-            if isSubsort
-                then bindVariable matchType v (Injection source2 source1 trm2)
-                else failWith (DifferentSorts trm1 trm2)
-        | FunctionApplication{} <- trm2 = do
+            -- cases below require a subsort relation (and source1 ==
+            -- source2 is already handled)
+            unless (s1IsSubsort || s2IsSubsort) $
+                failWith (DifferentSorts trm1 trm2)
             -- Functions may have a more general sort than the actual result.
             -- This means we cannot simply fail the rewrite: the match is
             -- indeterminate if the function result is.
-            subsorts <- gets mSubsorts
-            isSubsort <- -- rule requires a more specific sort?
-                lift . withExcept (MatchFailed . SubsortingError) $
-                    checkSubsort subsorts source1 source2
-            if isSubsort
-                then addIndeterminate trm1 trm2
-                else failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2))
-        | otherwise =
-            failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2))
+            case (s1IsSubsort, trm2) of
+                (True, FunctionApplication{}) ->
+                    addIndeterminate trm1 trm2
+                _ -> do
+                    -- If the rule has a variable with a supersort of the
+                    -- subject, trm2 can be bound with a suitable injection
+                    case (s2IsSubsort, trm1) of
+                        (True, Var v) ->
+                            bindVariable matchType v (Injection source2 source1 trm2)
+                        _ ->
+                            -- truly different sorts, safe to just fail
+                            failWith $
+                                DifferentSorts
+                                    (Injection source1 target1 trm1)
+                                    (Injection source2 target2 trm2)
 {-# INLINE matchInj #-}
 
 ----- Symbol Applications