From 28b2a2ce34b3fcc080bae0caca0e047c301dcd9c Mon Sep 17 00:00:00 2001
From: Scott Guest <scott.guest@runtimeverification.com>
Date: Tue, 12 Dec 2023 10:27:49 -0500
Subject: [PATCH] Add support for strict casts

---
 .../inference/SortInferencer.java             | 35 +++++++------------
 1 file changed, 13 insertions(+), 22 deletions(-)

diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java
index 7c88927d511..2eca3be457a 100644
--- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java
+++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java
@@ -88,10 +88,10 @@ public SortInferencer(Module mod) {
 
   /**
    * Determine whether a Term is supported by the current SortInferencer algorithm. Supported terms
-   * can contain neither ambiguities, strict casts, nor parametric sorts.
+   * can contain neither ambiguities nor parametric sorts.
    */
   public static boolean isSupported(Term t) {
-    return !hasAmbiguity(t) && !hasStrictCast(t) && !hasParametricSorts(t);
+    return !hasAmbiguity(t) && !hasParametricSorts(t);
   }
 
   private static boolean hasAmbiguity(Term t) {
@@ -104,24 +104,6 @@ private static boolean hasAmbiguity(Term t) {
     return ((TermCons) t).items().stream().anyMatch(SortInferencer::hasAmbiguity);
   }
 
-  private static boolean hasStrictCast(Term t) {
-    if (t instanceof Ambiguity amb) {
-      return amb.items().stream().anyMatch(SortInferencer::hasStrictCast);
-    }
-    ProductionReference pr = (ProductionReference) t;
-    if (pr.production().klabel().isDefined()) {
-      KLabel klabel = pr.production().klabel().get();
-      String label = klabel.name();
-      if (label.equals("#SyntacticCast") || label.equals("#SyntacticCastBraced")) {
-        return true;
-      }
-    }
-    if (t instanceof Constant) {
-      return false;
-    }
-    return ((TermCons) t).items().stream().anyMatch(SortInferencer::hasStrictCast);
-  }
-
   private static boolean hasParametricSorts(Term t) {
     if (t instanceof Ambiguity amb) {
       return amb.items().stream().anyMatch(SortInferencer::hasParametricSorts);
@@ -264,7 +246,16 @@ private BoundedSort infer(Term t, boolean isAnywhereRule, InferenceDriver driver
           driver.sortToBoundedSort(lhsDeclaredPr.production().sort(), lhsDeclaredPr);
       BoundedSort rhsSort = infer(tc.get(1), false, driver);
       driver.constrain(rhsSort, lhsDeclaredSort, (ProductionReference) tc.get(1));
-      return lhsSort;
+    }
+
+    if (tc.production()
+        .klabel()
+        .filter(k -> k.name().equals("#SyntacticCast") || k.name().equals("#SyntacticCastBraced"))
+        .isDefined()) {
+      BoundedSort castedSort = driver.sortToBoundedSort(tc.production().sort(), tc);
+      BoundedSort childSort = infer(tc.get(0), isAnywhereRule, driver);
+      // Constrain castedSort <: childSort, and the general case handles childSort <: castedSort
+      driver.constrain(castedSort, childSort, tc);
     }
 
     for (int prodI = 0, tcI = 0; prodI < tc.production().items().size(); prodI++) {
@@ -277,7 +268,7 @@ private BoundedSort infer(Term t, boolean isAnywhereRule, InferenceDriver driver
       tcI++;
     }
     BoundedSort resSort = new BoundedSort.Variable();
-    driver.constrain(driver.sortToBoundedSort(tc.production().sort(), pr), resSort, pr);
+    driver.constrain(driver.sortToBoundedSort(tc.production().sort(), tc), resSort, tc);
     return resSort;
   }