Inline Tools class into KMIR and replumb

Makefile

@@ -1,12 +1,14 @@
 UV     := uv --directory kmir
 UV_RUN := $(UV) run
 
+PARALLEL := 4
+
 TOP_DIR    := $(shell pwd)
 
 default: check build
 
 build:
-	$(UV_RUN) kdist -v build mir-semantics\.* -j4
+	$(UV_RUN) kdist -v build mir-semantics\.* -j$(PARALLEL)
 
 .PHONY: test
 test: test-unit test-integration smir-parse-tests
@@ -46,7 +48,7 @@ test-unit:
 
 test-integration: build
 	$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
-			--durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
+			--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)
 
 # Checks and formatting
 

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.136"
+version = "0.3.137"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.136'
+VERSION: Final = '0.3.137'

kmir/src/kmir/__main__.py

@@ -11,7 +11,7 @@
 from pyk.proof.reachability import APRProof, APRProver
 from pyk.proof.tui import APRProofViewer
 
-from .build import HASKELL_DEF_DIR, LLVM_LIB_DIR, haskell_semantics, llvm_semantics
+from .build import HASKELL_DEF_DIR, LLVM_DEF_DIR, LLVM_LIB_DIR
 from .kmir import KMIR, KMIRAPRNodePrinter
 from .options import GenSpecOpts, ProvePruneOpts, ProveRSOpts, ProveRunOpts, ProveViewOpts, RunOpts
 from .parse.parser import parse_json
@@ -29,7 +29,7 @@
 
 
 def _kmir_run(opts: RunOpts) -> None:
-    tools = haskell_semantics() if opts.haskell_backend else llvm_semantics()
+    kmir = KMIR(HASKELL_DEF_DIR) if opts.haskell_backend else KMIR(LLVM_DEF_DIR)
 
     smir_file: Path
     if opts.file:
@@ -39,16 +39,16 @@ def _kmir_run(opts: RunOpts) -> None:
         target = opts.bin if opts.bin else cargo.default_target
         smir_file = cargo.smir_for(target)
 
-    parse_result = parse_json(tools.definition, smir_file, 'Pgm')
+    parse_result = parse_json(kmir.definition, smir_file, 'Pgm')
     if parse_result is None:
         print('Parse error!', file=sys.stderr)
         sys.exit(1)
 
     kmir_kast, _ = parse_result
 
-    result = tools.run_parsed(kmir_kast, opts.start_symbol, opts.depth)
+    result = kmir.run_parsed(kmir_kast, opts.start_symbol, opts.depth)
 
-    print(tools.kprint.kore_to_pretty(result))
+    print(kmir.kore_to_pretty(result))
 
 
 def _kmir_prove_rs(opts: ProveRSOpts) -> None:

kmir/src/kmir/build.py

@@ -4,19 +4,9 @@
 
 from pyk.kdist import kdist
 
-from .tools import Tools
-
 if TYPE_CHECKING:
     from typing import Final
 
 LLVM_DEF_DIR: Final = kdist.which('mir-semantics.llvm')
 LLVM_LIB_DIR: Final = kdist.which('mir-semantics.llvm-library')
 HASKELL_DEF_DIR: Final = kdist.which('mir-semantics.haskell')
-
-
-def llvm_semantics() -> Tools:
-    return Tools(LLVM_DEF_DIR)
-
-
-def haskell_semantics() -> Tools:
-    return Tools(HASKELL_DEF_DIR)

kmir/src/kmir/kmir.py

@@ -6,8 +6,9 @@
 
 from pyk.cli.utils import bug_report_arg
 from pyk.cterm import CTerm, cterm_symbolic
-from pyk.kast.inner import KApply, KInner, KSequence, Subst
+from pyk.kast.inner import KApply, KInner, KSequence, KSort, Subst
 from pyk.kast.manip import split_config_from
+from pyk.kast.prelude.string import stringToken
 from pyk.kcfg import KCFG
 from pyk.kcfg.explore import KCFGExplore
 from pyk.kcfg.semantics import DefaultSemantics
@@ -17,23 +18,24 @@
 from pyk.proof.reachability import APRProof, APRProver
 from pyk.proof.show import APRProofNodePrinter
 
+from .kparse import KParse
 from .parse.parser import Parser
 from .rust.cargo import cargo_get_smir_json
-from .tools import Tools
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
     from pathlib import Path
     from typing import Final
 
+    from pyk.kore.syntax import Pattern
     from pyk.utils import BugReport
 
     from .options import ProveRSOpts
 
 _LOGGER: Final = logging.getLogger(__name__)
 
 
-class KMIR(KProve, KRun):
+class KMIR(KProve, KRun, KParse):
     llvm_library_dir: Path | None
     bug_report: BugReport | None
 
