Factor out CTermShow class for simpler node printing (#4808)

~Blocked on: #4819

This is a refactoring to how our display of nodes/KCFGs works, ideally
to make it easier to thread options through to them. We're specifically
trying to capture all the common options for how `CTerm` should be
displayed in one place, and remove those options from other places. This
came about as I was trying to implement some asks from the KMIR team on
changing the display in the TUI viewer, and realized that currently all
the options are threaded through in different ways and controlled at
different points.

This is a breaking change in pyk API, and so corresponding changes into
downstream repos will need to be added to the update-deps PRs.

Another big change that happens here: the `kcfg` directory no longer
needs a `KPrint` because we use a `kast.pretty.PrettyPrinter` directly
instead. Before, it was using `KPrint.pretty_print`, which was just
constructing a `PrettyPrinter` then using it. So we skip the
intermediate class. That means that several classes which took in a
`KPrint` now just take in a `KDefinition`.

Changes in particular:

- A new class `CTermShow` is introduced, which enables printing out
`CTerm` using a `PrettyPrinter`, via `CTermShow.show_config`,
`CTermShow.show_constraints` and `CTermShow.show`. It takes several
options controlling how printing can occur, including:
- `extra_unparsing_modules`, `patch_symbol_table`, `unalias`, and
`sort_ac_collections`: all the same as `PrettyPrinter`.
- `minimize`: collapse unused cell-variables into `...`, and the
recursively collapse the `...` as much as possible in the configuration.
- `break_cell_collections`: enable line-breaking collections (`List`,
`Set`, `Map`) which are stored directly in cells, as usually you want
one item printer per line in this case.
- `omit_labels`: a set of labels to always replace occurrences of with
`...`, so they do not get printed.
- `NodePrinter` (and `APRProofNodePrinter`) now take a `CTermShow`
instead of a `KPrint`, which also means they don't take the options
controlling printing directly (like `minimize`). These options must be
set when building teh `CTermShow` that is passed in for the
`NodePrinter` to use.
- Similarly, `KCFGShow` (and `APRProofShow`) now take a `KDefinition`
instead of a `KPrint` and build a `PrettyPrinter` directly. This means
that the `NodePrinter` (and thus `CTermShow`) is responsible for setting
options related to node printing like `sort_collections` ahead of time.
- The `KCFGViewer` (and `APRProofViewer`) are now taking directly a
`KDefinition` instead of a `KPrint`, and similar to the `*Show`
counterparts offloading decisions about how to print items to how the
`CTermShow` is setup in the client application.
- Tests are updated with the new pattern (of constructing a `CTermShow`
ahead of time and passing it in), which provides an example of what's
needed downstream. In particular, before we were mocking an entire
`KPrint` in the unit tests, but now we only need to mock a `CTermShow`,
which is much more compact. We rename the file from `mock_kprint.py` to
`mock.py`, so it can be for all mocks.

Author: ehildenb

pyk/src/pyk/__main__.py

@@ -16,6 +16,7 @@
 from .cli.utils import LOG_FORMAT, loglevel
 from .coverage import get_rule_by_id, strip_coverage_logger
 from .cterm import CTerm
+from .cterm.show import CTermShow
 from .cterm.symbolic import cterm_symbolic
 from .kast import KAst
 from .kast.att import KAtt
@@ -275,8 +276,10 @@ def explore_context() -> Iterator[KCFGExplore]:
             if type(failure_info) is APRFailureInfo:
                 print('\n'.join(failure_info.print()))
         if options.show_kcfg and type(proof) is APRProof:
-            node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False)
-            show = APRProofShow(kprove, node_printer=node_printer)
+            node_printer = APRProofNodePrinter(
+                proof, CTermShow(PrettyPrinter(kprove.definition).print, minimize=False), full_printer=True
+            )
+            show = APRProofShow(kprove.definition, node_printer=node_printer)
             print('\n'.join(show.show(proof, minimize=False)))
     sys.exit(len([p.id for p in proofs if not p.passed]))
 

pyk/src/pyk/cterm/show.py

