Merge branch 'noah/node-attributes' of https://github.com/runtimeverification/pyk into noah/node-attributes

Author: nwatson22

docs/conf.py

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

package/version

@@ -1 +1 @@
-0.1.722
+0.1.724

pyproject.toml

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

src/pyk/kast/outer.py

@@ -14,7 +14,7 @@
 
 from ..prelude.kbool import TRUE
 from ..prelude.ml import ML_QUANTIFIERS
-from ..utils import POSet, filter_none, single, unique
+from ..utils import FrozenDict, POSet, filter_none, single, unique
 from .att import EMPTY_ATT, Atts, Format, KAst, KAtt, WithKAtt
 from .inner import (
     KApply,
@@ -37,8 +37,6 @@
     from os import PathLike
     from typing import Any, Final, TypeVar
 
-    from ..utils import FrozenDict
-
     RL = TypeVar('RL', bound='KRuleLike')
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -1001,7 +999,6 @@ class KDefinition(KOuter, WithKAtt, Iterable[KFlatModule]):
 
     main_module: InitVar[KFlatModule]
 
-    _production_for_klabel: dict[KLabel, KProduction]
     _init_config: dict[KSort, KInner]
     _empty_config: dict[KSort, KInner]
 
@@ -1027,7 +1024,6 @@ def __init__(
         object.__setattr__(self, 'requires', tuple(requires))
         object.__setattr__(self, 'att', att)
         object.__setattr__(self, 'main_module', main_module)
-        object.__setattr__(self, '_production_for_klabel', {})
         object.__setattr__(self, '_init_config', {})
         object.__setattr__(self, '_empty_config', {})
 
@@ -1162,28 +1158,6 @@ def sentence_by_unique_id(self) -> dict[str, KSentence]:
                     unique_id_map[unique_id] = sent
         return unique_id_map
 
-    def production_for_klabel(self, klabel: KLabel) -> KProduction:
-        """Returns the original production for a given `KLabel` (failing if 0 or >1 are returned)."""
-        if klabel not in self._production_for_klabel:
-            prods = [prod for prod in self.productions if prod.klabel and prod.klabel.name == klabel.name]
-            _prods = [prod for prod in prods if Atts.UNPARSE_AVOID not in prod.att]
-            if len(_prods) < len(prods):
-                _LOGGER.warning(
-                    f'Discarding {len(prods) - len(_prods)} productions with `unparseAvoid` attribute for label: {klabel}'
-                )
-                prods = _prods
-            # Automatically defined symbols like isInt may get multiple
-            # definitions in different modules.
-            _prods = list({prod.let_att(prod.att.drop_source()) for prod in prods})
-            if len(_prods) < len(prods):
-                _LOGGER.warning(f'Discarding {len(prods) - len(_prods)} equivalent productions')
-                prods = _prods
-            try:
-                self._production_for_klabel[klabel] = single(prods)
-            except ValueError as err:
-                raise ValueError(f'Expected a single production for label {klabel}, not: {prods}') from err
-        return self._production_for_klabel[klabel]
-
     def production_for_cell_sort(self, sort: KSort) -> KProduction:
         """Returns the production for a given cell-declaration syntax from the cell's declared sort."""
         # Typical cell production has 3 productions:
@@ -1208,11 +1182,11 @@ def module(self, name: str) -> KFlatModule:
 
     def return_sort(self, label: KLabel) -> KSort:
         """Returns the return sort of a given `KLabel` by looking up the production."""
-        return self.production_for_klabel(label).sort
+        return self.symbols[label.name].sort
 
     def argument_sorts(self, label: KLabel) -> list[KSort]:
         """Returns the argument sorts of a given `KLabel` by looking up the production."""
-        return self.production_for_klabel(label).argument_sorts
+        return self.symbols[label.name].argument_sorts
 
     @cached_property
     def subsort_table(self) -> FrozenDict[KSort, frozenset[KSort]]:
@@ -1224,6 +1198,22 @@ def subsorts(self, sort: KSort) -> frozenset[KSort]:
         """Return all subsorts of a given `KSort` by inspecting the definition."""
         return self.subsort_table.get(sort, frozenset())
 
+    @cached_property
+    def symbols(self) -> FrozenDict[str, KProduction]:
+        symbols: dict[str, KProduction] = {}
+        for prod in self.productions:
+            if not prod.klabel:
+                continue
+            symbol = prod.klabel.name
+            if symbol in symbols:  # Check if duplicate
+                other = symbols[symbol]
+                if prod.let(att=prod.att.drop_source()) != other.let(att=prod.att.drop_source()):
+                    prods = [other, prod]
+                    raise AssertionError(f'Found multiple productions for {symbol}: {prods}')
+                continue
+            symbols[symbol] = prod
+        return FrozenDict(symbols)
+
     def sort(self, kast: KInner) -> KSort | None:
         """Computes the sort of a given term using best-effort simple sorting algorithm, returns `None` on algorithm failure."""
         match kast:
@@ -1238,7 +1228,7 @@ def sort(self, kast: KInner) -> KSort | None:
             case KSequence(_):
                 return KSort('K')
             case KApply(label, _):
-                prod = self.production_for_klabel(label)
+                prod = self.symbols[label.name]
                 if prod.sort not in prod.params:
                     return prod.sort
                 elif len(prod.params) == len(label.params):
@@ -1293,7 +1283,7 @@ def _add_ksequence_under_k_productions(_kast: KInner) -> KInner:
             if type(_kast) is not KApply:
                 return _kast
 
-            prod = self.production_for_klabel(_kast.label)
+            prod = self.symbols[_kast.label.name]
             return KApply(
                 _kast.label,
                 [
@@ -1358,7 +1348,7 @@ def transform(
                     del occurrences[var.name]
                     return (Subst(subst)(term), occurrences)
                 else:
-                    prod = self.production_for_klabel(term.label)
+                    prod = self.symbols[term.label.name]
                     if len(prod.params) == 0:
                         for t, a in zip(prod.argument_sorts, term.args, strict=True):
                             if type(a) is KVariable:
@@ -1386,7 +1376,7 @@ def add_sort_params(self, kast: KInner) -> KInner:
 
         def _add_sort_params(_k: KInner) -> KInner:
             if type(_k) is KApply:
-                prod = self.production_for_klabel(_k.label)
+                prod = self.symbols[_k.label.name]
                 if len(_k.label.params) == 0 and len(prod.params) > 0:
                     sort_dict: dict[KSort, KSort] = {}
                     for psort, asort in zip(prod.argument_sorts, map(self.sort, _k.args), strict=True):
@@ -1467,7 +1457,7 @@ def _kdefinition_empty_config(_sort: KSort) -> KApply:
             cell_prod = self.production_for_cell_sort(_sort)
             cell_klabel = cell_prod.klabel
             assert cell_klabel is not None
-            production = self.production_for_klabel(cell_klabel)
+            production = self.symbols[cell_klabel.name]
             args: list[KInner] = []
             num_nonterminals = 0
             num_freshvars = 0
@@ -1490,8 +1480,8 @@ def instantiate_cell_vars(self, term: KInner) -> KInner:
 
         def _cell_vars_to_labels(_kast: KInner) -> KInner:
             if type(_kast) is KApply and _kast.is_cell:
-                production = self.production_for_klabel(_kast.label)
-                production_arity = [prod_item.sort for prod_item in production.items if type(prod_item) is KNonTerminal]
+                production = self.symbols[_kast.label.name]
+                production_arity = [item.sort for item in production.non_terminals]
                 new_args = []
                 for sort, arg in zip(production_arity, _kast.args, strict=True):
                     if sort.name.endswith('Cell') and type(arg) is KVariable:

src/pyk/ktool/kprove.py

@@ -312,10 +312,7 @@ def prove_claim_rpc(
             proof: Proof
             prover: Prover
             lhs_top = extract_lhs(claim.body)
-            if (
-                type(lhs_top) is KApply
-                and self.definition.production_for_klabel(lhs_top.label) in self.definition.functions
-            ):
+            if type(lhs_top) is KApply and self.definition.symbols[lhs_top.label.name] in self.definition.functions:
                 proof = EqualityProof.from_claim(claim, self.definition)
                 prover = ImpliesProver(proof, kcfg_explore)
             else:

src/pyk/testing/_kompiler.py

@@ -167,7 +167,7 @@ class KoreClientTest(KompiledTest):
     KOMPILE_BACKEND: ClassVar = 'haskell'
     LLVM_ARGS: ClassVar[dict[str, Any]] = {}
 
-    CLIENT_TIMEOUT: ClassVar = 2000
+    CLIENT_TIMEOUT: ClassVar = 5000
 
     @pytest.fixture(scope='class', params=['legacy', 'booster'])
     def server_type(self, request: FixtureRequest, use_server: UseServer) -> ServerType: