Merge branch 'master' into cterm-free-vars

Author: ehildenb

deps/k_release

@@ -1 +1 @@
-6.3.64
+6.3.66

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.746'
-release = '0.1.746'
+version = '0.1.750'
+release = '0.1.750'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.746
+0.1.750

pyproject.toml

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

regression-new/checkWarns/singletonOverload.k.out

@@ -8,6 +8,6 @@
 	Location(10,19,10,54)
 	10 |	                | Exp  "." Id [unused, overload(_._)]
 	   .	                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-[Error] Compiler: Had 2 structural errors.
+[Error] Compiler: Had 2 errors after compilation.
 [ERROR] Running process failed with returncode 113:
     kompile singletonOverload.k --md-selector k --emit-json --warnings all -w2e --no-exc-wrap --backend haskell --output-definition singletonOverload-kompiled --type-inference-mode checked

src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.3.64'
+K_VERSION: Final = '6.3.66'

src/pyk/kast/outer.py

@@ -11,7 +11,7 @@
 from enum import Enum
 from functools import cached_property
 from itertools import pairwise, product
-from typing import TYPE_CHECKING, final
+from typing import TYPE_CHECKING, final, overload
 
 from ..prelude.kbool import TRUE
 from ..prelude.ml import ML_QUANTIFIERS
@@ -34,10 +34,11 @@
 from .kast import kast_term
 
 if TYPE_CHECKING:
-    from collections.abc import Iterator, Mapping
+    from collections.abc import Callable, Iterator, Mapping
     from os import PathLike
     from typing import Any, Final, TypeVar
 
+    S = TypeVar('S', bound='KSentence')
     RL = TypeVar('RL', bound='KRuleLike')
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -900,6 +901,18 @@ def claims(self) -> tuple[KClaim, ...]:
     def sentence_by_unique_id(self) -> dict[str, KSentence]:
         return {sent.unique_id: sent for sent in self.sentences if sent.unique_id is not None}
 
+    @overload
+    def map_sentences(self, f: Callable[[S], S], *, of_type: type[S]) -> KFlatModule: ...
+
+    @overload
+    def map_sentences(self, f: Callable[[KSentence], KSentence], *, of_type: None = None) -> KFlatModule: ...
+
+    # Uses overload instead of default argument as a workaround: https://github.com/python/mypy/issues/3737
+    def map_sentences(self, f: Callable, *, of_type: Any = None) -> KFlatModule:
+        if of_type is None:
+            of_type = KSentence
+        return self.let(sentences=tuple(f(sent) if isinstance(sent, of_type) else sent for sent in self.sentences))
+
     @staticmethod
     def from_dict(d: Mapping[str, Any]) -> KFlatModule:
         return KFlatModule(

src/pyk/kcfg/show.py

@@ -158,7 +158,7 @@ def _print_cover(cover: KCFG.Cover) -> Iterable[str]:
         def _print_split_edge(split: KCFG.Split, target_id: int) -> list[str]:
             csubst = split.splits[target_id]
             ret_split_lines: list[str] = []
-            substs = csubst.subst.items()
+            substs = csubst.subst.minimize().items()
             constraints = [ml_pred_to_bool(c, unsafe=True) for c in csubst.constraints]
             if len(constraints) == 1:
                 first_line, *rest_lines = self.kprint.pretty_print(constraints[0]).split('\n')

src/pyk/konvert/_module_to_kore.py

@@ -782,8 +782,7 @@ def _transform_module(self, module: KFlatModule) -> KFlatModule: ...
 class RulePass(SingleModulePass, ABC):
     @final
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        sentences = tuple(self._transform_rule(sent) if isinstance(sent, KRule) else sent for sent in module.sentences)
-        return module.let(sentences=sentences)
+        return module.map_sentences(self._transform_rule, of_type=KRule)
 
     @abstractmethod
     def _transform_rule(self, rule: KRule) -> KRule: ...
@@ -880,8 +879,7 @@ def _transform_module(self, module: KFlatModule) -> KFlatModule:
             Atts.UNIT in att for _, att in concat_atts.items()
         )  # TODO Could be saved with a different attribute structure: concat(Element, Unit)
 
-        sentences = tuple(self._update(sent, concat_atts) if isinstance(sent, KSyntaxSort) else sent for sent in module)
-        return module.let(sentences=sentences)
+        return module.map_sentences(lambda syntax_sort: self._update(syntax_sort, concat_atts), of_type=KSyntaxSort)
 
     @staticmethod
     def _update(syntax_sort: KSyntaxSort, concat_atts: Mapping[KSort, KAtt]) -> KSyntaxSort:
@@ -914,14 +912,13 @@ class AddDomainValueAtts(SingleModulePass):
 
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
         token_sorts = self._token_sorts(module)
-        sentences = tuple(self._update(sent, token_sorts) if isinstance(sent, KSyntaxSort) else sent for sent in module)
-        return module.let(sentences=sentences)
 
