kprint.pretty_print: Overload to allow printing Substs

We don't add pretty print as a member to Subst since this causes a circular dependency between kprint.py and kast.py
runtimeverification · Jun 5, 2022 · 8ad6728 · 8ad6728
1 parent c3274e4
commit 8ad6728
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 8 deletions.
diff --git a/pyk/src/pyk/kcfg.py b/pyk/src/pyk/kcfg.py
@@ -256,9 +256,6 @@ def show_node(node: KCFG.Node) -> str:
         def add_indent(indent: str, lines: List[str]) -> Iterable[str]:
             return map(lambda line: indent + line, lines)
 
-        def pretty_print_subst(subst: Subst) -> List[str]:
-            return [f'{k:>10} |-> {kprint.pretty_print(v)}' for k, v in subst.minimize().items()]
-
         def edge_likes_from(node: KCFG.Node) -> List[KCFG.EdgeLike]:
             return cast(List[KCFG.EdgeLike], self.edges(source_id=node.id)) \
                  + cast(List[KCFG.EdgeLike], self.covers(source_id=node.id))
@@ -300,7 +297,7 @@ def print_subgraph(indent: str, curr_node: KCFG.Node) -> List[str]:
                 elif isinstance(edge_like, KCFG.Cover):
                     ret.append(indent + '│  constraint: ' + str(kprint.pretty_print(edge_like.constraint)))
                     ret.append(indent + '│  subst:')
-                    ret.extend(add_indent(indent + '│  ', pretty_print_subst(edge_like.subst)))
+                    ret.extend(add_indent(indent + '│  ', kprint.pretty_print(edge_like.subst)))
 
                 ret.append((indent + elbow + ' ' + show_node(edge_like.target)))
                 ret.extend(print_subgraph(new_indent, edge_like.target))

diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py
@@ -5,6 +5,7 @@
     TRUE,
     KApply,
     KAs,
+    KAst,
     KAtt,
     KBubble,
     KClaim,
@@ -28,6 +29,7 @@
     KTerminal,
     KToken,
     KVariable,
+    Subst,
     flattenLabel,
     ktokenDots,
     readKastTerm,
@@ -46,13 +48,17 @@ def __init__(self, kompiled_directory):
         self.symbol_table = build_symbol_table(self.definition, opinionated=True)
         self.definition_hash = hash_str(self.definition)
 
-    def pretty_print(self, kast, debug=False):
-        """Given a KAST term, pretty-print it using the current definition.
+    def pretty_print(self, subject, debug=False):
+        """ subject: KAST term or Subst from variables to KAST terms.
 
-        -   Input: KAST term in JSON.
+        -   Input: KAST term, or Subst.
         -   Output: Best-effort pretty-printed representation of the KAST term.
         """
-        return prettyPrintKast(kast, self.symbol_table, debug=debug)
+        if isinstance(subject, Subst):
+            return [f'{k:>10} |-> {self.pretty_print(v)}' for k, v in subst.minimize().items()]
+        if isinstance(subject, KAst): 
+            return prettyPrintKast(subject, self.symbol_table, debug=debug)
+        assert(False)
 
 
 def unparser_for_production(prod):