Skip to content

Commit eed1405

Browse files
author
Dwight Guth
committed
first revision of ocaml backend
Former-commit-id: e91d7236bc6547b8ed7419378b923d4eba33b828 [formerly 7249794cf965e8a718a14f6dcbb069d8d893da25] Former-commit-id: 4a08053f0b6446f560fb3518e2ad6a14cc85210d
1 parent 470169c commit eed1405

72 files changed

Lines changed: 2944 additions & 263 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

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

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,9 @@
1818
import org.kframework.kil.Attribute;
1919
import org.kframework.kore.KApply;
2020
import org.kframework.kore.KLabel;
21+
import org.kframework.kore.KVariable;
22+
import org.kframework.kore.convertors.KOREtoKIL;
23+
import org.kframework.tiny.KVar;
2124

2225
import java.util.List;
2326
import java.util.stream.Collectors;
@@ -61,6 +64,9 @@ public KApply KApply(KLabel klabel, org.kframework.kore.KList klist, Att att) {
6164
}
6265

6366
public Term KApply1(org.kframework.kore.KLabel klabel, org.kframework.kore.KList klist, Att att) {
67+
if (klabel instanceof KVariable) {
68+
return KItem.of(KVariable(klabel.name(), ((KVariable) klabel).att()), KList(klist.items()), context);
69+
}
6470
return KItem.of(KLabel(klabel.name()), KList(klist.items()), context);
6571
}
6672