-    @staticmethod
-    def _update(syntax_sort: KSyntaxSort, token_sorts: set[KSort]) -> KSyntaxSort:
-        if syntax_sort.sort not in token_sorts:
-            return syntax_sort
-        return syntax_sort.let(att=syntax_sort.att.update([Atts.HAS_DOMAIN_VALUES(None)]))
+        def update(syntax_sort: KSyntaxSort) -> KSyntaxSort:
+            if syntax_sort.sort not in token_sorts:
+                return syntax_sort
+            return syntax_sort.let(att=syntax_sort.att.update([Atts.HAS_DOMAIN_VALUES(None)]))
+
+        return module.map_sentences(update, of_type=KSyntaxSort)
 
     @staticmethod
     def _token_sorts(module: KFlatModule) -> set[KSort]:
@@ -959,13 +956,23 @@ def execute(self, definition: KDefinition) -> KDefinition:
         if len(definition.modules) > 1:
             raise ValueError('Expected a single module')
         module = definition.modules[0]
-
         rules = self._rules_by_klabel(module)
 
-        sentences = tuple(
-            self._update(sent, definition, rules) if isinstance(sent, KProduction) else sent for sent in module
-        )
-        module = module.let(sentences=sentences)
+        def update(production: KProduction) -> KProduction:
+            if not production.klabel:
+                return production
+
+            klabel = production.klabel
+
+            if any(Atts.ANYWHERE in rule.att for rule in rules.get(klabel, [])):
+                return production.let(att=production.att.update([Atts.ANYWHERE(None)]))
+
+            if klabel.name in definition.overloads:
+                return production.let(att=production.att.update([Atts.ANYWHERE(None)]))
+
+            return production
+
+        module = module.map_sentences(update, of_type=KProduction)
         return KDefinition(module.name, (module,))
 
     @staticmethod
@@ -984,21 +991,6 @@ def _rules_by_klabel(module: KFlatModule) -> dict[KLabel, list[KRule]]:
             res.setdefault(label, []).append(rule)
         return res
 
-    @staticmethod
-    def _update(production: KProduction, definition: KDefinition, rules: Mapping[KLabel, list[KRule]]) -> KProduction:
-        if not production.klabel:
-            return production
-
-        klabel = production.klabel
-
-        if any(Atts.ANYWHERE in rule.att for rule in rules.get(klabel, [])):
-            return production.let(att=production.att.update([Atts.ANYWHERE(None)]))
-
-        if klabel.name in definition.overloads:
-            return production.let(att=production.att.update([Atts.ANYWHERE(None)]))
-
-        return production
-
 
 @dataclass
 class AddSymbolAtts(SingleModulePass):
@@ -1008,9 +1000,7 @@ class AddSymbolAtts(SingleModulePass):
     pred: Callable[[KAtt], bool]
 
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        return module.let(
-            sentences=tuple(self._update(sent) if isinstance(sent, KProduction) else sent for sent in module)
-        )
+        return module.map_sentences(self._update, of_type=KProduction)
 
     def _update(self, production: KProduction) -> KProduction:
         if not production.klabel:  # filter for symbol productions
@@ -1090,8 +1080,7 @@ def __init__(self, hook_namespaces: Iterable[str] = ()):
         self.active_prefixes = tuple(f'{namespace}.' for namespace in namespaces)
 
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        sentences = tuple(self._update(sent) if isinstance(sent, KProduction) else sent for sent in module)
-        return module.let(sentences=sentences)
+        return module.map_sentences(self._update, of_type=KProduction)
 
     def _update(self, production: KProduction) -> KProduction:
         if not production.klabel:
@@ -1120,8 +1109,7 @@ def __init__(self, keys: Iterable[AttKey]):
         self.keys = frozenset(keys)
 
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        sentences = tuple(self._update(sent) if isinstance(sent, KProduction) else sent for sent in module)
-        return module.let(sentences=sentences)
+        return module.map_sentences(self._update, of_type=KProduction)
 
     def _update(self, production: KProduction) -> KProduction:
         if not production.klabel:
@@ -1135,8 +1123,7 @@ class AddDefaultFormatAtts(SingleModulePass):
     """Add a default format attribute value to each symbol profuction missing one."""
 
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        sentences = tuple(self._update(sent) if isinstance(sent, KProduction) else sent for sent in module)
-        return module.let(sentences=sentences)
+        return module.map_sentences(self._update, of_type=KProduction)
 
     @staticmethod
     def _update(production: KProduction) -> KProduction:
@@ -1154,8 +1141,7 @@ class DiscardFormatAtts(SingleModulePass):
     """Remove format attributes from symbol productions with items other than terminals and non-terminals."""
 
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        sentences = tuple(self._update(sent) if isinstance(sent, KProduction) else sent for sent in module)
-        return module.let(sentences=sentences)
+        return module.map_sentences(self._update, of_type=KProduction)
 
     @staticmethod
     def _update(production: KProduction) -> KProduction:
