Change pyk.ktool to utilize the --definition flag

pyk/pyk-tests/Makefile

@@ -23,7 +23,6 @@ clean:
 
 update-results: CHECK=cp
 update-results: test
-kompile: $(llvm_imp_kompiled) $(haskell_imp_kompiled)
 
 
 # Tests
@@ -34,31 +33,26 @@ test: test-kpyk
 
 test-kpyk: test-kpyk-graphviz test-kpyk-minimize-term
 
-test-kpyk-graphviz: imp-verification/haskell.kompiled
-	$(PYK) definitions/imp-verification/haskell/imp-verification-kompiled graph-imports
-	cat definitions/imp-verification/haskell/imp-verification-kompiled/import-graph | tr -cd '[:alnum:]\n' | grep . | tr '[:lower:]' '[:upper:]' | sort > import-graph.sorted
+test-kpyk-graphviz: imp-verification.kompiled
+	$(PYK) definitions/imp-verification graph-imports
+	cat definitions/imp-verification/import-graph | tr -cd '[:alnum:]\n' | grep . | tr '[:lower:]' '[:upper:]' | sort > import-graph.sorted
 	$(CHECK) import-graph.sorted imp-import-graph.expected
 
-test-kpyk-minimize-term: imp-verification/haskell.kompiled
-	$(PYK) definitions/imp-verification/haskell/imp-verification-kompiled prove ../k-files/imp-verification.k ../k-files/imp-unproveable-spec.k IMP-UNPROVEABLE-SPEC \
-	    | $(PYK) definitions/imp-verification/haskell/imp-verification-kompiled print /dev/stdin > imp-unproveable-spec.k.out
+test-kpyk-minimize-term: imp-verification.kompiled
+	$(PYK) definitions/imp-verification prove ../k-files/imp-verification.k ../k-files/imp-unproveable-spec.k IMP-UNPROVEABLE-SPEC \
+	    | $(PYK) definitions/imp-verification print /dev/stdin > imp-unproveable-spec.k.out
 	$(CHECK) imp-unproveable-spec.k.out imp-unproveable-spec.k.expected
 
 
 ## definitions to build ahead of time
 
-KOMPILE_BACKEND  = haskell
-KOMPILE_COVERAGE =
-KOMPILE_OPTS     =
-
-definitions := imp-verification/haskell
+definitions := imp-verification
 
 build-definitions: $(definitions:=.kompiled)
 
 %.kompiled:
-	$(KOMPILE) --directory definitions/$*    \
-	    -I k-files                           \
-	    --backend $(KOMPILE_BACKEND)         \
-	    --emit-json $(KOMPILE_COVERAGE)      \
-	    $(KOMPILE_OPTS)                      \
-	    ../k-files/$(patsubst %/,%,$(dir $@)).k
+	$(KOMPILE) ../k-files/$*.k             \
+	    --output-definition definitions/$* \
+	    --backend haskell                  \
+	    -I k-files                         \
+	    --emit-json

pyk/src/pyk/integration_tests/kompiled_test.py

@@ -32,7 +32,5 @@ def setUp(self):
             emit_json=self.KOMPILE_EMIT_JSON,
         )
 
-        self.assertTrue(self.kompiled_dir.is_dir())
-
     def tearDown(self):
         shutil.rmtree(self.kompiled_dir)

pyk/src/pyk/integration_tests/test_configuration.py

@@ -24,10 +24,10 @@
 class ConfigurationTest(KompiledTest, ABC):
     KOMPILE_MAIN_FILE = 'k-files/imp.k'
     KOMPILE_BACKEND = KompileBackend.HASKELL
-    KOMPILE_OUTPUT_DIR = 'definitions/imp/haskell'
+    KOMPILE_OUTPUT_DIR = 'definitions/imp'
     KOMPILE_EMIT_JSON = True
 
-    COMPILED_JSON_PATH = 'definitions/imp/haskell/imp-kompiled/compiled.json'
+    COMPILED_JSON_PATH = 'definitions/imp/compiled.json'
     MODULE_NAME = 'IMP-VERIFICATION'
 
     K_CELL = KApply('<k>', [KSequence([KVariable('S1'), KVariable('_DotVar0')])])