@@ -0,0 +1,99 @@
+from __future__ import annotations
+
+import logging
+from dataclasses import dataclass
+from typing import TYPE_CHECKING
+
+from ..kast.inner import KApply, KSort, KToken, flatten_label, top_down
+from ..kast.manip import free_vars, minimize_term
+from ..kast.prelude.k import DOTS
+from .cterm import CTerm
+
+if TYPE_CHECKING:
+    from collections.abc import Callable, Iterable
+    from typing import Final
+
+    from ..kast.inner import KInner
+
+_LOGGER: Final = logging.getLogger(__name__)
+
+
+@dataclass
+class CTermShow:
+    _printer: Callable[[KInner], str]
+    _minimize: bool
+    _break_cell_collections: bool
+    _omit_labels: tuple[str, ...]
+
+    def __init__(
+        self,
+        printer: Callable[[KInner], str],
+        minimize: bool = True,
+        break_cell_collections: bool = True,
+        omit_labels: Iterable[str] = (),
+    ):
+        self._printer = printer
+        self._minimize = minimize
+        self._break_cell_collections = break_cell_collections
+        self._omit_labels = tuple(omit_labels)
+
+    def print_lines(self, kast: KInner) -> list[str]:
+        return self._printer(kast).split('\n')
+
+    def let(
+        self,
+        minimize: bool | None = None,
+        break_cell_collections: bool | None = None,
+        omit_labels: Iterable[str] | None = None,
+    ) -> CTermShow:
+        return CTermShow(
+            self._printer,
+            minimize=(self._minimize if minimize is None else minimize),
+            break_cell_collections=(
+                self._break_cell_collections if break_cell_collections is None else break_cell_collections
+            ),
+            omit_labels=(self._omit_labels if omit_labels is None else omit_labels),
+        )
+
+    def show(self, cterm: CTerm) -> list[str]:
+        ret_strs: list[str] = []
+        ret_strs.extend(self.show_config(cterm))
+        ret_strs.extend(self.show_constraints(cterm))
+        return ret_strs
+
+    def show_config(self, cterm: CTerm) -> list[str]:
+        if self._break_cell_collections:
+            cterm = CTerm(top_down(self._break_cells_visitor, cterm.config), cterm.constraints)
+        if self._omit_labels:
+            cterm = CTerm(top_down(self._omit_labels_visitor, cterm.config), cterm.constraints)
+        if self._minimize:
+            cterm = CTerm(minimize_term(cterm.config, keep_vars=free_vars(cterm.constraint)), cterm.constraints)
+        return self.print_lines(cterm.config)
+
+    def show_constraints(self, cterm: CTerm) -> list[str]:
+        ret_strs: list[str] = []
+        for constraint in cterm.constraints:
+            constraint_strs = self.print_lines(constraint)
+            if len(constraint_strs) > 0:
+                constraint_strs = [f'#And {cstr}' for cstr in constraint_strs]
+                ret_strs.append(constraint_strs[0])
+                ret_strs.extend([f'  {constraint_str}' for constraint_str in constraint_strs[1:]])
+        return ret_strs
+
+    def _break_cells_visitor(self, kast: KInner) -> KInner:
+        if (
+            type(kast) is KApply
+            and kast.is_cell
+            and len(kast.args) == 1
+            and type(kast.args[0]) is KApply
+            and kast.args[0].label.name in {'_Set_', '_List_', '_Map_'}
+        ):
+            items = flatten_label(kast.args[0].label.name, kast.args[0])
+            printed = KToken('\n'.join(map(self._printer, items)), KSort(kast.label.name[1:-1]))
+            return KApply(kast.label, [printed])
+        return kast
+
+    def _omit_labels_visitor(self, kast: KInner) -> KInner:
+        if type(kast) == KApply and kast.label.name in self._omit_labels:
+            return DOTS
+        return kast

pyk/src/pyk/kcfg/show.py

@@ -5,6 +5,7 @@
 
 from graphviz import Digraph
 
