Merge remote-tracking branch 'origin/develop'

pyk/src/pyk/kast/markdown.py

@@ -40,7 +40,7 @@ def code_blocks(text: str) -> Iterator[CodeBlock]:
 
 def parse_tags(text: str) -> set[str]:
     def check_tag(tag: str) -> None:
-        if not (tag and all(c.isalnum() or c == '_' for c in tag)):
+        if not (tag and all(c.isalnum() or c in '_-' for c in tag)):
             raise ValueError(f'Invalid tag: {tag!r}')
 
     if not text:

pyk/src/pyk/kast/utils.py

@@ -43,11 +43,12 @@ def slurp_definitions(
     main_file: str | Path,
     *,
     include_dirs: Iterable[str | Path] = (),
-    md_selector: str = 'k',
+    md_selector: str | None = None,
     include_source: bool = True,
 ) -> dict[Path, Definition]:
     main_file = Path(main_file).resolve()
     _include_dirs = [Path(include_dir) for include_dir in include_dirs]
+    md_selector = md_selector or 'k'
 
     result: dict[Path, Definition] = {}
 

pyk/src/pyk/ktool/claim_loader.py

@@ -0,0 +1,121 @@
+from __future__ import annotations
+
+import json
+import logging
+from typing import TYPE_CHECKING, NamedTuple
+
+from ..kast.outer import KFlatModuleList
+from ..kast.utils import slurp_definitions
+from ..utils import hash_str
+from .claim_index import ClaimIndex
+
+if TYPE_CHECKING:
+    from collections.abc import Iterable, Mapping
+    from pathlib import Path
+    from typing import Any, Final
+
+    from ..kast.outer import KClaim
+    from . import TypeInferenceMode
+    from .kprove import KProve
+
+
+_LOGGER: Final = logging.getLogger(__name__)
+
+
+class ClaimLoader:
+    """Load and cache spec files as JSON."""
+
+    _kprove: KProve
+
+    def __init__(self, kprove: KProve):
+        self._kprove = kprove
+
+    def load_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,
+        include_dependencies: bool = True,
+        type_inference_mode: TypeInferenceMode | None = None,
+    ) -> list[KClaim]:
+        """Attempt to load a spec from JSON, write file on cache miss.
+
+        Args:
+            spec_file: Spec file to load.
+            spec_module_name (optional): Spec module to load.
+            include_dirs (optional): Includes.
+            md_selector (optional): Selector expression for Markdown tags.
+            claim_labels (optional): Claim labels to include in the result.
+            exclude_claim_labels (optional): Claim labels to exclude from the result.
+            include_dependencies (optional): If ``True``, claim dependencies are transitively included.
+            type_inference_mode (optional): Type inference mode.
+        """
+        _LOGGER.info(f'Loading spec file: {spec_file}')
+
+        digest = self._digest(spec_file, include_dirs=include_dirs, md_selector=md_selector)
+        _LOGGER.info(f'Calculated digest: {digest}')
+
+        claim_file = spec_file.with_suffix('.json')
+
+        cache_hit = False
+        if claim_file.exists():
+            _LOGGER.info(f'Loading claim file: {claim_file}')
+            module_list, loaded_digest = _ClaimModuleList.from_dict(json.loads(claim_file.read_text()))
+            cache_hit = digest == loaded_digest
+
+        if not cache_hit:
+            _LOGGER.info('Generating claim modules')
+            module_list = self._kprove.get_claim_modules(
+                spec_file=spec_file,
+                spec_module_name=spec_module_name,
+                include_dirs=include_dirs,
+                md_selector=md_selector,
+                type_inference_mode=type_inference_mode,
+            )
+            claim_module_list = _ClaimModuleList(module_list=module_list, digest=digest)
+            _LOGGER.info(f'Writing claim file: {claim_file}')
+            claim_file.write_text(json.dumps(claim_module_list.to_dict()))
+
+        claim_index = ClaimIndex.from_module_list(module_list)
+
+        labels = claim_index.labels(
+            include=claim_labels,
+            exclude=exclude_claim_labels,
+            with_depends=include_dependencies,
+        )
+
+        return [claim_index[label] for label in labels]
+
+    @staticmethod
+    def _digest(spec_file: Path, *, include_dirs: Iterable[Path], md_selector: str | None) -> str:
+        from .utils import K_DISTRIBUTION
+
+        definitions = slurp_definitions(
+            spec_file,
+            include_dirs=list(include_dirs) + ([K_DISTRIBUTION.builtin_dir] if K_DISTRIBUTION else []),
+            md_selector=md_selector,
+        )
+        definitions = {key: definitions[key] for key in sorted(definitions)}
+        return hash_str(definitions)
+
+
+class _ClaimModuleList(NamedTuple):
+    module_list: KFlatModuleList
+    digest: str
+
+    @staticmethod
+    def from_dict(dct: Mapping[str, Any]) -> _ClaimModuleList:
+        return _ClaimModuleList(
+            module_list=KFlatModuleList.from_dict(dct['moduleList']),
+            digest=dct['digest'],
+        )
+
+    def to_dict(self) -> dict[str, Any]:
+        return {
+            'moduleList': self.module_list.to_dict(),
+            'digest': self.digest,
+        }

pyk/src/pyk/ktool/utils.py

@@ -0,0 +1,47 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+from pathlib import Path
+from typing import TYPE_CHECKING, final
+
+from ..utils import run_process_2
+
+if TYPE_CHECKING:
+    from typing import Final
+
+
+@final
+@dataclass(frozen=True)
+class KDistribution:
+    """Represent the path to the K distribution.
+
+    Attributes:
+        path: Path to the K distribution.
+    """
+
+    path: Path
+
+    @property
+    def builtin_dir(self) -> Path:
+        """The path to the `builtin` directory."""
+        return self.path / 'include/kframework/builtin'
+
+    @staticmethod
+    def create() -> KDistribution | None:
+        """Instantiate the class based on the path to the `kompile` binary."""
+        kompile_bin = KDistribution._which_kompile()
+        if kompile_bin is None:
+            return None
+        return KDistribution(kompile_bin.parents[1])
+
+    @staticmethod
+    def _which_kompile() -> Path | None:
+        proc_res = run_process_2(['which', 'kompile'])
+        if proc_res.returncode:
+            return None
+        res = Path(proc_res.stdout.rstrip())
+        assert res.is_file()
+        return res
+
+
+K_DISTRIBUTION: Final = KDistribution.create()

pyk/src/pyk/utils.py

@@ -340,7 +340,7 @@ def is_hexstring(x: str) -> bool:
 # Hashes
 
 
-def hash_str(x: Any) -> str:
+def hash_str(x: object) -> str:
     hash = hashlib.sha256()
     hash.update(str(x).encode('utf-8'))
     return str(hash.hexdigest())