better KMIR show & new kmir info to get the de-refed type (#648)

- provide more options to `kmir show`;
- add a new command `kmir info` to show the dereferenced types.

Author: Stevengre

README.md

@@ -96,11 +96,46 @@ uv --project kmir run kmir link file1.smir.json file2.smir.json file3.smir.json
 uv --project kmir run kmir link file1.smir.json file2.smir.json
 ```
 
+**`kmir info`** - Inspect SMIR JSON metadata (currently: types)
+```bash
+# Show information about specific type IDs in a SMIR JSON
+uv --project kmir run kmir info path/to/program.smir.json --types "1,2,3"
+
+# Notes
+# - The --types option accepts a comma-separated list of numeric Stable MIR type IDs.
+# - Output format: one line per requested type, e.g.:
+#   Type Ty(1): Int(....)
+#   Type Ty(2): StructT(name=..., adt_def=..., fields=[...])
+# - If --types is omitted, the command currently produces no output.
+```
+
 ### Analysis Commands
 
-**`kmir show`** - Display proof information
+**`kmir show`** - Display proof information with advanced filtering options
 ```bash
+# Basic usage
 uv --project kmir run kmir show proof_id --proof-dir ./proof_dir
+
+# Show specific nodes only
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3"
+
+# Show node deltas (transitions between specific nodes)
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2,3:4"
+
+# Display full node information (default is compact)
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer
+
+# Show static information cells (functions, types, etc.)
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-static-info
+
+# Show current body cell content
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-current-body
+
+# Omit specific cells from output
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --omit-cells "cell1,cell2"
+
+# Combine multiple options for detailed analysis
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info --nodes "1,2" --verbose
 ```
 
 **`kmir view`** - Detailed view of proof results
@@ -128,7 +163,16 @@ uv --project kmir run kmir show-rules proof_id source_node target_node --proof-d
 
 3. **View Results**:
    ```bash
+   # Quick overview (compact format, static info hidden)
    uv --project kmir run kmir show proof_id --proof-dir ./proof_dir
+   
+   # Detailed analysis with full information
+   uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info
+   
+   # Focus on specific nodes
+   uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3"
+   
+   # Interactive view
    uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose
    ```
 
@@ -137,6 +181,32 @@ uv --project kmir run kmir show-rules proof_id source_node target_node --proof-d
    uv --project kmir run kmir show-rules proof_id 1 3 --proof-dir ./proof_dir
    ```
 
+### Advanced Show Usage Examples
+
+**Debugging workflow:**
+```bash
+# 1. Start with a quick overview
+uv --project kmir run kmir show my_proof --proof-dir ./proofs
+
+# 2. Focus on problematic nodes (e.g., nodes 5, 6, 7)
+uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "5,6,7"
+
+# 3. Examine transitions between specific nodes
+uv --project kmir run kmir show my_proof --proof-dir ./proofs --node-deltas "5:6,6:7"
+
+# 4. Get full details for deep debugging
+uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "6" --full-printer --no-omit-static-info --no-omit-current-body
+```
+
+**Performance analysis:**
+```bash
+# Hide verbose cells but show execution flow
+uv --project kmir run kmir show my_proof --proof-dir ./proofs --omit-cells "locals,heap" --verbose
+
+# Focus on function calls and type information
+uv --project kmir run kmir show my_proof --proof-dir ./proofs --no-omit-static-info --omit-cells "currentBody"
+```
+
 ### Command Options
 
 Most commands support:
@@ -146,6 +216,15 @@ Most commands support:
 - `--max-depth DEPTH`: Maximum execution depth
 - `--max-iterations ITERATIONS`: Maximum iterations
 
+**`kmir show` specific options:**
+- `--nodes NODES`: Comma separated list of node IDs to show (e.g., "1,2,3")
+- `--node-deltas DELTAS`: Comma separated list of node deltas in format "source:target" (e.g., "1:2,3:4")
+- `--omit-cells CELLS`: Comma separated list of cell names to omit from output
+- `--full-printer`: Display the full node in output (default is compact)
+- `--no-omit-static-info`: Display static information cells (functions, start-symbol, types, adt-to-ty)
+- `--no-omit-current-body`: Display the `<currentBody>` cell completely
+- `--smir-info SMIR_INFO`: Path to SMIR JSON file to improve debug messaging
+
 For complete options, use `--help` with each command.
 
 ### Supporters

kmir/src/kmir/__main__.py

@@ -20,6 +20,7 @@
 from .linker import link
 from .options import (
     GenSpecOpts,
+    InfoOpts,
     LinkOpts,
     ProveRawOpts,
     ProveRSOpts,
@@ -30,7 +31,7 @@
     ViewOpts,
 )
 from .parse.parser import parse_json
-from .smir import SMIRInfo
+from .smir import SMIRInfo, Ty
 
 if TYPE_CHECKING:
     from argparse import Namespace
@@ -130,14 +131,38 @@ def _kmir_view(opts: ViewOpts) -> None:
 
 
 def _kmir_show(opts: ShowOpts) -> None:
+    from pyk.kast.pretty import PrettyPrinter
+
+    from .kprint import KMIRPrettyPrinter
+
     kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR)
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
-    printer = PrettyPrinter(kmir.definition)
-    omit_labels = ('<currentBody>',) if opts.omit_current_body else ()
-    cterm_show = CTermShow(printer.print, omit_labels=omit_labels)
+
+    # Use custom KMIR printer by default, switch to standard printer if requested
+    if opts.use_default_printer:
+        printer = PrettyPrinter(kmir.definition)
+        _LOGGER.info('Using standard PrettyPrinter')
+    else:
+        printer = KMIRPrettyPrinter(kmir.definition)
+        _LOGGER.info('Using custom KMIRPrettyPrinter')
+
+    all_omit_cells = list(opts.omit_cells or ())
+    if opts.omit_current_body:
+        all_omit_cells.append('<currentBody>')
+
+    cterm_show = CTermShow(printer.print, omit_labels=tuple(all_omit_cells))
     node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts)
     shower = APRProofShow(kmir.definition, node_printer=node_printer)
