Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support strict casts in the SimpleSub inferencer #3870

Merged
merged 6 commits into from
Dec 18, 2023
Merged

Support strict casts in the SimpleSub inferencer #3870

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
213f2af
Improve --type-inference-mode checked error message
Scott-Guest Dec 17, 2023
a9bac14
Add missing production constraints for anywhere rules
Scott-Guest Dec 17, 2023
23aa1e7
Add support for strict casts
Scott-Guest Dec 17, 2023
5954a3b
Temporarily enable CHECKED for a CI run
Scott-Guest Dec 17, 2023
776df3f
Disable CHECKED for merge
Scott-Guest Dec 18, 2023
818ef2b
Merge branch 'develop' into simplesub-strict-casts
Scott-Guest Dec 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 27 additions & 1 deletion kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -445,7 +445,7 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> 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);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you have any examples of such differences?
It would be interesting to document them and add regression tests.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not aware of any actual differences - the improved error message was just useful while debugging when I unintentionally broke something and caused a difference

}
} else {
rez = z3Rez;
Expand Down Expand Up @@ -495,6 +495,32 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> parseStringTe
}
}

private static KEMException typeInferenceCheckError(
Term term, Either<Set<KEMException>, Term> z3, Either<Set<KEMException>, 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;
Expand Down
6 changes: 6 additions & 0 deletions ...l/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
*
Expand Down
51 changes: 24 additions & 27 deletions ...el/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) {
Expand All @@ -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);
Expand Down Expand Up @@ -259,26 +240,42 @@ 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);
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);
}

/**
Expand Down