Skip to content

Commit a5c05c5

Browse files
author
dwightguth
committed
Revert "added support for cells with multiplicity=* in the kore to java-backe…"
Former-commit-id: ae1cea6ce52699d6efd544abf28c094431de7749 [formerly 36b72f70eca5119414be1f91260d28c91c32ba18] Former-commit-id: 644f8962c21549bf710943859864e1ac8f88aed1
1 parent 7e31c32 commit a5c05c5

22 files changed

Lines changed: 92 additions & 245 deletions

File tree

‎java-backend/pom.xml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@
3636
<dependency>
3737
<groupId>uk.com.robust-it</groupId>
3838
<artifactId>cloning</artifactId>
39-
<version>1.9.2</version>
39+
<version>1.9.0</version>
4040
</dependency>
4141
<dependency>
4242
<groupId>com.microsoft.z3</groupId>

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

Lines changed: 4 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,10 @@
55
import org.kframework.attributes.Att;
66
import org.kframework.attributes.Location;
77
import org.kframework.attributes.Source;
8-
import org.kframework.backend.java.kil.CellCollection;
9-
import org.kframework.backend.java.kil.CellLabel;
10-
import org.kframework.backend.java.kil.Definition;
118
import org.kframework.backend.java.kil.InjectedKLabel;
129
import org.kframework.backend.java.kil.KCollection;
1310
import org.kframework.backend.java.kil.KItem;
1411
import org.kframework.backend.java.kil.KLabelConstant;
15-
import org.kframework.backend.java.kil.KLabelInjection;
1612
import org.kframework.backend.java.kil.KList;
1713
import org.kframework.backend.java.kil.KSequence;
1814
import org.kframework.backend.java.kil.Kind;
@@ -24,17 +20,13 @@
2420
import org.kframework.backend.java.kil.Variable;
2521
import org.kframework.backend.java.symbolic.ConjunctiveFormula;
2622
import org.kframework.definition.Module;
27-
import org.kframework.compile.ConfigurationInfo;
2823
import org.kframework.kil.Attribute;
29-
import org.kframework.kil.Cell;
30-
import org.kframework.kore.Assoc;
3124
import org.kframework.kore.K;
3225
import org.kframework.kore.KApply;
3326
import org.kframework.kore.KLabel;
3427
import org.kframework.kore.KVariable;
3528
import org.kframework.kore.compile.RewriteToTop;
3629
import org.kframework.kore.convertors.KOREtoKIL;
37-
import scala.Option;
3830

3931
import java.util.Collections;
4032
import java.util.List;
@@ -46,13 +38,9 @@
4638
*/
4739
public class KOREtoBackendKIL extends org.kframework.kore.AbstractConstructors<org.kframework.kore.K> {
4840

49-
private final Module module;
50-
private final Definition definition;
5141
private final TermContext context;
5242

53-
public KOREtoBackendKIL(Module module, Definition definition, TermContext context) {
54-
this.module = module;
55-
this.definition = definition;
43+
public KOREtoBackendKIL(TermContext context) {
5644
this.context = context;
5745
}
5846

@@ -121,42 +109,14 @@ private Term convert(KLabel klabel) {
121109
}
122110
}
123111

124-
private Term CellCollection(org.kframework.kore.KLabel klabel, org.kframework.kore.KList klist) {
125-
final CellCollection.Builder builder = CellCollection.builder(definition);
126-
Assoc.flatten(klabel, klist.items(), module).stream().forEach(k -> {
127-
if (k instanceof KApply) {
128-
builder.put(
129-
CellLabel.of(((KApply) k).klabel().name()),
130-
KList(((KApply) k).klist().items()));
131-
} else if (k instanceof KVariable) {
132-
// TODO(AndreiS): ensure the ... variables do not have sort K
133-
// assert k.att().contains(Attribute.SORT_KEY);
134-
builder.concatenate(new Variable(((org.kframework.kore.KVariable) k).name(), Sort.BAG));
135-
} else {
136-
assert false : "unexpected CellCollection term " + k;
137-
}
138-
});
139-
return builder.build();
140-
}
141-
142112
public Term convert(org.kframework.kore.K k) {
143113
if (k instanceof Term)
144114
return (Term) k;
145115
else if (k instanceof org.kframework.kore.KToken)
146116
return KToken(((org.kframework.kore.KToken) k).s(), ((org.kframework.kore.KToken) k).sort(), k.att());
147-
else if (k instanceof org.kframework.kore.KApply) {
148-
KLabel klabel = ((KApply) k).klabel();
149-
org.kframework.kore.KList klist = ((KApply) k).klist();
150-
Option<Att> attOption = module.attributesFor().get(klabel);
151-
if (attOption.isDefined() && attOption.get().contains(Attribute.CELL_BAG))
152-
return KLabelInjection.injectionOf(CellCollection(klabel, klist), context);
153-
else if (definition.cellMultiplicity(CellLabel.of(klabel.name())) == ConfigurationInfo.Multiplicity.STAR)
154-
return KLabelInjection.injectionOf(
155-
CellCollection.builder(definition).put(CellLabel.of(klabel.name()), KList(klist.items())).build(),
156-
context);
157-
else
158-
return KApply1(klabel, klist, k.att());
159-
} else if (k instanceof org.kframework.kore.KSequence)
117+
else if (k instanceof org.kframework.kore.KApply)
118+
return KApply1(((KApply) k).klabel(), ((KApply) k).klist(), k.att());
119+
else if (k instanceof org.kframework.kore.KSequence)
160120
return KSequence(((org.kframework.kore.KSequence) k).items(), k.att());
161121
else if (k instanceof org.kframework.kore.KVariable)
162122
return KVariable(((org.kframework.kore.KVariable) k).name(), k.att());
@@ -200,20 +160,4 @@ public Rule convert(Optional<Module> module, org.kframework.definition.Rule rule
200160
context);
201161

202162
}
203-
204-
205-
public static ConfigurationInfo.Multiplicity kil2koreMultiplicity(Cell.Multiplicity multiplicity) {
206-
switch (multiplicity) {
207-
case ONE:
208-
return ConfigurationInfo.Multiplicity.ONE;
209-
case ANY:
210-
case SOME:
211-
return ConfigurationInfo.Multiplicity.STAR;
212-
case MAYBE:
213-
return ConfigurationInfo.Multiplicity.OPTIONAL;
214-
default:
215-
throw new IllegalArgumentException(multiplicity.toString());
216-
}
217-
}
218-
219163
}