@@ -43,6 +45,7 @@ def __init__(
         self.bug_report = bug_report_arg(bug_report) if bug_report is not None else None
         KProve.__init__(self, definition_dir, bug_report=self.bug_report)
         KRun.__init__(self, definition_dir, bug_report=self.bug_report)
+        KParse.__init__(self, definition_dir)
         self.llvm_library_dir = llvm_library_dir
 
     class Symbols:
@@ -59,11 +62,27 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:
         ) as cts:
             yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
 
+    def make_init_config(
+        self, parsed_smir: KInner, start_symbol: KInner | str = 'main', sort: str = 'GeneratedTopCell'
+    ) -> KInner:
+        if isinstance(start_symbol, str):
+            start_symbol = stringToken(start_symbol)
+
+        subst = Subst({'$PGM': parsed_smir, '$STARTSYM': start_symbol})
+        init_config = subst.apply(self.definition.init_config(KSort(sort)))
+        return init_config
+
+    def run_parsed(self, parsed_smir: KInner, start_symbol: KInner | str = 'main', depth: int | None = None) -> Pattern:
+        init_config = self.make_init_config(parsed_smir, start_symbol)
+        init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell'))
+        result = self.run_pattern(init_kore, depth=depth)
+
+        return result
+
     def apr_proof_from_kast(
         self, id: str, kmir_kast: KInner, sort: str = 'GeneratedTopCell', proof_dir: Path | None = None
     ) -> APRProof:
-        tools = Tools(self.definition_dir)
-        config = tools.make_init_config(kmir_kast, 'main', sort=sort)
+        config = self.make_init_config(kmir_kast, 'main', sort=sort)
         config_with_cell_vars, _ = split_config_from(config)
 
         lhs = CTerm(config)

kmir/src/kmir/kparse.py

@@ -2,30 +2,41 @@
 
 from pathlib import Path
 from subprocess import CalledProcessError
-from typing import TYPE_CHECKING
+from typing import TYPE_CHECKING, Callable, Iterable
 
 if TYPE_CHECKING:
     from subprocess import CompletedProcess
     from pyk.kore.syntax import Pattern
     from pyk.kast.inner import KInner
+    from pyk.kast.outer import KFlatModule
+    from pyk.kast.pretty import SymbolTable
+    from pyk.utils import BugReport
 
 from pyk.kore.parser import KoreParser
 from pyk.ktool.kprint import KPrint
 from pyk.utils import run_process
 
 
 class KParse(KPrint):
-    command: str
+    parser: str
 
     def __init__(
         self,
         definition_dir: Path,
+        use_directory: Path | None = None,
+        bug_report: BugReport | None = None,
+        extra_unparsing_modules: Iterable[KFlatModule] = (),
+        patch_symbol_table: Callable[[SymbolTable], None] | None = None,
         command: str = 'kparse',
     ):
         super().__init__(
             definition_dir,
+            use_directory=use_directory,
+            bug_report=bug_report,
+            extra_unparsing_modules=extra_unparsing_modules,
+            patch_symbol_table=patch_symbol_table,
         )
-        self.command = command
+        self.parser = command
 
     def parse_process(
         self,
@@ -38,7 +49,7 @@ def parse_process(
             ntf.flush()
 
             return _kparse(
-                command=self.command,
+                command=self.parser,
                 input_file=Path(ntf.name),
                 definition_dir=self.definition_dir,
                 sort=sort,

kmir/src/kmir/parse/__main__.py

@@ -2,8 +2,8 @@
 import sys
 from pathlib import Path
 
-from kmir.build import llvm_semantics
-
+from ..build import LLVM_DEF_DIR
+from ..kmir import KMIR
 from .parser import parse_json
 
 
@@ -17,13 +17,13 @@ def parse_args() -> argparse.Namespace:
 def main() -> None:
     sys.setrecursionlimit(10000000)
     args = parse_args()
-    tools = llvm_semantics()
+    kmir = KMIR(LLVM_DEF_DIR)
 
-    result = parse_json(tools.definition, Path(args.json), args.sort)
+    result = parse_json(kmir.definition, Path(args.json), args.sort)
 
     if result is None:
         print('Parse error!', file=sys.stderr)
         sys.exit(1)
 
     term, _ = result
-    print(tools.krun.pretty_print(term))
+    print(kmir.pretty_print(term))

kmir/src/kmir/testing/__init__.py

@@ -1 +1 @@
-from .fixtures import tools
+

kmir/src/kmir/testing/fixtures.py

@@ -1,20 +1,10 @@
 from __future__ import annotations
 
-from typing import TYPE_CHECKING
-
 import pytest
 
-from kmir.build import HASKELL_DEF_DIR, LLVM_LIB_DIR, llvm_semantics
+from kmir.build import HASKELL_DEF_DIR, LLVM_LIB_DIR
 from kmir.kmir import KMIR
 
-if TYPE_CHECKING:
-    from kmir.tools import Tools
-
-
-@pytest.fixture
-def tools() -> Tools:
-    return llvm_semantics()
-
 
 @pytest.fixture
 def kmir() -> KMIR: