Skip to content

Commit aca882d

Browse files
coscos
committed
Merge remote-tracking branch 'origin/master' into kore
Conflicts: k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java kernel/src/main/java/org/kframework/parser/concrete2kore/disambiguation/TreeCleanerVisitor.java Former-commit-id: 461d89d48687b5a6357b8ba002d17d2d6fe0bdce [formerly 567f0636a9ed682e2acf08a0b3e622d53fbb500c] Former-commit-id: ef3231b1b13f5f7307d44d41f7ffee6128051751
2 parents 1a5dbec + 61a0209 commit aca882d

36 files changed

Lines changed: 1363 additions & 165 deletions

File tree

‎java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinIntOperations.java‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,11 +24,19 @@ public static IntToken mul(IntToken term1, IntToken term2, TermContext context)
2424
}
2525

2626
public static IntToken div(IntToken term1, IntToken term2, TermContext context) {
27-
return IntToken.of(term1.bigIntegerValue().divide(term2.bigIntegerValue()));
27+
try {
28+
return IntToken.of(term1.bigIntegerValue().divide(term2.bigIntegerValue()));
29+
} catch (ArithmeticException e) {
30+
return null;
31+
}
2832
}
2933

3034
public static IntToken rem(IntToken term1, IntToken term2, TermContext context) {
31-
return IntToken.of(term1.bigIntegerValue().remainder(term2.bigIntegerValue()));
35+
try {
36+
return IntToken.of(term1.bigIntegerValue().remainder(term2.bigIntegerValue()));
37+
} catch (ArithmeticException e) {
38+
return null;
39+
}
3240
}
3341

