Skip to content
This repository was archived by the owner on Feb 1, 2020. It is now read-only.

Commit 761391e

Browse files
msaxena2msaxena2
committed
changes to make compilation work
1 parent 9c58b35 commit 761391e

File tree

19 files changed

+148
-139
lines changed

19 files changed

+148
-139
lines changed

‎k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java

+4-4
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,15 @@
88
import org.kframework.backend.Backends;
99
import org.kframework.builtin.Sorts;
1010
import org.kframework.definition.Module;
11+
import org.kframework.frontend.K;
12+
import org.kframework.frontend.KApply;
13+
import org.kframework.frontend.KORE;
14+
import org.kframework.frontend.KToken;
1115
import org.kframework.kale.KaleBackend;
1216
import org.kframework.kale.KaleRewriter;
1317
import org.kframework.kompile.CompiledDefinition;
1418
import org.kframework.kompile.Kompile;
1519
import org.kframework.kompile.KompileOptions;
16-
import org.kframework.frontend.K;
17-
import org.kframework.frontend.KApply;
18-
import org.kframework.frontend.KORE;
19-
import org.kframework.frontend.KToken;
2020
import org.kframework.main.GlobalOptions;
2121
import org.kframework.parser.ProductionReference;
2222
import org.kframework.unparser.AddBrackets;

‎kdoc/src/main/scala/org/kframework/kdoc/KDoc.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ class KDoc(docStyle: String, separator: String = " ") {
4646
case o => super.apply(o)
4747
}
4848

