Skip to content

Commit

Permalink
add "trace_node_blocked" field to trace nodes
Browse files Browse the repository at this point in the history
this indicates if the current trace node is itself blocked
if it has no blocked sub-elements then it is the blocking prompt
otherwise it will contain at least one blocked sub-element
  • Loading branch information
danmatichuk committed Nov 5, 2024
1 parent 2552402 commit ead1f4e
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 7 deletions.
3 changes: 2 additions & 1 deletion tools/pate-repl/Repl.hs
Original file line number Diff line number Diff line change
Expand Up @@ -524,8 +524,9 @@ ls' = do
p <- prettyNextNodes 0 False
(Some ((TraceNode lbl v _) :: TraceNode sym arch nm)) <- gets replNode
tags <- gets replTags
blocked <- isBlocked
let thisPretty = prettyDetailAt @'(sym, arch) @nm tags lbl v
let p' = PO.tagOutput (Just thisPretty) (Just (symbolRepr (knownSymbol @nm))) p
let p' = PO.tagOutput (Just thisPretty) (Just (symbolRepr (knownSymbol @nm))) blocked p
PO.printOutput p'
PO.printBreak

Expand Down
14 changes: 8 additions & 6 deletions tools/pate/Output.hs
Original file line number Diff line number Diff line change
Expand Up @@ -67,10 +67,11 @@ data Output = Output
{ outputC :: Output_
, output_this :: Maybe (PP.Doc ())
, output_tag :: Maybe (Text.Text)
, output_blocked :: Bool
}

output :: Output_ -> Output
output o = Output o Nothing Nothing
output o = Output o Nothing Nothing False

jsonOutputHandle :: IO.IORef (Maybe IO.Handle)
jsonOutputHandle = IO.unsafePerformIO (IO.newIORef Nothing)
Expand Down Expand Up @@ -147,8 +148,8 @@ ppOutputElem nd =
_ -> p'
in PP.pretty (outIdx nd) <> ":" <+> (PP.indent (outIndent nd) p'')

tagOutput :: Maybe (PP.Doc ()) -> Maybe (Text.Text) -> Output -> Output
tagOutput msg tag o = Output (outputC o) msg tag
tagOutput :: Maybe (PP.Doc ()) -> Maybe (Text.Text) -> Bool -> Output -> Output
tagOutput msg tag isBlocked o = Output (outputC o) msg tag isBlocked

ppOutput_ :: Output_ -> [PP.Doc ()]
ppOutput_ (OutputElemList es) = map ppOutputElem es
Expand All @@ -159,8 +160,8 @@ ppOutput_ (OutputPrompt str) = [PP.pretty str]
ppOutput_ OutputHeartbeat = ["."]

ppOutput :: Output -> PP.Doc ()
ppOutput (Output out_ Nothing _) = PP.vsep $ ppOutput_ out_
ppOutput (Output out_ (Just this_) _) = PP.vsep $ this_:(ppOutput_ out_)
ppOutput (Output out_ Nothing _ _) = PP.vsep $ ppOutput_ out_
ppOutput (Output out_ (Just this_) _ _) = PP.vsep $ this_:(ppOutput_ out_)

{-
mkJSON' :: [OutputElem] -> ([JSON.Value], [OutputElem])
Expand Down Expand Up @@ -202,13 +203,14 @@ outputElemJSON e =
]

jsonOutput :: Output -> JSON.Value
jsonOutput (Output out_ this_ tag_) =
jsonOutput (Output out_ this_ tag_ isBlocked) =
case out_ of
OutputElemList es | Just this__ <- this_ ->
JSON.object
[ "this" JSON..= show this__
, "trace_node_kind" JSON..= tag_
, "trace_node_contents" JSON..= map outputElemJSON es
, "trace_node_blocked" JSON..= isBlocked
]
OutputElemList es -> JSON.toJSON $ map outputElemJSON es
OutputInfo msg -> JSON.object ["message" JSON..= show msg]
Expand Down

0 comments on commit ead1f4e

Please sign in to comment.