diff --git a/package/version b/package/version index 2f3fb9d02..30b978323 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.540 +0.1.541 diff --git a/pyproject.toml b/pyproject.toml index 62db5aeac..8af4ce38b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.540" +version = "0.1.541" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/ktool/kompile.py b/src/pyk/ktool/kompile.py index 0a940f3e8..33107b4c1 100644 --- a/src/pyk/ktool/kompile.py +++ b/src/pyk/ktool/kompile.py @@ -30,12 +30,20 @@ def __init__(self, kompile_command: str): super().__init__(f'Kompile command not found: {str}') +class TypeInferenceMode(Enum): + Z3 = 'z3' + SIMPLESUB = 'simplesub' + CHECKED = 'checked' + DEFAULT = 'default' + + def kompile( main_file: str | Path, *, command: Iterable[str] = ('kompile',), output_dir: str | Path | None = None, temp_dir: str | Path | None = None, + type_inference_mode: str | TypeInferenceMode | None = None, debug: bool = False, verbose: bool = False, cwd: Path | None = None, @@ -48,6 +56,7 @@ def kompile( command=command, output_dir=output_dir, temp_dir=temp_dir, + type_inference_mode=type_inference_mode, debug=debug, verbose=verbose, cwd=cwd, @@ -115,6 +124,7 @@ def __call__( *, output_dir: str | Path | None = None, temp_dir: str | Path | None = None, + type_inference_mode: str | TypeInferenceMode | None = None, debug: bool = False, verbose: bool = False, cwd: Path | None = None, @@ -138,6 +148,10 @@ def __call__( temp_dir = Path(temp_dir) args += ['--temp-dir', str(temp_dir)] + if type_inference_mode is not None: + type_inference_mode = TypeInferenceMode(type_inference_mode) + args += ['--type-inference-mode', type_inference_mode.value] + if debug: args += ['--debug'] diff --git a/src/pyk/testing/_kompiler.py b/src/pyk/testing/_kompiler.py index 5ee125770..2b0893a80 100644 --- a/src/pyk/testing/_kompiler.py +++ b/src/pyk/testing/_kompiler.py @@ -11,7 +11,7 @@ from ..kllvm.importer import import_runtime from ..kore.pool import KoreServerPool from ..kore.rpc import BoosterServer, KoreClient, KoreServer -from ..ktool.kompile import DefinitionInfo, Kompile +from ..ktool.kompile import DefinitionInfo, Kompile, TypeInferenceMode from ..ktool.kprint import KPrint from ..ktool.kprove import KProve from ..ktool.krun import KRun @@ -43,7 +43,7 @@ def __call__(self, main_file: str | Path, **kwargs: Any) -> Path: kompile = Kompile.from_dict(kwargs) if kompile not in self._cache: output_dir = self._path / self._uid(kompile) - self._cache[kompile] = kompile(output_dir=output_dir) + self._cache[kompile] = kompile(output_dir=output_dir, type_inference_mode=TypeInferenceMode.CHECKED) return self._cache[kompile]