Skip to content

Commit

Permalink
Merge branch 'main' into georgy/fix-collection-hashes
Browse files Browse the repository at this point in the history
  • Loading branch information
@geo2a
geo2a authored Apr 3, 2024
2 parents 300ec03 + bafee82 commit 3dcf217
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 3dcf217

Please sign in to comment.