Skip to content

Commit 41c3e29

Browse files
author
dwightguth
authored
Sort Synonyms (runtimeverification#791)
* add kil for sort synonym * outer parsing sort synonym * kore for sort synonyms * kiltokore for sort synonyms * json parsing/unparsing for sort synonyms * sort annotations for sort synonyms * resolve sort synonyms before inner parsing * tests * fix whitespace
1 parent d0ecc56 commit 41c3e29

15 files changed

Lines changed: 199 additions & 16 deletions

File tree

‎k-distribution/tests/regression-new/synonym/1.test‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
0

‎k-distribution/tests/regression-new/synonym/1.test.out‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
<generatedTop>
2+
<k>
3+
1
4+
</k>
5+
<r>
6+
0
7+
</r>
8+
</generatedTop>

‎k-distribution/tests/regression-new/synonym/Makefile‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
DEF=test
2+
EXT=test
3+
TESTDIR=.
4+
KOMPILE_BACKEND=llvm
5+
6+
include ../../../include/ktest.mak

‎k-distribution/tests/regression-new/synonym/test.k‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
requires "rat.k"
2+
3+
module TEST
4+
imports RAT
5+
6+
syntax Wad = Rat
7+
8+
configuration <k> $PGM:K </k> <r> 0:Wad </r>
9+
10+
syntax Wad ::= Wad "+Wad" Wad [function]
11+
12+
rule 0 => (0 +Wad 0) +Rat 1
13+
rule R +Wad R => R +Rat R
14+
15+
endmodule

‎kernel/src/main/java/org/kframework/kil/SortSynonym.java‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
package org.kframework.kil;
3+
4+
import org.kframework.kore.Sort;
5+
6+
import org.kframework.utils.StringUtil;
7+
8+
import java.util.ArrayList;
9+
import java.util.List;
10+
11+
public class SortSynonym extends ModuleItem {
12+
13+
public final Sort newSort;
14+
public final Sort oldSort;
15+
16+
public SortSynonym(SortSynonym node) {
17+
super(node);
18+
this.newSort = node.newSort;
19+
this.oldSort = node.oldSort;
20+
}
21+
22+
public SortSynonym(NonTerminal newSort, NonTerminal oldSort) {
23+
super();
24+
this.newSort = newSort.getSort();
25+
this.oldSort = oldSort.getSort();
26+
}
27+
28+
@Override
29+
public boolean equals(Object obj) {
30+
if (this == obj)
31+
return true;
32+
if (obj == null)
33+
return false;
34+
if (getClass() != obj.getClass())
35+
return false;
36+
SortSynonym other = (SortSynonym) obj;
37+
if (!newSort.equals(other.newSort))
38+
return false;
39+
if (!oldSort.equals(other.oldSort))
40+
return false;
41+
return true;
42+
}
43+
44+
@Override
45+
public int hashCode() {
46+
final int prime = 31;
47+
int result = 1;
48+
result = prime * result + newSort.hashCode();
49+
result = prime * result + oldSort.hashCode();
50+
return result;
51+
}
52+
53+
@Override
54+
public SortSynonym shallowCopy() {
55+
return new SortSynonym(this);
56+
}
57+
}

‎kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -122,6 +122,10 @@ public Set<org.kframework.definition.Sentence> apply(ModuleItem i) {
122122
}
123123
}
124124

