Skip to content

Commit df70d1a

Browse files
committed
Update _proof_node_printer
1 parent 1cd6243 commit df70d1a

File tree

1 file changed

+8
-21
lines changed

1 file changed

+8
-21
lines changed

src/kriscv/kprovex/_kprovex.py

Lines changed: 8 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@
1010
from .api import Config
1111

1212
if TYPE_CHECKING:
13-
from pyk.kcfg import KCFG
1413
from pyk.proof import ProofStatus
1514
from pyk.proof.show import APRProofNodePrinter
1615
from pyk.utils import BugReport
@@ -115,7 +114,7 @@ def show_proof(
115114

116115
proof = self._load_proof(proof_id)
117116
node_printer = self._proof_node_printer(proof, show_id=show_id, full_printer=True)
118-
proof_show = APRProofShow(self.config.kprove, node_printer=node_printer)
117+
proof_show = APRProofShow(self.config.definition, node_printer=node_printer)
119118
lines = proof_show.show(proof)
120119
if truncate:
121120
lines = [_truncate(line, 120) for line in lines]
@@ -194,30 +193,18 @@ def _proof_node_printer(
194193
full_printer: bool = False,
195194
minimize: bool = False,
196195
) -> APRProofNodePrinter:
197-
from pyk.kast.manip import minimize_term
196+
from pyk.cterm.show import CTermShow
198197
from pyk.proof.show import APRProofNodePrinter
199198

200199
show = self._load_show(show_id=show_id)
201-
config = self.config
202-
203-
class _NodePrinter(APRProofNodePrinter):
204-
def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
205-
attrs = self.node_attrs(kcfg, node)
206-
attr_str = ' (' + ', '.join(attrs) + ')' if attrs else ''
207-
node_strs = [f'{node.id}{attr_str}']
208-
if self.full_printer:
209-
kast = node.cterm.kast
210-
if self.minimize:
211-
kast = minimize_term(kast)
212-
show_res = show(config, kast)
213-
node_strs.extend(' ' + line for line in show_res.split('\n'))
214-
return node_strs
215-
216-
return _NodePrinter(
200+
printer = lambda kast: show(self.config, kast)
201+
return APRProofNodePrinter(
217202
proof=proof,
218-
kprint=None, # type: ignore [arg-type]
203+
cterm_show=CTermShow(
204+
printer=printer,
205+
minimize=minimize,
206+
),
219207
full_printer=full_printer,
220-
minimize=minimize,
221208
)
222209

223210

0 commit comments

Comments
 (0)