Refactor TestEmitJsonSpec (#490)

Uses the `kprove` fixture to generate the JSON spec in a temporary
directory.

---------

Co-authored-by: devops <[email protected]>

Author: tothtamas28

package/version

@@ -1 +1 @@
-0.1.328
+0.1.329

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.328"
+version = "0.1.329"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/ktool/kprove.py

@@ -308,15 +308,13 @@ def prove_cterm(
         next_states = [mlAnd([constraint_subst.unapply(ns), constraint_subst.ml_pred]) for ns in next_states]
         return next_states if len(next_states) > 0 else [mlTop()]
 
-    def get_claims(
+    def get_claim_modules(
         self,
         spec_file: Path,
         spec_module_name: str | None = None,
         include_dirs: Iterable[Path] = (),
         md_selector: str | None = None,
-        claim_labels: Iterable[str] | None = None,
-        exclude_claim_labels: Iterable[str] | None = None,
-    ) -> list[KClaim]:
+    ) -> KFlatModuleList:
         with self._temp_file() as ntf:
             self.prove(
                 spec_file,
@@ -326,10 +324,25 @@ def get_claims(
                 dry_run=True,
                 args=['--emit-json-spec', ntf.name],
             )
-            flat_module_list = kast_term(json.loads(Path(ntf.name).read_text()), KFlatModuleList)
+            return kast_term(json.loads(Path(ntf.name).read_text()), KFlatModuleList)
 
-        all_claims = {c.label: c for m in flat_module_list.modules for c in m.claims}
+    def get_claims(
+        self,
+        spec_file: Path,
+        spec_module_name: str | None = None,
+        include_dirs: Iterable[Path] = (),
+        md_selector: str | None = None,
+        claim_labels: Iterable[str] | None = None,
+        exclude_claim_labels: Iterable[str] | None = None,
+    ) -> list[KClaim]:
+        flat_module_list = self.get_claim_modules(
+            spec_file=spec_file,
+            spec_module_name=spec_module_name,
+            include_dirs=include_dirs,
+            md_selector=md_selector,
+        )
 
+        all_claims = {c.label: c for m in flat_module_list.modules for c in m.claims}
         unfound_labels = []
         claim_labels = list(all_claims.keys()) if claim_labels is None else claim_labels
         exclude_claim_labels = [] if exclude_claim_labels is None else exclude_claim_labels

src/tests/integration/kprove/test_emit_json_spec.py

@@ -1,17 +1,14 @@
 from __future__ import annotations
 
-import json
 from pathlib import Path
 from typing import TYPE_CHECKING
 
 import pytest
 
-from pyk.kast import kast_term
 from pyk.kast.inner import EMPTY_ATT
 from pyk.kast.manip import remove_generated_cells
-from pyk.kast.outer import KDefinition, KFlatModuleList, KRequire
+from pyk.kast.outer import KDefinition, KRequire
 from pyk.kast.pretty import paren
-from pyk.ktool.kprove import _kprove
 from pyk.prelude.ml import is_top
 from pyk.testing import KProveTest
 
@@ -31,12 +28,10 @@ class TestEmitJsonSpec(KProveTest):
     def _update_symbol_table(symbol_table: SymbolTable) -> None:
         symbol_table['_+Int_'] = paren(symbol_table['_+Int_'])
 
-    @pytest.fixture(scope='class')
-    def spec_module(self, definition_dir: Path) -> KFlatModule:
+    @pytest.fixture
+    def spec_module(self, kprove: KProve) -> KFlatModule:
         spec_file = K_FILES / 'looping-spec.k'
-        spec_json_file = definition_dir / 'looping-spec.json'
-        _kprove(spec_file, kompiled_dir=definition_dir, emit_json_spec=spec_json_file, dry_run=True)
-        kfml = kast_term(json.loads(spec_json_file.read_text()), KFlatModuleList)
+        kfml = kprove.get_claim_modules(spec_file)
         module = kfml.modules[0]
         claim = module.claims[0]
         claim = claim.let(body=remove_generated_cells(claim.body), att=EMPTY_ATT)