pyk/src/pyk/integration_tests/test_defn.py

@@ -16,7 +16,7 @@
 class DefnTest(KProveTest):
     KOMPILE_MAIN_FILE = 'k-files/imp-verification.k'
     KOMPILE_BACKEND = KompileBackend.HASKELL
-    KOMPILE_OUTPUT_DIR = 'definitions/imp-verification/haskell'
+    KOMPILE_OUTPUT_DIR = 'definitions/imp-verification'
     KOMPILE_EMIT_JSON = True
 
     KPROVE_USE_DIR = '.defn-test'

pyk/src/pyk/integration_tests/test_emit_json_spec.py

@@ -12,21 +12,20 @@ class EmitJsonSpecTest(KProveTest):
 
     KOMPILE_MAIN_FILE = f'k-files/{MAIN_FILE_NAME}'
     KOMPILE_BACKEND = KompileBackend.HASKELL
-    KOMPILE_OUTPUT_DIR = 'definitions/imp-verification/haskell'
+    KOMPILE_OUTPUT_DIR = 'definitions/imp-verification'
     KOMPILE_EMIT_JSON = True
 
     KPROVE_USE_DIR = '.emit-json-spec-test'
 
     SPEC_FILE = 'k-files/looping-spec.k'
-    SPEC_JSON_FILE = 'definitions/imp-verification/haskell/looping-spec.json'
+    SPEC_JSON_FILE = 'definitions/imp-verification/looping-spec.json'
 
     def setUp(self):
         super().setUp()
 
         spec_file = Path(self.SPEC_FILE)
-        directory = Path(self.KOMPILE_OUTPUT_DIR)
         emit_json_spec = Path(self.SPEC_JSON_FILE)
-        kprovex(spec_file, directory=directory, emit_json_spec=emit_json_spec, dry_run=True)
+        kprovex(spec_file, kompiled_dir=self.KOMPILE_OUTPUT_DIR, emit_json_spec=emit_json_spec, dry_run=True)
 
         with open(self.SPEC_JSON_FILE, 'r') as spec_file:
             module = KAst.from_dict(json.load(spec_file)['term'])

pyk/src/pyk/integration_tests/test_kompile.py

@@ -5,7 +5,7 @@
 class SimpleKompileTest(KompiledTest):
     KOMPILE_MAIN_FILE = 'k-files/imp.k'
     KOMPILE_BACKEND = KompileBackend.HASKELL
-    KOMPILE_OUTPUT_DIR = 'definitions/imp/haskell'
+    KOMPILE_OUTPUT_DIR = 'definitions/imp'
     KOMPILE_EMIT_JSON = True
 
     def test(self):

pyk/src/pyk/integration_tests/test_parse_kast.py

@@ -21,10 +21,10 @@ def setUp(self):
 class KSortSynonymTest(ParseKAstTest):
     KOMPILE_MAIN_FILE = 'k-files/sort-synonym.k'
     KOMPILE_BACKEND = KompileBackend.HASKELL
-    KOMPILE_OUTPUT_DIR = 'definitions/sort-synonym/haskell'
+    KOMPILE_OUTPUT_DIR = 'definitions/sort-synonym'
     KOMPILE_EMIT_JSON = True
 
-    COMPILED_JSON_PATH = 'definitions/sort-synonym/haskell/sort-synonym-kompiled/compiled.json'
+    COMPILED_JSON_PATH = 'definitions/sort-synonym/compiled.json'
     MODULE_NAME = 'SORT-SYNONYM-SYNTAX'
 
     def test(self):
@@ -36,10 +36,10 @@ def test(self):
 class KAsTest(ParseKAstTest):
     KOMPILE_MAIN_FILE = 'k-files/contextual-function.k'
     KOMPILE_BACKEND = KompileBackend.HASKELL
-    KOMPILE_OUTPUT_DIR = 'definitions/contextual-function/haskell'
+    KOMPILE_OUTPUT_DIR = 'definitions/contextual-function'
     KOMPILE_EMIT_JSON = True
 
