Factor out CTermShow class for simpler node printing

[ehildenb]

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.

[ehildenb]

Downstream repos to open branches into:

• https://github.com/runtimeverification/evm-semantics
  • Update: Update dependency: deps/k_release evm-semantics#2751
  • To this PR: Update dependency: deps/k_release evm-semantics#2764
• https://github.com/runtimeverification/mir-semantics
  • Update: Update dependency: deps/k_release mir-semantics#565
  • To this PR: Update dependency: deps/k_release mir-semantics#585
• https://github.com/runtimeverification/wasm-semantics
  • Update: Update dependency: deps/k_release wasm-semantics#724
  • To this PR: Update dependency: deps/k_release wasm-semantics#725
• https://github.com/runtimeverification/riscv-semantics
  • Update: Update dependency: deps/k_release riscv-semantics#86
  • To this PR: Update dependency: deps/k_release riscv-semantics#113
• https://github.com/runtimeverification/skribe
  • Update: Update dependency: deps/k_release skribe#12
  • To this PR: Update dependency: deps/k_release skribe#14
• https://github.com/runtimeverification/komet
  • Update: Update dependency: deps/kwasm_release komet#79
  • To this PR: Update dependency: deps/kwasm_release komet#80
• https://github.com/runtimeverification/kontrol
  • Update: Update dependency: deps/kevm_release kontrol#1008

[ehildenb]

Adjustments to import graph.

Before:

After:

In particular, kcfg is no longer importing ktool.

[ehildenb]

I have one more refactoring in mind, which should eliminate the need for eth NodePrinter class heirarchy (in favor of customizing CTermShow class and passing it around), but that should wait for a follow-up and is a bit more invasive.

Once that refactoring s in, our display heirarchy should be significantly simplified.

[tothtamas28]

I have one more refactoring in mind, which should eliminate the need for eth NodePrinter class heirarchy (in favor of customizing CTermShow class and passing it around), but that should wait for a follow-up and is a bit more invasive.

I see two issues that I think should be addressed when refactoring these classes.

1. Parallel class hierarchies: KCFGShow, KCFGViewer, NodePrinter vs APRProofShow, APRProofViewer, APRProofNodePrinter. My current understanding is that the only difference between these is that when printing a proof, there's a different set of node labels we want to show.

2. Coupling: these printing utilities (KCFGShow, KCFGViewer and the APRPRoof variants) depend on layers of concrete implementations of how a KAST term is printed (NodePrinter, which depends on PrettyPrinter, which depends on KDefinition, ...). Instead, they should define their own interface in terms of abstractions (e.g. a function that takes a Node and a KCFGViewer-specific set of configuration parameters, and returns a str for the node content to be printed). This makes configuration of the tools for a given semantics downstreams much more feasible.

[ehildenb]

1. I want to tackle this one. I will start by first getting rid of print_node in the NodePrinter heirarchy. Then it would be nice to handle the attrs directly at the KCFG level, but this is tricky because the attributes are different based on how you interpret the KCFG (as a raw KCFG or as an APRProof).
2. Also agreed. One step/improvement at a time though, this is what I have time for to get KMIR printing to look better, and I want to get it merged downstream all the way first, before introducing more potential breakages.