-    lines = shower.show(proof)
+    shower.kcfg_show.pretty_printer = printer
+    _LOGGER.info(
+        f'Showing {proof.id} with\n nodes: {opts.nodes},\n node_deltas: {opts.node_deltas},\n omit_cells: {tuple(all_omit_cells)}'
+    )
+    lines = shower.show(
+        proof,
+        nodes=opts.nodes or (),
+        node_deltas=opts.node_deltas or (),
+        omit_cells=tuple(all_omit_cells),
+    )
     print('\n'.join(lines))
 
 
@@ -164,6 +189,16 @@ def _kmir_prune(opts: PruneOpts) -> None:
     proof.write_proof_data()
 
 
+def _kmir_info(opts: InfoOpts) -> None:
+    smir_info = SMIRInfo.from_file(opts.smir_file)
+
+    if opts.types:
+        print(f'\nTypes requested: {opts.types}')
+        chosen_types = [Ty(type_id) for type_id in opts.types]
+        for type_id in chosen_types:
+            print(f'Type {type_id}: {smir_info.unref_type(type_id)}')
+
+
 def _kmir_link(opts: LinkOpts) -> None:
     result = link([SMIRInfo.from_file(f) for f in opts.smir_files])
     result.dump(opts.output_file)
@@ -178,6 +213,8 @@ def kmir(args: Sequence[str]) -> None:
             _kmir_run(opts)
         case GenSpecOpts():
             _kmir_gen_spec(opts)
+        case InfoOpts():
+            _kmir_info(opts)
         case ProveRawOpts():
             _kmir_prove_raw(opts)
         case ViewOpts():
@@ -221,6 +258,12 @@ def _arg_parser() -> ArgumentParser:
         '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
     )
 
+    info_parser = command_parser.add_parser(
+        'info', help='Show information about a SMIR JSON file', parents=[kcli_args.logging_args]
+    )
+    info_parser.add_argument('smir_file', metavar='FILE', help='SMIR JSON file to analyze')
+    info_parser.add_argument('--types', metavar='TYPES', help='Comma separated list of type IDs to show details for')
+
     prove_args = ArgumentParser(add_help=False)
     prove_args.add_argument('--proof-dir', metavar='DIR', help='Proof directory')
     prove_args.add_argument('--bug-report', metavar='PATH', help='path to optional bug report')
@@ -247,11 +290,11 @@ def _arg_parser() -> ArgumentParser:
 
     display_args = ArgumentParser(add_help=False)
     display_args.add_argument(
-        '--no-full-printer',
+        '--full-printer',
         dest='full_printer',
-        action='store_false',
-        default=True,
-        help='Do not display the full node in output.',
+        action='store_true',
+        default=False,
+        help='Display the full node in output.',
     )
     display_args.add_argument(
         '--smir-info',
@@ -268,9 +311,30 @@ def _arg_parser() -> ArgumentParser:
         help='Display the <currentBody> cell completely.',
     )
 
