Skip to content

Commit 2746c4a

Browse files
jbertholdjberthold
committed
make subject variable matches indeterminate to retain acceptable performance
1 parent d378e7c commit 2746c4a

File tree

2 files changed

+17
-18
lines changed

2 files changed

+17
-18
lines changed

‎booster/library/Booster/Pattern/Match.hs

Lines changed: 16 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -79,8 +79,6 @@ data FailReason
7979
SubsortingError SortError
8080
| -- | The two terms have differing argument lengths
8181
ArgLengthsDiffer Term Term
82-
| -- | Not a matching substitution
83-
SubjectVariableMatch Term Variable
8482
deriving stock (Eq, Show)
8583

8684
instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) where
@@ -115,8 +113,6 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) whe
115113
pretty $ show err
116114
ArgLengthsDiffer t1 t2 ->
117115
hsep ["Argument length differ", pretty' @mods t1, pretty' @mods t2]
118-
SubjectVariableMatch t v ->
119-
hsep ["Cannot match variable in subject:", pretty' @mods v, pretty' @mods t]
120116

121117
{- | Attempts to find a simple unifying substitution for the given
122118
terms.
@@ -217,9 +213,10 @@ match1 _ t1@DomainValue{} t2@ConsApplication{}
217213
match1 _ t1@DomainValue{} t2@FunctionApplication{} = addIndeterminate t1 t2
218214
-- match with var on the RHS must be indeterminate when evaluating functions. see: https://github.com/runtimeverification/hs-backend-booster/issues/231
219215
match1 Eval t1@DomainValue{} t2@Var{} = addIndeterminate t1 t2
220-
-- match with var on RHS is specially marked at the moment but must abort the rewriting (or lead to branching), see https://github.com/runtimeverification/haskell-backend/issues/4100
221-
match1 Rewrite t1@DomainValue{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
222-
match1 Implies t1@DomainValue{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
216+
-- match with var on RHS may lead to branching during rewriting, see https://github.com/runtimeverification/haskell-backend/issues/4100
217+
-- Related cases are currently marked with a special function so they can be identified and changed together later (extending branching functionality)
218+
match1 Rewrite t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2
219+
match1 Implies t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2
223220
match1 Eval t1@Injection{} t2@AndTerm{} = addIndeterminate t1 t2
224221
match1 _ t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
225222
match1 _ t1@Injection{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2
@@ -229,7 +226,7 @@ match1 _ t1@Injection{} t2@KList{}
229226
match1 _ t1@Injection{} t2@KSet{} = failWith $ DifferentSymbols t1 t2
230227
match1 _ t1@Injection{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
231228
match1 _ t1@Injection{} t2@FunctionApplication{} = addIndeterminate t1 t2
232-
match1 Rewrite t1@Injection{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
229+
match1 Rewrite t1@Injection{} (Var v2) = subjectVariableMatch t1 v2
233230
match1 _ t1@Injection{} t2@Var{} = addIndeterminate t1 t2
234231
match1 Eval t1@KMap{} t2@AndTerm{} = addIndeterminate t1 t2
235232
match1 _ t1@KMap{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -241,7 +238,7 @@ match1 _ t1@KMap{} t2@KList{}
241238
match1 _ t1@KMap{} t2@KSet{} = failWith $ DifferentSymbols t1 t2
242239
match1 _ t1@KMap{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
243240
match1 _ t1@KMap{} t2@FunctionApplication{} = addIndeterminate t1 t2
244-
match1 Rewrite t1@KMap{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
241+
match1 Rewrite t1@KMap{} (Var v2) = subjectVariableMatch t1 v2
245242
match1 _ t1@KMap{} t2@Var{} = addIndeterminate t1 t2
246243
match1 Eval t1@KList{} t2@AndTerm{} = addIndeterminate t1 t2
247244
match1 _ t1@KList{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -254,7 +251,7 @@ match1 _ t1@(KList def1 heads1 rest1) t2@(KList def2 heads2
254251
match1 _ t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2
255252
match1 _ t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
256253
match1 _ t1@KList{} t2@FunctionApplication{} = addIndeterminate t1 t2
257-
match1 Rewrite t1@KList{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
254+
match1 Rewrite t1@KList{} (Var t2) = subjectVariableMatch t1 t2
258255
match1 _ t1@KList{} t2@Var{} = addIndeterminate t1 t2
259256
match1 Eval t1@KSet{} t2@AndTerm{} = addIndeterminate t1 t2
260257
match1 _ t1@KSet{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -266,7 +263,7 @@ match1 _ t1@KSet{} t2@KList{}
266263
match1 _ t1@(KSet def1 patElements patRest) t2@(KSet def2 subjElements subjRest) = if def1 == def2 then matchSets def1 patElements patRest subjElements subjRest else failWith $ DifferentSorts t1 t2
267264
match1 _ t1@KSet{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
268265
match1 _ t1@KSet{} t2@FunctionApplication{} = addIndeterminate t1 t2
269-
match1 Rewrite t1@KSet{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
266+
match1 Rewrite t1@KSet{} (Var t2) = subjectVariableMatch t1 t2
270267
match1 _ t1@KSet{} t2@Var{} = addIndeterminate t1 t2
271268
match1 Eval t1@ConsApplication{} t2@AndTerm{} = addIndeterminate t1 t2
272269
match1 _ t1@ConsApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -278,7 +275,7 @@ match1 _ t1@ConsApplication{} t2@KSet{}
278275
match1 matchTy (ConsApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications matchTy symbol1 sorts1 args1 symbol2 sorts2 args2
279276
match1 Eval (ConsApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2
280277
match1 _ t1@ConsApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2
281-
match1 Rewrite t1@ConsApplication{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
278+
match1 Rewrite t1@ConsApplication{} (Var t2) = subjectVariableMatch t1 t2
282279
match1 _ t1@ConsApplication{} t2@Var{} = addIndeterminate t1 t2
283280
match1 Eval t1@FunctionApplication{} t2@AndTerm{} = addIndeterminate t1 t2
284281
match1 _ t1@FunctionApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -296,7 +293,7 @@ match1 Eval (FunctionApplication symbol1 sorts1 args1) (ConsApplication symbo
296293
match1 _ t1@FunctionApplication{} t2@ConsApplication{} = addIndeterminate t1 t2
297294
match1 Eval (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2
298295
match1 _ t1@FunctionApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2
299-
match1 Rewrite t1@FunctionApplication{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
296+
match1 Rewrite t1@FunctionApplication{} (Var t2) = subjectVariableMatch t1 t2
300297
match1 _ t1@FunctionApplication{} t2@Var{} = addIndeterminate t1 t2
301298
match1 Eval t1@Var{} t2@AndTerm{} = addIndeterminate t1 t2
302299
match1 _ t1@Var{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -450,6 +447,12 @@ matchVar
450447
else Injection termSort variableSort term2
451448
else failWith $ DifferentSorts (Var var) term2
452449

450+
-- Subject variable matches are currently marked as indeterminate.
451+
-- The code may be extended to collect these as separate conditional
452+
-- results (for branching).
453+
subjectVariableMatch :: Term -> Variable -> StateT MatchState (Except MatchResult) ()
454+
subjectVariableMatch t v = addIndeterminate t (Var v)
455+
453456
{- | pair up the argument lists and return the pairs in the first argument. If the lists
454457
are of equal length, return Nothing in second, else return the remaining
455458
terms in the longer list, tagged with their origin).

‎booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ import Booster.Pattern.Base
6464
import Booster.Pattern.Bool
6565
import Booster.Pattern.Index qualified as Idx
6666
import Booster.Pattern.Match (
67-
FailReason (ArgLengthsDiffer, SubjectVariableMatch, SubsortingError),
67+
FailReason (ArgLengthsDiffer, SubsortingError),
6868
MatchResult (MatchFailed, MatchIndeterminate, MatchSuccess),
6969
MatchType (Rewrite),
7070
SortError,
@@ -392,10 +392,6 @@ applyRule pat@Pattern{ceilConditions} rule =
392392
withContext CtxError $
393393
logPretty' @mods err
394394
failRewrite $ InternalMatchError $ renderText $ pretty' @mods err
395-
MatchFailed err@(SubjectVariableMatch t v) -> do
396-
withContext CtxError $
397-
logPretty' @mods err
398-
failRewrite $ RuleApplicationUnclear rule pat.term $ NE.singleton (t, Var v)
399395
MatchFailed reason -> do
400396
withContext CtxFailure $ logPretty' @mods reason
401397
returnNotApplied

0 commit comments

Comments
 (0)