Fix KLabel for #Exists (#4410)

Preparatory refactoring for: * #4418 In KAST, ML quantifiers are defined with two sort parameters: https://github.com/runtimeverification/k/blob/9100689e357a7e5820362869a73684468ef9c91b/k-distribution/include/kframework/builtin/kast.md?plain=1#L154-L155 However, `pyk` falsely assumed these symbols only have a single sort parameter as in KORE: https://github.com/runtimeverification/haskell-backend/blob/master/docs/kore-syntax.md?plain=1#L194-L197 This PR fixes that.
runtimeverification · Jun 5, 2024 · 7d7db4f · 7d7db4f
1 parent 837f7bd
commit 7d7db4f
Show file tree

Hide file tree

Showing 5 changed files with 25 additions and 13 deletions.
diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py
@@ -24,7 +24,7 @@
     UnsatResult,
     kore_server,
 )
-from ..prelude.k import GENERATED_TOP_CELL
+from ..prelude.k import GENERATED_TOP_CELL, K_ITEM
 from ..prelude.ml import is_top, mlAnd, mlEquals
 
 if TYPE_CHECKING:
@@ -233,7 +233,9 @@ def implies(
                 bind_text, bind_label = ('universally', '#Forall')
             _LOGGER.debug(f'Binding variables in consequent {bind_text}: {unbound_consequent}')
             for uc in unbound_consequent:
-                _consequent = KApply(KLabel(bind_label, [GENERATED_TOP_CELL]), [KVariable(uc), _consequent])
+                # Setting Sort1 to KItem in #Exists to avoid inferring the type of each uc.
+                # This should not have any effect on the resulting KORE pattern (\exists only has Sort2 as sort variable).
+                _consequent = KApply(KLabel(bind_label, [K_ITEM, GENERATED_TOP_CELL]), [KVariable(uc), _consequent])
         antecedent_kore = self.kast_to_kore(antecedent.kast)
         consequent_kore = self.kast_to_kore(_consequent)
         try:

diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py
@@ -223,8 +223,9 @@ def _kapply_to_kore(kapply: KApply, patterns: list[Pattern]) -> Pattern:
 def _kapply_to_ml_quant(kapply: KApply, patterns: list[Pattern]) -> MLQuant:
     label = kapply.label
     symbol = ML_QUANT_LABELS[label.name]
-    sorts = tuple(_ksort_to_kore(ksort) for ksort in label.params)
-    return MLQuant.of(symbol, sorts, patterns)
+    _, ksort = label.params
+    sort = _ksort_to_kore(ksort)
+    return MLQuant.of(symbol, (sort,), patterns)
 
 
 def _kapply_to_pattern(kapply: KApply, patterns: list[Pattern]) -> Pattern:

diff --git a/pyk/src/pyk/konvert/_kore_to_kast.py b/pyk/src/pyk/konvert/_kore_to_kast.py
@@ -110,9 +110,11 @@ def _pattern_to_kast(pattern: Pattern, terms: list[KInner]) -> KInner:
             return mlNot(karg, sort=_sort_to_kast(sort))
 
         case Exists(sort, EVar(vname, vsort), _):
-            kvar = KVariable(name=unmunge(vname[3:]), sort=_sort_to_kast(vsort))
+            ksort = _sort_to_kast(sort)
+            kvsort = _sort_to_kast(vsort)
+            kvar = KVariable(name=unmunge(vname[3:]), sort=kvsort)
             (body,) = terms
-            return mlExists(kvar, body, sort=_sort_to_kast(sort))
+            return mlExists(kvar, body, sort1=kvsort, sort2=ksort)
 
         case Equals(op_sort, sort, _, _):
             larg, rarg = terms

diff --git a/pyk/src/pyk/prelude/ml.py b/pyk/src/pyk/prelude/ml.py
@@ -5,7 +5,7 @@
 from pyk.utils import single
 
 from ..kast.inner import KApply, KLabel, build_assoc, flatten_label
-from .k import GENERATED_TOP_CELL
+from .k import GENERATED_TOP_CELL, K_ITEM
 from .kbool import BOOL, FALSE, TRUE
 
 if TYPE_CHECKING:
@@ -93,8 +93,13 @@ def mlImplies(antecedent: KInner, consequent: KInner, sort: str | KSort = GENERA
     return KLabel('#Implies', sort)(antecedent, consequent)
 
 
-def mlExists(var: KVariable, body: KInner, sort: str | KSort = GENERATED_TOP_CELL) -> KApply:  # noqa: N802
-    return KLabel('#Exists', sort)(var, body)
+def mlExists(  # noqa: N802
+    var: KVariable,
+    body: KInner,
+    sort1: str | KSort = K_ITEM,
+    sort2: str | KSort = GENERATED_TOP_CELL,
+) -> KApply:
+    return KLabel('#Exists', sort1, sort2)(var, body)
 
 
 def mlCeil(  # noqa: N802

diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py
@@ -153,7 +153,7 @@
         KSort('Bool'),
         r'\exists{SortBool{}}(VarX : SortBool{}, VarX : SortBool{})',
         KApply(
-            KLabel('#Exists', [KSort('Bool')]),
+            KLabel('#Exists', [KSort('Bool'), KSort('Bool')]),
             [
                 KVariable('X', sort=KSort('Bool')),
                 KVariable('X', sort=KSort('Bool')),
@@ -379,7 +379,7 @@
         'ml-exists-var-inference',
         KSort('Foo'),
         r'\exists{SortFoo{}}(VarX : SortBar{}, Lblfoo{}(VarX : SortBar{}))',
-        KApply(KLabel('#Exists', [KSort('Foo')]), [KVariable('X'), KApply('foo', [KVariable('X')])]),
+        KApply(KLabel('#Exists', [KSort('Bar'), KSort('Foo')]), [KVariable('X'), KApply('foo', [KVariable('X')])]),
     ),
     (
         'ml-multiple-exists-var-inference',
@@ -392,7 +392,7 @@
             KLabel('#And', [KSort('Foo')]),
             [
                 KApply(
-                    KLabel('#Exists', [KSort('Foo')]),
+                    KLabel('#Exists', [KSort('K'), KSort('Foo')]),
                     [
                         KVariable('X'),
                         KApply(
@@ -401,7 +401,9 @@
                         ),
                     ],
                 ),
-                KApply(KLabel('#Exists', [KSort('Foo')]), [KVariable('X'), KApply('foo', [KVariable('X')])]),
+                KApply(
+                    KLabel('#Exists', [KSort('Bar'), KSort('Foo')]), [KVariable('X'), KApply('foo', [KVariable('X')])]
+                ),
             ],
         ),
     ),