Skip to content

Commit

Permalink
Merge branch 'develop' into _update-deps/runtimeverification/hs-backe…
Browse files Browse the repository at this point in the history 
…nd-booster
  • Loading branch information
@rv-jenkins
rv-jenkins authored Nov 15, 2023
2 parents a9379b0 + 2f7b344 commit 18f6198
Show file tree
Hide file tree
Showing 4 changed files with 25 additions and 73 deletions.
1 change: 0 additions & 1 deletion kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -929,7 +929,6 @@ private Stream<? extends K> parseBubble(
source,
startLine,
startColumn,
true,
isAnywhere);
parsedBubbles.getAndIncrement();
registerWarnings(result._2());
Expand Down
30 changes: 3 additions & 27 deletions kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -211,7 +210,7 @@ public void initialize() {
public Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> 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);
}
}

Expand Down Expand Up @@ -281,8 +280,7 @@ public String tokenizeString(String input, Source source) {
public Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> 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);
}
}

Expand Down Expand Up @@ -325,7 +323,6 @@ public Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> parseString(
Source source,
int startLine,
int startColumn,
boolean inferSortChecks,
boolean isAnywhere) {
final Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> result =
parseStringTerm(
Expand All @@ -336,7 +333,6 @@ public Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> parseString(
source,
startLine,
startColumn,
inferSortChecks,
isAnywhere);
Either<Set<KEMException>, K> parseInfo;
if (result._1().isLeft()) {
Expand Down Expand Up @@ -370,7 +366,6 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> parseStringTe
Source source,
int startLine,
int startColumn,
boolean inferSortChecks,
boolean isAnywhere) {
if (!parsingModule.definedSorts().contains(startSymbol.head()))
throw KEMException.innerParserError(
Expand Down Expand Up @@ -419,10 +414,7 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> 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;

Expand Down Expand Up @@ -482,20 +474,4 @@ public void close() {
}
inferencers.clear();
}

public static Term disambiguateForUnparse(Module mod, Term ambiguity) {
Term rez3 = new PushTopAmbiguityUp().apply(ambiguity);
Either<Set<KEMException>, Term> rez;
Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> 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();
}
}
4 changes: 3 additions & 1 deletion kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -569,10 +569,12 @@ public static Tuple3<Module, Module, Module> 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<Sentence> res = new HashSet<>();
Expand Down
63 changes: 19 additions & 44 deletions kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,28 +50,17 @@
*/
public class TypeInferenceVisitor extends SetsTransformerWithErrors<KEMException> {
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;
}

Expand Down Expand Up @@ -190,7 +179,14 @@ public Either<Set<KEMException>, Term> apply(Term t) {
public class TypeCheckVisitor extends SetsTransformerWithErrors<KEMException> {

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;
Expand Down Expand Up @@ -244,7 +240,7 @@ public Either<Set<KEMException>, 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
Expand All @@ -257,21 +253,17 @@ public Either<Set<KEMException>, 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;
Expand All @@ -281,8 +273,7 @@ public Either<Set<KEMException>, Term> apply(Term term) {
Either<Set<KEMException>, 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());
Expand All @@ -295,33 +286,17 @@ public Either<Set<KEMException>, Term> apply(Term term) {
}

private Either<Set<KEMException>, 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);
}
}
}

0 comments on commit 18f6198

Please sign in to comment.