Skip to content

Commit

Permalink
Return rule-id's in execute response (#561)
Browse files Browse the repository at this point in the history 
fixes #536 by returning the app;lied rule id and
`rule-substitution/predicate` for branching responses
  • Loading branch information
@goodlyrottenapple
goodlyrottenapple authored Apr 3, 2024
1 parent 2672c00 commit bafee82
Show file tree
Hide file tree
Showing 5 changed files with 502 additions and 15 deletions.
29 changes: 15 additions & 14 deletions library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ import Numeric.Natural
import Prettyprinter (pretty)
import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs)

import Booster.Definition.Attributes.Base (getUniqueId, uniqueId)
import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
import Booster.Definition.Base (KoreDefinition (..))
import Booster.Definition.Base qualified as Definition (RewriteRule (..))
import Booster.LLVM as LLVM (API)
Expand Down Expand Up @@ -543,9 +543,9 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
{ reason = RpcTypes.Branching
, depth
, logs
, state = toExecState p originalSubstitution unsupported
, state = toExecState p originalSubstitution unsupported Nothing
, nextStates =
Just $ map (\(_, _, p') -> toExecState p' originalSubstitution unsupported) $ toList nexts
Just $ map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported muid) $ toList nexts
, rule = Nothing
, unknownPredicate = Nothing
}
Expand All @@ -556,7 +556,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
{ reason = RpcTypes.Stuck
, depth
, logs
, state = toExecState p originalSubstitution unsupported
, state = toExecState p originalSubstitution unsupported Nothing
, nextStates = Nothing
, rule = Nothing
, unknownPredicate = Nothing
Expand All @@ -568,7 +568,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
{ reason = RpcTypes.Vacuous
, depth
, logs
, state = toExecState p originalSubstitution unsupported
, state = toExecState p originalSubstitution unsupported Nothing
, nextStates = Nothing
, rule = Nothing
, unknownPredicate = Nothing
Expand All @@ -580,8 +580,8 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
{ reason = RpcTypes.CutPointRule
, depth
, logs
, state = toExecState p originalSubstitution unsupported
, nextStates = Just [toExecState next originalSubstitution unsupported]
, state = toExecState p originalSubstitution unsupported Nothing
, nextStates = Just [toExecState next originalSubstitution unsupported Nothing]
, rule = Just lbl
, unknownPredicate = Nothing
}
Expand All @@ -592,7 +592,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
{ reason = RpcTypes.TerminalRule
, depth
, logs
, state = toExecState p originalSubstitution unsupported
, state = toExecState p originalSubstitution unsupported Nothing
, nextStates = Nothing
, rule = Just lbl
, unknownPredicate = Nothing
Expand All @@ -604,7 +604,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
{ reason = RpcTypes.DepthBound
, depth
, logs
, state = toExecState p originalSubstitution unsupported
, state = toExecState p originalSubstitution unsupported Nothing
, nextStates = Nothing
, rule = Nothing
, unknownPredicate = Nothing
Expand All @@ -622,7 +622,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
(logSuccessfulSimplifications, logFailedSimplifications)
(RewriteStepFailed failure)
in logs <|> abortRewriteLog
, state = toExecState p originalSubstitution unsupported
, state = toExecState p originalSubstitution unsupported Nothing
, nextStates = Nothing
, rule = Nothing
, unknownPredicate = Nothing
Expand Down Expand Up @@ -650,15 +650,16 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
(Nothing, xs@(_ : _)) -> Just xs
(Just t, xs) -> Just (t : xs)

toExecState :: Pattern -> Map Variable Term -> [Syntax.KorePattern] -> RpcTypes.ExecuteState
toExecState pat sub unsupported =
toExecState ::
Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
toExecState pat sub unsupported muid =
RpcTypes.ExecuteState
{ term = addHeader t
, predicate = addHeader <$> addUnsupported p
, substitution = addHeader <$> s
, ruleSubstitution = Nothing
, rulePredicate = Nothing
, ruleId = Nothing
, ruleId = getUniqueId <$> muid
}
where
(t, p, s) = externalisePattern pat sub
Expand Down Expand Up @@ -826,7 +827,7 @@ mkLogRewriteTrace
let final = singleton $ case failure of
ApplyEquations.IndexIsNone trm ->
Simplification
{ originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty mempty
{ originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty mempty Nothing
, originalTermIndex = Nothing
, origin = Booster
, result = Failure{reason = "No index found for term", _ruleId = Nothing}
Expand Down
74 changes: 74 additions & 0 deletions test/rpc-integration/resources/module-addition/state-c.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
{
"format": "KORE",
"version": 1,
"term": {
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'k'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "inj",
"sorts": [
{
"tag": "SortApp",
"name": "SortState",
"args": []
},
{
"tag": "SortApp",
"name": "SortKItem",
"args": []
}
],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"value": "c"
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
}
Loading

0 comments on commit bafee82

Please sign in to comment.