diff --git a/package/version b/package/version index cba7147d8..7ea3e8bb0 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.344 +0.1.345 diff --git a/pyproject.toml b/pyproject.toml index 7895c50c1..3e37502aa 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.344" +version = "0.1.345" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/kast/kast.py b/src/pyk/kast/kast.py index c53ff3b45..c8841c480 100644 --- a/src/pyk/kast/kast.py +++ b/src/pyk/kast/kast.py @@ -88,7 +88,7 @@ def _freeze(m: Any) -> Any: if isinstance(m, (int, str, tuple, FrozenDict, frozenset)): return m elif isinstance(m, list): - return tuple(v for v in m) + return tuple(_freeze(v) for v in m) elif isinstance(m, dict): return FrozenDict((k, _freeze(v)) for (k, v) in m.items()) raise ValueError(f"Don't know how to freeze attribute value {m} of type {type(m)}.") @@ -133,6 +133,10 @@ def update(self, atts: Mapping[str, Any]) -> KAtt: def remove(self, atts: Iterable[str]) -> KAtt: return KAtt({k: v for k, v in self.atts.items() if k not in atts}) + def drop_source(self) -> KAtt: + new_atts = {key: value for key, value in self.atts.items() if key != self.SOURCE and key != self.LOCATION} + return KAtt(atts=new_atts) + @property def pretty(self) -> str: if len(self) == 0: diff --git a/src/pyk/kast/manip.py b/src/pyk/kast/manip.py index a5fd72458..22d9ac30a 100644 --- a/src/pyk/kast/manip.py +++ b/src/pyk/kast/manip.py @@ -493,15 +493,7 @@ def minimize_rule(rule: RL, keep_vars: Iterable[str] = ()) -> RL: def remove_source_map(definition: KDefinition) -> KDefinition: - def _remove_source_map(att: KAtt) -> KAtt: - atts = att.atts - new_atts = {} - for att_key in atts: - if att_key != 'org.kframework.attributes.Source' and att_key != 'org.kframework.attributes.Location': - new_atts[att_key] = atts[att_key] - return KAtt(atts=new_atts) - - return on_attributes(definition, _remove_source_map) + return on_attributes(definition, lambda att: att.drop_source()) def remove_attrs(term: KInner) -> KInner: diff --git a/src/pyk/kast/outer.py b/src/pyk/kast/outer.py index 3c283bfe1..c3efcc56b 100644 --- a/src/pyk/kast/outer.py +++ b/src/pyk/kast/outer.py @@ -1029,10 +1029,16 @@ def production_for_klabel(self, klabel: KLabel) -> KProduction: prods = [prod for prod in self.productions if prod.klabel and prod.klabel.name == klabel.name] _prods = [prod for prod in prods if 'unparseAvoid' not in prod.att] if len(_prods) < len(prods): - prods = _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: diff --git a/src/tests/integration/k-files/multiple-definitions.k b/src/tests/integration/k-files/multiple-definitions.k new file mode 100644 index 000000000..edbf929b9 --- /dev/null +++ b/src/tests/integration/k-files/multiple-definitions.k @@ -0,0 +1,20 @@ +module MULTIPLE-DEFINITIONS + imports A + imports B + imports BOOL + + syntax KItem ::= a(KItem) [symbol, label(a)] + | "b" [symbol, label(b)] + | "c" [symbol, label(c)] + rule a(X) => b requires isInt(X) + rule a(X) => b requires notBool isInt(X) + rule b => c +endmodule + +module A + syntax Int +endmodule + +module B + syntax Int +endmodule diff --git a/src/tests/integration/kcfg/test_multiple_definitions.py b/src/tests/integration/kcfg/test_multiple_definitions.py new file mode 100644 index 000000000..2ad52ae6f --- /dev/null +++ b/src/tests/integration/kcfg/test_multiple_definitions.py @@ -0,0 +1,70 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest + +from pyk.cterm import CTerm +from pyk.kast.inner import KApply, KSequence, KVariable +from pyk.prelude.ml import mlTop +from pyk.testing import KCFGExploreTest + +from ..utils import K_FILES + +if TYPE_CHECKING: + from collections.abc import Iterable + + from pyk.kcfg import KCFGExplore + + +EXECUTE_TEST_DATA: Iterable[tuple[str]] = (('branch',),) + + +class TestMultipleDefinitionsProof(KCFGExploreTest): + KOMPILE_MAIN_FILE = K_FILES / 'multiple-definitions.k' + + @staticmethod + def config() -> CTerm: + return CTerm( + KApply( + '', + KApply('', KSequence(KApply('a', [KVariable('X')]))), + KVariable('GENERATED_COUNTER_CELL'), + ), + (mlTop(),), + ) + + @pytest.mark.parametrize( + 'test_id', + EXECUTE_TEST_DATA, + ids=[test_id for test_id, *_ in EXECUTE_TEST_DATA], + ) + def test_execute( + self, + kcfg_explore: KCFGExplore, + test_id: str, + ) -> None: + split_depth, split_post_term, split_next_terms, _logs = kcfg_explore.cterm_execute(self.config(), depth=1) + + split_k = kcfg_explore.kprint.pretty_print(split_post_term.cell('K_CELL')) + split_next_k = [kcfg_explore.kprint.pretty_print(split_post_term.cell('K_CELL')) for term in split_next_terms] + + assert split_depth == 0 + assert len(split_next_terms) == 2 + assert 'a ( X:KItem )' == split_k + assert [ + 'a ( X:KItem )', + 'a ( X:KItem )', + ] == split_next_k + + step_1_depth, step_1_post_term, step_1_next_terms, _logs = kcfg_explore.cterm_execute( + split_next_terms[0], depth=1 + ) + step_1_k = kcfg_explore.kprint.pretty_print(step_1_post_term.cell('K_CELL')) + assert 'c' == step_1_k + + step_2_depth, step_2_post_term, step_2_next_terms, _logs = kcfg_explore.cterm_execute( + split_next_terms[1], depth=1 + ) + step_2_k = kcfg_explore.kprint.pretty_print(step_1_post_term.cell('K_CELL')) + assert 'c' == step_2_k