Add --rules and node-deltas-pro optios for kmir show (#649)

- Added options for displaying additional node deltas and rules in `kmir
show`.
- Updated the README to reflect new command usage and examples.
- Removed the deprecated `show-rules` command and integrated its
functionality into `kmir show`.
- Introduced a utility function to render rules as Markdown links for
better readability.

Author: Stevengre

README.md

@@ -122,6 +122,9 @@ 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"
 
+# Show additional deltas after the main output, and also print rules for those edges
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2" --node-deltas-pro "3:4"
+
 # Display full node information (default is compact)
 uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer
 
@@ -143,9 +146,9 @@ uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer
 uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose
 ```
 
-**`kmir show-rules`** - Show rules applied between nodes
+**Rules within `kmir show`** - Show rules applied between nodes
 ```bash
-uv --project kmir run kmir show-rules proof_id source_node target_node --proof-dir ./proof_dir
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "SOURCE:TARGET[,SOURCE:TARGET...]"
 ```
 
 ### Recommended Workflow
@@ -178,7 +181,7 @@ uv --project kmir run kmir show-rules proof_id source_node target_node --proof-d
 
 4. **Analyze Rules**:
    ```bash
-   uv --project kmir run kmir show-rules proof_id 1 3 --proof-dir ./proof_dir
+   uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "1:3"
    ```
 
 ### Advanced Show Usage Examples
@@ -219,6 +222,8 @@ Most commands support:
 **`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")
+- `--node-deltas-pro DELTAS`: Additional node deltas (same format as `--node-deltas`). Equivalent to "print the corresponding deltas again, and automatically print the rules for these edges".
+- `--rules EDGES`: Comma separated list of edges in format "source:target". Prints rules for each edge in Markdown link format `[label](file:///abs/path#LstartLine)` when available
 - `--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)

kmir/src/kmir/__main__.py

@@ -27,11 +27,11 @@
     PruneOpts,
     RunOpts,
     ShowOpts,
-    ShowRulesOpts,
     ViewOpts,
 )
 from .parse.parser import parse_json
 from .smir import SMIRInfo, Ty
+from .utils import render_rules
 
 if TYPE_CHECKING:
     from argparse import Namespace
@@ -154,32 +154,23 @@ def _kmir_show(opts: ShowOpts) -> None:
     node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts)
     shower = APRProofShow(kmir.definition, node_printer=node_printer)
     shower.kcfg_show.pretty_printer = printer
+    effective_node_deltas = tuple(sorted({*(opts.node_deltas or ()), *(opts.node_deltas_pro or ())}))
+    effective_rule_edges = tuple(sorted({*(opts.rules or ()), *(opts.node_deltas_pro or ())}))
+
     _LOGGER.info(
-        f'Showing {proof.id} with\n nodes: {opts.nodes},\n node_deltas: {opts.node_deltas},\n omit_cells: {tuple(all_omit_cells)}'
+        f'Showing {proof.id} with\n nodes: {opts.nodes},\n node_deltas: {effective_node_deltas},\n omit_cells: {tuple(all_omit_cells)}'
     )
     lines = shower.show(
         proof,
         nodes=opts.nodes or (),
-        node_deltas=opts.node_deltas or (),
+        node_deltas=effective_node_deltas,
         omit_cells=tuple(all_omit_cells),
     )
-    print('\n'.join(lines))
-
+    if effective_rule_edges:
+        lines.append('# Rules: ')
+        lines.extend(render_rules(proof, effective_rule_edges))
 
-def _kmir_show_rules(opts: ShowRulesOpts) -> None:
-    """Show rules applied on the edge from source to target node."""
-    proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
-    edge = proof.kcfg.edge(opts.source, opts.target)
-    if edge is None:
-        print(f'Error: No edge found from node {opts.source} to node {opts.target}')
-        return
-    rules = edge.rules
-    print(f'Rules applied on edge {opts.source} -> {opts.target}:')
-    print(f'Total rules: {len(rules)}')
-    print('-' * 80)
-    for rule in rules:
-        print(rule)
-        print('-' * 80)
+    print('\n'.join(lines))
 
 
 def _kmir_prune(opts: PruneOpts) -> None:
@@ -221,8 +212,6 @@ def kmir(args: Sequence[str]) -> None:
             _kmir_view(opts)
         case ShowOpts():
             _kmir_show(opts)
-        case ShowRulesOpts():
-            _kmir_show_rules(opts)
         case PruneOpts():
             _kmir_prune(opts)
         case ProveRSOpts():
@@ -318,6 +307,9 @@ def _arg_parser() -> ArgumentParser:
     show_parser.add_argument(
         '--node-deltas', metavar='DELTAS', help='Comma separated list of node deltas in format "source:target"'
     )
+    show_parser.add_argument(
+        '--node-deltas-pro', metavar='DELTAS', help='Extra node deltas (printed after main output)'
+    )
     show_parser.add_argument(
         '--omit-cells', metavar='CELLS', help='Comma separated list of cell names to omit from output'
     )
@@ -336,11 +328,7 @@ def _arg_parser() -> ArgumentParser:
         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]
-    )
-    show_rules_parser.add_argument('source', type=int, metavar='SOURCE', help='Source node ID')
-    show_rules_parser.add_argument('target', type=int, metavar='TARGET', help='Target node ID')
+    show_parser.add_argument('--rules', metavar='EDGES', help='Comma separated list of edges in format "source:target"')
 
     command_parser.add_parser(
         'view', help='View proof information', parents=[kcli_args.logging_args, proof_args, display_args]
@@ -411,17 +399,12 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 omit_current_body=ns.omit_current_body,
                 nodes=ns.nodes,
                 node_deltas=ns.node_deltas,
+                node_deltas_pro=ns.node_deltas_pro,
+                rules=ns.rules,
                 omit_cells=ns.omit_cells,
                 omit_static_info=ns.omit_static_info,
                 use_default_printer=ns.use_default_printer,
             )
-        case 'show-rules':
-            return ShowRulesOpts(
-                proof_dir=Path(ns.proof_dir),
-                id=ns.id,
-                source=ns.source,
-                target=ns.target,
-            )
         case 'view':
             proof_dir = Path(ns.proof_dir)
             return ViewOpts(

kmir/src/kmir/options.py

@@ -153,6 +153,8 @@ def __init__(
 class ShowOpts(DisplayOpts):
     nodes: tuple[int, ...] | None
     node_deltas: tuple[tuple[int, int], ...] | None
+    node_deltas_pro: tuple[tuple[int, int], ...] | None
+    rules: tuple[tuple[int, int], ...] | None
     omit_cells: tuple[str, ...] | None
     omit_static_info: bool
     use_default_printer: bool
@@ -166,6 +168,8 @@ def __init__(
         omit_current_body: bool = True,
         nodes: str | None = None,
         node_deltas: str | None = None,
+        node_deltas_pro: str | None = None,
+        rules: str | None = None,
         omit_cells: str | None = None,
         omit_static_info: bool = True,
         use_default_printer: bool = False,
@@ -174,15 +178,20 @@ def __init__(
         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(','):
+
+        def _parse_pairs(text: str | None) -> tuple[tuple[int, int], ...] | None:
+            if text is None:
+                return None
+            pairs: list[tuple[int, int]] = []
+            for delta in text.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
+                if len(parts) == 2 and parts[0].strip() and parts[1].strip():
+                    pairs.append((int(parts[0].strip()), int(parts[1].strip())))
+            return tuple(pairs)
+
+        self.node_deltas = _parse_pairs(node_deltas)
+        self.node_deltas_pro = _parse_pairs(node_deltas_pro)
+        self.rules = _parse_pairs(rules)
 
         static_info_cells = ('<functions>', '<start-symbol>', '<types>', '<adt-to-ty>')
 
@@ -198,24 +207,6 @@ def __init__(
 class ViewOpts(DisplayOpts): ...
 
 
-@dataclass
-class ShowRulesOpts(ProofOpts):
-    source: int
-    target: int
-
-    def __init__(
-        self,
-        proof_dir: Path | str,
-        id: str,
-        source: int,
-        target: int,
-    ) -> None:
-        self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
-        self.id = id
-        self.source = source
-        self.target = target
-
-
 @dataclass
 class PruneOpts(ProofOpts):
     node_id: int

kmir/src/kmir/utils.py

@@ -0,0 +1,104 @@
+from __future__ import annotations
+
+import re
+from pathlib import Path
+from typing import TYPE_CHECKING, Sequence
+
+if TYPE_CHECKING:
+    from pyk.proof.reachability import APRProof
+
+
+def _rule_to_markdown_link(rule: object) -> str:
+    """Render a single rule as a Markdown file link if possible.
+
+    The function tries, in order:
+    - Parse the first line of str(rule) for pattern: <id>:/abs/path:(startLine, startCol, endLine, endCol)
+    - Use rule attributes 'source' and 'location' when available
+
+    Fallback to the first line of str(rule) if no path can be determined.
+    """
+    text_first = str(rule).splitlines()[0]
+
+    # 1) Parse textual representation first (most robust across backends)
+    m_text = re.match(r'^[^:]+:(/[^:]+):\((\d+)\s*,\s*\d+\s*,\s*\d+\s*,\s*\d+\)\s*$', text_first)
+    if m_text:
+        file_path = m_text.group(1)
+        start_line = int(m_text.group(2))
+        uri = Path(file_path).resolve().as_uri()
+        label_text = f'{Path(file_path).name}:{start_line}'
+        return f'[{label_text}]({uri}#L{start_line})'
+
+    # 2) Try attributes on the rule object (when present)
+    try:
+        att = getattr(rule, 'att', None)
+        source_file: str | None = None
+        if att is not None:
+            get = getattr(att, 'get', None)
+            if callable(get):
+                source_file = get('source')
+                loc = get('location')
+            else:
+                try:
+                    source_file = att['source']  # type: ignore[index]
+                except Exception:
+                    source_file = None
+                try:
+                    loc = att['location']  # type: ignore[index]
+                except Exception:
+                    loc = None
+
+            if isinstance(loc, str):
+                # Format 1: startLine:startCol-endLine:endCol
+                m = re.match(r'^(\d+):(\d+)-(\d+):(\d+)$', loc)
+                if m:
+                    start_line = int(m.group(1))
+                else:
+                    # Format 2: (startLine, startCol, endLine, endCol)
+                    m2 = re.match(r'^\(\s*(\d+)\s*,\s*\d+\s*,\s*\d+\s*,\s*\d+\s*\)$', loc)
+                    if m2:
+                        start_line = int(m2.group(1))
+
+            if source_file is not None:
+                uri = Path(source_file).resolve().as_uri()
+                line_anchor = f'#L{start_line}' if start_line is not None else ''
+                label_text = (
+                    f'{Path(source_file).name}:{start_line}' if start_line is not None else Path(source_file).name
+                )
+                return f'[{label_text}]({uri}{line_anchor})'
+    except Exception:
+        pass
+
+    # 3) Fallback: raw first line
+    return text_first
+
+
+def render_rules(proof: APRProof, edges: Sequence[tuple[int, int]]) -> list[str]:
+    """Render rules for a collection of edges as markdown text lines.
+
+    - proof: APRProof containing the kcfg with edges
+    - edges: iterable of (src, dst)
+    """
+    # Deduplicate while preserving a stable ordering
+    seen: set[tuple[int, int]] = set()
+    ordered_unique_edges: list[tuple[int, int]] = []
+    for e in edges:
+        if e not in seen:
+            seen.add(e)
+            ordered_unique_edges.append(e)
+
+    lines: list[str] = []
+    for src, dst in ordered_unique_edges:
+        edge = proof.kcfg.edge(src, dst)
+        if edge is None:
+            lines.append(f'Rules applied on edge {src} -> {dst}:')
+            lines.append('No edge found')
+            continue
+        applied = edge.rules
+        lines.append(f'Rules applied on edge {src} -> {dst}:')
+        lines.append(f'Total rules: {len(applied)}')
+        lines.append('-' * 80)
+        for rule in applied:
+            lines.append(_rule_to_markdown_link(rule))
+            lines.append('-' * 80)
+
+    return lines