3442
public static IntToken mod(IntToken term1, IntToken term2, TermContext context) {

‎java-backend/src/main/java/org/kframework/backend/java/compile/DataStructureToLookupUpdate.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -231,7 +231,7 @@ public ASTNode visit(Rule node, Void _void) {
231231
((BuiltinLookup) queue.get(i)).variables(),
232232
((BuiltinLookup) queue.get(j)).variables());
233233
if (!commonVariables.isEmpty()) {
234-
throw KExceptionManager.criticalError("Unsupported map pattern in the rule left-hand side", node);
234+
throw KExceptionManager.criticalError("Unsupported map, list, or set pattern in the rule left-hand side", node);
235235
}
236236
}
237237
}
@@ -258,7 +258,7 @@ public ASTNode visit(Rule node, Void _void) {
258258
if (setLookup.key() instanceof Variable && !variables.contains(setLookup.key())) {
259259
lookups.add(new SetLookup(setLookup.base(), setLookup.key(), true));
260260
} else {
261-
throw KExceptionManager.criticalError("Unsupported map pattern in the rule left-hand side", node);
261+
throw KExceptionManager.criticalError("Unsupported set pattern in the rule left-hand side", node);
262262
}
263263
} else {
264264
assert false: "unexpected builtin data structure type";

‎java-backend/src/main/java/org/kframework/backend/java/kil/Definition.java‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -410,8 +410,16 @@ public RuleIndex getIndex() {
410410
return index;
411411
}
412412

413-
public Map<KItem.CacheTableColKey, KItem.CacheTableValue> getSortCacheTable() {
414-
return sortCacheTable;
413+
public KItem.CacheTableValue getSortCacheValue(KItem.CacheTableColKey key) {
414+
synchronized(sortCacheTable) {
415+
return sortCacheTable.get(key);
416+
}
417+
}
418+
419+
public void putSortCacheValue(KItem.CacheTableColKey key, KItem.CacheTableValue value) {
420+
synchronized(sortCacheTable) {
421+
sortCacheTable.put(key, value);
422+
}
415423
}
416424

417425
// added from context

‎java-backend/src/main/java/org/kframework/backend/java/kil/KItem.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@
1818
import org.kframework.backend.java.util.Subsorts;
1919
import org.kframework.backend.java.util.Utils;
2020
import org.kframework.kil.*;
21-
import org.kframework.kore.KApply;
2221
import org.kframework.main.GlobalOptions;
2322
import org.kframework.main.Tool;
2423
import org.kframework.utils.errorsystem.KException.ExceptionType;
@@ -126,7 +125,7 @@ private KItem(Term kLabel, Term kList, TermContext termContext, Tool tool, Sourc
126125
&& definition.sortPredicateRulesOn(kLabelConstant).isEmpty();
127126
if (enableCache) {
128127
cacheTabColKey = new CacheTableColKey(kLabelConstant, (KList) kList);
129-
cacheTabVal = definition.getSortCacheTable().get(cacheTabColKey);
128+
cacheTabVal = definition.getSortCacheValue(cacheTabColKey);
130129
if (cacheTabVal != null) {
131130
sort = cacheTabVal.sort;
132131
isExactSort = cacheTabVal.isExactSort;
@@ -237,7 +236,9 @@ private void computeSort() {
237236
Sort sort = sorts.isEmpty() ? kind.asSort() : subsorts.getGLBSort(sorts);
238237
if (sort == null) {
239238
throw KExceptionManager.criticalError("Cannot compute least sort of term: " +
240-
this.toString() + "\nPossible least sorts are: " + sorts);
239+
this.toString() + "\nPossible least sorts are: " + sorts +
240+
"\nAll terms must have a unique least sort; " +
241+
"consider assigning unique KLabels to overloaded productions", this);
241242
}
242243
/* the sort is exact iff the klabel is a constructor and there is no other possible sort */
243244
boolean isExactSort = kLabelConstant.isConstructor() && possibleSorts.isEmpty();
@@ -250,7 +251,7 @@ private void computeSort() {
250251
CacheTableValue cacheTabVal = new CacheTableValue(sort, isExactSort, possibleSorts);
251252

252253
if (enableCache) {
253-
definition.getSortCacheTable().put(new CacheTableColKey(kLabelConstant, (KList) kList), cacheTabVal);
254+
definition.putSortCacheValue(new CacheTableColKey(kLabelConstant, (KList) kList), cacheTabVal);
254255
}
255256
}
256257

‎k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ public DefinitionWithContext(Definition d, Context c) {
4949

5050
private File testResource(String baseName) {
5151
return new File(new File("k-distribution/src/test/resources" + baseName)
52-
.getAbsoluteFile().toString().replaceAll("k-distribution.k-distribution", "k-distribution"));
52+
.getAbsoluteFile().toString().replace("k-distribution" + File.separator + "k-distribution", "k-distribution"));
5353
// a bit of a hack to get around not having a clear working directory
5454
// Eclipse runs tests within k/k-distribution, IntelliJ within /k
5555
}

‎k-distribution/src/test/java/org/kframework/kore/convertors/BubbleParsing.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -24,11 +24,11 @@
2424
import org.kframework.parser.Ambiguity;
2525
import org.kframework.parser.Term;
2626
import org.kframework.parser.TreeNodesToKORE;
27-
import org.kframework.parser.concrete2kore.Grammar;
28-
import org.kframework.parser.concrete2kore.KSyntax2GrammarStatesFilter;
29-
import org.kframework.parser.concrete2kore.Parser;
30-
import org.kframework.parser.concrete2kore.Parser.ParseError;
31-
import org.kframework.parser.concrete2kore.TreeCleanerVisitor;
27+
import org.kframework.parser.concrete2kore.kernel.Grammar;
28+
import org.kframework.parser.concrete2kore.kernel.KSyntax2GrammarStatesFilter;
29+
import org.kframework.parser.concrete2kore.kernel.Parser;
30+
import org.kframework.parser.concrete2kore.kernel.Parser.ParseError;
31+
import org.kframework.parser.concrete2kore.disambiguation.TreeCleanerVisitor;
3232
import org.kframework.parser.outer.Outer;
3333

3434
/**

‎kernel/src/main/java/org/kframework/main/GlobalOptions.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,12 @@ public GlobalOptions() {}
1818
@Inject
1919
public GlobalOptions(Void v) {}
2020

21+
public GlobalOptions(boolean debug, Warnings warnings, boolean verbose) {
22+
this.debug = debug;
23+
this.warnings = warnings;
24+
this.verbose = verbose;
25+
}
26+
2127
public static enum Warnings {
2228
/**
2329
* All warnings and errors

‎kernel/src/main/java/org/kframework/parser/concrete2kore/ParseInModule.java‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework.parser.concrete2kore;
3+
4+
import org.kframework.definition.Module;
5+
import org.kframework.parser.Ambiguity;
6+
import org.kframework.parser.Term;
7+
import org.kframework.parser.concrete2kore.disambiguation.AmbFilter;
8+
import org.kframework.parser.concrete2kore.disambiguation.CorrectCastPriorityVisitor;
9+
import org.kframework.parser.concrete2kore.disambiguation.CorrectKSeqPriorityVisitor;
10+
import org.kframework.parser.concrete2kore.disambiguation.CorrectRewritePriorityVisitor;
11+
import org.kframework.parser.concrete2kore.disambiguation.PreferAvoidVisitor;
12+
import org.kframework.parser.concrete2kore.disambiguation.PriorityVisitor;
13+
import org.kframework.parser.concrete2kore.disambiguation.TreeCleanerVisitor;
14+
import org.kframework.parser.concrete2kore.disambiguation.VariableTypeInferenceFilter;
15+
import org.kframework.parser.concrete2kore.kernel.Grammar;
16+
import org.kframework.parser.concrete2kore.kernel.KSyntax2GrammarStatesFilter;
17+
import org.kframework.parser.concrete2kore.kernel.Parser;
18+
import org.kframework.utils.errorsystem.ParseFailedException;
19+
import scala.Tuple2;
20+
import scala.util.Either;
21+
import scala.util.Right;
22+
23+
import java.io.Serializable;
24+
import java.util.Set;
25+
26+
/**
27+
* A wrapper that takes a module and one can call the parser
28+
* for that module in thread safe way.
29+
* Declarative disambiguation filters are also applied.
30+
*/
31+
public class ParseInModule implements Serializable {
32+
private final Module module;
33+
private final Grammar grammar;
34+
public ParseInModule(Module module) {
35+
this.module = module;
36+
this.grammar = KSyntax2GrammarStatesFilter.getGrammar(module);
37+
}
38+
39+
/**
40+
* Parse as input the given string and start symbol using the module stored in the object.
41+
* @param input the string to parse.
42+
* @param startSymbol the start symbol from which to parse.
43+
* @return the Term representation of the parsed input.
44+
*/
45+
// TODO: require source location to this call
46+
// TODO: figure out how to handle parsing errors
47+
public Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>> parseString(CharSequence input, String startSymbol) {
48+
Parser parser = new Parser(input);
49+
Term parsed = parser.parse(grammar.get(startSymbol), 0);
50+
51+
if (parsed.equals(Ambiguity.apply())) {
52+
Parser.ParseError errors = parser.getErrors();
53+
throw new AssertionError("There are parsing errors: " + errors.toString());
54+
}
55+
Set<ParseFailedException> warn = new AmbFilter().warningUnit();
56+
57+
Either<Set<ParseFailedException>, Term> rez = new TreeCleanerVisitor().apply(parsed);
58+
if (rez.isLeft())
59+
return new Tuple2<>(rez, warn);
60+
rez = new CorrectRewritePriorityVisitor().apply(rez.right().get());
61+
if (rez.isLeft())
62+
return new Tuple2<>(rez, warn);
63+
rez = new CorrectKSeqPriorityVisitor().apply(rez.right().get());
64+
if (rez.isLeft())
65+
return new Tuple2<>(rez, warn);
66+
rez = new CorrectCastPriorityVisitor().apply(rez.right().get());
67+
if (rez.isLeft())
68+
return new Tuple2<>(rez, warn);
69+
rez = new PriorityVisitor(module.priorities(), module.leftAssoc(), module.rightAssoc()).apply(rez.right().get());
70+
if (rez.isLeft())
71+
return new Tuple2<>(rez, warn);
72+
Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>> rez2 = new VariableTypeInferenceFilter(module.subsorts(), module.definedSorts()).apply(rez.right().get());
73+
if (rez2._1().isLeft())
74+
return rez2;
75+
warn = rez2._2();
76+
77+
Term rez3 = new PreferAvoidVisitor().apply(rez2._1().right().get());
78+
rez2 = new AmbFilter().apply(rez3);
79+
warn = new AmbFilter().mergeWarnings(rez2._2(), warn);
80+
81+
return new Tuple2<>(Right.apply(rez2._1().right().get()), warn);
82+
}
83+
}

‎kernel/src/main/java/org/kframework/parser/concrete2kore/ParserUtils.java‎

Lines changed: 36 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -2,16 +2,13 @@
22
package org.kframework.parser.concrete2kore;
33

44
import org.apache.commons.io.FileUtils;
5+
import org.kframework.definition.Module;
56
import org.kframework.kil.Definition;
67
import org.kframework.kil.Sources;
78
import org.kframework.kore.K;
89
import org.kframework.kore.convertors.KILtoKORE;
9-
import org.kframework.definition.Module;
10-
import org.kframework.parser.Ambiguity;
1110
import org.kframework.parser.Term;
1211
import org.kframework.parser.TreeNodesToKORE;
13-
import org.kframework.parser.concrete2kore.disambiguation.PreferAvoidVisitor;
14-
import org.kframework.parser.concrete2kore.disambiguation.PriorityVisitor;
1512
import org.kframework.parser.outer.Outer;
1613

1714
import java.io.File;
@@ -22,7 +19,10 @@
2219
*/
2320
public class ParserUtils {
2421

25-
public static K parseWithFile(CharSequence theTextToParse, String mainModule, String startSymbol, File definitionFile) {
22+
public static K parseWithFile(CharSequence theTextToParse,
23+
String mainModule,
24+
String startSymbol,
25+
File definitionFile) {
2626
String definitionText;
2727
try {
2828
definitionText = FileUtils.readFileToString(definitionFile);
@@ -32,38 +32,42 @@ public static K parseWithFile(CharSequence theTextToParse, String mainModule, St
3232
return parseWithString(theTextToParse, mainModule, startSymbol, definitionText);
3333
}
3434

35-
public static K parseWithString(CharSequence theTextToParse, String mainModule, String startSymbol, String definitionText) {
36-
Definition def = new Definition();
37-
def.setItems(Outer.parse(Sources.generatedBy(ParserUtils.class), definitionText, null));
38-
def.setMainModule(mainModule);
39-
def.setMainSyntaxModule(mainModule);
40-
41-
KILtoKORE kilToKore = new KILtoKORE(null);
42-
org.kframework.definition.Definition koreDef = kilToKore.apply(def);
43-
return parseWithDef(theTextToParse, mainModule, startSymbol, koreDef);
35+
public static K parseWithString(CharSequence theTextToParse,
36+
String mainModule,
37+
String startSymbol,
38+
String definitionText) {
39+
Module kastModule = parseMainModuleOuterSyntax(definitionText, mainModule);
40+
return parseWithModule(theTextToParse, startSymbol, kastModule);
4441
}
4542

46-
public static K parseWithDef(CharSequence theTextToParse, String mainModule, String startSymbol, org.kframework.definition.Definition definition) {
47-
48-
Module kastModule = definition.getModule(mainModule).get();
49-
50-
Grammar kastGrammar = KSyntax2GrammarStatesFilter.getGrammar(kastModule);
51-
return parseWithGrammar(theTextToParse, startSymbol, kastModule, kastGrammar);
43+
public static K parseWithModule(CharSequence theTextToParse,
44+
String startSymbol,
45+
org.kframework.definition.Module kastModule) {
46+
ParseInModule parser = new ParseInModule(kastModule);
47+
return parseWithModule(theTextToParse, startSymbol, parser);
5248
}
5349

54-
public static K parseWithGrammar(CharSequence theTextToParse, String startSymbol, org.kframework.definition.Module kastModule, Grammar grammar) {
55-
Parser parser = new Parser(theTextToParse);
56-
Term parsed = parser.parse(grammar.get(startSymbol), 0);
57-
58-
if (parsed.equals(Ambiguity.apply())) {
59-
Parser.ParseError errors = parser.getErrors();
60-
throw new AssertionError("There are parsing errors: " + errors.toString());
61-
}
50+
public static K parseWithModule(CharSequence theTextToParse,
51+
String startSymbol,
52+
ParseInModule kastModule) {
53+
Term cleaned = kastModule.parseString(theTextToParse, startSymbol)._1().right().get();
54+
return TreeNodesToKORE.apply(cleaned);
55+
}
6256

63-
Term cleaned = new TreeCleanerVisitor().apply(parsed).right().get();
64-
cleaned = new PreferAvoidVisitor().apply(cleaned);
65-
cleaned = new PriorityVisitor(kastModule.priorities(), kastModule.leftAssoc(), kastModule.rightAssoc()).apply(cleaned).right().get();
57+
/**
58+
* Takes a definition in e-kore textual format and a main module name, and returns the KORE
59+
* representation of that module. Current implementation uses JavaCC and goes through KIL.
60+
* @param definitionText textual representation of the modules.
61+
* @param mainModule main module name.
62+
* @return KORE representation of the main module.
63+
*/
64+
public static Module parseMainModuleOuterSyntax(String definitionText, String mainModule) {
65+
Definition def = new Definition();
66+
def.setItems(Outer.parse(Sources.generatedBy(ParserUtils.class), definitionText, null));
67+
def.setMainModule(mainModule);
68+
def.setMainSyntaxModule(mainModule);
6669

67-
return TreeNodesToKORE.apply(cleaned);
70+
KILtoKORE kilToKore = new KILtoKORE(null);
71+
return kilToKore.apply(def).getModule(mainModule).get();
6872
}
6973
}

‎kernel/src/main/java/org/kframework/parser/concrete2kore/disambiguation/AmbFilter.java‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework.parser.concrete2kore.disambiguation;
3+
4+
import org.kframework.parser.Ambiguity;
5+
import org.kframework.parser.ProductionReference;
6+
import org.kframework.parser.SetsGeneralTransformer;
7+
import org.kframework.parser.Term;
8+
import org.kframework.utils.errorsystem.KException;
9+
import org.kframework.utils.errorsystem.KException.ExceptionType;
10+
import org.kframework.utils.errorsystem.KException.KExceptionGroup;
11+
import org.kframework.utils.errorsystem.ParseFailedException;
12+
import scala.Tuple2;
13+
import scala.util.Either;
14+
import scala.util.Right;
15+
16+
import java.util.Set;
17+
18+
/**
19+
* Eliminate remaining ambiguities by choosing one of them.
20+
*/
21+
public class AmbFilter extends SetsGeneralTransformer<ParseFailedException, ParseFailedException> {
22+
23+
@Override
24+
public Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>> apply(Ambiguity amb) {
25+
26+
String msg = "Parsing ambiguity. Arbitrarily choosing the first.";
27+
28+
for (int i = 0; i < amb.items().size(); i++) {
29+
msg += "\n" + (i + 1) + ": ";
30+
Term elem = (Term) amb.items().toArray()[i];
31+
if (elem instanceof ProductionReference) {
32+
ProductionReference tc = (ProductionReference) elem;
33+
msg += tc.production().sort() + " ::= ";
34+
msg += tc.production().toString();
35+
}
36+
// TODO: use the unparser
37+
//Unparser unparser = new Unparser(context);
38+
//msg += "\n " + unparser.print(elem).replace("\n", "\n ");
39+
msg += "\n " + elem;
40+
}
41+
// TODO: add location information
42+
ParseFailedException w = new ParseFailedException(
43+
new KException(ExceptionType.WARNING, KExceptionGroup.INNER_PARSER, msg, null, amb.items().iterator().next().location().get()));
44+
45+
Tuple2<Either<Set<ParseFailedException>, Term>, Set<ParseFailedException>> rez = this.apply(amb.items().iterator().next());
46+
return new Tuple2<>(Right.apply(rez._1().right().get()), this.mergeWarnings(this.makeWarningSet(w), rez._2()));
47+
}
48+
}

0 commit comments

Comments
 (0)