Add parameter type_inference_mode to kompile (runtimeverification/pyk#767)

And use `--type-inference-mode checked` when kompiling using the test
fixtures.

---------

Co-authored-by: devops <devops@runtimeverification.com>

Author: 2 people

pyk/package/version

@@ -1 +1 @@
-0.1.540
+0.1.541

pyk/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. <contact@runtimeverification.com>",

pyk/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']
 

pyk/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]