Generalize KAST-to-KORE conversion for KSequence (#4874)

* Allow items of sort `K` to appear at any position within a
`KSequence`, not just at the end. During `_kast_to_kore`, an application
of `append` is generated in such cases.
* Conversely, during `_kore_to_kast`, generate a `KSequence` for each
`append`.
* Fix `KVariable` sort inference so that it does not override declared
sorts of `KSequence` items.
* Update `test_kast_to_kore_frontend` to compare the Frontend’s result
against expected outputs, rather than `pyk`'s results. This makes it
easier to add new tests based on the Frontend’s output.

Author: tothtamas28

pyk/src/pyk/kast/outer.py

@@ -30,6 +30,7 @@
     top_down,
 )
 from .kast import kast_term
+from .prelude.k import K_ITEM, K
 from .rewrite import indexed_rewrite
 
 if TYPE_CHECKING:
@@ -1460,13 +1461,15 @@ def transform(
                         for t, a in zip(prod.argument_sorts, term.args, strict=True):
                             if type(a) is KVariable:
                                 occurrences[a.name].append(a.let_sort(t))
-            elif isinstance(term, KSequence) and term.arity > 0:
-                for a in term.items[0:-1]:
-                    if type(a) is KVariable:
-                        occurrences[a.name].append(a.let_sort(KSort('KItem')))
-                last_a = term.items[-1]
-                if type(last_a) is KVariable:
-                    occurrences[last_a.name].append(last_a.let_sort(KSort('K')))
+            elif isinstance(term, KSequence):
+                for i, item in enumerate(term.items):
+                    if isinstance(item, KVariable):
+                        if item.sort is not None:
+                            occurrences[item.name].append(item)
+                        elif i == term.arity - 1:
+                            occurrences[item.name].append(item.let_sort(K))
+                        else:
+                            occurrences[item.name].append(item.let_sort(K_ITEM))
             return (term, occurrences)
 
         (new_term, var_occurrences) = bottom_up_with_summary(transform, kast)

pyk/src/pyk/konvert/_kast_to_kore.py

@@ -82,41 +82,43 @@ def kast_to_kore(definition: KDefinition, kast: KInner, sort: KSort | None = Non
     kast = definition.sort_vars(kast, sort)
     kast = definition.add_cell_map_items(kast)
     kast = definition.add_sort_params(kast)
-    kast = _replace_ksequence_by_kapply(kast)
+    kast = _replace_ksequence_by_kapply(definition, kast)
     kast = _add_sort_injections(definition, kast, sort)
     kore = _kast_to_kore(kast)
     return kore
 
 
-def _replace_ksequence_by_kapply(term: KInner) -> KInner:
+def _replace_ksequence_by_kapply(definition: KDefinition, term: KInner) -> KInner:
     dotk = KApply('dotk')
     kseq = KLabel('kseq')
+    append = KLabel('append')
 
-    def transform(term: KInner) -> KInner:
-        match term:
-            case KSequence(items):
-                return transform_items(items)
-            case _:
-                return term
+    def kapply(x: KInner, y: KInner) -> KApply:
+        return append(x, y) if definition.sort_strict(x) == K else kseq(x, y)
+
+    def ksequence_to_kapply(term: KInner) -> KInner:
+        if not isinstance(term, KSequence):
+            return term
+
+        items = term.items
 
-    def transform_items(items: tuple[KInner, ...]) -> KInner:
         if not items:
             return dotk
 
         unit: KInner
         args: tuple[KInner, ...]
 
         last = items[-1]
-        if isinstance(last, KVariable) and last.sort == K:
+        if definition.sort_strict(last) == K:
             unit = last
             args = items[:-1]
         else:
             unit = dotk
             args = items
 
-        return reduce(lambda x, y: kseq(y, x), reversed(args), unit)
+        return reduce(lambda x, y: kapply(y, x), reversed(args), unit)
 
-    return top_down(transform, term)
+    return top_down(ksequence_to_kapply, term)
 
 
 def _add_sort_injections(definition: KDefinition, term: KInner, sort: KSort) -> KInner:
@@ -179,6 +181,8 @@ def _argument_sorts(definition: KDefinition, term: KInner) -> tuple[KSort, ...]:
                     return (K_ITEM, K)
                 case 'dotk':
                     return ()
+                case 'append':
+                    return (K, K)
                 case '#Forall' | '#Exists':
                     _, argument_sorts = definition.resolve_sorts(term.label)
                     _, argument_sort = argument_sorts
@@ -202,7 +206,7 @@ def _let_arguments(term: KInner, args: list[KInner]) -> KInner:
 def _inject(definition: KDefinition, term: KInner, sort: KSort) -> KInner:
     actual_sort: KSort
     match term:
-        case KApply(KLabel('kseq' | 'dotk')):  # Special case: pseudo-labels
+        case KApply(KLabel('kseq' | 'dotk' | 'append')):  # Special case: pseudo-labels
             actual_sort = K
         case _:
             actual_sort = definition.sort_strict(term)
@@ -437,7 +441,7 @@ def _kapply_to_pattern(kapply: KApply, patterns: list[Pattern]) -> Pattern:
 
 
 def _label_to_kore(label: str) -> str:
-    if label in ['inj', 'kseq', 'dotk']:  # pseudo-labels introduced during KAST-to-KORE tranformation
+    if label in ['inj', 'kseq', 'dotk', 'append']:  # pseudo-labels introduced during KAST-to-KORE tranformation
         return label
 
     if label in ML_PATTERN_LABELS:

pyk/src/pyk/konvert/_kore_to_kast.py

@@ -93,6 +93,10 @@ def _pattern_to_kast(pattern: Pattern, terms: list[KInner]) -> KInner:
                     _, _ = terms
                     return KSequence(terms)
 
+                elif symbol == 'append':
+                    _, _ = terms
+                    return KSequence(terms)
+
                 else:
                     klabel = KLabel(unmunge(symbol[3:]))
                     return KApply(klabel, terms)

pyk/src/tests/integration/konvert/test_simple_proofs.py

@@ -211,6 +211,59 @@
         """,
         KSequence([KApply('foo_SIMPLE-PROOFS_KItem'), KApply('foo-bar_SIMPLE-PROOFS_Baz')]),
     ),
+    (
+        'kseq-with-k-head',
+        KSort('K'),
+        r'append{}(VarX : SortK{}, kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1")), dotk{}()))',
+        KSequence(KVariable('X', 'K'), intToken(1)),
+    ),
+    (
+        'kseq-with-k-middle',
+        KSort('K'),
+        r"""
+        kseq{}(
+            inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1")),
+            append{}(
+                VarX : SortK{},
+                kseq{}(
+                    inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("2")),
+                    dotk{}()
+                )
+            )
+        )
+        """,
+        KSequence(intToken(1), KVariable('X', 'K'), intToken(2)),
+    ),
+    (
+        'kseq-with-multiple-ks',
+        KSort('K'),
+        r"""
+        kseq{}(
+            inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1")),
+            append{}(
+                VarX1 : SortK{},
+                append{}(
+                    VarX2 : SortK{},
+                    append{}(
+                        VarX3 : SortK{},
+                        kseq{}(
+                            inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("2")),
+                            VarX4 : SortK{}
+                        )
+                    )
+                )
+            )
+        )
+        """,
+        KSequence(
+            intToken(1),
+            KVariable('X1', 'K'),
+            KVariable('X2', 'K'),
+            KVariable('X3', 'K'),
+            intToken(2),
+            KVariable('X4', 'K'),
+        ),
+    ),
     (
         'if-then-else',
         KSort('K'),
@@ -699,20 +752,20 @@ def test_kast_to_kore(
         kast: KInner,
     ) -> None:
         # Given
-        kore = KoreParser(kore_text).pattern()
+        expected_kore = KoreParser(kore_text).pattern()
 
         # When
         actual_kore = kast_to_kore(definition, kast, sort=sort)
 
         # Then
-        assert actual_kore == kore
+        assert actual_kore == expected_kore
 
     @pytest.mark.parametrize(
         'test_id,sort,kore_text,kast',
         KAST_TO_KORE_TEST_DATA,
         ids=[test_id for test_id, *_ in KAST_TO_KORE_TEST_DATA],
     )
-    def test_kast_to_kore_frontend_comp(
+    def test_kast_to_kore_frontend(
         self,
         definition: KDefinition,
         test_id: str,
@@ -725,13 +778,13 @@ def test_kast_to_kore_frontend_comp(
             pytest.skip()
 
         # Given
-        frontend_kore = kprint.kast_to_kore(kast=kast, sort=sort, force_kast=True)
+        expected_kore = KoreParser(kore_text).pattern()
 
         # When
-        actual_kore = kast_to_kore(definition, kast, sort=sort)
+        actual_kore = kprint.kast_to_kore(kast=kast, sort=sort, force_kast=True)
 
         # Then
-        assert actual_kore == frontend_kore
+        assert actual_kore == expected_kore
 
     @pytest.mark.parametrize(
         'test_id,_sort,kore_text,kast',

pyk/src/tests/integration/test-data/frontend-comp-skip

@@ -4,6 +4,9 @@ if-then-else-no-sort-param-k
 kseq-empty
 kseq-singleton
 kseq-two-element
+kseq-with-k-head
+kseq-with-k-middle
+kseq-with-multiple-ks
 ksequence-duo-var-1
 ksequence-duo-var-2
 ksequence-empty