Skip to content

Commit 672bc9e

Browse files
coscos
committed
clearing up the boundary between kore and builtins
Former-commit-id: 45a379ffab7aa9e2b0ce0bff02ca5154af1ea246 [formerly a6cbddee68c62467cb0ae345fa5b0fb847b9e218] Former-commit-id: 9332923e90207ea1ae184038dfb06c3c8da4575e
1 parent 3b97e13 commit 672bc9e

14 files changed

Lines changed: 83 additions & 66 deletions

File tree

‎k-distribution/src/test/resources/convertor-tests/configuration-expected.k‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,5 +13,5 @@ endmodule
1313

1414
module TEST [location(startLine(4),startColumn(1),endLine(7),endColumn(9))]
1515
imports INCLUDE [location(startLine(5),startColumn(3),endLine(5),endColumn(17))]
16-
configuration <t><k>.K</k> <env>'.Map() [location(startLine(6),startColumn(70),endLine(6),endColumn(74)) sort(Map)]</env> <stack>.Bag</stack></t> ensures true
17-
endmodule
16+
configuration <t>KBag(k(.K) [cell()],env('.Map() [location(startLine(6),startColumn(70),endLine(6),endColumn(74)) sort(Map)]) [cell()],stack(KBag()) [cell()])</t> ensures true
17+
endmodule

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

Lines changed: 22 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@
1313
import java.util.stream.Collectors;
1414
import java.util.stream.Stream;
1515

16+
import org.kframework.builtin.Labels;
17+
import org.kframework.builtin.Sorts;
1618
import org.kframework.kil.ASTNode;
1719
import org.kframework.kil.AbstractVisitor;
1820
import org.kframework.kil.Attributes;
@@ -82,23 +84,25 @@ public KILtoInnerKORE(org.kframework.kil.loader.Context context) {
8284

8385
public K apply(Bag body) {
8486
List<K> contents = body.getContents().stream().map(this).collect(Collectors.toList());
85-
return KBag(KList(contents));
87+
return KApply(Labels.KBag(), (KList(contents)));
8688
}
8789

88-
// public K apply(TermComment c) {
89-
// return KList();
90-
// }
90+
// public K apply(TermComment c) {
91+
// return KList();
92+
// }
9193

9294
private KApply cellMarker = org.kframework.kore.outer.Configuration.cellMarker();
9395

9496
@SuppressWarnings("unchecked")
9597
public KApply apply(Cell body) {
96-
K x = apply(body.getContents());
97-
if (x instanceof KBag && !((KBag) x).isEmpty()) {
98-
return KApply(KLabel(body.getLabel()), KList(((KBag) x)), Attributes(cellMarker));
99-
} else {
100-
return KApply(KLabel(body.getLabel()), KList(x), Attributes(cellMarker));
101-
}
98+
// K x = ;
99+
// if (x instanceof KApply && ((KApply) x).klabel() == Labels.KBag()
100+
// && ((KApply) x).size() == 0) {
101+
return KApply(KLabel(body.getLabel()), KList(apply(body.getContents())), Attributes(cellMarker));
102+
// } else {
103+
// return KApply(KLabel(body.getLabel()), KList(x),
104+
// Attributes(cellMarker));
105+
// }
102106
}
103107

104108
public K apply(org.kframework.kil.KLabelConstant c) {
@@ -123,7 +127,8 @@ public KApply apply(ListTerminator t) {
123127
Production production = context.listProductions.get(t.getSort());
124128
String terminatorKLabel = production.getTerminatorKLabel();
125129

126-
// NOTE: we don't covert it back to ListTerminator because Radu thinks it is not necessary
130+
// NOTE: we don't covert it back to ListTerminator because Radu thinks
131+
// it is not necessary
127132

128133
return KApply(KLabel(terminatorKLabel), KList(), Attributes().add(LIST_TERMINATOR));
129134
}
@@ -166,7 +171,7 @@ private org.kframework.kore.Attributes sortAttributes(Term cons) {
166171
}
167172

168173
public KApply apply(Hole hole) {
169-
return KApply(Hole(), KList(KToken(Sort(hole.getSort().getName()), "")),
174+
return KApply(Labels.Hole(), KList(KToken(Sort(hole.getSort().getName()), "")),
170175
sortAttributes(hole));
171176
}
172177

@@ -182,7 +187,7 @@ public K applyOrTrue(Term t) {
182187
if (t != null)
183188
return apply(t);
184189
else
185-
return new KBoolean(true, Attributes());
190+
return KToken(Sorts.KBoolean(), "true");
186191
}
187192

188193
public org.kframework.kore.Attributes convertAttributes(ASTNode t) {
@@ -199,13 +204,14 @@ public org.kframework.kore.Attributes convertAttributes(ASTNode t) {
199204
KList(KToken(Sort("AttributeValue"), valueString)));
200205
}).collect(Collectors.toSet());
201206

202-
return Attributes(immutable(attributesSet)).addAll(attributesFromLocation(t.getLocation()));
207+
return Attributes(immutable(attributesSet))
208+
.addAll(attributesFromLocation(t.getLocation()));
203209
}
204210

205211
private org.kframework.kore.Attributes attributesFromLocation(Location location) {
206-
if(location != null)
212+
if (location != null)
207213
return Attributes(Location(location.lineStart, location.columnStart, location.lineEnd,
208-
location.columnEnd));
214+
location.columnEnd));
209215
else
210216
return Attributes();
211217
}

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

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22

33
package org.kframework.kore.convertors;
44

5+
import org.kframework.builtin.Labels;
6+
import org.kframework.builtin.Sorts;
57
import org.kframework.kil.Attribute;
68
import org.kframework.kil.KLabelConstant;
79
import org.kframework.kil.Production;
@@ -411,7 +413,8 @@ public org.kframework.kil.Attributes convertAttributes(Attributes koreAttributes
411413
if (a instanceof KApply) {
412414
KApply attr = (KApply) a;
413415
KLabel key = attr.klabel();
414-
if (!(key != KLabel("location"))) { // ignoring location information
416+
if (!(key != KLabel("location"))) { // ignoring location
417+
// information
415418
KList klist = attr.klist();
416419
if (klist.size() == 1 && klist.get(0) instanceof KToken) {
417420
String value = ((KToken) klist.get(0)).s();
@@ -461,14 +464,14 @@ public org.kframework.kil.Term convertK(K k) {
461464
// KORE KApply, we need to figure out every one of them and handle
462465
// here
463466
return convertKApply(kApply);
464-
} else if (k instanceof KBag) {
465-
KBag kBag = (KBag) k;
467+
} else if (k instanceof KApply && ((KApply) k).klabel() == Labels.KBag()) {
468+
KApply kBag = (KApply) k;
466469
List<K> bagItems = kBag.list();
467470
org.kframework.kil.Bag kilBag = new org.kframework.kil.Bag();
468471
List<org.kframework.kil.Term> kilBagItems = new ArrayList<>();
469472
for (K bagItem : bagItems) {
470-
if (bagItem instanceof KBag) {
471-
KBag item = (KBag) bagItem;
473+
if (k instanceof KApply && ((KApply) k).klabel() == Labels.KBag()) {
474+
KApply item = (KApply) bagItem;
472475
List<K> kbagItems = item.list();
473476
kilBagItems.addAll(kbagItems.stream().map(this::convertK)
474477
.collect(Collectors.toList()));
@@ -536,16 +539,17 @@ public org.kframework.kil.Variable convertKVariable(KVariable var) {
536539
}
537540

538541
public org.kframework.kil.Term convertKBool(K k) {
539-
if (k instanceof KBoolean) {
542+
if(k instanceof KToken && ((KToken) k).sort() == Sorts.KBoolean()) {
540543
return null; // FIXME
544+
// throw new AssertionError("Unimplemented");
541545
}
542546
return convertK(k);
543547
}
544548

545549
public org.kframework.kil.Term convertKApply(KApply kApply) {
546550
KLabel label = kApply.klabel();
547551
List<K> contents = kApply.list();
548-
if (label == Hole$.MODULE$) {
552+
if (label == Labels.Hole()) {
549553
Sort sort = ((KToken) contents.get(0)).sort();
550554
return new org.kframework.kil.Hole(org.kframework.kil.Sort.of(sort.name()));
551555
} else {

‎kore/src/main/scala/org/kframework/builtin/Labels.scala‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package org.kframework.builtin
2+
3+
import org.kframework.kore.KLabel
4+
5+
object Labels {
6+
val Hole = KLabel("HOLE")
7+
val KBag = KLabel("KBag")
8+
}

‎kore/src/main/scala/org/kframework/builtin/Sorts.scala‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// Copyright (c) 2014 K Team. All Rights Reserved.
2+
3+
package org.kframework.builtin
4+
5+
import org.kframework.kore.UninterpretedSort
6+
import org.kframework.kore.KLabel
7+
8+
object Sorts {
9+
val KString = UninterpretedSort("KString")
10+
val KBoolean = UninterpretedSort("KBoolean")
11+
val KInt = UninterpretedSort("KInt")
12+
}

kore/src/main/scala/org/kframework/kore/builtins.scala renamed to kore/src/main/scala/org/kframework/builtin/builtins.scala

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
11
// Copyright (c) 2014 K Team. All Rights Reserved.
22

3-
package org.kframework.kore
3+
package org.kframework.builtin
44

55
import org.kframework._
6-
6+
import kore._
77
import KORE._
8-
import KBoolean._
98
import scala.collection.mutable.Builder
109
import scala.collection.mutable.SetBuilder
1110

@@ -47,7 +46,7 @@ object KString extends Sort with KLabel {
4746
val name: String = "Int"
4847
}
4948

50-
case class KBag private[kore] (val klist: KList) extends KAbstractCollection with Associative[KBag] {
49+
case class KBag(val klist: KList) extends KAbstractCollection with Associative[KBag] {
5150
type This = KBag
5251

5352
def canEqual(that: Any) = that.isInstanceOf[KBag]
@@ -60,7 +59,7 @@ case class KBag private[kore] (val klist: KList) extends KAbstractCollection wit
6059
override def toString = if (isEmpty) ".Bag" else "Bag(" + mkString(",") + ")"
6160
}
6261

63-
case class KSet private[kore] (val content: Set[K]) extends KAbstractCollection with Associative[KBag] {
62+
case class KSet(val content: Set[K]) extends KAbstractCollection with Associative[KBag] {
6463
type This = KSet
6564

6665
def canEqual(that: Any) = that.isInstanceOf[KSet]
@@ -84,10 +83,6 @@ object KBag extends Sort with KLabel {
8483
val name: String = "Bag"
8584
}
8685

87-
case object Hole extends KLabel with Sort {
88-
val name = "HOLE"
89-
}
90-
9186
object Location {
9287
import KInt._
9388

‎kore/src/main/scala/org/kframework/kore/Attributes.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
package org.kframework.kore
22

33
import org.kframework._
4-
54
import scala.collection.mutable.SetBuilder
65
import scala.collection.mutable.Builder
6+
import org.kframework.builtin.Sorts
77

88
case class Attributes(att: Set[K] = Set()) extends Collection[K] with Indexed[String, KList] with AttributesToString {
99
type This = Attributes
@@ -31,7 +31,7 @@ case class Attributes(att: Set[K] = Set()) extends Collection[K] with Indexed[St
3131

3232
def +(k: K): Attributes = new Attributes(att + k)
3333
def +(k: String): Attributes = add(KApply(KLabel(k), KList()))
34-
def +(kv: (String, String)): Attributes = add(KApply(KLabel(kv._1), KList(KToken(KString, kv._2))))
34+
def +(kv: (String, String)): Attributes = add(KApply(KLabel(kv._1), KList(KToken(Sorts.KString, kv._2))))
3535

3636
def ++(that: Attributes) = new Attributes(att ++ that.att)
3737

‎kore/src/main/scala/org/kframework/kore/Constructors.scala‎

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ package org.kframework.kore;
55
import java.util.List
66
import scala.collection.Seq
77
import collection.JavaConverters._
8-
import org.kframework.kore
8+
import org.kframework._
99
import org.kframework.Collector
1010
import org.kframework.CombinerFromBuilder
1111

@@ -22,15 +22,11 @@ object Constructors {
2222
def Attributes(ks: Set[K]) = kore.Attributes(ks)
2323
@annotation.varargs def Attributes(ks: K*) = kore.Attributes(ks: _*)
2424

25-
def Hole = kore.Hole
25+
// @annotation.varargs def KBag(ks: K*) = kore.KBag(ks)
2626

27-
def KBagLabel = kore.KBag
27+
def Location(startLine: Int, startColumn: Int, endLine: Int, endColumn: Int) = builtin.Location(startLine, startColumn, endLine, endColumn)
2828

29-
@annotation.varargs def KBag(ks: K*) = kore.KBag(ks)
30-
31-
def Location(startLine: Int, startColumn: Int, endLine: Int, endColumn: Int) = kore.Location(startLine, startColumn, endLine, endColumn)
32-
33-
def KBag(ks: KList) = kore.KBag(ks);
29+
// def KBag(ks: KList) = kore.KBag(ks);
3430

3531
def Sort(name: String) = kore.Sort(name);
3632

@@ -63,7 +59,7 @@ object Constructors {
6359

6460
def KRewrite(left: K, right: K, att: Attributes) = kore.KRewrite(left, right, att)
6561

66-
def KInt(n: Int) = kore.KInt(n)
62+
// def KInt(n: Int) = kore.KInt(n)
6763

6864
def stream(c: KCollection) = org.kframework.Collections.stream(c);
6965

‎kore/src/main/scala/org/kframework/kore/Sorts.scala‎

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,3 @@ object Sort {
1212
}
1313

1414
case class UninterpretedSort(name: String) extends Sort
15-
16-
object Sorts {
17-
import org.kframework.kore
18-
19-
def KString = kore.KString
20-
}

‎kore/src/main/scala/org/kframework/kore/kast.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ trait KToken extends KItem with KORE with KTokenToString {
4040

4141
/* Data Structures */
4242

43-
class KList(protected[kore] val delegate: List[K])
43+
class KList(val delegate: List[K])
4444
extends Collection[K] with Indexed[Int, K]
4545
with KListToString with KORE {
4646
type This = KList

0 commit comments

Comments
 (0)