From 213f2af2bc3d3d312414ac992e79e07c94d6e212 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Sun, 17 Dec 2023 16:19:31 -0500 Subject: [PATCH 1/5] Improve --type-inference-mode checked error message --- .../parser/inner/ParseInModule.java | 28 ++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java index f1dea8b64de..e671e13f5ac 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java @@ -445,7 +445,7 @@ private Tuple2, Term>, Set> parseStringTe boolean equalRight = rez.isRight() && z3Rez.isRight() && rez.right().get().equals(z3Rez.right().get()); if (!(bothLeft || equalRight)) { - throw KEMException.criticalError("Z3 and SimpleSub algorithms differ!"); + throw typeInferenceCheckError(rez3, z3Rez, rez); } } else { rez = z3Rez; @@ -495,6 +495,32 @@ private Tuple2, Term>, Set> parseStringTe } } + private static KEMException typeInferenceCheckError( + Term term, Either, Term> z3, Either, Term> simple) { + StringBuilder msg = new StringBuilder("Z3 and SimpleSub sort inference algorithms differ!\n"); + msg.append(term.source().isPresent() ? term.source().get().toString() : "").append("\n"); + msg.append(term.location().isPresent() ? term.location().get().toString() : "").append("\n"); + msg.append("\nZ3:\n"); + if (z3.isLeft()) { + msg.append( + z3.left().get().stream().map(KEMException::getMessage).collect(Collectors.joining("\n"))); + } else { + msg.append(z3.right().get()); + } + msg.append("\n"); + msg.append("\nSimpleSub:\n"); + if (simple.isLeft()) { + msg.append( + simple.left().get().stream() + .map(KEMException::getMessage) + .collect(Collectors.joining("\n"))); + } else { + msg.append(simple.right().get()); + } + msg.append("\n"); + return KEMException.criticalError(msg.toString()); + } + private boolean isDebug(Source source, int startLine) { if (typeInferenceDebug == null) { return false; From a9bac14d2e27f62e165710f709b4cd865d334994 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Sun, 17 Dec 2023 17:02:05 -0500 Subject: [PATCH 2/5] Add missing production constraints for anywhere rules --- .../disambiguation/inference/SortInferencer.java | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) 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..6f4533cc434 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 @@ -259,12 +259,21 @@ private BoundedSort infer(Term t, boolean isAnywhereRule, InferenceDriver driver // Note that we do actually need the LHS's declared sort. The LHS's inferred sort // is a variable X with a bound L <: X, and constraining against X would just add a // new lower bound aka permit widening. + // + // It's also safe to assume the LHS is not an Ambiguity due to PushTopAmbiguitiesUp ProductionReference lhsDeclaredPr = (ProductionReference) stripBrackets(tc.get(0)); BoundedSort lhsDeclaredSort = driver.sortToBoundedSort(lhsDeclaredPr.production().sort(), lhsDeclaredPr); BoundedSort rhsSort = infer(tc.get(1), false, driver); driver.constrain(rhsSort, lhsDeclaredSort, (ProductionReference) tc.get(1)); - return lhsSort; + + // Handle usual production constraints + BoundedSort rewriteParam = driver.sortToBoundedSort(tc.production().sort(), tc); + driver.constrain(lhsSort, rewriteParam, tc); + driver.constrain(rhsSort, rewriteParam, tc); + BoundedSort resSort = new BoundedSort.Variable(); + driver.constrain(rewriteParam, resSort, tc); + return resSort; } for (int prodI = 0, tcI = 0; prodI < tc.production().items().size(); prodI++) { From 23aa1e73be2fbff70deb539f4aae01435836e8da Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Sun, 17 Dec 2023 17:16:49 -0500 Subject: [PATCH 3/5] Add support for strict casts --- .../inference/InferenceDriver.java | 6 +++ .../inference/SortInferencer.java | 46 +++++++------------ 2 files changed, 23 insertions(+), 29 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java index c038c4620ef..7b724a79805 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java @@ -75,6 +75,12 @@ public BoundedSort sortToBoundedSort(Sort sort, ProductionReference prOrNull) { return new BoundedSort.Constructor(sort.head()); } + public BoundedSort returnSort(ProductionReference pr) throws ConstraintError { + BoundedSort resSort = new BoundedSort.Variable(); + constrain(sortToBoundedSort(pr.production().sort(), pr), resSort, pr); + return resSort; + } + /** * Update sub-/super-type constraints to record the fact that lhs <: rhs. * 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 6f4533cc434..90f3d1c7dbf 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 @@ -19,7 +19,6 @@ import org.kframework.definition.Module; import org.kframework.definition.NonTerminal; import org.kframework.definition.Production; -import org.kframework.kore.KLabel; import org.kframework.kore.Sort; import org.kframework.kore.SortHead; import org.kframework.parser.Ambiguity; @@ -88,10 +87,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 +103,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); @@ -271,23 +252,30 @@ private BoundedSort infer(Term t, boolean isAnywhereRule, InferenceDriver driver BoundedSort rewriteParam = driver.sortToBoundedSort(tc.production().sort(), tc); driver.constrain(lhsSort, rewriteParam, tc); driver.constrain(rhsSort, rewriteParam, tc); - BoundedSort resSort = new BoundedSort.Variable(); - driver.constrain(rewriteParam, resSort, tc); - return resSort; + return driver.returnSort(tc); + } + + 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); + driver.constrain(castedSort, childSort, tc); + driver.constrain(childSort, castedSort, tc); + return driver.returnSort(tc); } for (int prodI = 0, tcI = 0; prodI < tc.production().items().size(); prodI++) { if (!(tc.production().items().apply(prodI) instanceof NonTerminal nt)) { continue; } - BoundedSort expectedSort = driver.sortToBoundedSort(nt.sort(), pr); + BoundedSort expectedSort = driver.sortToBoundedSort(nt.sort(), tc); BoundedSort childSort = infer(tc.get(tcI), isAnywhereRule, driver); - driver.constrain(childSort, expectedSort, pr); + driver.constrain(childSort, expectedSort, tc); tcI++; } - BoundedSort resSort = new BoundedSort.Variable(); - driver.constrain(driver.sortToBoundedSort(tc.production().sort(), pr), resSort, pr); - return resSort; + return driver.returnSort(tc); } /** From 5954a3b128a6c5dadfbeb96df73473a4328efb3b Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Sun, 17 Dec 2023 18:59:21 -0500 Subject: [PATCH 4/5] Temporarily enable CHECKED for a CI run --- .../main/java/org/kframework/parser/inner/ParseInModule.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java index e671e13f5ac..ff0206b0ae5 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java @@ -142,7 +142,7 @@ private ParseInModule( this.typeInferenceDebug = typeInferenceDebug; this.typeInferenceMode = typeInferenceMode == InnerParsingOptions.TypeInferenceMode.DEFAULT - ? InnerParsingOptions.TypeInferenceMode.Z3 + ? InnerParsingOptions.TypeInferenceMode.CHECKED : typeInferenceMode; this.partialParseDebug = partialParseDebug; } From 776df3fcc6ff3e2d2bc845b1d639e347ba0c8f4f Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Sun, 17 Dec 2023 19:46:22 -0500 Subject: [PATCH 5/5] Disable CHECKED for merge --- .../main/java/org/kframework/parser/inner/ParseInModule.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java index ff0206b0ae5..e671e13f5ac 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java @@ -142,7 +142,7 @@ private ParseInModule( this.typeInferenceDebug = typeInferenceDebug; this.typeInferenceMode = typeInferenceMode == InnerParsingOptions.TypeInferenceMode.DEFAULT - ? InnerParsingOptions.TypeInferenceMode.CHECKED + ? InnerParsingOptions.TypeInferenceMode.Z3 : typeInferenceMode; this.partialParseDebug = partialParseDebug; }