Deduplicate productions (#505)

Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.344
+0.1.345

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. <[email protected]>",

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:

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:

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:

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

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(
+                '<generatedTop>',
+                KApply('<k>', 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