feat: model checking results display

Author: dranov

ProofWidgets/Component/TraceDisplay.lean

@@ -8,37 +8,9 @@ section
 namespace ProofWidgets
 open Lean Server
 
-/-- The `State` is expected to have a `ToJson` instance that returns an object,
-where the keys are field names (as strings) and the values are the field
-values (as numbers, strings, arrays, or objects). -/
-structure Step (State TransitionLabel : Type) where
-  label : TransitionLabel
-  postState : State
-deriving Repr, Inhabited
-
-structure Trace (State TransitionLabel : Type) where
-  start : State
-  steps : List (Step State TransitionLabel)
-deriving Repr, Inhabited
-
-instance jsonOfTrace {State TransitionLabel : Type} [ToJson State] [ToJson TransitionLabel] : ToJson (Trace State TransitionLabel) where
-  toJson := fun tr =>
-    let states : Array Json :=
-      #[ Json.mkObj
-        [ ("index", toJson 0),
-          ("fields", toJson tr.start),
-          ("transition", "after_init") ]] ++
-      (tr.steps.toArray.mapIdx (fun i st =>
-        let idx := i + 1
-        Json.mkObj
-        [ ("index", toJson idx),
-          ("fields", toJson st.postState),
-          ("transition", toJson st.label)]))
-    Json.arr states
-
 structure TraceDisplayProps where
-  /-- The trace to display, as the JSON-encoded value of a `Trace` instance. -/
-  trace : Json
+  /-- The model checking result to display, as the JSON-encoded value of a `ModelCheckingResult` instance. -/
+  result : Json
   /-- Display orientation: "vertical" or "horizontal" -/
   layout : String := "vertical"
 deriving RpcEncodable
@@ -49,14 +21,14 @@ def TraceDisplayViewer : Component TraceDisplayProps where
 
 namespace DisplayTraceCommand
 
-/-- Display a value of type `Json` (obtained from a `Trace` instance) in the infoview. -/
+/-- Display a value of type `Json` (obtained from a `ModelCheckingResult` instance) in the infoview. -/
 syntax (name := displayTraceCmd) "#displayTrace " term : command
 
 open Lean Elab Command in
 @[command_elab displayTraceCmd]
 def elabDisplayTraceCmd : CommandElab := fun
-  | stx@`(#displayTrace $trace) => do
-    let t ← `(open ProofWidgets.Jsx in <TraceDisplayViewer trace={$trace} layout={"vertical"} />)
+  | stx@`(#displayTrace $result) => do
+    let t ← `(open ProofWidgets.Jsx in <TraceDisplayViewer result={$result} layout={"vertical"} />)
     let html ← ← liftTermElabM <| ProofWidgets.HtmlCommand.evalCommandMHtml <| ← ``(HtmlEval.eval $t)
     liftCoreM <| Widget.savePanelWidgetInfo
       (hash HtmlDisplayPanel.javascript)