Extract class KoreSortTable (#738)

Moves methods `is_subsort`, `meet_sort` and related logic from
`KompiledKore` to a new class.

---------

Co-authored-by: devops <devops@runtimeverification.com>

package/version

@@ -1 +1 @@
-0.1.511
+0.1.512

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.511"
+version = "0.1.512"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/pyk/kore/kompiled.py

@@ -1,15 +1,13 @@
 from __future__ import annotations
 
 import logging
-from collections import defaultdict
 from dataclasses import dataclass
-from functools import cached_property, reduce
+from functools import cached_property
 from itertools import chain
 from pathlib import Path
 from typing import TYPE_CHECKING, Final, final
 
 from ..cli.utils import check_dir_path, check_file_path
-from ..utils import FrozenDict
 from .parser import KoreParser
 from .syntax import DV, ML_SYMBOL_DECLS, App, MLPattern, MLQuant, SortApp, SortVar, WithSort
 
@@ -48,33 +46,68 @@ def definition(self) -> Definition:
         _LOGGER.info(f'Parsing kore definition: {self.path}')
         return KoreParser(kore_text).definition()
 
+    @cached_property
+    def sort_table(self) -> KoreSortTable:
+        return KoreSortTable.for_definition(self.definition)
+
     @cached_property
     def symbol_table(self) -> KoreSymbolTable:
         return KoreSymbolTable.for_definition(self.definition)
 
-    @cached_property
-    def _subsort_table(self) -> FrozenDict[Sort, frozenset[Sort]]:
-        axioms = (axiom for module in self.definition for axiom in module.axioms)
-        attrs = (attr for axiom in axioms for attr in axiom.attrs)
-        subsort_attrs = (attr for attr in attrs if attr.symbol == 'subsort')
-        subsort_attr_sorts = (attr.sorts for attr in subsort_attrs)
+    def add_injections(self, pattern: Pattern, sort: Sort | None = None) -> Pattern:
+        if sort is None:
+            sort = SortApp('SortK')
+        patterns = pattern.patterns
+        sorts = self.symbol_table.pattern_sorts(pattern)
+        pattern = pattern.let_patterns(self.add_injections(p, s) for p, s in zip(patterns, sorts, strict=True))
+        return self._inject(pattern, sort)
 
-        direct_subsorts: dict[Sort, set[Sort]] = defaultdict(set)
-        for subsort, supersort in subsort_attr_sorts:
-            direct_subsorts[supersort].add(subsort)
+    def _inject(self, pattern: Pattern, sort: Sort) -> Pattern:
+        actual_sort = self.symbol_table.infer_sort(pattern)
+
+        if actual_sort == sort:
+            return pattern
+
+        if self.sort_table.is_subsort(actual_sort, sort):
+            return App('inj', (actual_sort, sort), (pattern,))
 
-        supersorts = direct_subsorts.keys()
+        raise ValueError(f'Sort {actual_sort.name} is not a subsort of {sort.name}: {pattern}')
+
+
+class KoreSortTable:
+    _subsort_table: dict[Sort, set[Sort]]
+
+    def __init__(self, subsorts: Iterable[tuple[Sort, Sort]]):
+        self._subsort_table = self._create_subsort_table(subsorts)
+
+    @staticmethod
+    def _create_subsort_table(subsorts: Iterable[tuple[Sort, Sort]]) -> dict[Sort, set[Sort]]:
+        res: dict[Sort, set[Sort]] = {}
 
-        subsort_table = dict(direct_subsorts)
+        for subsort, supersort in subsorts:
+            if supersort not in res:
+                res[supersort] = set()
+            res[supersort].add(subsort)
+
+        supersorts = res.keys()
         for sort_k in supersorts:
             for sort_j in supersorts:
-                if sort_k not in subsort_table[sort_j]:
+                if sort_k not in res[sort_j]:
                     continue
 
-                for sort_i in subsort_table[sort_k]:
-                    subsort_table[sort_j].add(sort_i)
+                for sort_i in res[sort_k]:
+                    res[sort_j].add(sort_i)
 
-        return FrozenDict((supersort, frozenset(subsorts)) for supersort, subsorts in subsort_table.items())
+        return res
+
+    @staticmethod
+    def for_definition(definition: Definition) -> KoreSortTable:
+        axioms = (axiom for module in definition for axiom in module.axioms)
+        attrs = (attr for axiom in axioms for attr in axiom.attrs)
+        subsort_attrs = (attr for attr in attrs if attr.symbol == 'subsort')
+        subsort_attr_sorts = (attr.sorts for attr in subsort_attrs)
+        subsorts = ((subsort, supersort) for subsort, supersort in subsort_attr_sorts)
+        return KoreSortTable(subsorts)
 
     def is_subsort(self, sort1: Sort, sort2: Sort) -> bool:
         if sort1 == sort2:
@@ -86,9 +119,9 @@ def is_subsort(self, sort1: Sort, sort2: Sort) -> bool:
         if sort1 == SortApp('SortK'):
             return False
 
-        return sort1 in self._subsort_table.get(sort2, frozenset())
+        return sort1 in self._subsort_table.get(sort2, ())
 
-    def meet_sorts(self, sort1: Sort, sort2: Sort) -> Sort:
+    def meet(self, sort1: Sort, sort2: Sort) -> Sort:
         if self.is_subsort(sort1, sort2):
             return sort1
 
@@ -106,29 +139,6 @@ def meet_sorts(self, sort1: Sort, sort2: Sort) -> Sort:
         (subsort,) = max_subsorts
         return subsort
 
-    def meet_all_sorts(self, sorts: Iterable[Sort]) -> Sort:
-        unit: Sort = SortApp('SortK')
-        return reduce(self.meet_sorts, sorts, unit)
-
-    def add_injections(self, pattern: Pattern, sort: Sort | None = None) -> Pattern:
-        if sort is None:
-            sort = SortApp('SortK')
-        patterns = pattern.patterns
-        sorts = self.symbol_table.pattern_sorts(pattern)
-        pattern = pattern.let_patterns(self.add_injections(p, s) for p, s in zip(patterns, sorts, strict=True))
-        return self._inject(pattern, sort)
-
-    def _inject(self, pattern: Pattern, sort: Sort) -> Pattern:
-        actual_sort = self.symbol_table.infer_sort(pattern)
-
-        if actual_sort == sort:
-            return pattern
-
-        if self.is_subsort(actual_sort, sort):
-            return App('inj', (actual_sort, sort), (pattern,))
-
-        raise ValueError(f'Sort {actual_sort.name} is not a subsort of {sort.name}: {pattern}')
-
 
 class KoreSymbolTable:
     _symbol_table: dict[str, SymbolDecl]

src/tests/unit/test_konvert.py

@@ -6,15 +6,14 @@
 import pytest
 
 from pyk.konvert import munge, unmunge
-from pyk.kore.kompiled import KompiledKore
+from pyk.kore.kompiled import KoreSortTable
+from pyk.kore.parser import KoreParser
 from pyk.kore.syntax import SortApp
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
     from typing import Final
 
-    from pytest import TempPathFactory
-
 
 def munge_test_data_reader() -> Iterator[tuple[str, str]]:
     test_data_file = Path(__file__).parent / 'test-data/munge-tests'
@@ -55,25 +54,7 @@ def test_unmunge(symbol: str, expected: str) -> None:
     assert actual == expected
 
 
-class KoreFactory:
-    _tmp_path_factory: TempPathFactory
-
-    def __init__(self, tmp_path_factory: TempPathFactory):
-        self._tmp_path_factory = tmp_path_factory
-
-    def __call__(self, definition_text: str) -> KompiledKore:
-        path = self._tmp_path_factory.mktemp('kompiled-defn')
-        (path / 'definition.kore').write_text(definition_text)
-        (path / 'timestamp').touch()
-        return KompiledKore(path)
-
-
-@pytest.fixture(scope='session')
-def kore_factory(tmp_path_factory: TempPathFactory) -> KoreFactory:
-    return KoreFactory(tmp_path_factory)
-
-
-def test_subsort_table(kore_factory: KoreFactory) -> None:
+def test_kore_sort_table() -> None:
     # When
     definition_text = r"""
         []
@@ -85,7 +66,8 @@ def test_subsort_table(kore_factory: KoreFactory) -> None:
             axiom{R} \top{R}() [subsort{B{}, D{}}()]
         endmodule []
     """
-    kompiled_kore = kore_factory(definition_text)
+    definition = KoreParser(definition_text).definition()
+    sort_table = KoreSortTable.for_definition(definition)
 
     a, b, c, d = (SortApp(name) for name in ['A', 'B', 'C', 'D'])
     expected = {
@@ -95,7 +77,7 @@ def test_subsort_table(kore_factory: KoreFactory) -> None:
     }
 
     # When
-    actual = kompiled_kore._subsort_table
+    actual = sort_table._subsort_table
 
     # Then
     assert actual == expected