49-
override def apply(k: KToken) = k match {
49+
override def apply(k: KToken): K = k match {
5050
case c@KToken(contents, Sort("Bubble")) =>
5151
currentParser(ADT.Sort("RuleContent", ModuleName("REQUIRES-ENSURES")), contents) match {
5252
case (Some(parsedBubble), _) => currentKToLatex(parsedBubble)

‎kernel/src/main/java/org/kframework/frontend/compile/ConvertDataStructureToLookup.java

+20-20
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,7 @@ private K infer(K term, KLabel collectionLabel) {
205205
public K apply(KApply k) {
206206
if (k.klabel().equals(wrappedLabel)) {
207207
KLabel elementLabel = KLabel(m.attributesFor().apply(collectionLabel).<String>get("element").get());
208-
return KApply(elementLabel, super.apply(k));
208+
return KORE.KApply(elementLabel, super.apply(k));
209209
}
210210
return super.apply(k);
211211
}
@@ -302,11 +302,11 @@ private K convertList(KApply k, KLabel collectionLabel, List<K> components) {
302302
if (elementsRight.size() == 0 && matchOnConsList) {
303303
K tail;
304304
if (frame == null) {
305-
tail = KApply(KLabel(m.attributesFor().apply(collectionLabel).<String>get(Attribute.UNIT_KEY).get()));
305+
tail = KORE.KApply(KLabel(m.attributesFor().apply(collectionLabel).<String>get(Attribute.UNIT_KEY).get()));
306306
} else {
307307
tail = frame;
308308
}
309-
list = Lists.reverse(elementsLeft).stream().map(e -> (K) KApply(elementLabel, e)).reduce(tail, (res, el) -> KApply(collectionLabel, el, res));
309+
list = Lists.reverse(elementsLeft).stream().map(e -> (K) KORE.KApply(elementLabel, e)).reduce(tail, (res, el) -> KORE.KApply(collectionLabel, el, res));
310310
} else {
311311
list = newDotVariable(m.productionsFor().get(collectionLabel).get().head().sort());
312312
// Ctx[ListItem(5) Frame ListItem(X) ListItem(foo(Y))] => Ctx [L]
@@ -318,29 +318,29 @@ private K convertList(KApply k, KLabel collectionLabel, List<K> components) {
318318
list = k;
319319
} else {
320320
if (frame != null) {
321-
state.add(KApply(KLabel("#match"), frame, KApply(KLabel("List:range"), list,
321+
state.add(KORE.KApply(KLabel("#match"), frame, KORE.KApply(KLabel("List:range"), list,
322322
KToken(Integer.toString(elementsLeft.size()), Sorts.Int()),
323323
KToken(Integer.toString(elementsRight.size()), Sorts.Int()))));
324324
} else {
325325
KLabel unit = KLabel(m.attributesFor().apply(collectionLabel).<String>get("unit").get());
326326
// Ctx[.List] => Ctx[L] requires L ==K range(L, 0, 0)
327-
state.add(KApply(KLabel("_==K_"), KApply(unit), KApply(KLabel("List:range"), list,
327+
state.add(KORE.KApply(KLabel("_==K_"), KORE.KApply(unit), KORE.KApply(KLabel("List:range"), list,
328328
KToken(Integer.toString(elementsLeft.size()), Sorts.Int()),
329329
KToken(Integer.toString(elementsRight.size()), Sorts.Int()))));
330330
}
331331
}
332332
KLabel elementWrapper = KLabel(m.attributesFor().apply(collectionLabel).<String>get("element").get());
333333
for (int i = 0; i < elementsLeft.size(); i++) {
334-
state.add(KApply(
334+
state.add(KORE.KApply(
335335
KLabel("#match"),
336-
KApply(elementWrapper, elementsLeft.get(i)),
337-
KApply(KLabel("List:get"), list, KToken(Integer.toString(i), Sorts.Int()))));
336+
KORE.KApply(elementWrapper, elementsLeft.get(i)),
337+
KORE.KApply(KLabel("List:get"), list, KToken(Integer.toString(i), Sorts.Int()))));
338338
}
339339
for (int i = 0; i < elementsRight.size(); i++) {
340-
state.add(KApply(
340+
state.add(KORE.KApply(
341341
KLabel("#match"),
342-
KApply(elementWrapper, elementsRight.get(i)),
343-
KApply(KLabel("List:get"), list, KToken(Integer.toString(i - elementsRight.size()), Sorts.Int()))));
342+
KORE.KApply(elementWrapper, elementsRight.get(i)),
343+
KORE.KApply(KLabel("List:get"), list, KToken(Integer.toString(i - elementsRight.size()), Sorts.Int()))));
344344
}
345345
}
346346
if (lhsOf == null && RewriteToTop.hasRewrite(k)) {
@@ -394,17 +394,17 @@ private K convertMap(KApply k, KLabel collectionLabel, List<K> components, Multi
394394
KVariable map = newDotVariable(m.productionsFor().get(collectionLabel).get().head().sort());
395395
// K1,Ctx[K1 |-> K2 K3] => K1,Ctx[M] requires K3 := M[K1<-undef] andBool K1 := choice(M) andBool K2 := M[K1]
396396
if (frame != null) {
397-
state.add(KApply(KLabel("#match"), frame, elements.keySet().stream().reduce(map, (a1, a2) -> KApply(KLabel("_[_<-undef]"), a1, a2))));
397+
state.add(KORE.KApply(KLabel("#match"), frame, elements.keySet().stream().reduce(map, (a1, a2) -> KORE.KApply(KLabel("_[_<-undef]"), a1, a2))));
398398
} else {
399399
KLabel unit = KLabel(m.attributesFor().apply(collectionLabel).<String>get("unit").get());
400-
state.add(KApply(KLabel("_==K_"), KApply(unit), elements.keySet().stream().reduce(map, (a1, a2) -> KApply(KLabel("_[_<-undef]"), a1, a2))));
400+
state.add(KORE.KApply(KLabel("_==K_"), KORE.KApply(unit), elements.keySet().stream().reduce(map, (a1, a2) -> KORE.KApply(KLabel("_[_<-undef]"), a1, a2))));
401401
}
402402
for (Map.Entry<K, K> element : elements.entrySet()) {
403403
// TODO(dwightguth): choose better between lookup and choice.
404404
if (element.getKey() instanceof KVariable && varConstraints.count(element.getKey()) == 1) {
405-
state.add(KApply(KLabel("#mapChoice"), element.getKey(), map));
405+
state.add(KORE.KApply(KLabel("#mapChoice"), element.getKey(), map));
406406
}
407-
state.add(KApply(KLabel("#match"), element.getValue(), KApply(KLabel(KLabels.MAP_LOOKUP), map, element.getKey())));
407+
state.add(KORE.KApply(KLabel("#match"), element.getValue(), KORE.KApply(KLabel(KLabels.MAP_LOOKUP), map, element.getKey())));
408408
}
409409
if (lhsOf == null && RewriteToTop.hasRewrite(k)) {
410410
// An outermost map may contain nested rewrites, so the term
@@ -468,18 +468,18 @@ private K convertSet(KApply k, KLabel collectionLabel, List<K> components, Multi
468468
Multiset<KVariable> vars = HashMultiset.create();
469469
gatherVars(element, vars);
470470
if (vars.isEmpty() || (element instanceof KVariable && varConstraints.count(element) != 1)) {
471-
state.add(KApply(KLabel("Set:in"), element, accum));
471+
state.add(KORE.KApply(KLabel("Set:in"), element, accum));
472472
} else {
473473
//set choice
474-
state.add(KApply(KLabel("#setChoice"), element, accum));
474+
state.add(KORE.KApply(KLabel("#setChoice"), element, accum));
475475
}
476-
accum = KApply(KLabel("Set:difference"), accum, KApply(elementLabel, element));
476+
accum = KORE.KApply(KLabel("Set:difference"), accum, KORE.KApply(elementLabel, element));
477477
}
478478
KLabel unit = KLabel(m.attributesFor().apply(collectionLabel).<String>get("unit").get());
479479
if (frame != null) {
480-
state.add(KApply(KLabel("#match"), frame, accum));
480+
state.add(KORE.KApply(KLabel("#match"), frame, accum));
481481
} else {
482-
state.add(KApply(KLabel("_==K_"), KApply(unit), accum));
482+
state.add(KORE.KApply(KLabel("_==K_"), KORE.KApply(unit), accum));
483483
}
484484
if (lhsOf == null && RewriteToTop.hasRewrite(k)) {
485485
// An outermost set may contain nested rewrites, so the term

‎kernel/src/main/java/org/kframework/frontend/compile/ConvertStrictToContexts.java

+4-3
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
import org.kframework.definition.NonTerminal;
1010
import org.kframework.definition.Production;
1111
import org.kframework.definition.Sentence;
12+
import org.kframework.frontend.KORE;
1213
import org.kframework.kil.Attribute;
1314
import org.kframework.kompile.KompileOptions;
1415
import org.kframework.frontend.K;
@@ -53,7 +54,7 @@ public Set<Sentence> resolve(Set<Production> strictProductions) {
5354
}
5455

5556
private static KApply cast(Sort sort, K k) {
56-
return KApply(KLabel("#SemanticCastTo" + sort.name()), k);
57+
return KORE.KApply(KLabel("#SemanticCastTo" + sort.name()), k);
5758
}
5859

5960
public Set<Sentence> resolve(Production production, boolean sequential) {
@@ -106,14 +107,14 @@ public Set<Sentence> resolve(Production production, boolean sequential) {
106107
}
107108

108109
// is seqstrict the elements before the argument should be KResult
109-
Optional<KApply> sideCondition = strictnessPositions.subList(0, i).stream().map(j -> KApply(KLabel("isKResult@BASIC-K"), KVariable("K" + (j - 1)))).reduce(BooleanUtils::and);
110+
Optional<KApply> sideCondition = strictnessPositions.subList(0, i).stream().map(j -> KORE.KApply(KLabel("isKResult@BASIC-K"), KVariable("K" + (j - 1)))).reduce(BooleanUtils::and);
110111
K requires;
111112
if (!sideCondition.isPresent() || !sequential) {
112113
requires = BooleanUtils.TRUE;
113114
} else {
114115
requires = sideCondition.get();
115116
}
116-
Context ctx = Context(KApply(production.klabel().get(), KList(items)), requires, production.att());
117+
Context ctx = Context(KORE.KApply(production.klabel().get(), KList(items)), requires, production.att());
117118
contexts.add(ctx);
118119
}
119120
return contexts;

‎kernel/src/main/java/org/kframework/frontend/compile/DeconstructIntegerAndFloatLiterals.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -123,7 +123,7 @@ public K apply(KToken k) {
123123
if (lhs) {
124124
if (k.sort().equals(Sorts.Int()) || k.sort().equals(Sorts.Float())) {
125125
KVariable var = newDotVariable(k.sort());
126-
state.add(KApply(KLabel("_==" + k.sort().name() + "_"), var, k));
126+
state.add(KORE.KApply(KLabel("_==" + k.sort().name() + "_"), var, k));
127127
return var;
128128
}
129129
}
@@ -145,7 +145,7 @@ public K apply(KApply k) {
145145
K l = apply(k.klist().items().get(0));
146146
lhs = false;
147147
if (l != k.klist().items().get(0) || r != k.klist().items().get(1)) {
148-
return KApply(k.klabel(), l, r);
148+
return KORE.KApply(k.klabel(), l, r);
149149
} else {
150150
return k;
151151
}

‎kernel/src/main/java/org/kframework/frontend/compile/GenerateSentencesFromConfigDecl.java

+12-12
Original file line numberDiff line numberDiff line change
@@ -121,10 +121,10 @@ private static Tuple3<Set<Sentence>, List<Sort>, K> genInternal(K term, K ensure
121121
if (initializerProduction.get().size() == 1) { // should be only a single initializer
122122
if (initializerProduction.get().head().items().size() == 1) {
123123
// XCell ::= "initXCell"
124-
return Tuple3.apply(Set(), Lists.newArrayList(sort), KApply(KLabel(getInitLabel(sort))));
124+
return Tuple3.apply(Set(), Lists.newArrayList(sort), KORE.KApply(KLabel(getInitLabel(sort))));
125125
} else if (initializerProduction.get().head().items().size() == 4) {
126126
// XCell ::= "initXCell" "(" Map ")"
127-
return Tuple3.apply(Set(), Lists.newArrayList(sort), KApply(KLabel(getInitLabel(sort)), KVariable("Init")));
127+
return Tuple3.apply(Set(), Lists.newArrayList(sort), KORE.KApply(KLabel(getInitLabel(sort)), KVariable("Init")));
128128
}
129129
}
130130
}
@@ -137,7 +137,7 @@ private static Tuple3<Set<Sentence>, List<Sort>, K> genInternal(K term, K ensure
137137
if (ensures != null) {
138138
//top level cell, therefore, should be the children of the generatedTop cell
139139
KToken cellLabel = KToken(KLabels.GENERATED_TOP_CELL, Sort("#CellName"));
140-
K generatedTop = KApply(KLabel("#configCell"), cellLabel, KApply(KLabel("#cellPropertyListTerminator")), term, cellLabel);
140+
K generatedTop = KORE.KApply(KLabel("#configCell"), cellLabel, KORE.KApply(KLabel("#cellPropertyListTerminator")), term, cellLabel);
141141
return genInternal(generatedTop, ensures, cfgAtt, m);
142142
}
143143
List<K> cells = Assoc.flatten(kapp.klabel(), kapp.klist().items(), m);
@@ -151,7 +151,7 @@ private static Tuple3<Set<Sentence>, List<Sort>, K> genInternal(K term, K ensure
151151
sorts.addAll(childResult._2());
152152
initializers.add(childResult._3());
153153
}
154-
return Tuple3.apply(accumSentences, sorts, KApply(KLabel(KLabels.CELLS), immutable(initializers)));
154+
return Tuple3.apply(accumSentences, sorts, KORE.KApply(KLabel(KLabels.CELLS), immutable(initializers)));
155155
}
156156
//TODO: call generic getSort method of some kind
157157
// child of a leaf cell. Generate no productions, but inform parent that it has a child of a particular sort.
@@ -211,7 +211,7 @@ private static K getLeafInitializer(K leafContents) {
211211
@Override
212212
public K apply(KToken k) {
213213
if (k.sort().equals(Sorts.KConfigVar())) {
214-
return KApply(KLabel(KLabels.MAP_LOOKUP), KVariable("Init"), k);
214+
return KORE.KApply(KLabel(KLabels.MAP_LOOKUP), KVariable("Init"), k);
215215
}
216216
return k;
217217
}
@@ -282,10 +282,10 @@ private static Tuple3<Set<Sentence>, Sort, K> computeSentencesOfWellFormedCell(
282282
Rule initializerRule;
283283
if (hasConfigurationOrRegularVariable || isStream) {
284284
initializer = Production(initLabel, sort, Seq(Terminal(initLabel), Terminal("("), NonTerminal(Sort("Map")), Terminal(")")), Att().add("initializer").add("function"));
285-
initializerRule = Rule(KRewrite(KApply(KLabel(initLabel), KVariable("Init")), IncompleteCellUtils.make(KLabel("<" + cellName + ">"), false, childInitializer, false)), BooleanUtils.TRUE, ensures == null ? BooleanUtils.TRUE : ensures, Att().add("initializer"));
285+
initializerRule = Rule(KRewrite(KORE.KApply(KLabel(initLabel), KVariable("Init")), IncompleteCellUtils.make(KLabel("<" + cellName + ">"), false, childInitializer, false)), BooleanUtils.TRUE, ensures == null ? BooleanUtils.TRUE : ensures, Att().add("initializer"));
286286
} else {
287287
initializer = Production(initLabel, sort, Seq(Terminal(initLabel)), Att().add("initializer").add("function"));
288-
initializerRule = Rule(KRewrite(KApply(KLabel(initLabel)), IncompleteCellUtils.make(KLabel("<" + cellName + ">"), false, childInitializer, false)), BooleanUtils.TRUE, ensures == null ? BooleanUtils.TRUE : ensures, Att().add("initializer"));
288+
initializerRule = Rule(KRewrite(KORE.KApply(KLabel(initLabel)), IncompleteCellUtils.make(KLabel("<" + cellName + ">"), false, childInitializer, false)), BooleanUtils.TRUE, ensures == null ? BooleanUtils.TRUE : ensures, Att().add("initializer"));
289289
}
290290
sentences.add(initializer);
291291
sentences.add(initializerRule);
@@ -398,9 +398,9 @@ private static Tuple3<Set<Sentence>, Sort, K> computeSentencesOfWellFormedCell(
398398
// rule initCell(Init) => <cell> initChildren(Init)... </cell>
399399
cellsSort = sort;
400400
if (hasConfigurationOrRegularVariable || isStream) {
401-
rhs = KApply(KLabel(initLabel), KVariable("Init"));
401+
rhs = KORE.KApply(KLabel(initLabel), KVariable("Init"));
402402
} else {
403-
rhs = KApply(KLabel(initLabel));
403+
rhs = KORE.KApply(KLabel(initLabel));
404404
}
405405
}
406406
return Tuple3.apply(immutable(sentences),cellsSort,rhs);
@@ -412,11 +412,11 @@ private static Tuple3<Set<Sentence>, Sort, K> computeSentencesOfWellFormedCell(
412412
*/
413413
private static KApply optionalCellInitializer(boolean initializeOptionalCell, Att cellProperties, String initLabel) {
414414
if (initializeOptionalCell) {
415-
return KApply(KLabel(initLabel), KVariable("Init"));
415+
return KORE.KApply(KLabel(initLabel), KVariable("Init"));
416416
} else if (cellProperties.contains("initial")) {
417-
return KApply(KLabel(initLabel));
417+
return KORE.KApply(KLabel(initLabel));
418418
} else {
419-
return KApply(KLabel(KLabels.CELLS));
419+
return KORE.KApply(KLabel(KLabels.CELLS));
420420
}
421421
}
422422

‎kernel/src/main/java/org/kframework/frontend/compile/IncompleteCellUtils.java

+6-5
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
import org.kframework.frontend.K;
66
import org.kframework.frontend.KApply;
77
import org.kframework.frontend.KLabel;
8+
import org.kframework.frontend.KORE;
89
import org.kframework.utils.errorsystem.KEMException;
910

1011
import java.util.ArrayList;
@@ -23,8 +24,8 @@
2324
* (which this class will allow with arbitrary arity).
2425
*/
2526
public class IncompleteCellUtils {
26-
private final static KApply dots = KApply(KLabel(KLabels.DOTS));
27-
private final static KApply noDots = KApply(KLabel(KLabels.NO_DOTS));
27+
private final static KApply dots = KORE.KApply(KLabel(KLabels.DOTS));
28+
private final static KApply noDots = KORE.KApply(KLabel(KLabels.NO_DOTS));
2829

2930
private static boolean isOpen(K flag) {
3031
if (dots.equals(flag)) {
@@ -69,14 +70,14 @@ private static K makeBody(List<? extends K> children) {
6970
if (children.size() == 1) {
7071
return children.get(0);
7172
} else {
72-
return KApply(KLabel(KLabels.CELLS), KList(children));
73+
return KORE.KApply(KLabel(KLabels.CELLS), KList(children));
7374
}
7475
}
7576

7677
public static KApply make(KLabel label, boolean openLeft, K child, boolean openRight) {
77-
return KApply(label, KList(makeDots(openLeft), child, makeDots(openRight)));
78+
return KORE.KApply(label, KList(makeDots(openLeft), child, makeDots(openRight)));
7879
}
7980
public static KApply make(KLabel label, boolean openLeft, List<? extends K> children, boolean openRight) {
80-
return KApply(label, KList(makeDots(openLeft), makeBody(children), makeDots(openRight)));
81+
return KORE.KApply(label, KList(makeDots(openLeft), makeBody(children), makeDots(openRight)));
8182
}
8283
}

0 commit comments

Comments
 (0)