diff --git a/pyk/src/pyk/kast/markdown.py b/pyk/src/pyk/kast/markdown.py index b0f132ba5ac..9736ea91672 100644 --- a/pyk/src/pyk/kast/markdown.py +++ b/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: diff --git a/pyk/src/pyk/kast/utils.py b/pyk/src/pyk/kast/utils.py index 3795c7a2259..dd2677520e1 100644 --- a/pyk/src/pyk/kast/utils.py +++ b/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] = {} diff --git a/pyk/src/pyk/ktool/claim_loader.py b/pyk/src/pyk/ktool/claim_loader.py new file mode 100644 index 00000000000..451bccff393 --- /dev/null +++ b/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, + } diff --git a/pyk/src/pyk/ktool/utils.py b/pyk/src/pyk/ktool/utils.py new file mode 100644 index 00000000000..180e5dd71b4 --- /dev/null +++ b/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() diff --git a/pyk/src/pyk/utils.py b/pyk/src/pyk/utils.py index bea79e8baa3..04c650482e2 100644 --- a/pyk/src/pyk/utils.py +++ b/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())