-    command_parser.add_parser(
+    show_parser = command_parser.add_parser(
         'show', help='Show proof information', parents=[kcli_args.logging_args, proof_args, display_args]
     )
+    show_parser.add_argument('--nodes', metavar='NODES', help='Comma separated list of node IDs to show')
+    show_parser.add_argument(
+        '--node-deltas', metavar='DELTAS', help='Comma separated list of node deltas in format "source:target"'
+    )
+    show_parser.add_argument(
+        '--omit-cells', metavar='CELLS', help='Comma separated list of cell names to omit from output'
+    )
+    show_parser.add_argument(
+        '--no-omit-static-info',
+        dest='omit_static_info',
+        action='store_false',
+        default=True,
+        help='Display static information cells (functions, start-symbol, types, adt-to-ty)',
+    )
+    show_parser.add_argument(
+        '--use-default-printer',
+        dest='use_default_printer',
+        action='store_true',
+        default=False,
+        help='Use standard PrettyPrinter instead of custom KMIR printer',
+    )
 
     show_rules_parser = command_parser.add_parser(
         'show-rules', help='Show rules applied on a specific edge', parents=[kcli_args.logging_args, proof_args]
@@ -324,6 +388,8 @@ def _parse_args(ns: Namespace) -> KMirOpts:
             )
         case 'gen-spec':
             return GenSpecOpts(input_file=Path(ns.input_file), output_file=ns.output_file, start_symbol=ns.start_symbol)
+        case 'info':
+            return InfoOpts(smir_file=Path(ns.smir_file), types=ns.types)
         case 'prove':
             proof_dir = Path(ns.proof_dir)
             return ProveRawOpts(
@@ -343,6 +409,11 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 full_printer=ns.full_printer,
                 smir_info=Path(ns.smir_info) if ns.smir_info else None,
                 omit_current_body=ns.omit_current_body,
+                nodes=ns.nodes,
+                node_deltas=ns.node_deltas,
+                omit_cells=ns.omit_cells,
+                omit_static_info=ns.omit_static_info,
+                use_default_printer=ns.use_default_printer,
             )
         case 'show-rules':
             return ShowRulesOpts(

kmir/src/kmir/kprint.py

@@ -0,0 +1,28 @@
+from __future__ import annotations
+
+import logging
+from typing import TYPE_CHECKING
+
+from pyk.kast.pretty import PrettyPrinter, indent
+
+_LOGGER: logging.Logger = logging.getLogger(__name__)
+
+if TYPE_CHECKING:
+    from pyk.kast.outer import KDefinition
+
+
+class KMIRPrettyPrinter(PrettyPrinter):
+    """
+    Custom Pretty Printer for improved ListItem display formatting.
+    Formats ListItem elements with line breaks for better readability.
+    """
+
+    def __init__(self, definition: KDefinition) -> None:
+        """
+        Initialize KMIR Pretty Printer
+
+        Args:
+            definition: K definition
+        """
+        super().__init__(definition)
+        self.symbol_table['ListItem'] = lambda *args: 'ListItem (' + (indent(', '.join(args))).strip() + ')\n'

kmir/src/kmir/options.py

@@ -138,7 +138,7 @@ def __init__(
         self,
         proof_dir: Path | str,
         id: str,
-        full_printer: bool = True,
+        full_printer: bool = False,
         smir_info: Path | None = None,
         omit_current_body: bool = True,
     ) -> None:
@@ -150,7 +150,48 @@ def __init__(
 
 
 @dataclass
-class ShowOpts(DisplayOpts): ...
+class ShowOpts(DisplayOpts):
+    nodes: tuple[int, ...] | None
+    node_deltas: tuple[tuple[int, int], ...] | None
+    omit_cells: tuple[str, ...] | None
+    omit_static_info: bool
+    use_default_printer: bool
+
+    def __init__(
+        self,
+        proof_dir: Path | str,
+        id: str,
+        full_printer: bool = False,
+        smir_info: Path | None = None,
+        omit_current_body: bool = True,
+        nodes: str | None = None,
+        node_deltas: str | None = None,
+        omit_cells: str | None = None,
+        omit_static_info: bool = True,
+        use_default_printer: bool = False,
+    ) -> None:
+        super().__init__(proof_dir, id, full_printer, smir_info, omit_current_body)
+        self.omit_static_info = omit_static_info
+        self.use_default_printer = use_default_printer
+        self.nodes = tuple(int(n.strip()) for n in nodes.split(',')) if nodes is not None else None
+        if node_deltas is not None:
+            deltas = []
+            for delta in node_deltas.split(','):
+                parts = delta.strip().split(':')
+                if len(parts) == 2:
+                    deltas.append((int(parts[0].strip()), int(parts[1].strip())))
+            self.node_deltas = tuple(deltas)
+        else:
+            self.node_deltas = None
+
+        static_info_cells = ('<functions>', '<start-symbol>', '<types>', '<adt-to-ty>')
+
+        user_omit_cells = tuple(cell.strip() for cell in omit_cells.split(',')) if omit_cells is not None else ()
+
+        if omit_static_info:
+            self.omit_cells = static_info_cells + user_omit_cells
+        else:
+            self.omit_cells = user_omit_cells if user_omit_cells else None
 
 
 @dataclass
@@ -180,6 +221,16 @@ class PruneOpts(ProofOpts):
     node_id: int
 
 
+@dataclass
+class InfoOpts(KMirOpts):
+    smir_file: Path
+    types: tuple[int, ...] | None
+
+    def __init__(self, smir_file: Path, types: str | None = None) -> None:
+        self.smir_file = smir_file
+        self.types = tuple(int(t.strip()) for t in types.split(',')) if types is not None else None
+
+
 @dataclass
 class LinkOpts(KMirOpts):
     smir_files: list[Path]