Move distribution handling inside KImp (#33)

The goal is to make instantiation of `KImp` as simple as possible. This
makes REPL use more convenient.

README.md

@@ -11,23 +11,40 @@ KIMP consists of two major components:
 
 ## Trying it out in `docker` (EASY)
 
-We have prepared a Docker image that allows both using `kimp` as-is and hacking on it.
+The project defines a Docker image that allows both using `kimp` as-is and hacking on it.
 
 First off, clone the project and step into its directory:
 
 ```
 git clone https://github.com/runtimeverification/imp-semantics
 cd imp-semantics
-git checkout bob2024
 ```
 
-Use the following to start a container with an interactive shell:
+Then, build the image:
 
 ```
-docker run --rm -it -v "$PWD":/home/k-user/workspace -u $(id -u):$(id -g) geo2a/bob24:latest /bin/bash
+make docker TAG=imp-semantics:latest
 ```
 
-This command will download the docker image and mount the current working directory under `~/workspace`, ensuring you can work on the examples and have them transparently available in the container.
+Run the following command to start a container with an interactive shell:
+
+```
+docker run --rm -it imp-semantics:latest /bin/bash
+```
+
+The `examples` folder, as well as a test script `smoke-tests.sh` is already copied into the workspace.
+You can run the tests with:
+
+```
+./smoke-test.sh
+```
+
+To work with files from the host, run the countainer with a volume mounted.
+For example, the following command starts the container and mounts the current working directory under `~/workspace`, ensuring you can work on the examples and have them transparently available in the container.
+
+```
+docker run --rm -it -v "$PWD":/home/k-user/workspace -u $(id -u):$(id -g) imp-semantics:latest /bin/bash
+```
 
 If everything is up and running, feel free to jump straight to the **Usage** section below. If you don't want to use `docker`, read the next section to build `kimp` manually.
 

kimp/src/kimp/__init__.py

@@ -0,0 +1 @@
+from .kimp import KImp

kimp/src/kimp/__main__.py

@@ -1,54 +1,21 @@
 from __future__ import annotations
 
 import logging
-import os
 from argparse import ArgumentParser
-from pathlib import Path
 from typing import TYPE_CHECKING, Any, Final
 
-from pyk.cli.utils import dir_path, file_path
+from pyk.cli.utils import file_path
 
 from .kimp import KImp
 
 if TYPE_CHECKING:
     from argparse import Namespace
+    from pathlib import Path
 
 _LOGGER: Final = logging.getLogger(__name__)
 _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
 
 
-def find_target(target: str) -> Path:
-    """
-    Find a `kdist` target:
-    * if KIMP_${target.upper}_DIR is set --- use that
-    * otherwise ask `kdist`
-    """
-
-    env_target_dir = os.environ.get(f'KIMP_{target.upper()}_DIR')
-    if env_target_dir:
-        path = Path(env_target_dir).resolve()
-        _LOGGER.info(f'Using target at {path}')
-        return path
-    else:
-        from pyk.kdist import kdist
-
-        return kdist.which(f'imp-semantics.{target}')
-
-
-def find_k_src_dir() -> Path:
-    """
-    A heuristic way to find the the k-src dir with the K sources is located:
-    * if KIMP_K_SRC environment variable is set --- use that
-    * otherwise, use ./k-src and hope it works
-    """
-    ksrc_dir_str = os.environ.get('KIMP_K_SRC')
-    if ksrc_dir_str is not None:
-        ksrc_dir = Path(ksrc_dir_str).resolve()
-    else:
-        ksrc_dir = Path('./k-src')
-    return ksrc_dir
-
-
 def main() -> None:
     parser = create_argument_parser()
     args = parser.parse_args()
@@ -65,12 +32,10 @@ def main() -> None:
 def exec_run(
     input_file: Path,
     env_list: list[list[tuple[str, int]]] | None,
-    definition_dir: Path | None,
     depth: int | None = None,
     **kwargs: Any,
 ) -> None:
-    definition_dir = find_target('llvm') if definition_dir is None else definition_dir
-    kimp = KImp(definition_dir, definition_dir)
+    kimp = KImp()
     pgm = input_file.read_text()
     env = {var: val for assign in env_list for var, val in assign} if env_list else {}
     pattern = kimp.pattern(pgm=pgm, env=env)
@@ -79,64 +44,40 @@ def exec_run(
 
 
 def exec_prove(
-    definition_dir: str,
     spec_file: str,
     spec_module: str,
     claim_id: str,
     max_iterations: int,
     max_depth: int,
-    ignore_return_code: bool = False,
     reinit: bool = False,
     **kwargs: Any,
 ) -> None:
-    if definition_dir is None:
-        definition_dir = str(find_target('haskell'))
-    k_src_dir = str(find_target('source') / 'imp-semantics')
-
-    kimp = KImp(definition_dir, definition_dir)
-
-    try:
-        kimp.prove(
-            spec_file=spec_file,
-            spec_module=spec_module,
-            claim_id=claim_id,
-            max_iterations=max_iterations,
-            max_depth=max_depth,
-            includes=[k_src_dir],
-            reinit=reinit,
-        )
-    except ValueError as err:
-        _LOGGER.critical(err.args)
-        raise
-    except RuntimeError as err:
-        if ignore_return_code:
-            msg, stdout, stderr = err.args
-            print(stdout)
-            print(stderr)
-            print(msg)
-        else:
-            raise
+    kimp = KImp()
+    kimp.prove(
+        spec_file=spec_file,
+        spec_module=spec_module,
+        claim_id=claim_id,
+        max_iterations=max_iterations,
+        max_depth=max_depth,
+        reinit=reinit,
+    )
 
 
 def exec_show(
-    definition_dir: str,
     spec_module: str,
     claim_id: str,
     **kwargs: Any,
 ) -> None:
-    definition_dir = str(find_target('haskell'))
-    kimp = KImp(definition_dir, definition_dir)
+    kimp = KImp()
     kimp.show_kcfg(spec_module, claim_id)
 
 
 def exec_view(
-    definition_dir: str,
     spec_module: str,
     claim_id: str,
     **kwargs: Any,
 ) -> None:
-    definition_dir = str(find_target('haskell'))
-    kimp = KImp(definition_dir, definition_dir)
+    kimp = KImp()
     kimp.view_kcfg(spec_module, claim_id)
 
 
@@ -145,12 +86,6 @@ def create_argument_parser() -> ArgumentParser:
     shared_args = ArgumentParser(add_help=False)
     shared_args.add_argument('--verbose', '-v', default=False, action='store_true', help='Verbose output.')
     shared_args.add_argument('--debug', default=False, action='store_true', help='Debug output.')
-    shared_args.add_argument(
-        '--definition',
-        dest='definition_dir',
-        type=dir_path,
-        help='Path to compiled K definition to use.',
-    )
 
     # args shared by proof/prover/kcfg commands
     spec_file_shared_args = ArgumentParser(add_help=False)

kimp/src/kimp/kimp.py

@@ -28,7 +28,7 @@
 from pyk.utils import single
 
 if TYPE_CHECKING:
-    from collections.abc import Iterable, Iterator, Mapping
+    from collections.abc import Callable, Iterable, Iterator, Mapping
     from typing import Final
 
     from pyk.cterm.cterm import CTerm
@@ -85,36 +85,81 @@ def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool:
 
 @final
 @dataclass(frozen=True)
-class KImp:
+class ImpDist:
+    source_dir: Path
     llvm_dir: Path
     haskell_dir: Path
-    proof_dir: Path
 
-    def __init__(self, llvm_dir: str | Path, haskell_dir: str | Path):
+    def __init__(self, *, source_dir: str | Path, llvm_dir: str | Path, haskell_dir: str | Path):
+        source_dir = Path(source_dir)
+        check_dir_path(source_dir)
+
         llvm_dir = Path(llvm_dir)
         check_dir_path(llvm_dir)
 
         haskell_dir = Path(haskell_dir)
         check_dir_path(haskell_dir)
 
+        object.__setattr__(self, 'source_dir', source_dir)
+        object.__setattr__(self, 'llvm_dir', llvm_dir)
+        object.__setattr__(self, 'haskell_dir', haskell_dir)
+
+    @staticmethod
+    def load() -> ImpDist:
+        return ImpDist(
+            source_dir=ImpDist._find('source'),
+            llvm_dir=ImpDist._find('llvm'),
+            haskell_dir=ImpDist._find('haskell'),
+        )
+
+    @staticmethod
+    def _find(target: str) -> Path:
+        """
+        Find a `kdist` target:
+        * if KIMP_${target.upper}_DIR is set --- use that
+        * otherwise ask `kdist`
+        """
+
+        from os import getenv
+
+        from pyk.kdist import kdist
+
+        env_dir = getenv(f'KIMP_{target.upper()}_DIR')
+        if env_dir:
+            path = Path(env_dir)
+            check_dir_path(path)
+            _LOGGER.info(f'Using target at {path}')
+            return path
+
+        return kdist.get(f'imp-semantics.{target}')
+
+
+@final
+@dataclass(frozen=True)
+class KImp:
+    dist: ImpDist
+    proof_dir: Path
+
+    def __init__(self) -> None:
+        dist = ImpDist.load()
+
         proof_dir = Path('.') / '.kimp' / 'proofs'
         proof_dir.mkdir(exist_ok=True, parents=True)
 
-        object.__setattr__(self, 'llvm_dir', llvm_dir)
-        object.__setattr__(self, 'haskell_dir', haskell_dir)
+        object.__setattr__(self, 'dist', dist)
         object.__setattr__(self, 'proof_dir', proof_dir)
 
     @cached_property
     def definition(self) -> KDefinition:
-        return read_kast_definition(self.llvm_dir / 'compiled.json')
+        return read_kast_definition(self.dist.llvm_dir / 'compiled.json')
 
     @cached_property
     def format(self) -> Formatter:
         return Formatter(self.definition)
 
     @cached_property
     def kprove(self) -> KProve:
-        return KProve(definition_dir=self.haskell_dir, use_directory=self.proof_dir)
+        return KProve(definition_dir=self.dist.haskell_dir, use_directory=self.proof_dir)
 
     def run(
         self,
@@ -124,7 +169,7 @@ def run(
     ) -> Pattern:
         from pyk.ktool.krun import llvm_interpret
 
-        return llvm_interpret(definition_dir=self.llvm_dir, pattern=pattern, depth=depth)
+        return llvm_interpret(definition_dir=self.dist.llvm_dir, pattern=pattern, depth=depth)
 
     def pattern(self, *, pgm: str, env: Mapping[str, int]) -> Pattern:
         from pyk.kore.prelude import ID, INT, SORT_K_ITEM, inj, map_pattern, top_cell_initializer
@@ -151,7 +196,7 @@ def parse(self, pgm: str) -> Pattern:
         from pyk.kore.parser import KoreParser
         from pyk.utils import run_process_2
 
-        parser = self.llvm_dir / 'parser_PGM'
+        parser = self.dist.llvm_dir / 'parser_PGM'
         args = [str(parser), '/dev/stdin']
 
         kore_text = run_process_2(args, input=pgm).stdout
@@ -160,22 +205,48 @@ def parse(self, pgm: str) -> Pattern:
     def pretty(self, pattern: Pattern, color: bool | None = None) -> str:
         from pyk.kore.tools import kore_print
 
-        return kore_print(pattern, definition_dir=self.llvm_dir, color=bool(color))
+        return kore_print(pattern, definition_dir=self.dist.llvm_dir, color=bool(color))
+
+    def debug(self, pattern: Pattern) -> Callable[[int | None], None]:
+        """Return a closure that enables step-by-step debugging in a REPL.
+
+        Each call to the function pretty-prints the resulting configuration.
+
+        Example:
+            step = KImp().debug(pattern)
+            step()            # Run a single step
+            step(1)           # Run a single step
+            step(0)           # Just print the current configuration
+            step(bound=None)  # Run to completion
+        """
+
+        def step(bound: int | None = 1) -> None:
+            nonlocal pattern
+            pattern = self.run(pattern, depth=bound)
+            print(self.pretty(pattern, color=True))
+
+        return step
 
     def prove(
         self,
+        *,
         spec_file: str,
         spec_module: str,
-        includes: Iterable[str],
         claim_id: str,
         max_iterations: int,
         max_depth: int,
         reinit: bool,
+        includes: Iterable[str | Path] | None = None,
     ) -> None:
-        include_dirs = [Path(include) for include in includes]
+        include_dirs = [self.dist.source_dir / 'imp-semantics'] + (
+            [Path(include) for include in includes] if includes is not None else []
+        )
 
         claims = ClaimLoader(self.kprove).load_claims(
-            Path(spec_file), spec_module_name=spec_module, claim_labels=[claim_id], include_dirs=include_dirs
+            Path(spec_file),
+            spec_module_name=spec_module,
+            claim_labels=[claim_id],
+            include_dirs=include_dirs,
         )
         claim = single(claims)
         spec_label = f'{spec_module}.{claim_id}'