@@ -74,7 +80,9 @@ public <KK extends org.kframework.kore.K> KSequence KSequence(List<KK> items, At
7480

7581
@Override
7682
public Variable KVariable(String name, Att att) {
77-
return new Variable(name, Sort.of(att.<String>getOptional(Attribute.SORT_KEY).orElse("K")));
83+
Variable var = new Variable(name, Sort.of(att.<String>getOptional(Attribute.SORT_KEY).orElse("K")));
84+
var.setAttributes(new KOREtoKIL().convertAttributes(att));
85+
return var;
7886
}
7987

8088
@Override
@@ -84,6 +92,9 @@ public org.kframework.kore.KRewrite KRewrite(org.kframework.kore.K left, org.kfr
8492

8593
@Override
8694
public InjectedKLabel InjectedKLabel(org.kframework.kore.KLabel klabel, Att att) {
95+
if (klabel instanceof KVariable) {
96+
return new InjectedKLabel(KVariable(klabel.name(), att));
97+
}
8798
return new InjectedKLabel(KLabel(klabel.name()));
8899
}
89100

java-backend/src/main/java/org/kframework/backend/java/kil/AssociativeCommutativeCollection.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
* Common parent for {@link org.kframework.backend.java.kil.BuiltinMap} and
1111
* {@link org.kframework.backend.java.kil.BuiltinSet}.
1212
*/
13-
public abstract class AssociativeCommutativeCollection extends Collection {
13+
public abstract class AssociativeCommutativeCollection extends Collection implements KItemCollection {
1414

1515
protected final ImmutableMultiset<KItem> collectionPatterns;
1616
protected final ImmutableMultiset<Term> collectionFunctions;

java-backend/src/main/java/org/kframework/backend/java/kil/BuiltinList.java

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,11 @@
11
// Copyright (c) 2013-2015 K Team. All Rights Reserved.
22
package org.kframework.backend.java.kil;
33

4+
import com.google.common.base.Joiner;
5+
import com.google.common.collect.ImmutableList;
6+
import com.google.common.collect.Iterables;
7+
import com.google.common.collect.Lists;
8+
import org.apache.commons.collections4.ListUtils;
49
import org.kframework.backend.java.symbolic.Matcher;
510
import org.kframework.backend.java.symbolic.Transformer;
611
import org.kframework.backend.java.symbolic.Unifier;
@@ -10,25 +15,19 @@
1015
import org.kframework.kil.DataStructureSort;
1116
import org.kframework.utils.errorsystem.KEMException;
1217
import org.kframework.utils.errorsystem.KExceptionManager;
18+
1319
import java.util.ArrayList;
1420
import java.util.List;
1521
import java.util.function.Consumer;
1622
import java.util.stream.Collectors;
1723

18-
import org.apache.commons.collections4.ListUtils;
19-
20-
import com.google.common.base.Joiner;
21-
import com.google.common.collect.ImmutableList;
22-
import com.google.common.collect.Iterables;
23-
import com.google.common.collect.Lists;
24-
2524

2625
/**
2726
* Class representing a list.
2827
*
2928
* @author: YilongL
3029
*/
31-
public class BuiltinList extends Collection {
30+
public class BuiltinList extends Collection implements KItemCollection {
3231

3332
private static enum BaseTermType {
3433
VARIABLE, FUNCTION, PATTERN, LIST;

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
11
// Copyright (c) 2013-2015 K Team. All Rights Reserved.
22
package org.kframework.backend.java.kil;
33

4+
import com.google.common.collect.ImmutableListMultimap;
5+
import com.google.common.collect.ImmutableMultiset;
6+
import com.google.common.collect.ListMultimap;
7+
import com.google.common.collect.Multiset;
48
import org.kframework.backend.java.symbolic.Matcher;
59
import org.kframework.backend.java.symbolic.Transformer;
610
import org.kframework.backend.java.symbolic.Unifier;
@@ -13,14 +17,8 @@
1317

1418
import java.io.Serializable;
1519
import java.util.Iterator;
16-
import java.util.List;
1720
import java.util.Set;
1821

19-
import com.google.common.collect.ImmutableListMultimap;
20-
import com.google.common.collect.ImmutableMultiset;
21-
import com.google.common.collect.ListMultimap;
22-
import com.google.common.collect.Multiset;
23-
2422

2523
/**
2624
* Represents a collection of cells. The ordering of the internal cells
@@ -282,11 +280,6 @@ public String toString() {
282280
}
283281
}
284282

285-
@Override
286-
public List<Term> getKComponents() {
287-
throw new UnsupportedOperationException();
288-
}
289-
290283
@Override
291284
public void accept(Unifier unifier, Term pattern) {
292285
unifier.unify(this, pattern);

java-backend/src/main/java/org/kframework/backend/java/kil/Collection.java

Lines changed: 5 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
* @author AndreiS
1313
*/
1414
@SuppressWarnings("serial")
15-
public abstract class Collection extends Term implements CollectionInternalRepresentation {
15+
public abstract class Collection extends Term {
1616

1717
/**
1818
* Represents the rest part of this {@code Collection} which is not
@@ -81,28 +81,6 @@ public final boolean isSymbolic() {
8181
return false;
8282
}
8383

84-
@Override
85-
public Term toKore() {
86-
return toKore(context);
87-
}
88-
89-
@Override
90-
public KLabel constructorLabel() {
91-
return KLabelConstant.of(
92-
context.definition().dataStructureSortOf(sort()).constructorLabel(),
93-
context.definition());
94-
}
95-
96-
@Override
97-
public KItem unit() {
98-
return KItem.of(
99-
KLabelConstant.of(
100-
context.definition().dataStructureSortOf(sort()).unitLabel(),
101-
context.definition()),
102-
KList.EMPTY,
103-
context);
104-
}
105-
10684
@Override
10785
public void accept(Visitor visitor) {
10886
visitor.visit(this);
@@ -113,4 +91,8 @@ public ASTNode accept(Transformer transformer) {
11391
return transformer.transform(this);
11492
}
11593

94+
public TermContext context() {
95+
return context;
96+
}
97+
11698
}

java-backend/src/main/java/org/kframework/backend/java/kil/KCollection.java

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -106,11 +106,6 @@ public String toString() {
106106
return stringBuilder.toString();
107107
}
108108

109-
@Override
110-
public List<Term> getKComponents() {
111-
throw new UnsupportedOperationException();
112-
}
113-
114109
@Override
115110
public void accept(Visitor visitor) {
116111
visitor.visit(this);
Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework.backend.java.kil;
3+
4+
/**
5+
* Created by dwightguth on 5/8/15.
6+
*/
7+
public interface KItemCollection extends CollectionInternalRepresentation {
8+
9+
TermContext context();
10+
Sort sort();
11+
12+
@Override
13+
default Term toKore() {
14+
return toKore(context());
15+
}
16+
17+
@Override
18+
default KLabel constructorLabel() {
19+
return KLabelConstant.of(
20+
context().definition().dataStructureSortOf(sort()).constructorLabel(),
21+
context().definition());
22+
}
23+
24+
@Override
25+
default KItem unit() {
26+
return KItem.of(
27+
KLabelConstant.of(
28+
context().definition().dataStructureSortOf(sort()).unitLabel(),
29+
context().definition()),
30+
KList.EMPTY,
31+
context());
32+
}
33+
}

java-backend/src/main/java/org/kframework/backend/java/kil/KSequence.java

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,17 @@
11
// Copyright (c) 2013-2015 K Team. All Rights Reserved.
22
package org.kframework.backend.java.kil;
33

4-
import java.util.Collections;
5-
import java.util.List;
6-
4+
import com.google.common.collect.ImmutableList;
5+
import org.apache.commons.collections4.ListUtils;
76
import org.kframework.backend.java.symbolic.Matcher;
87
import org.kframework.backend.java.symbolic.Transformer;
98
import org.kframework.backend.java.symbolic.Unifier;
109
import org.kframework.backend.java.symbolic.Visitor;
1110
import org.kframework.kil.ASTNode;
11+
import org.kframework.kore.K;
1212

13-
import com.google.common.collect.ImmutableList;
13+
import java.util.Collections;
14+
import java.util.List;
1415

1516

1617
/**
@@ -102,6 +103,15 @@ private KSequence(ImmutableList<Term> contents, Variable frame, ImmutableList<Va
102103
this.kSequenceVariables = kSequenceVariables;
103104
}
104105

106+
@Override
107+
public List<K> items() {
108+
if (frame != null) {
109+
return ListUtils.union(super.items(), Collections.singletonList(frame));
110+
} else {
111+
return super.items();
112+
}
113+
}
114+
105115
@Override
106116
public Term fragment(int fromIndex) {
107117
if (fromIndex == contents.size()) {

java-backend/src/main/java/org/kframework/backend/java/kil/Term.java

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
package org.kframework.backend.java.kil;
33

44
import org.kframework.attributes.Att;
5-
import org.kframework.attributes.Source;
65
import org.kframework.attributes.Location;
6+
import org.kframework.attributes.Source;
77
import org.kframework.backend.java.indexing.IndexingPair;
88
import org.kframework.backend.java.symbolic.BottomUpVisitor;
99
import org.kframework.backend.java.symbolic.CopyOnShareSubstAndEvalTransformer;
@@ -13,6 +13,7 @@
1313
import org.kframework.backend.java.symbolic.Transformable;
1414
import org.kframework.backend.java.symbolic.Unifiable;
1515
import org.kframework.backend.java.util.Utils;
16+
import org.kframework.kore.convertors.KILtoInnerKORE;
1617

1718
import java.util.ArrayList;
1819
import java.util.Collections;
@@ -246,7 +247,7 @@ public final int hashCode() {
246247
public abstract boolean equals(Object object);
247248

248249
public Att att() {
249-
return Att.apply();
250+
return new KILtoInnerKORE(null, true).convertAttributes(this);
250251
}
251252

252253
public Location location() { return getLocation(); }

0 commit comments

Comments
 (0)