Implement APRProofViewer as an APRProof specific TUI (#507)

Following runtimeverification/pyk#489, it turns
out that KEVM's TUI is broken because it relies on the old way of doing
Node printing.

This makes a new `APRProofViewer` class, which largely inherits from
`KCFGViewer`, but adjusts it to handle the more spceific node viewers.

I have tested this with both KEVM+Foundry and raw KEVM specs, and it
seems to work.

---------

Co-authored-by: devops <devops@runtimeverification.com>

Author: ehildenb

pyk/package/version

@@ -1 +1 @@
-0.1.342
+0.1.343

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.342"
+version = "0.1.343"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

pyk/src/pyk/kcfg/tui.py

@@ -11,9 +11,10 @@
 from ..cterm import CTerm
 from ..kast.inner import KApply, KRewrite
 from ..kast.manip import flatten_label, minimize_term, push_down_rewrites
-from ..kcfg import KCFG, KCFGShow
 from ..prelude.kbool import TRUE
 from ..utils import shorten_hashes, single
+from .kcfg import KCFG
+from .show import KCFGShow
 
 if TYPE_CHECKING:
     from collections.abc import Callable, Iterable
@@ -23,6 +24,7 @@
 
     from ..kast import KInner
     from ..ktool.kprint import KPrint
+    from .show import NodePrinter
 
 
 KCFGElem = Union[KCFG.Node, KCFG.Successor]
@@ -57,15 +59,15 @@ class BehaviorView(Widget):
     _kcfg: KCFG
     _kprint: KPrint
     _minimize: bool
-    _node_printer: Callable[[CTerm], Iterable[str]] | None
+    _node_printer: NodePrinter | None
     _kcfg_nodes: Iterable[GraphChunk]
 
     def __init__(
         self,
         kcfg: KCFG,
         kprint: KPrint,
         minimize: bool = True,
-        node_printer: Callable[[CTerm], Iterable[str]] | None = None,
+        node_printer: NodePrinter | None = None,
         id: str = '',
     ):
         super().__init__(id=id)
@@ -74,7 +76,7 @@ def __init__(
         self._minimize = minimize
         self._node_printer = node_printer
         self._kcfg_nodes = []
-        kcfg_show = KCFGShow(kprint)
+        kcfg_show = KCFGShow(kprint, node_printer=node_printer)
         for lseg_id, node_lines in kcfg_show.pretty_segments(self._kcfg, minimize=self._minimize):
             self._kcfg_nodes.append(GraphChunk(lseg_id, node_lines))
 
@@ -236,7 +238,7 @@ class KCFGViewer(App):
     _kcfg: KCFG
     _kprint: KPrint
 
-    _node_printer: Callable[[CTerm], Iterable[str]] | None
+    _node_printer: NodePrinter | None
     _custom_view: Callable[[KCFGElem], Iterable[str]] | None
 
     _minimize: bool
@@ -248,7 +250,7 @@ def __init__(
         self,
         kcfg: KCFG,
         kprint: KPrint,
-        node_printer: Callable[[CTerm], Iterable[str]] | None = None,
+        node_printer: NodePrinter | None = None,
         custom_view: Callable[[KCFGElem], Iterable[str]] | None = None,
         minimize: bool = True,
     ) -> None:

pyk/src/pyk/proof/style.css

@@ -0,0 +1,61 @@
+#navigation {
+    dock: left;
+    width: 35%;
+    height: 100%;
+    layout: vertical;
+}
+#behavior {
+    height: 1fr;
+    border: solid;
+    overflow-x: auto;
+    overflow-y: auto;
+}
+
+.cfg-node {
+    height: auto;
+    width: auto;
+}
+
+.hidden {
+    display: none;
+}
+
+#display {
+    layout: vertical;
+}
+#info-view {
+    height: 2fr;
+    border: solid;
+    overflow: auto scroll;
+}
+#term-view {
+    height: 15fr;
+    border: solid;
+    overflow: auto scroll;
+}
+#constraint-view {
+    height: 5fr;
+    border: solid;
+    overflow: auto scroll;
+}
+#custom-view {
+    height: 15fr;
+    border: solid;
+    overflow: auto scroll;
+}
+#info {
+    width: auto;
+    height: auto;
+}
+#term {
+    width: auto;
+    height: auto;
+}
+#constraint {
+    width: auto;
+    height: auto;
+}
+#custom {
+    width: auto;
+    height: auto;
+}

pyk/src/pyk/proof/tui.py

@@ -0,0 +1,76 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+from textual.containers import Horizontal, Vertical
+from textual.widget import Widget
+from textual.widgets import Footer
+
+from ..kcfg.tui import GraphChunk, KCFGViewer, NodeView
+from .show import APRProofShow
+
+if TYPE_CHECKING:
+    from collections.abc import Callable, Iterable
+
+    from textual.app import ComposeResult
+
+    from ..kcfg.show import NodePrinter
+    from ..kcfg.tui import KCFGElem
+    from ..ktool.kprint import KPrint
+    from .reachability import APRProof
+
+
+class APRProofBehaviorView(Widget):
+    _proof: APRProof
+    _kprint: KPrint
+    _minimize: bool
+    _node_printer: NodePrinter | None
+    _proof_nodes: Iterable[GraphChunk]
+
+    def __init__(
+        self,
+        proof: APRProof,
+        kprint: KPrint,
+        minimize: bool = True,
+        node_printer: NodePrinter | None = None,
+        id: str = '',
+    ):
+        super().__init__(id=id)
+        self._proof = proof
+        self._kprint = kprint
+        self._minimize = minimize
+        self._node_printer = node_printer
+        self._proof_nodes = []
+        proof_show = APRProofShow(kprint, node_printer=node_printer)
+        for lseg_id, node_lines in proof_show.pretty_segments(self._proof, minimize=self._minimize):
+            self._proof_nodes.append(GraphChunk(lseg_id, node_lines))
+
+    def compose(self) -> ComposeResult:
+        return self._proof_nodes
+
+
+class APRProofViewer(KCFGViewer):
+    CSS_PATH = 'style.css'
+
+    _proof: APRProof
+
+    def __init__(
+        self,
+        proof: APRProof,
+        kprint: KPrint,
+        node_printer: NodePrinter | None = None,
+        custom_view: Callable[[KCFGElem], Iterable[str]] | None = None,
+        minimize: bool = True,
+    ) -> None:
+        super().__init__(proof.kcfg, kprint, node_printer=node_printer, custom_view=custom_view, minimize=minimize)
+        self._proof = proof
+
+    def compose(self) -> ComposeResult:
+        yield Horizontal(
+            Vertical(
+                APRProofBehaviorView(self._proof, self._kprint, node_printer=self._node_printer, id='behavior'),
+                id='navigation',
+            ),
+            Vertical(NodeView(self._kprint, custom_view=self._custom_view, id='node-view'), id='display'),
+        )
+        yield Footer()