125+
public org.kframework.definition.Sentence apply(SortSynonym synonym) {
126+
return new org.kframework.definition.SortSynonym(synonym.newSort, synonym.oldSort, convertAttributes(synonym));
127+
}
128+
125129
public org.kframework.definition.Bubble apply(StringSentence sentence) {
126130
org.kframework.attributes.Att attrs =
127131
convertAttributes(sentence)

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

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
package org.kframework.parser.concrete2kore;
3+
4+
import org.kframework.definition.Module;
5+
import org.kframework.definition.NonTerminal;
6+
import org.kframework.definition.Production;
7+
import org.kframework.definition.ProductionItem;
8+
import org.kframework.definition.Sentence;
9+
import org.kframework.kore.Sort;
10+
11+
import java.util.ArrayList;
12+
import java.util.List;
13+
14+
import static org.kframework.definition.Constructors.*;
15+
import static org.kframework.Collections.*;
16+
17+
public class ApplySynonyms {
18+
19+
public Production apply(Module m, Production p) {
20+
Sort returnSort = m.sortSynonymMap().applyOrElse(p.sort(), s -> p.sort());
21+
List<ProductionItem> pis = new ArrayList<>();
22+
for (ProductionItem pi : iterable(p.items())) {
23+
if (pi instanceof NonTerminal) {
24+
NonTerminal nt = (NonTerminal)pi;
25+
pis.add(NonTerminal(m.sortSynonymMap().applyOrElse(nt.sort(), s -> nt.sort()), nt.name()));
26+
} else {
27+
pis.add(pi);
28+
}
29+
}
30+
return Production(p.klabel(), returnSort, immutable(pis), p.att());
31+
}
32+
33+
public Sentence apply(Module m, Sentence s) {
34+
if (s instanceof Production) {
35+
return apply(m, (Production)s);
36+
} else {
37+
return s;
38+
}
39+
}
40+
}

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
import org.kframework.attributes.Att;
66
import org.kframework.attributes.Source;
77
import org.kframework.definition.Module;
8+
import org.kframework.definition.ModuleTransformer;
89
import org.kframework.kil.Definition;
910
import org.kframework.kil.DefinitionItem;
1011
import org.kframework.kil.Require;
@@ -196,7 +197,13 @@ public Set<Module> loadModules(
196197
koreModules.putAll(previousModules.stream().collect(Collectors.toMap(Module::name, m -> m)));
197198
HashSet<org.kframework.kil.Module> kilModulesSet = new HashSet<>(kilModules);
198199

199-
return kilModules.stream().map(m -> kilToKore.apply(m, kilModulesSet, koreModules)).flatMap(m -> Stream.concat(Stream.of(m), Stream.of(koreModules.get(m.name() + "$SYNTAX")))).collect(Collectors.toSet());
200+
Set<Module> finalModules = kilModules.stream().map(m -> kilToKore.apply(m, kilModulesSet, koreModules)).flatMap(m -> Stream.concat(Stream.of(m), Stream.of(koreModules.get(m.name() + "$SYNTAX")))).collect(Collectors.toSet());
201+
Set<Module> result = new HashSet<>();
202+
ModuleTransformer applySynonyms = ModuleTransformer.fromSentenceTransformer(new ApplySynonyms()::apply, "Apply sort synonyms");
203+
for (Module mod : finalModules) {
204+
result.add(applySynonyms.apply(mod));
205+
}
206+
return result;
200207
}
201208

202209
public org.kframework.definition.Definition loadDefinition(

‎kernel/src/main/java/org/kframework/parser/concrete2kore/generator/RuleGrammarGenerator.java‎

Lines changed: 14 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import org.kframework.definition.ProductionItem;
1717
import org.kframework.definition.RegexTerminal;
1818
import org.kframework.definition.Sentence;
19+
import org.kframework.definition.SortSynonym;
1920
import org.kframework.definition.Terminal;
2021
import org.kframework.definition.UserList;
2122
import org.kframework.kil.loader.Constants;
@@ -205,13 +206,16 @@ public static ParseInModule getCombinedGrammar(Module mod, boolean strict, boole
205206
for (Sort srt : iterable(mod.definedSorts())) {
206207
if (!isParserSort(srt) || mod.subsorts().directlyLessThan(Sorts.KVariable(), srt)) {
207208
// K ::= K "::Sort" | K ":Sort" | K "<:Sort" | K ":>Sort"
208-
prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), srt));
209+
prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), srt, srt));
209210
}
210211
}
211-
prods.addAll(makeCasts(Sorts.KLabel(), Sorts.KLabel(), Sorts.KLabel()));
212-
prods.addAll(makeCasts(Sorts.KList(), Sorts.KList(), Sorts.KList()));
213-
prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), Sorts.KItem()));
214-
prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), Sorts.K()));
212+
prods.addAll(makeCasts(Sorts.KLabel(), Sorts.KLabel(), Sorts.KLabel(), Sorts.KLabel()));
213+
prods.addAll(makeCasts(Sorts.KList(), Sorts.KList(), Sorts.KList(), Sorts.KList()));
214+
prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), Sorts.KItem(), Sorts.KItem()));
215+
prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), Sorts.K(), Sorts.K()));
216+
for (SortSynonym syn : iterable(mod.sortSynonyms())) {
217+
prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), syn.newSort(), syn.oldSort()));
218+
}
215219
}
216220