-    COMPILED_JSON_PATH = 'definitions/contextual-function/haskell/contextual-function-kompiled/compiled.json'
+    COMPILED_JSON_PATH = 'definitions/contextual-function/compiled.json'
     MODULE_NAME = 'CONTEXTUAL-FUNCTION'
 
     def test(self):

pyk/src/pyk/integration_tests/test_proofs.py

@@ -6,7 +6,7 @@
 class SimpleProofTest(KProveTest):
     KOMPILE_MAIN_FILE = 'k-files/simple-proofs.k'
     KOMPILE_BACKEND = KompileBackend.HASKELL
-    KOMPILE_OUTPUT_DIR = 'definitions/simple-proofs/haskell'
+    KOMPILE_OUTPUT_DIR = 'definitions/simple-proofs'
     KOMPILE_EMIT_JSON = True
 
     KPROVE_USE_DIR = '.simple-proof-test'

pyk/src/pyk/ktool/kompile.py

@@ -33,7 +33,9 @@ def kompile(
     if proc_res.returncode:
         raise RuntimeError(f'Kompilation failed for: {main_file}')
 
-    return _kompiled_dir(main_file, output_dir)
+    kompiled_dir = _kompiled_dir(main_file, output_dir)
+    assert kompiled_dir.is_dir()
+    return kompiled_dir
 
 
 def _build_arg_list(
@@ -49,7 +51,7 @@ def _build_arg_list(
         args += ['--backend', backend.value]
 
     if output_dir:
-        args += ['--directory', str(output_dir)]
+        args += ['--output-definition', str(output_dir)]
 
     for include_dir in include_dirs:
         args += ['-I', str(include_dir)]
@@ -67,9 +69,7 @@ def _kompile(main_file: str, *args: str) -> CompletedProcess:
 
 
 def _kompiled_dir(main_file: Path, output_dir: Optional[Path] = None) -> Path:
-    kompiled_dir_name = main_file.stem + '-kompiled'
-
-    if not output_dir:
-        output_dir = main_file.parent
+    if output_dir:
+        return output_dir
 
-    return output_dir / kompiled_dir_name
+    return Path(main_file.stem + '-kompiled')

pyk/src/pyk/ktool/kprove.py

@@ -28,7 +28,7 @@
 def kprovex(
     spec_file: Path,
     *,
-    directory: Optional[Path] = None,
+    kompiled_dir: Optional[Path] = None,
     include_dirs: Iterable[Path] = (),
     emit_json_spec: Optional[Path] = None,
     dry_run=False,
@@ -39,7 +39,7 @@ def kprovex(
         check_dir_path(include_dir)
 
     args = _build_arg_list(
-        directory=directory,
+        kompiled_dir=kompiled_dir,
         include_dirs=include_dirs,
         dry_run=dry_run,
         emit_json_spec=emit_json_spec,
@@ -53,15 +53,15 @@ def kprovex(
 
 def _build_arg_list(
     *,
-    directory: Optional[Path],
+    kompiled_dir: Optional[Path],
     include_dirs: Iterable[Path],
     emit_json_spec: Optional[Path],
     dry_run: bool,
 ) -> List[str]:
     args = []
 
-    if directory:
-        args += ['--directory', str(directory)]
+    if kompiled_dir:
+        args += ['--definition', str(kompiled_dir)]
 
     for include_dir in include_dirs:
         args += ['-I', str(include_dir)]
@@ -110,7 +110,7 @@ def prove(self, specFile, specModuleName, args=[], haskellArgs=[], logAxiomsFile
         haskellLogArgs = ['--log', str(logFile), '--log-format', 'oneline', '--log-entries', 'DebugTransition']
         command = [c for c in self.prover]
         command += [str(specFile)]
-        command += ['--directory', str(self.directory), '-I', str(self.directory), '--spec-module', specModuleName, '--output', 'json']
+        command += ['--definition', str(self.kompiledDirectory), '-I', str(self.directory), '--spec-module', specModuleName, '--output', 'json']
         command += [c for c in self.proverArgs]
         command += args
         commandEnv = os.environ.copy()