+from ..cterm.show import CTermShow
 from ..kast.inner import KApply, KRewrite, top_down
 from ..kast.manip import (
     flatten_label,
@@ -19,6 +20,7 @@
 from ..kast.outer import KRule
 from ..kast.prelude.k import DOTS
 from ..kast.prelude.ml import mlAnd
+from ..kast.pretty import PrettyPrinter
 from ..utils import add_indent, ensure_dir_path
 from .kcfg import KCFG
 
@@ -30,31 +32,26 @@
     from ..cterm import CSubst
     from ..kast import KInner
     from ..kast.outer import KDefinition, KFlatModule, KImport, KSentence
-    from ..ktool.kprint import KPrint
     from .kcfg import NodeIdLike
 
 _LOGGER: Final = logging.getLogger(__name__)
 
 
 class NodePrinter:
-    kprint: KPrint
+    cterm_show: CTermShow
     full_printer: bool
     minimize: bool
 
-    def __init__(self, kprint: KPrint, full_printer: bool = False, minimize: bool = False):
-        self.kprint = kprint
+    def __init__(self, cterm_show: CTermShow, full_printer: bool = False):
+        self.cterm_show = cterm_show
         self.full_printer = full_printer
-        self.minimize = minimize
 
     def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
         attrs = self.node_attrs(kcfg, node)
         attr_str = ' (' + ', '.join(attrs) + ')' if attrs else ''
         node_strs = [f'{node.id}{attr_str}']
         if self.full_printer:
-            kast = node.cterm.kast
-            if self.minimize:
-                kast = minimize_term(kast)
-            node_strs.extend('  ' + line for line in self.kprint.pretty_print(kast).split('\n'))
+            node_strs.extend('  ' + line for line in self.cterm_show.show(node.cterm))
         return node_strs
 
     def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
@@ -74,12 +71,12 @@ def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
 
 
 class KCFGShow:
-    kprint: KPrint
+    pretty_printer: PrettyPrinter
     node_printer: NodePrinter
 
-    def __init__(self, kprint: KPrint, node_printer: NodePrinter | None = None):
-        self.kprint = kprint
-        self.node_printer = node_printer if node_printer is not None else NodePrinter(kprint)
+    def __init__(self, defn: KDefinition, node_printer: NodePrinter | None = None):
+        self.pretty_printer = PrettyPrinter(defn)
+        self.node_printer = node_printer if node_printer else NodePrinter(CTermShow(self.pretty_printer.print))
 
     def node_short_info(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
         return self.node_printer.print_node(kcfg, node)
@@ -140,7 +137,7 @@ def _print_csubst(
             csubst: CSubst, subst_first: bool = False, indent: int = 4, minimize: bool = False
         ) -> list[str]:
             _constraint_strs = [
-                self.kprint.pretty_print(ml_pred_to_bool(constraint, unsafe=True)) for constraint in csubst.constraints
+                self.pretty_printer.print(ml_pred_to_bool(constraint, unsafe=True)) for constraint in csubst.constraints
             ]
             constraint_strs = _multi_line_print('constraint', _constraint_strs, 'true')
             if len(csubst.subst.minimize()) > 0 and minimize:
@@ -149,7 +146,7 @@ def _print_csubst(
                 _subst_strs = [
                     line
                     for k, v in csubst.subst.minimize().items()
-                    for line in f'{k} <- {self.kprint.pretty_print(v)}'.split('\n')
+                    for line in f'{k} <- {self.pretty_printer.print(v)}'.split('\n')
                 ]
                 subst_strs = _multi_line_print('subst', _subst_strs, '.Subst')
             if subst_first:
@@ -325,7 +322,6 @@ def show(
         node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (),
         to_module: bool = False,
         minimize: bool = True,
-        sort_collections: bool = False,
         omit_cells: Iterable[str] = (),
         module_name: str | None = None,
     ) -> list[str]:
@@ -344,7 +340,7 @@ def show(
             res_lines.append('')
             res_lines.append(f'Node {node_id}:')
             res_lines.append('')
-            res_lines.append(self.kprint.pretty_print(kast, sort_collections=sort_collections))
+            res_lines.append(self.pretty_printer.print(kast))
             res_lines.append('')
 
         for node_id_1, node_id_2 in node_deltas:
@@ -358,7 +354,7 @@ def show(
             res_lines.append('')
             res_lines.append(f'State Delta {node_id_1} => {node_id_2}:')
             res_lines.append('')
-            res_lines.append(self.kprint.pretty_print(config_delta, sort_collections=sort_collections))
+            res_lines.append(self.pretty_printer.print(config_delta))
             res_lines.append('')
 
         if not (nodes_printed):
@@ -368,7 +364,7 @@ def show(
 
         if to_module:
             module = self.to_module(cfg, module_name, omit_cells=omit_cells)
-            res_lines.append(self.kprint.pretty_print(module, sort_collections=sort_collections))
+            res_lines.append(self.pretty_printer.print(module))
 
         return res_lines
 
@@ -396,7 +392,7 @@ def _short_label(label: str) -> str:
 
         for cover in kcfg.covers():
             label = ', '.join(
-                f'{k} |-> {self.kprint.pretty_print(v)}' for k, v in cover.csubst.subst.minimize().items()
+                f'{k} |-> {self.pretty_printer.print(v)}' for k, v in cover.csubst.subst.minimize().items()
             )
             label = _short_label(label)
             attrs = {'class': 'abstraction', 'style': 'dashed'}
@@ -405,7 +401,7 @@ def _short_label(label: str) -> str:
         for split in kcfg.splits():
             for target_id, csubst in split.splits.items():
                 label = '\n#And'.join(
-                    f'{self.kprint.pretty_print(v)}' for v in split.source.cterm.constraints + csubst.constraints
+                    f'{self.pretty_printer.print(v)}' for v in split.source.cterm.constraints + csubst.constraints
                 )
                 graph.edge(tail_name=split.source.id, head_name=target_id, label=f'  {label}        ')
 
@@ -438,15 +434,15 @@ def dump(self, cfgid: str, cfg: KCFG, dump_dir: Path, dot: bool = False) -> None
 
             config = node.cterm.config
             if not node_file.exists():
-                node_file.write_text(self.kprint.pretty_print(config))
+                node_file.write_text(self.pretty_printer.print(config))
                 _LOGGER.info(f'Wrote node file {cfgid}: {node_file}')
             config = minimize_term(config)
             if not node_minimized_file.exists():
-                node_minimized_file.write_text(self.kprint.pretty_print(config))
+                node_minimized_file.write_text(self.pretty_printer.print(config))
                 _LOGGER.info(f'Wrote node file {cfgid}: {node_minimized_file}')
             if not node_constraint_file.exists():
                 constraint = mlAnd(node.cterm.constraints)
-                node_constraint_file.write_text(self.kprint.pretty_print(constraint))
+                node_constraint_file.write_text(self.pretty_printer.print(constraint))
                 _LOGGER.info(f'Wrote node file {cfgid}: {node_constraint_file}')
 
         edges_dir = dump_dir / 'edges'
@@ -457,11 +453,11 @@ def dump(self, cfgid: str, cfg: KCFG, dump_dir: Path, dot: bool = False) -> None
 
             config = push_down_rewrites(KRewrite(edge.source.cterm.config, edge.target.cterm.config))
             if not edge_file.exists():
-                edge_file.write_text(self.kprint.pretty_print(config))
+                edge_file.write_text(self.pretty_printer.print(config))
                 _LOGGER.info(f'Wrote edge file {cfgid}: {edge_file}')
             config = minimize_term(config)
             if not edge_minimized_file.exists():
-                edge_minimized_file.write_text(self.kprint.pretty_print(config))
+                edge_minimized_file.write_text(self.pretty_printer.print(config))
                 _LOGGER.info(f'Wrote edge file {cfgid}: {edge_minimized_file}')
 
         covers_dir = dump_dir / 'covers'
@@ -471,12 +467,12 @@ def dump(self, cfgid: str, cfg: KCFG, dump_dir: Path, dot: bool = False) -> None
             cover_constraint_file = covers_dir / f'constraint_{cover.source.id}_{cover.target.id}.txt'
 
             subst_equalities = flatten_label(
-                '#And', cover.csubst.pred(sort_with=self.kprint.definition, constraints=False)
+                '#And', cover.csubst.pred(sort_with=self.pretty_printer.definition, constraints=False)
             )
 
             if not cover_file.exists():
-                cover_file.write_text('\n'.join(self.kprint.pretty_print(se) for se in subst_equalities))
+                cover_file.write_text('\n'.join(self.pretty_printer.print(se) for se in subst_equalities))
                 _LOGGER.info(f'Wrote cover file {cfgid}: {cover_file}')
             if not cover_constraint_file.exists():
-                cover_constraint_file.write_text(self.kprint.pretty_print(cover.csubst.constraint))
+                cover_constraint_file.write_text(self.pretty_printer.print(cover.csubst.constraint))
                 _LOGGER.info(f'Wrote cover file {cfgid}: {cover_constraint_file}')