Make kmir run parse in smir pretty jsons (#436)

Co-authored-by: devops <[email protected]>
Co-authored-by: Daniel Cumming <[email protected]>

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.63"
+version = "0.3.64"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.63'
+VERSION: Final = '0.3.64'

kmir/src/kmir/__main__.py

@@ -6,7 +6,10 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
+from pyk.kast.inner import KSort, Subst
+
 from kmir.build import semantics
+from kmir.convert_from_definition.v2parser import parse_json
 
 if TYPE_CHECKING:
     from collections.abc import Sequence
@@ -23,8 +26,20 @@ class RunOpts(KMirOpts):
 
 def _kmir_run(opts: RunOpts) -> None:
     tools = semantics()
-    rc, result = tools.krun.krun(opts.input_file)
-    print(tools.kprint.pretty_print(result))
+
+    parse_result = parse_json(tools.definition, opts.input_file, 'Pgm')
+    if parse_result is None:
+        print('Parse error!', file=sys.stderr)
+        sys.exit(1)
+
+    kmir_kast, _ = parse_result
+
+    subst = Subst({'$PGM': kmir_kast})
+    init_config = subst.apply(tools.definition.init_config(KSort('GeneratedTopCell')))
+    init_kore = tools.krun.kast_to_kore(init_config, KSort('GeneratedTopCell'))
+    result = tools.krun.run_pattern(init_kore)
+
+    print(tools.kprint.kore_to_pretty(result))
 
 
 def kmir(args: Sequence[str]) -> None:

kmir/src/kmir/convert_from_definition/__main__.py

@@ -1,10 +1,10 @@
 import argparse
-import json
 import sys
+from pathlib import Path
 
 from kmir.build import semantics
 
-from .v2parser import Parser
+from .v2parser import parse_json
 
 
 def parse_args() -> argparse.Namespace:
@@ -17,11 +17,9 @@ def parse_args() -> argparse.Namespace:
 def main() -> None:
     args = parse_args()
     tools = semantics()
-    p = Parser(tools.definition)
 
-    with open(args.json, 'r') as f:
-        json_data = json.load(f)
-    result = p.parse_mir_json(json_data, args.sort)
+    result = parse_json(tools.definition, Path(args.json), args.sort)
+
     if result is None:
         print('Parse error!', file=sys.stderr)
         sys.exit(1)

kmir/src/kmir/convert_from_definition/v2parser.py

@@ -1,5 +1,6 @@
 from __future__ import annotations
 
+import json
 from collections.abc import Sequence
 from functools import cached_property
 from typing import TYPE_CHECKING
@@ -9,13 +10,26 @@
 from pyk.kast.outer import KTerminal
 
 if TYPE_CHECKING:
+    from pathlib import Path
+
     from pyk.kast.outer import KDefinition, KProduction
 
 # Expected json
 JSON = dict | str | int | bool | Sequence | None
 ParseResult = tuple[KApply | KToken, KSort] | None
 
 
+def parse_json(definition: KDefinition, json_file: Path, sort: str) -> ParseResult:
+    p = Parser(definition)
+
+    with open(json_file, 'r') as f:
+        json_data = json.load(f)
+
+    result = p.parse_mir_json(json_data, sort)
+
+    return result
+
+
 # Return true if a production has been annotated with a mir* group
 def _is_mir_production(prod: KProduction) -> bool:
     group = prod.att.get(Atts.GROUP)

package/version

@@ -1 +1 @@
-0.3.63
+0.3.64