Factor out CTermShow class for simpler node printing

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}')