‎java-backend/src/main/java/org/kframework/backend/java/indexing/IndexingCellsCollector.java‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77
import org.kframework.backend.java.kil.CellCollection;
88
import org.kframework.backend.java.kil.CellLabel;
99
import org.kframework.backend.java.kil.Definition;
10-
import org.kframework.backend.java.kil.KItem;
1110
import org.kframework.backend.java.kil.Term;
1211
import org.kframework.backend.java.symbolic.BottomUpVisitor;
1312
import org.kframework.kil.Attribute;
@@ -56,7 +55,4 @@ public void visit(CellCollection cellCollection) {
5655
}
5756
}
5857
}
59-
60-
@Override
61-
public void visit(KItem kItem) {}
6258
}

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

Lines changed: 13 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -8,18 +8,14 @@
88
import org.kframework.backend.java.symbolic.Transformer;
99
import org.kframework.backend.java.symbolic.Visitor;
1010
import org.kframework.backend.java.util.Utils;
11-
import org.kframework.compile.ConfigurationInfo;
1211
import org.kframework.kil.ASTNode;
1312
import org.kframework.kil.DataStructureSort;
1413
import org.kframework.kil.DataStructureSort.Label;
15-
import org.kframework.kore.KApply;
1614
import org.kframework.utils.errorsystem.KEMException;
1715

1816
import java.io.Serializable;
1917
import java.util.Iterator;
20-
import java.util.List;
2118
import java.util.Set;
22-
import java.util.stream.Collectors;
2319

2420