217221
if (mod.importedModuleNames().contains(RECORD_PRODS)) {
@@ -444,13 +448,13 @@ private static void makeAllSortTuples(int level, int size, List<Sort> sorts, Lis
444448
}
445449
}
446450

447-
private static Set<Sentence> makeCasts(Sort outerSort, Sort innerSort, Sort castSort) {
451+
private static Set<Sentence> makeCasts(Sort outerSort, Sort innerSort, Sort castSort, Sort labelSort) {
448452
Set<Sentence> prods = new HashSet<>();
449453
Att attrs1 = Att().add(Sort.class, castSort);
450-
prods.add(Production(KLabel("#SyntacticCast"), castSort, Seq(NonTerminal(castSort), Terminal("::" + castSort.toString())), attrs1));
451-
prods.add(Production(KLabel("#SemanticCastTo" + castSort.toString()), castSort, Seq(NonTerminal(castSort), Terminal(":" + castSort.toString())), attrs1));
452-
prods.add(Production(KLabel("#InnerCast"), outerSort, Seq(Terminal("{"), NonTerminal(castSort), Terminal("}"), Terminal("<:" + castSort.toString())), attrs1));
453-
prods.add(Production(KLabel("#OuterCast"), castSort, Seq(Terminal("{"), NonTerminal(innerSort), Terminal("}"), Terminal(":>" + castSort.toString())), attrs1));
454+
prods.add(Production(KLabel("#SyntacticCast"), castSort, Seq(NonTerminal(labelSort), Terminal("::" + castSort.toString())), attrs1));
455+
prods.add(Production(KLabel("#SemanticCastTo" + labelSort.toString()), labelSort, Seq(NonTerminal(labelSort), Terminal(":" + castSort.toString())), attrs1));
456+
prods.add(Production(KLabel("#InnerCast"), outerSort, Seq(Terminal("{"), NonTerminal(labelSort), Terminal("}"), Terminal("<:" + castSort.toString())), attrs1));
457+
prods.add(Production(KLabel("#OuterCast"), labelSort, Seq(Terminal("{"), NonTerminal(innerSort), Terminal("}"), Terminal(":>" + castSort.toString())), attrs1));
454458
return prods;
455459
}
456460
}

‎kernel/src/main/java/org/kframework/parser/json/JsonParser.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import org.kframework.definition.RegexTerminal;
1717
import org.kframework.definition.Rule;
1818
import org.kframework.definition.Sentence;
19+
import org.kframework.definition.SortSynonym;
1920
import org.kframework.definition.SyntaxAssociativity;
2021
import org.kframework.definition.SyntaxPriority;
2122
import org.kframework.definition.SyntaxSort;
@@ -84,6 +85,7 @@ public class JsonParser {
8485
, KRULE = "KRule"
8586
, KSEQUENCE = "KSequence"
8687
, KSORT = "KSort"
88+
, KSORTSYNONYM = "KSortSynonym"
8789
, KSYNTAXASSOCIATIVITY = "KSyntaxAssociativity"
8890
, KSYNTAXPRIORITY = "KSyntaxPriority"
8991
, KSYNTAXSORT = "KSyntaxSort"
@@ -219,6 +221,12 @@ public static Sentence toSentence(JsonObject data) throws IOException {
219221
Att att = toAtt(data.getJsonObject("att"));
220222
return new SyntaxSort(sort, att);
221223
}
224+
case KSORTSYNONYM: {
225+
Sort newSort = toSort(data.getJsonObject("newSort"));
226+
Sort oldSort = toSort(data.getJsonObject("oldSort"));
227+
Att att = toAtt(data.getJsonObject("att"));
228+
return new SortSynonym(newSort, oldSort, att);
229+
}
222230
case KBUBBLE: {
223231
String sentenceType = data.getString("sentenceType");
224232
String contents = data.getString("contents");

0 commit comments

Comments
 (0)