Skip to content

Tighten rules about anywhere rules #507

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

Merged
dwightguth merged 4 commits into from
Jun 3, 2019
Merged

Tighten rules about anywhere rules #507

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4590864
tests
May 28, 2019
74c3185
enforce rhs <= lhs of anywhere rules
May 28, 2019
fba0c01
fix bug
May 28, 2019
77e2f1d
fix bug in output file
May 28, 2019
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
8 changes: 8 additions & 0 deletions k-distribution/tests/regression-new/checks/wideningAnywhere.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
module WIDENINGANYWHERE

syntax Foo ::= "foo"
syntax KItem ::= "bar"

rule foo => bar [anywhere]

endmodule
8 changes: 8 additions & 0 deletions k-distribution/tests/regression-new/checks/wideningAnywhere.k.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
[Error] Compiler: Had 1 parsing errors.
[Error] Critical: Unexpected sort KItem for term parsed as production syntax
KItem ::= "bar". Expected Foo.
Source(wideningAnywhere.k)
Location(6,13,6,16)
[Warning] Compiler: Could not find main syntax module with name
WIDENINGANYWHERE-SYNTAX in definition. Use --syntax-module to specify one.
Using WIDENINGANYWHERE as default.
2 changes: 1 addition & 1 deletion kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -396,7 +396,7 @@ private Stream<? extends K> performParse(Map<String, ParsedSentence> cache, Pars
return Stream.of(parse.getParse());
}
}
result = parser.parseString(b.contents(), START_SYMBOL, scanner, source, startLine, startColumn, true);
result = parser.parseString(b.contents(), START_SYMBOL, scanner, source, startLine, startColumn, true, b.att().contains("anywhere"));
parsedBubbles.getAndIncrement();
if (kem.options.warnings2errors && !result._2().isEmpty()) {
for (KEMException err : result._2()) {
Expand Down
16 changes: 8 additions & 8 deletions kernel/src/main/java/org/kframework/parser/concrete2kore/ParseInModule.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ public void initialize() {
public Tuple2<Either<Set<ParseFailedException>, K>, Set<ParseFailedException>>
parseString(String input, Sort startSymbol, Source source) {
try (Scanner scanner = getScanner()) {
return parseString(input, startSymbol, scanner, source, 1, 1, true);
return parseString(input, startSymbol, scanner, source, 1, 1, true, false);
}
}

Expand All @@ -139,9 +139,9 @@ public Scanner getScanner() {
}

public Tuple2<Either<Set<ParseFailedException>, K>, Set<ParseFailedException>>
parseString(String input, Sort startSymbol, Scanner scanner, Source source, int startLine, int startColumn, boolean inferSortChecks) {
parseString(String input, Sort startSymbol, Scanner scanner, Source source, int startLine, int startColumn, boolean inferSortChecks, boolean isAnywhere) {
final Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>> result
= parseStringTerm(input, startSymbol, scanner, source, startLine, startColumn, inferSortChecks);
= parseStringTerm(input, startSymbol, scanner, source, startLine, startColumn, inferSortChecks, isAnywhere);
Either<Set<ParseFailedException>, K> parseInfo;
if (result._1().isLeft()) {
parseInfo = Left.apply(result._1().left().get());
Expand All @@ -168,7 +168,7 @@ public Scanner getScanner() {
* @return
*/
private Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>>
parseStringTerm(String input, Sort startSymbol, Scanner scanner, Source source, int startLine, int startColumn, boolean inferSortChecks) {
parseStringTerm(String input, Sort startSymbol, Scanner scanner, Source source, int startLine, int startColumn, boolean inferSortChecks, boolean isAnywhere) {
scanner = getGrammar(scanner);

long start = 0;
Expand Down Expand Up @@ -209,10 +209,10 @@ public Scanner getScanner() {
if (rez.isLeft())
return new Tuple2<>(rez, warn);
Term rez3 = new PushTopAmbiguityUp().apply(rez.right().get());
rez = new ApplyTypeCheckVisitor(disambModule.subsorts()).apply(rez3);
rez = new ApplyTypeCheckVisitor(disambModule.subsorts(), isAnywhere).apply(rez3);
if (rez.isLeft())
return new Tuple2<>(rez, warn);
Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>> rez2 = new VariableTypeInferenceFilter(disambModule.subsorts(), disambModule.definedSorts(), disambModule.productionsFor(), strict && inferSortChecks, true).apply(rez.right().get());
Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>> rez2 = new VariableTypeInferenceFilter(disambModule.subsorts(), disambModule.definedSorts(), disambModule.productionsFor(), strict && inferSortChecks, true, isAnywhere).apply(rez.right().get());
if (rez2._1().isLeft())
return rez2;
warn = rez2._2();
Expand Down Expand Up @@ -270,13 +270,13 @@ public void close() {

public static Term disambiguateForUnparse(Module mod, Term ambiguity) {
Term rez3 = new PushTopAmbiguityUp().apply(ambiguity);
Either<Set<ParseFailedException>, Term> rez = new ApplyTypeCheckVisitor(mod.subsorts()).apply(rez3);
Either<Set<ParseFailedException>, Term> rez = new ApplyTypeCheckVisitor(mod.subsorts(), false).apply(rez3);
Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>> rez2;
if (rez.isLeft()) {
rez2 = new AmbFilter(false).apply(rez3);
return rez2._1().right().get();
}
rez2 = new VariableTypeInferenceFilter(mod.subsorts(), mod.definedSorts(), mod.productionsFor(), false, false).apply(rez.right().get());
rez2 = new VariableTypeInferenceFilter(mod.subsorts(), mod.definedSorts(), mod.productionsFor(), false, false, false).apply(rez.right().get());
if (rez2._1().isLeft()) {
rez2 = new AmbFilter(false).apply(rez.right().get());
return rez2._1().right().get();
Expand Down
6 changes: 4 additions & 2 deletions ...c/main/java/org/kframework/parser/concrete2kore/disambiguation/ApplyTypeCheckVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,11 @@

public class ApplyTypeCheckVisitor extends SetsTransformerWithErrors<ParseFailedException> {
private final POSet<Sort> subsorts;
private final boolean isAnywhere;

public ApplyTypeCheckVisitor(POSet<Sort> subsorts) {
public ApplyTypeCheckVisitor(POSet<Sort> subsorts, boolean isAnywhere) {
this.subsorts = subsorts;
this.isAnywhere = isAnywhere;
}

public Either<java.util.Set<ParseFailedException>, Term> apply(TermCons tc) {
Expand All @@ -39,7 +41,7 @@ public Either<java.util.Set<ParseFailedException>, Term> apply(TermCons tc) {
&& (tc.production().klabel().get().name().equals("#SyntacticCast")
|| tc.production().klabel().get().name().startsWith("#SemanticCastTo")
|| tc.production().klabel().get().name().equals("#InnerCast"))
|| (VariableTypeInferenceFilter.isFunctionRule(tc) && j == 0)) {
|| (VariableTypeInferenceFilter.isFunctionRule(tc, isAnywhere) && j == 0)) {
Term t = tc.get(0);
boolean strict = tc.production().klabel().get().name().equals("#SyntacticCast") || tc.production().klabel().get().name().equals("#InnerCast");
Either<Set<ParseFailedException>, Term> rez = new ApplyTypeCheck2(VariableTypeInferenceFilter.getSortOfCast(tc), strict).apply(t);
Expand Down
16 changes: 9 additions & 7 deletions .../java/org/kframework/parser/concrete2kore/disambiguation/VariableTypeInferenceFilter.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,14 +52,16 @@ public enum VarType { CONTEXT, USER }
private final scala.collection.Map<KLabel, scala.collection.Set<Production>> productions;
private final boolean inferSortChecks;
private final boolean inferCasts;
private final boolean isAnywhere;
private Set<ParseFailedException> warnings = Sets.newHashSet();
public VariableTypeInferenceFilter(POSet<Sort> subsorts, scala.collection.Set<Sort> sortSet, scala.collection.Map<
KLabel, scala.collection.Set<Production>> productions, boolean inferSortChecks, boolean inferCasts) {
KLabel, scala.collection.Set<Production>> productions, boolean inferSortChecks, boolean inferCasts, boolean isAnywhere) {
this.subsorts = subsorts;
this.sortSet = sortSet;
this.productions = productions;
this.inferSortChecks = inferSortChecks;
this.inferCasts = inferCasts;
this.isAnywhere = isAnywhere;
}

/** Return the set of all known sorts which are a lower bound on
Expand Down Expand Up @@ -368,16 +370,16 @@ public String toString() {
}
}

public static boolean isFunctionRule(TermCons tc) {
if ((tc.production().sort().name().equals("#RuleContent") || tc.production().sort().name().equals("#RuleBody")) && !(tc.get(0) instanceof TermCons && isFunctionRule((TermCons)tc.get(0)))) {
public static boolean isFunctionRule(TermCons tc, boolean isAnywhere) {
if ((tc.production().sort().name().equals("#RuleContent") || tc.production().sort().name().equals("#RuleBody")) && !(tc.get(0) instanceof TermCons && isFunctionRule((TermCons)tc.get(0), isAnywhere))) {
ProductionReference child = (ProductionReference) tc.get(0);
if (child.production().klabel().isDefined() && child.production().klabel().get().name().equals("#withConfig")) {
child = (ProductionReference)((TermCons)child).get(0);
}
if (child.production().klabel().isDefined() && child.production().klabel().get().equals(KLabels.KREWRITE)) {
child = (ProductionReference)((TermCons)child).get(0);
}
return child.production().att().contains(Attribute.FUNCTION_KEY);
return child.production().att().contains(Attribute.FUNCTION_KEY) || isAnywhere;
}
return false;
}
Expand Down Expand Up @@ -423,7 +425,7 @@ public Tuple2<Either<java.util.Set<ParseFailedException>, Term>, java.util.Set<V
|| tc.production().klabel().get().name().equals("#InnerCast"))) {
Term t = tc.get(0);
collector = new CollectVariables2(getSortOfCast(tc), VarType.USER).apply(t)._2();
} else if (tc.production().klabel().isDefined() && isFunctionRule(tc) && j == 0) {
} else if (tc.production().klabel().isDefined() && isFunctionRule(tc, isAnywhere) && j == 0) {
Term t = tc.get(0);
collector = new CollectVariables2(getSortOfCast(tc), VarType.CONTEXT).apply(t)._2();
j++;
Expand Down Expand Up @@ -476,7 +478,7 @@ public Either<java.util.Set<ParseFailedException>, Term> apply(TermCons tc) {
&& (tc.production().klabel().get().name().equals("#SyntacticCast")
|| tc.production().klabel().get().name().startsWith("#SemanticCastTo")
|| tc.production().klabel().get().name().equals("#InnerCast")
|| (isFunctionRule(tc)) && j == 0)) {
|| (isFunctionRule(tc, isAnywhere)) && j == 0)) {
Term t = tc.get(0);
boolean strictSortEquality = tc.production().klabel().get().name().equals("#SyntacticCast") || tc.production().klabel().get().name().equals("#InnerCast");
Either<Set<ParseFailedException>, Term> rez = new ApplyTypeCheck2(getSortOfCast(tc), true, strictSortEquality, strictSortEquality && inferSortChecks).apply(t);
Expand Down Expand Up @@ -651,7 +653,7 @@ public Term apply(TermCons tc) {
&& (tc.production().klabel().get().name().equals("#SyntacticCast")
|| tc.production().klabel().get().name().startsWith("#SemanticCastTo")
|| tc.production().klabel().get().name().equals("#InnerCast"))
|| (isFunctionRule(tc) && j == 0)) {
|| (isFunctionRule(tc, isAnywhere) && j == 0)) {
Term t = tc.get(0);
new CollectUndeclaredVariables2(getSortOfCast(tc)).apply(t);
j++;
Expand Down