Parametrize ModuleToKore for functional claims

runtimeverification · Nov 15, 2023 · 9345c0e · 9345c0e
1 parent d3f7614
commit 9345c0e
Showing 1 changed file with 12 additions and 9 deletions.
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -1057,6 +1057,9 @@ private RuleInfo getRuleInfo(RuleOrClaim rule, boolean heatCoolEq, String topCel
         productionSortStr = topCellSortStr;
       }
       owise = rule.att().contains(Att.OWISE());
+    } else if (leftPattern instanceof KToken kt) {
+      productionSort = kt.sort();
+      productionSortStr = getSortStr(productionSort);
     }
 
     return new RuleInfo(
@@ -1348,38 +1351,38 @@ private void convertRule(
       } else {
         // LHS for claims
         sb.append("  claim{} ");
-        sb.append(String.format("\\implies{%s} (\n    ", topCellSortStr));
-        sb.append(String.format("  \\and{%s} (\n      ", topCellSortStr));
-        convertSideCondition(requires, topCellSortStr, sb);
+        sb.append(String.format("\\implies{%s} (\n    ", ruleInfo.productionSortStr));
+        sb.append(String.format("  \\and{%s} (\n      ", ruleInfo.productionSortStr));
+        convertSideCondition(requires, ruleInfo.productionSortStr, sb);
         sb.append(", ");
         convert(left, sb);
         sb.append("), ");
       }
 
       // generate rule RHS
       if (sentenceType == SentenceType.ALL_PATH) {
-        sb.append(String.format("%s{%s} (\n      ", ALL_PATH_OP, topCellSortStr));
+        sb.append(String.format("%s{%s} (\n      ", ALL_PATH_OP, ruleInfo.productionSortStr));
       } else if (sentenceType == SentenceType.ONE_PATH) {
-        sb.append(String.format("%s{%s} (\n      ", ONE_PATH_OP, topCellSortStr));
+        sb.append(String.format("%s{%s} (\n      ", ONE_PATH_OP, ruleInfo.productionSortStr));
       }
       if (!existentials.isEmpty()) {
         for (KVariable exists : existentials) {
-          sb.append(String.format(" \\exists{%s} (", topCellSortStr));
+          sb.append(String.format(" \\exists{%s} (", ruleInfo.productionSortStr));
           convert((K) exists, sb);
           sb.append(", ");
         }
         sb.append("\n      ");
       }
-      sb.append(String.format("\\and{%s} (\n      ", topCellSortStr));
+      sb.append(String.format("\\and{%s} (\n      ", ruleInfo.productionSortStr));
 
       if (options.enableKoreAntileft) {
-        convertSideCondition(ensures, topCellSortStr, sb);
+        convertSideCondition(ensures, ruleInfo.productionSortStr, sb);
         sb.append(", ");
         convert(right, sb);
       } else {
         convert(right, sb);
         sb.append(", ");
-        convertSideCondition(ensures, topCellSortStr, sb);
+        convertSideCondition(ensures, ruleInfo.productionSortStr, sb);
       }
 
       sb.append(')');