From 1ddf072e372616c207c7326bc234ded939190662 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Wed, 15 Nov 2023 15:04:47 +0200 Subject: [PATCH 1/2] Add `KItem` subsorts to the disambiguation module when parsing programs (#3814) Previously, when parsing programs, the subsort declarations `syntax KItem ::= Sort` were only added to the parsing module. However, sort inference is run in the disambiguation module, so they should be included there as well. This is necessary for #3601. --- .../org/kframework/parser/inner/RuleGrammarGenerator.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java index 93163bba47b..bf15b74d1a1 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java +++ b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java @@ -569,10 +569,12 @@ public static Tuple3 getCombinedGrammarImpl( // if no start symbol has been defined in the configuration, then use K for (Sort srt : iterable(mod.allSorts())) { if (!isParserSort(srt) && !mod.listSorts().contains(srt)) { - // K ::= Sort + // KItem ::= Sort prods3.add(Production(Seq(), Sorts.KItem(), Seq(NonTerminal(srt)), Att())); } } + // Add KItem subsorts to disambiguation for use by sort inference + disambProds.addAll(prods3); // for each triple, generate a new pattern which works better for parsing lists in programs. prods3.addAll(new HashSet<>(parseProds)); Set res = new HashSet<>(); From 2f7b34488ac47fba355b64cac35266c8e582044a Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Wed, 15 Nov 2023 19:02:44 +0200 Subject: [PATCH 2/2] Clean up cast insertion in `TypeInferenceVisitor` (#3813) This PR removes unused fields from `TypeInferenceVisitor` related to cast insertion then simplifies the algorithm accordingly. The commit history is clean and justifies each step in the clean-up sequentially. --------- Co-authored-by: rv-jenkins --- .../kframework/kompile/DefinitionParsing.java | 1 - .../parser/inner/ParseInModule.java | 30 +-------- .../disambiguation/TypeInferenceVisitor.java | 63 ++++++------------- 3 files changed, 22 insertions(+), 72 deletions(-) diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java index 3accece5257..8a9e2c29e28 100644 --- a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java +++ b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java @@ -929,7 +929,6 @@ private Stream parseBubble( source, startLine, startColumn, - true, isAnywhere); parsedBubbles.getAndIncrement(); registerWarnings(result._2()); 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 5630b4b86c2..38283092a65 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java @@ -12,7 +12,6 @@ import org.apache.commons.io.FileUtils; import org.kframework.attributes.Location; import org.kframework.attributes.Source; -import org.kframework.builtin.Sorts; import org.kframework.definition.Module; import org.kframework.definition.Terminal; import org.kframework.definition.TerminalLike; @@ -211,7 +210,7 @@ public void initialize() { public Tuple2, K>, Set> parseString( String input, Sort startSymbol, Source source) { try (Scanner scanner = getScanner()) { - return parseString(input, startSymbol, "unit test", scanner, source, 1, 1, true, false); + return parseString(input, startSymbol, "unit test", scanner, source, 1, 1, false); } } @@ -281,8 +280,7 @@ public String tokenizeString(String input, Source source) { public Tuple2, K>, Set> parseString( String input, Sort startSymbol, String startSymbolLocation, Source source) { try (Scanner scanner = getScanner()) { - return parseString( - input, startSymbol, startSymbolLocation, scanner, source, 1, 1, true, false); + return parseString(input, startSymbol, startSymbolLocation, scanner, source, 1, 1, false); } } @@ -325,7 +323,6 @@ public Tuple2, K>, Set> parseString( Source source, int startLine, int startColumn, - boolean inferSortChecks, boolean isAnywhere) { final Tuple2, Term>, Set> result = parseStringTerm( @@ -336,7 +333,6 @@ public Tuple2, K>, Set> parseString( source, startLine, startColumn, - inferSortChecks, isAnywhere); Either, K> parseInfo; if (result._1().isLeft()) { @@ -370,7 +366,6 @@ private Tuple2, Term>, Set> parseStringTe Source source, int startLine, int startColumn, - boolean inferSortChecks, boolean isAnywhere) { if (!parsingModule.definedSorts().contains(startSymbol.head())) throw KEMException.innerParserError( @@ -419,10 +414,7 @@ private Tuple2, Term>, Set> parseStringTe } } - rez = - new TypeInferenceVisitor( - currentInferencer, startSymbol, inferSortChecks, true, isAnywhere) - .apply(rez3); + rez = new TypeInferenceVisitor(currentInferencer, startSymbol, isAnywhere).apply(rez3); if (rez.isLeft()) return new Tuple2<>(rez, warn); endTypeInf = profileRules ? System.currentTimeMillis() : 0; @@ -482,20 +474,4 @@ public void close() { } inferencers.clear(); } - - public static Term disambiguateForUnparse(Module mod, Term ambiguity) { - Term rez3 = new PushTopAmbiguityUp().apply(ambiguity); - Either, Term> rez; - Tuple2, Term>, Set> rez2; - try (TypeInferencer inferencer = new TypeInferencer(mod, false)) { - rez = new TypeInferenceVisitor(inferencer, Sorts.K(), false, false, false).apply(rez3); - } - if (rez.isLeft()) { - rez2 = new AmbFilter().apply(rez3); - return rez2._1().right().get(); - } - rez3 = new PushAmbiguitiesDownAndPreferAvoid(mod.overloads()).apply(rez.right().get()); - rez2 = new AmbFilter().apply(rez3); - return rez2._1().right().get(); - } } diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java index 94247730d49..2a4cf418f1e 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java @@ -50,28 +50,17 @@ */ public class TypeInferenceVisitor extends SetsTransformerWithErrors { private final TypeInferencer inferencer; - private final boolean inferSortChecks; - private final boolean inferCasts; private final boolean isAnywhere; private final Sort topSort; /** * @param inferencer * @param topSort The expected sort of the top of the term. - * @param inferSortChecks true if we should add :Sort to variables - * @param inferCasts true if we should add ::Sort to variables * @param isAnywhere true if the term is an anywhere rule */ - public TypeInferenceVisitor( - TypeInferencer inferencer, - Sort topSort, - boolean inferSortChecks, - boolean inferCasts, - boolean isAnywhere) { + public TypeInferenceVisitor(TypeInferencer inferencer, Sort topSort, boolean isAnywhere) { this.inferencer = inferencer; this.topSort = topSort; - this.inferSortChecks = inferSortChecks; - this.inferCasts = inferCasts; this.isAnywhere = isAnywhere; } @@ -190,7 +179,14 @@ public Either, Term> apply(Term t) { public class TypeCheckVisitor extends SetsTransformerWithErrors { private Sort expectedSort; - private boolean hasCastAlready = false, hasCheckAlready = false; + + private enum CastContext { + NONE, + SEMANTIC, + STRICT + }; + + private CastContext castContext = CastContext.NONE; public TypeCheckVisitor(Sort topSort) { this.expectedSort = topSort; @@ -244,7 +240,7 @@ public Either, Term> apply(Term term) { // compute the instantiated production with its sort parameters Production substituted = pr.production().substitute(inferencer.getArgs(pr)); Sort actualSort = substituted.sort(); - boolean isExactSort = hasCastAlready && !hasCheckAlready; + boolean isExactSort = castContext == CastContext.STRICT; // check type: inner casts and syntactic casts indicate type equality, everything else is <= if ((isExactSort && !actualSort.equals(expectedSort)) || (!isExactSort @@ -257,21 +253,17 @@ public Either, Term> apply(Term term) { for (int i = 0, j = 0; i < substituted.items().size(); i++) { if (substituted.items().apply(i) instanceof NonTerminal) { // save prior value of variables - boolean wasCast = hasCastAlready; - boolean wasCheck = hasCheckAlready; + CastContext oldContext = castContext; // compute whether this is a cast already if (substituted.klabel().isDefined() && substituted.klabel().get().name().startsWith("#SemanticCastTo")) { - hasCheckAlready = true; - hasCastAlready = true; + castContext = CastContext.SEMANTIC; } else if (substituted.klabel().isDefined() && (substituted.klabel().get().name().equals("#SyntacticCast") || substituted.klabel().get().name().equals("#InnerCast"))) { - hasCastAlready = true; - hasCheckAlready = false; + castContext = CastContext.STRICT; } else { - hasCastAlready = false; - hasCheckAlready = false; + castContext = CastContext.NONE; } Term t = tc.get(j); Sort oldExpected = expectedSort; @@ -281,8 +273,7 @@ public Either, Term> apply(Term term) { Either, Term> rez = apply(t); // restore values expectedSort = oldExpected; - hasCastAlready = wasCast; - hasCheckAlready = wasCheck; + castContext = oldContext; if (rez.isLeft()) return rez; // apply result of visiting child to the term. tc = tc.with(j, rez.right().get()); @@ -295,33 +286,17 @@ public Either, Term> apply(Term term) { } private Either, Term> wrapTermWithCast(Constant c, Sort declared) { - Production cast; - if (inferSortChecks && !hasCheckAlready) { - // strictly typing variables and one does not already exist, so add :Sort - cast = + if (castContext != CastContext.SEMANTIC) { + // There isn't an existing :Sort, so add one + Production cast = inferencer .module() .productionsFor() .apply(KLabel("#SemanticCastTo" + declared.toString())) .head(); - } else if (inferCasts - && !hasCastAlready - && inferencer.module().productionsFor().contains(KLabel("#SyntacticCast"))) { - // casting variables and one doeds not already exist, so add ::Sort - cast = - stream(inferencer.module().productionsFor().apply(KLabel("#SyntacticCast"))) - .filter(p -> p.sort().equals(declared)) - .findAny() - .get(); - } else { - // unparsing or cast already exists, so do nothing - cast = null; - } - if (cast == null) { - return Right.apply(c); - } else { return Right.apply(TermCons.apply(ConsPStack.singleton(c), cast, c.location(), c.source())); } + return Right.apply(c); } } }