Skip to content

Commit 5e03d41

Browse files
geo2ageo2a
committed
Add rule predicates
1 parent fafaf13 commit 5e03d41

File tree

3 files changed

+27
-17
lines changed

3 files changed

+27
-17
lines changed

‎booster/library/Booster/JsonRpc.hs

+20-13
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..))
4848
import Booster.LLVM as LLVM (API)
4949
import Booster.Log
5050
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
51-
import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
51+
import Booster.Pattern.Base (Pattern (..), Predicate (..), Sort (SortApp), Term, Variable)
5252
import Booster.Pattern.Base qualified as Pattern
5353
import Booster.Pattern.Bool (pattern TrueBool)
5454
import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
@@ -604,10 +604,11 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
604604
{ reason = RpcTypes.Branching
605605
, depth
606606
, logs
607-
, state = toExecState p originalSubstitution unsupported Nothing
607+
, state = toExecState p originalSubstitution unsupported Nothing Nothing
608608
, nextStates =
609609
Just $
610-
map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $
610+
map
611+
(\(_, muid, p', mrulePred) -> toExecState p' originalSubstitution unsupported (Just muid) mrulePred) $
611612
toList nexts
612613
, rule = Nothing
613614
, unknownPredicate = Nothing
@@ -619,7 +620,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
619620
{ reason = RpcTypes.Stuck
620621
, depth
621622
, logs
622-
, state = toExecState p originalSubstitution unsupported Nothing
623+
, state = toExecState p originalSubstitution unsupported Nothing Nothing
623624
, nextStates = Nothing
624625
, rule = Nothing
625626
, unknownPredicate = Nothing
@@ -631,7 +632,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
631632
{ reason = RpcTypes.Vacuous
632633
, depth
633634
, logs
634-
, state = toExecState p originalSubstitution unsupported Nothing
635+
, state = toExecState p originalSubstitution unsupported Nothing Nothing
635636
, nextStates = Nothing
636637
, rule = Nothing
637638
, unknownPredicate = Nothing
@@ -643,8 +644,8 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
643644
{ reason = RpcTypes.CutPointRule
644645
, depth
645646
, logs
646-
, state = toExecState p originalSubstitution unsupported Nothing
647-
, nextStates = Just [toExecState next originalSubstitution unsupported Nothing]
647+
, state = toExecState p originalSubstitution unsupported Nothing Nothing
648+
, nextStates = Just [toExecState next originalSubstitution unsupported Nothing Nothing]
648649
, rule = Just lbl
649650
, unknownPredicate = Nothing
650651
}
@@ -655,7 +656,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
655656
{ reason = RpcTypes.TerminalRule
656657
, depth
657658
, logs
658-
, state = toExecState p originalSubstitution unsupported Nothing
659+
, state = toExecState p originalSubstitution unsupported Nothing Nothing
659660
, nextStates = Nothing
660661
, rule = Just lbl
661662
, unknownPredicate = Nothing
@@ -667,7 +668,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
667668
{ reason = RpcTypes.DepthBound
668669
, depth
669670
, logs
670-
, state = toExecState p originalSubstitution unsupported Nothing
671+
, state = toExecState p originalSubstitution unsupported Nothing Nothing
671672
, nextStates = Nothing
672673
, rule = Nothing
673674
, unknownPredicate = Nothing
@@ -684,7 +685,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
684685
(logSuccessfulRewrites, logFailedRewrites)
685686
(RewriteStepFailed failure)
686687
in logs <|> abortRewriteLog
687-
, state = toExecState p originalSubstitution unsupported Nothing
688+
, state = toExecState p originalSubstitution unsupported Nothing Nothing
688689
, nextStates = Nothing
689690
, rule = Nothing
690691
, unknownPredicate = Nothing
@@ -710,17 +711,23 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
710711
(Just t, xs) -> Just (t : xs)
711712

712713
toExecState ::
713-
Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
714-
toExecState pat sub unsupported muid =
714+
Pattern ->
715+
Map Variable Term ->
716+
[Syntax.KorePattern] ->
717+
Maybe UniqueId ->
718+
Maybe Predicate ->
719+
RpcTypes.ExecuteState
720+
toExecState pat sub unsupported muid mrulePredicate =
715721
RpcTypes.ExecuteState
716722
{ term = addHeader t
717723
, predicate = addHeader <$> addUnsupported p
718724
, substitution = addHeader <$> s
719725
, ruleSubstitution = Nothing
720-
, rulePredicate = Nothing
726+
, rulePredicate = addHeader <$> mrulePredExt
721727
, ruleId = getUniqueId <$> muid
722728
}
723729
where
730+
mrulePredExt = externalisePredicate (externaliseSort Pattern.SortBool) <$> mrulePredicate
724731
(t, p, s) = externalisePattern pat sub
725732
termSort = externaliseSort $ sortOfPattern pat
726733
allUnsupported = Syntax.KJAnd termSort unsupported

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

+6-3
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,8 @@ rewriteStep pat = do
175175
-- return `OnlyTrivial` if all elements of a list are `(r, Nothing)`. If the list is empty or contains at least one `(r, Just p)`,
176176
-- return an `AppliedRules` list of `(r, p)` pairs.
177177
filterOutTrivial ::
178-
[(RewriteRule "Rewrite", Maybe Pattern)] -> RewriteStepResult [(RewriteRule "Rewrite", Pattern)]
178+
[(RewriteRule "Rewrite", Maybe Pattern)] ->
179+
RewriteStepResult [(RewriteRule "Rewrite", Pattern)]
179180
filterOutTrivial = \case
180181
[] -> AppliedRules []
181182
[(_, Nothing)] -> OnlyTrivial
@@ -536,7 +537,7 @@ ruleLabelOrLoc rule =
536537
-- | Different rewrite results (returned from RPC execute endpoint)
537538
data RewriteResult pat
538539
= -- | branch point
539-
RewriteBranch pat (NonEmpty (Text, UniqueId, pat))
540+
RewriteBranch pat (NonEmpty (Text, UniqueId, pat, Maybe Predicate))
540541
| -- | no rules could be applied, config is stuck
541542
RewriteStuck pat
542543
| -- | cut point rule, return current (lhs) and single next state
@@ -904,7 +905,9 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
904905
pure $
905906
RewriteBranch pat' $
906907
NE.fromList $
907-
map (\(r, n) -> (ruleLabelOrLocT r, uniqueId r, n)) nextPats'
908+
map
909+
(\(r, n) -> (ruleLabelOrLocT r, uniqueId r, n, Just (collapseAndBools . Set.toList $ r.requires)))
910+
nextPats'
908911

909912
data RewriteStepsState = RewriteStepsState
910913
{ counter :: !Natural

‎booster/tools/booster/Proxy.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -567,7 +567,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
567567
-- this ensures the information from next states in a branch reponse doesn't get lost
568568
pure $
569569
Right
570-
( (Booster.toExecState p sub unsup Nothing)
570+
( (Booster.toExecState p sub unsup Nothing Nothing)
571571
{ ruleId = s.ruleId
572572
, ruleSubstitution = s.ruleSubstitution
573573
, rulePredicate = s.rulePredicate

0 commit comments

Comments
 (0)