@@ -1173,8 +1159,7 @@ class InlineFormatTerminals(SingleModulePass):
     """For a terminal `"foo"` change `%i` to `%cfoo%r`. For a non-terminal, decrease the index."""
 
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        sentences = tuple(self._update(sent) if isinstance(sent, KProduction) else sent for sent in module)
-        return module.let(sentences=sentences)
+        return module.map_sentences(self._update, of_type=KProduction)
 
     @staticmethod
     def _update(production: KProduction) -> KProduction:
@@ -1229,8 +1214,7 @@ def _inline_terminals(formatt: Format, production: KProduction) -> Format:
 @dataclass
 class AddColorAtts(SingleModulePass):
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        sentences = tuple(self._update(sent) if isinstance(sent, KProduction) else sent for sent in module)
-        return module.let(sentences=sentences)
+        return module.map_sentences(self._update, of_type=KProduction)
 
     @staticmethod
     def _update(production: KProduction) -> KProduction:
@@ -1254,8 +1238,7 @@ def _update(production: KProduction) -> KProduction:
 @dataclass
 class AddTerminalAtts(SingleModulePass):
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
-        sentences = tuple(self._update(sent) if isinstance(sent, KProduction) else sent for sent in module)
-        return module.let(sentences=sentences)
+        return module.map_sentences(self._update, of_type=KProduction)
 
     @staticmethod
     def _update(production: KProduction) -> KProduction:
@@ -1276,34 +1259,41 @@ def execute(self, definition: KDefinition) -> KDefinition:
             raise ValueError('Expected a single module')
         module = definition.modules[0]
 
-        sentences = tuple(self._update(sent, definition) if isinstance(sent, KProduction) else sent for sent in module)
-        module = module.let(sentences=sentences)
-        return KDefinition(module.name, (module,))
+        def update(production: KProduction) -> KProduction:
+            if not production.klabel:
+                return production
 
-    @staticmethod
-    def _update(production: KProduction, definition: KDefinition) -> KSentence:
-        if not production.klabel:
-            return production
+            if Atts.FORMAT not in production.att:
+                return production
 
-        if Atts.FORMAT not in production.att:
-            return production
+            tags = sorted(definition.priorities.get(production.klabel.name, []))
+            priorities = tuple(
+                KApply(tag).to_dict() for tag in tags if tag not in BUILTIN_LABELS
+            )  # TODO Add KType to pyk.kast.att
+            return production.let(att=production.att.update([Atts.PRIORITIES(priorities)]))
 
-        tags = sorted(definition.priorities.get(production.klabel.name, []))
-        priorities = tuple(
-            KApply(tag).to_dict() for tag in tags if tag not in BUILTIN_LABELS
-        )  # TODO Add KType to pyk.kast.att
-        return production.let(att=production.att.update([Atts.PRIORITIES(priorities)]))
+        module = module.map_sentences(update, of_type=KProduction)
+        return KDefinition(module.name, (module,))
 
 
 @dataclass
 class AddAssocAtts(SingleModulePass):
     def _transform_module(self, module: KFlatModule) -> KFlatModule:
         left_assocs = self._assocs(module, KAssoc.LEFT)
         right_assocs = self._assocs(module, KAssoc.RIGHT)
-        sentences = tuple(
-            self._update(sent, left_assocs, right_assocs) if isinstance(sent, KProduction) else sent for sent in module
-        )
-        return module.let(sentences=sentences)
+
+        def update(production: KProduction) -> KProduction:
+            if not production.klabel:
+                return production
+
+            if Atts.FORMAT not in production.att:
+                return production
+
+            left = tuple(KApply(tag).to_dict() for tag in sorted(left_assocs.get(production.klabel.name, [])))
+            right = tuple(KApply(tag).to_dict() for tag in sorted(right_assocs.get(production.klabel.name, [])))
+            return production.let(att=production.att.update([Atts.LEFT(left), Atts.RIGHT(right)]))
+
+        return module.map_sentences(update, of_type=KProduction)
 
     @staticmethod
     def _assocs(module: KFlatModule, assoc: KAssoc) -> dict[str, set[str]]:
@@ -1319,19 +1309,3 @@ def insert(dct: dict[str, set[str]], *, key: str, value: str) -> dict[str, set[s
             return dct
 
         return reduce(lambda res, pair: insert(res, key=pair[0], value=pair[1]), pairs, {})
-
-    @staticmethod
-    def _update(
-        production: KProduction,
-        left_assocs: Mapping[str, set[str]],
-        right_assocs: Mapping[str, set[str]],
-    ) -> KProduction:
-        if not production.klabel:
-            return production
-
-        if Atts.FORMAT not in production.att:
-            return production
-
-        left = tuple(KApply(tag).to_dict() for tag in sorted(left_assocs.get(production.klabel.name, [])))
-        right = tuple(KApply(tag).to_dict() for tag in sorted(right_assocs.get(production.klabel.name, [])))
-        return production.let(att=production.att.update([Atts.LEFT(left), Atts.RIGHT(right)]))