2521
/**
@@ -30,7 +26,7 @@
3026
* @author AndreiS
3127
*
3228
*/
33-
public class CellCollection extends Collection implements CollectionInternalRepresentation {
29+
public class CellCollection extends Collection {
3430

3531
public static class Cell implements Serializable {
3632
private final CellLabel cellLabel;
@@ -84,8 +80,7 @@ public String toString() {
8480
public static final CellCollection EMPTY = new CellCollection(
8581
ImmutableListMultimap.of(),
8682
ImmutableMultiset.of(),
87-
false,
88-
null);
83+
false);
8984

9085
/**
9186
* Choose {@code ListMultimap} over {@code SetMultimap} because we need to
@@ -102,8 +97,6 @@ public String toString() {
10297
// TODO(AndreiS): handle multiplicity='+'
10398
private final boolean hasMultiplicityCell;
10499

105-
private final Definition definition;
106-
107100
public static CellCollection singleton(CellLabel cellLabel, Term content, Definition definition) {
108101
return (CellCollection) builder(definition).put(cellLabel, content).build();
109102
}
@@ -125,19 +118,17 @@ private CellCollection(
125118
ListMultimap<CellLabel, Cell> cells,
126119
Multiset<Variable> collectionVariables,
127120
Definition definition) {
128-
this(cells, collectionVariables, numOfMultiplicityCellLabels(cells, definition) > 0, definition);
121+
this(cells, collectionVariables, numOfMultiplicityCellLabels(cells, definition) > 0);
129122
}
130123

131124
private CellCollection(
132125
ListMultimap<CellLabel, Cell> cells,
133126
Multiset<Variable> collectionVariables,
134-
boolean hasMultiplicityCell,
135-
Definition definition) {
127+
boolean hasMultiplicityCell) {
136128
super(computeFrame(collectionVariables), Kind.CELL_COLLECTION, null);
137129
this.cells = cells;
138130
this.collectionVariables = collectionVariables;
139131
this.hasMultiplicityCell = hasMultiplicityCell;
140-
this.definition = definition;
141132
}
142133

143134
private static Variable computeFrame(Multiset<Variable> collectionVariables) {
@@ -147,13 +138,15 @@ private static Variable computeFrame(Multiset<Variable> collectionVariables) {
147138
private static int numOfMultiplicityCellLabels(ListMultimap<CellLabel, Cell> cells, Definition definition) {
148139
int count = 0;
149140
for (CellLabel cellLabel : cells.keySet()) {
150-
if (definition.cellMultiplicity(cellLabel) == ConfigurationInfo.Multiplicity.STAR) {
151-
count++;
152-
} else {
153-
if (cells.get(cellLabel).size() != 1) {
154-
throw KEMException.criticalError("Cell label " + cellLabel + " does not have "
155-
+ "multiplicity='*', but multiple cells found: " + cells.get(cellLabel)
156-
+ "\nExamine the last rule applied to determine the source of the error.");
141+
if (definition.getConfigurationStructureMap().containsKey(cellLabel.name())) {
142+
if (definition.getConfigurationStructureMap().get(cellLabel.name()).isStarOrPlus()) {
143+
count++;
144+
} else {
145+
if (cells.get(cellLabel).size() != 1) {
146+
throw KEMException.criticalError("Cell label " + cellLabel + " does not have "
147+
+ "multiplicity='*', but multiple cells found: " + cells.get(cellLabel)
148+
+ "\nExamine the last rule applied to determine the source of the error.");
149+
}
157150
}
158151
}
159152
}
@@ -240,39 +233,6 @@ public boolean isExactSort() {
240233
return true;
241234
}
242235

243-
@Override
244-
public List<Term> getKComponents() {
245-
return cells.values().stream()
246-
.map(c -> new KItem(
247-
KLabelConstant.of(c.cellLabel.name(), definition),
248-
KList.concatenate(c.content),
249-
sort(),
250-
true))
251-
.collect(Collectors.toList());
252-
}
253-
254-
@Override
255-
public KLabel constructorLabel() {
256-
org.kframework.kore.KLabel kLabel = definition.configurationInfo().getConcat(getCellSort());
257-
return KLabelConstant.of(kLabel.name(), definition);
258-
}
259-
260-
@Override
261-
public Term unit() {
262-
org.kframework.kore.KApply kApply = definition.configurationInfo().getUnit(getCellSort());
263-
return new KItem(
264-
KLabelConstant.of(kApply.klabel().name(), definition),
265-
KList.EMPTY,
266-
sort(),
267-
true);
268-
}
269-
270-
private org.kframework.kore.Sort getCellSort() {
271-
assert hasMultiplicityCell;
272-
return definition.configurationInfo().getCellSort(
273-
KLabelConstant.of(cells.keys().iterator().next().name(), definition));
274-
}
275-
276236
@Override
277237
public Sort sort() {
278238
return kind.asSort();

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

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,7 @@ public interface CollectionInternalRepresentation extends KItemRepresentation {
1010
* The returned representation is not unique (due to associativity/commutativity).
1111
* {@link Term#evaluate} is the inverse operation.
1212
*/
13-
@Override
14-
default Term toKore() {
13+
public default Term toKore(TermContext context) {
1514
List<Term> components = getKComponents();
1615

1716
if (components.isEmpty()) {
@@ -21,11 +20,10 @@ default Term toKore() {
2120
Term result = components.get(components.size() - 1);
2221
for (int i = components.size() - 2; i >= 0; --i) {
2322
Term component = components.get(i);
24-
result = new KItem(
23+
result = KItem.of(
2524
constructorLabel(),
2625
KList.concatenate(component, result),
27-
sort(),
28-
true,
26+
context,
2927
component.getSource(),
3028
component.getLocation());
3129
}
@@ -43,12 +41,10 @@ default Term toKore() {
4341
/**
4442
* Returns the KLabel that constructs an instance of this collection/formula.
4543
*/
46-
KLabel constructorLabel();
44+
public KLabel constructorLabel();
4745

4846
/**
4947
* Returns the KItem representation of the unit of this collection/formula.
5048
*/
51-
Term unit();
52-
53-
Sort sort();
49+
public Term unit();
5450
}

0 commit comments

Comments
 (0)