Update dependency: deps/k_release

deps/k_release

@@ -1 +1 @@
-7.1.253
+7.1.257

flake.nix

@@ -1,7 +1,7 @@
 {
   description = "kmir - ";
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.253";
+    k-framework.url = "github:runtimeverification/k/v7.1.257";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";

kmir/pyproject.toml

@@ -4,11 +4,11 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.169"
+version = "0.3.170"
 description = ""
 requires-python = "~=3.10"
 dependencies = [
-    "kframework==v7.1.253",
+    "kframework==v7.1.257",
 ]
 
 [[project.authors]]

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.169'
+VERSION: Final = '0.3.170'

kmir/src/kmir/__main__.py

@@ -7,7 +7,9 @@
 from typing import TYPE_CHECKING
 
 from pyk.cli.args import KCLIArgs
+from pyk.cterm.show import CTermShow
 from pyk.kast.outer import KFlatModule, KImport
+from pyk.kast.pretty import PrettyPrinter
 from pyk.proof.reachability import APRProof, APRProver
 from pyk.proof.show import APRProofShow
 from pyk.proof.tui import APRProofViewer
@@ -115,7 +117,9 @@ def _kmir_view(opts: ViewOpts) -> None:
     smir_info = None
     if opts.smir_info is not None:
         smir_info = SMIRInfo.from_file(opts.smir_info)
-    node_printer = KMIRAPRNodePrinter(kmir, proof, smir_info=smir_info, full_printer=False)
+    printer = PrettyPrinter(kmir.definition)
+    cterm_show = CTermShow(printer.print)
+    node_printer = KMIRAPRNodePrinter(cterm_show, proof, smir_info=smir_info, full_printer=False)
     viewer = APRProofViewer(proof, kmir, node_printer=node_printer)
     viewer.run()
 
@@ -126,8 +130,10 @@ def _kmir_show(opts: ShowOpts) -> None:
     smir_info = None
     if opts.smir_info is not None:
         smir_info = SMIRInfo.from_file(opts.smir_info)
-    node_printer = KMIRAPRNodePrinter(kmir, proof, smir_info=smir_info, full_printer=opts.full_printer)
-    shower = APRProofShow(kmir, node_printer=node_printer)
+    printer = PrettyPrinter(kmir.definition)
+    cterm_show = CTermShow(printer.print)
+    node_printer = KMIRAPRNodePrinter(cterm_show, proof, smir_info=smir_info, full_printer=opts.full_printer)
+    shower = APRProofShow(kmir.definition, node_printer=node_printer)
     lines = shower.show(proof)
     print('\n'.join(lines))
 

kmir/src/kmir/kmir.py

@@ -31,6 +31,7 @@
     from pathlib import Path
     from typing import Final
 
+    from pyk.cterm.show import CTermShow
     from pyk.kore.syntax import Pattern
     from pyk.utils import BugReport
 
@@ -187,21 +188,18 @@ def is_terminal(self, cterm: CTerm) -> bool:
 
 
 class KMIRNodePrinter(NodePrinter):
-    kmir: KMIR
-
-    def __init__(self, kmir: KMIR, full_printer: bool = False) -> None:
-        NodePrinter.__init__(self, kmir, full_printer=full_printer)
-        self.kmir = kmir
+    def __init__(self, cterm_show: CTermShow, full_printer: bool = False) -> None:
+        NodePrinter.__init__(self, cterm_show, full_printer=full_printer)
 
 
 class KMIRAPRNodePrinter(KMIRNodePrinter, APRProofNodePrinter):
     smir_info: SMIRInfo | None
 
     def __init__(
-        self, kmir: KMIR, proof: APRProof, smir_info: SMIRInfo | None = None, full_printer: bool = False
+        self, cterm_show: CTermShow, proof: APRProof, smir_info: SMIRInfo | None = None, full_printer: bool = False
     ) -> None:
-        KMIRNodePrinter.__init__(self, kmir, full_printer=full_printer)
-        APRProofNodePrinter.__init__(self, proof, kmir, full_printer=full_printer)
+        KMIRNodePrinter.__init__(self, cterm_show, full_printer=full_printer)
+        APRProofNodePrinter.__init__(self, proof, cterm_show, full_printer=full_printer)
         self.smir_info = smir_info
 
     def _span(self, node: KCFG.Node) -> int | None:
@@ -246,7 +244,7 @@ def _function_name(self, node: KCFG.Node) -> str | None:
 
     def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
         ret_strs = super().print_node(kcfg, node)
-        ret_strs.append(self.kmir.pretty_print(node.cterm.cell('K_CELL'))[0:80])
+        ret_strs.append(self.cterm_show._printer(node.cterm.cell('K_CELL'))[0:80])
         curr_func = self._function_name(node)
         if curr_func is not None:
             ret_strs.append(f'function: {curr_func}')

kmir/src/tests/integration/test_integration.py

@@ -6,7 +6,9 @@
 from typing import TYPE_CHECKING
 
 import pytest
+from pyk.cterm.show import CTermShow
 from pyk.kast.inner import KApply, KSort, KToken
+from pyk.kast.pretty import PrettyPrinter
 from pyk.proof import Proof
 from pyk.proof.show import APRProofShow
 
@@ -469,12 +471,17 @@ def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> No
 
         apr_proof = kmir.prove_rs(prove_rs_opts)
 
+        printer = PrettyPrinter(kmir.definition)
+        cterm_show = CTermShow(printer.print)
+
         if not should_fail:
             assert apr_proof.passed
         else:
             assert apr_proof.failed
 
-        shower = APRProofShow(kmir, node_printer=KMIRAPRNodePrinter(kmir, apr_proof, full_printer=False))
+        shower = APRProofShow(
+            kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, full_printer=False)
+        )
         show_res = '\n'.join(shower.show(apr_proof))
         assert_or_update_show_output(
             show_res, PROVING_DIR / f'show/{rs_file.stem}.expected', update=update_expected_output
@@ -498,10 +505,15 @@ def test_prove_pinocchio(kmir: KMIR, update_expected_output: bool) -> None:
     ]
     prove_rs_opts = ProveRSOpts(pinocchio_token_program, smir=True)
 
+    printer = PrettyPrinter(kmir.definition)
+    cterm_show = CTermShow(printer.print)
+
     for start_symbol in start_symbols:
         prove_rs_opts.start_symbol = start_symbol
         apr_proof = kmir.prove_rs(prove_rs_opts)
-        shower = APRProofShow(kmir, node_printer=KMIRAPRNodePrinter(kmir, apr_proof, full_printer=True))
+        shower = APRProofShow(
+            kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, full_printer=True)
+        )
         show_res = '\n'.join(shower.show(apr_proof))
         assert_or_update_show_output(
             show_res,

package/version

@@ -1 +1 @@
-0.3.169
+0.3.170