Skip to content
Snippets Groups Projects
Commit 58ce9546 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

simplifications in types

parent 9281a54d
Branches
Tags
No related merge requests found
Pipeline #149331 passed
......@@ -31,10 +31,6 @@ public abstract class AbstractHasFollowers extends TLAType {
followers.remove(o);
}
public String followersToString() {
return followers.toString();
}
protected void setFollowersTo(TLAType newType) {
if (this.followers == null)
return;
......
package de.tla2b.types;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.util.ASTBuilder;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
......@@ -12,21 +13,12 @@ import java.util.Set;
public class EnumType extends AbstractHasFollowers {
public final Set<String> modelvalues;
public int id;
private boolean noVal = false;
public EnumType(List<String> enums) {
super(MODELVALUE);
modelvalues = new LinkedHashSet<>(enums);
}
public void setNoVal() {
noVal = true;
}
public boolean hasNoVal() {
return noVal;
}
public Set<String> getValues() {
return modelvalues;
}
......@@ -74,7 +66,7 @@ public class EnumType extends AbstractHasFollowers {
@Override
public PExpression getBNode() {
return BAstCreator.createIdentifierNode("ENUM" + id);
return ASTBuilder.createIdentifier("ENUM" + id);
}
public void apply(TypeVisitorInterface t) {
......
......@@ -11,32 +11,26 @@ import java.util.Map.Entry;
import java.util.Set;
public class StructOrFunctionType extends AbstractHasFollowers {
private final Map<String, TLAType> types;
private final Map<String, TLAType> types = new LinkedHashMap<>();
public StructOrFunctionType(String name, TLAType type) {
super(STRUCT_OR_FUNCTION);
types = new LinkedHashMap<>();
types.put(name, type);
}
public StructOrFunctionType() {
super(STRUCT_OR_FUNCTION);
types = new LinkedHashMap<>();
}
public void setNewType(TLAType old, TLAType New) {
Set<Entry<String, TLAType>> set = types.entrySet();
for (Entry<String, TLAType> entry : set) {
if (entry.getValue() == old) {
String key = entry.getKey();
if (New instanceof AbstractHasFollowers) {
// set new reference
types.forEach((name, type) -> {
if (type == old) {
if (New instanceof AbstractHasFollowers) { // set new reference
((AbstractHasFollowers) New).addFollower(this);
}
types.put(key, New);
}
types.put(name, New);
}
});
testRecord();
}
......
......@@ -5,16 +5,15 @@ import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
import java.util.*;
import java.util.Map.Entry;
import java.util.stream.Collectors;
public class StructType extends AbstractHasFollowers {
private final LinkedHashMap<String, TLAType> types;
private final Map<String, TLAType> types = new LinkedHashMap<>();
private boolean extensible;
private boolean incompleteStruct;
public StructType() {
super(STRUCT);
types = new LinkedHashMap<>();
extensible = false;
incompleteStruct = false;
}
......@@ -34,26 +33,17 @@ public class StructType extends AbstractHasFollowers {
}
public void add(String name, TLAType type) {
if (type instanceof AbstractHasFollowers) {
// set new reference
if (type instanceof AbstractHasFollowers) { // set new reference
((AbstractHasFollowers) type).addFollower(this);
}
types.put(name, type);
}
public void setNewType(TLAType old, TLAType New) {
Set<Entry<String, TLAType>> set = types.entrySet();
for (Entry<String, TLAType> entry : set) {
if (entry.getValue() == old) {
String key = entry.getKey();
if (New instanceof AbstractHasFollowers) {
// set new reference
((AbstractHasFollowers) New).addFollower(this);
}
types.put(key, New);
}
}
types.forEach((name, type) -> {
if (type == old)
add(name, New);
});
}
@Override
......@@ -71,22 +61,14 @@ public class StructType extends AbstractHasFollowers {
}
if (o.getKind() == UNTYPED)
return true;
if (o instanceof StructOrFunctionType) {
return o.compare(this);
}
if (o instanceof StructType) {
StructType s = (StructType) o;
for (String fieldName : types.keySet()) {
if (s.types.containsKey(fieldName)) {
if (!this.types.get(fieldName).compare(
s.types.get(fieldName))) {
return false;
}
}
}
return true;
return types.keySet().stream()
.filter(s.types::containsKey)
.allMatch(fieldName -> this.types.get(fieldName).compare(s.types.get(fieldName)));
}
return false;
}
......@@ -123,11 +105,7 @@ public class StructType extends AbstractHasFollowers {
TLAType res = this.types.get(fieldName).unify(sType);
this.types.put(fieldName, res);
} else {
if (sType instanceof AbstractHasFollowers) {
// set new reference
((AbstractHasFollowers) sType).addFollower(this);
}
this.types.put(fieldName, sType);
add(fieldName, sType);
}
this.incompleteStruct = false;
}
......@@ -139,68 +117,38 @@ public class StructType extends AbstractHasFollowers {
@Override
public StructType cloneTLAType() {
StructType clone = new StructType();
Set<Entry<String, TLAType>> set = this.types.entrySet();
for (Entry<String, TLAType> entry : set) {
String field = entry.getKey();
TLAType type = entry.getValue().cloneTLAType();
clone.add(field, type);
}
this.types.forEach((field, type) -> clone.add(field, type.cloneTLAType()));
return clone;
}
public ArrayList<String> getFields() {
ArrayList<String> fields = new ArrayList<>(this.types.keySet());
return fields;
public List<String> getFields() {
return new ArrayList<>(this.types.keySet());
}
@Override
public boolean contains(TLAType o) {
for (TLAType bType : types.values()) {
if (bType.equals(o) || bType.contains(o))
return true;
}
return false;
return types.values().stream().anyMatch(bType -> bType.equals(o) || bType.contains(o));
}
@Override
public String toString() {
StringBuilder sb = new StringBuilder();
sb.append("struct(");
Iterator<String> keys = types.keySet().iterator();
if (!keys.hasNext()) {
sb.append("...");
}
while (keys.hasNext()) {
String fieldName = keys.next();
sb.append(fieldName).append(":").append(types.get(fieldName));
if (keys.hasNext())
sb.append(",");
}
sb.append(")");
return sb.toString();
if (types.isEmpty())
return "struct(...)";
return "struct(" + types.entrySet().stream()
.map(entry -> entry.getKey() + ":" + entry.getValue())
.collect(Collectors.joining(",")) + ")";
}
@Override
public PExpression getBNode() {
List<PRecEntry> recList = new ArrayList<>();
for (Entry<String, TLAType> entry : types.entrySet()) {
ARecEntry rec = new ARecEntry();
rec.setIdentifier(new TIdentifierLiteral(entry.getKey()));
if (extensible) {
AMultOrCartExpression cart = new AMultOrCartExpression();
cart.setLeft(new ABoolSetExpression());
cart.setRight(entry.getValue().getBNode());
APowSubsetExpression pow = new APowSubsetExpression(cart);
rec.setValue(pow);
} else {
rec.setValue(entry.getValue().getBNode());
}
recList.add(rec);
}
types.forEach((id, type) -> {
PExpression value = extensible
? new APowSubsetExpression(new AMultOrCartExpression(new ABoolSetExpression(), type.getBNode()))
: type.getBNode();
recList.add(new ARecEntry(new TIdentifierLiteral(id), value));
});
return new AStructExpression(recList);
}
......@@ -208,7 +156,7 @@ public class StructType extends AbstractHasFollowers {
visitor.caseStructType(this);
}
public LinkedHashMap<String, TLAType> getTypeTable() {
public Map<String, TLAType> getTypes() {
return this.types;
}
......
......@@ -4,14 +4,11 @@ import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map.Entry;
import java.util.*;
import java.util.stream.Collectors;
public class TupleOrFunction extends AbstractHasFollowers {
private final LinkedHashMap<Integer, TLAType> types = new LinkedHashMap<>();
private final Map<Integer, TLAType> types = new LinkedHashMap<>();
public TupleOrFunction(Integer index, TLAType type) {
super(TUPLE_OR_FUNCTION);
......@@ -47,36 +44,22 @@ public class TupleOrFunction extends AbstractHasFollowers {
@Override
public String toString() {
StringBuilder sb = new StringBuilder();
sb.append("TupleOrFunction");
sb.append("(");
for (Iterator<Integer> keys = types.keySet().iterator(); keys.hasNext(); ) {
Integer key = keys.next();
sb.append(key);
sb.append(" : ").append(types.get(key));
if (keys.hasNext())
sb.append(", ");
}
sb.append(")");
return sb.toString();
return "TupleOrFunction(" + types.entrySet().stream()
.map(entry -> entry.getKey() + " : " + entry.getValue())
.collect(Collectors.joining(", ")) + ")";
// throw new RuntimeException("Type " + sb + "is incomplete");
}
@Override
public PExpression getBNode() {
FunctionType func = new FunctionType();
func.setDomain(IntType.getInstance());
func.setRange(new UntypedType());
FunctionType res;
FunctionType func = new FunctionType(IntType.getInstance(), new UntypedType());
try {
res = (FunctionType) func.unify(this);
FunctionType res = (FunctionType) func.unify(this);
return res.getBNode();
} catch (UnificationException e) {
// tuple
} catch (UnificationException e) { // tuple
boolean isTuple = true;
ArrayList<TLAType> typeList = new ArrayList<>();
for (int i = 1; i <= types.keySet().size(); i++) {
List<TLAType> typeList = new ArrayList<>();
for (int i = 1; i <= types.size(); i++) {
if (types.containsKey(i)) {
typeList.add(types.get(i));
} else {
......@@ -88,22 +71,9 @@ public class TupleOrFunction extends AbstractHasFollowers {
if (isTuple) {
return new TupleType(typeList).getBNode();
} else {
StringBuilder sb = new StringBuilder();
sb.append("(");
for (Iterator<Integer> keys = types.keySet().iterator(); keys
.hasNext(); ) {
Integer key = keys.next();
sb.append(key);
sb.append(" : ").append(types.get(key));
if (keys.hasNext())
sb.append(", ");
}
sb.append(")");
throw new RuntimeException("Type " + sb + "is incomplete");
throw new RuntimeException("Type " + this + " is incomplete");
}
}
}
@Override
......@@ -116,48 +86,30 @@ public class TupleOrFunction extends AbstractHasFollowers {
if (o instanceof FunctionType) {
FunctionType t = (FunctionType) o;
if (!t.getDomain().compare(IntType.getInstance())) {
return false;
}
for (TLAType type : this.types.values()) {
if (!type.compare(t.getRange())) {
return false;
}
}
return true;
return t.getDomain().compare(IntType.getInstance()) &&
this.types.values().stream().allMatch(type -> type.compare(t.getRange()));
}
if (o instanceof TupleType) {
TupleType tupleType = (TupleType) o;
for (Integer index : this.types.keySet()) {
if (index >= 1
&& index <= tupleType.getTypes().size()
&& this.types.get(index).compare(
tupleType.getTypes().get(index - 1))) {
} else {
return false;
}
}
return true;
return this.types.keySet().stream().allMatch(
index -> index >= 1 &&
index <= tupleType.getTypes().size() &&
this.types.get(index).compare(tupleType.getTypes().get(index - 1)));
}
if (o instanceof TupleOrFunction) {
TupleOrFunction other = (TupleOrFunction) o;
if (isTupleOrFunction(this, other)) {
if (isTupleOrFunction(this, other))
return true;
}
if (types.size() != other.types.size())
return false;
try {
for (int i = 1; i <= types.keySet().size(); i++) {
for (int i = 1; i <= types.size(); i++) {
if (!types.get(i).compare(other.types.get(i))) {
return false;
}
}
} catch (Exception e) {
return false;
}
return true;
}
// this type is not comparable to all other types
return false;
}
......@@ -171,12 +123,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
@Override
public boolean contains(TLAType o) {
for (TLAType type : this.types.values()) {
if (type.equals(o) || type.contains(o)) {
return true;
}
}
return false;
return this.types.values().stream().anyMatch(type -> type.equals(o) || type.contains(o));
}
@Override
......@@ -188,19 +135,14 @@ public class TupleOrFunction extends AbstractHasFollowers {
if (type.isUntyped())
return true;
}
FunctionType func = new FunctionType();
func.setDomain(IntType.getInstance());
func.setRange(new UntypedType());
FunctionType func = new FunctionType(IntType.getInstance(), new UntypedType());
return !func.compare(this);
}
@Override
public TLAType cloneTLAType() {
TupleOrFunction res = new TupleOrFunction();
for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
res.types.put(entry.getKey(), entry
.getValue().cloneTLAType());
}
res.types.putAll(this.types);
return res;
}
......@@ -229,8 +171,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
List<TLAType> typeList = new ArrayList<>();
for (int i = 0; i < tupleType.getTypes().size(); i++) {
if (this.types.containsKey(i + 1)) {
TLAType res = tupleType.getTypes().get(i)
.unify(this.types.get(i + 1));
TLAType res = tupleType.getTypes().get(i).unify(this.types.get(i + 1));
typeList.add(res);
} else {
typeList.add(tupleType.getTypes().get(i));
......@@ -245,19 +186,16 @@ public class TupleOrFunction extends AbstractHasFollowers {
if (o instanceof TupleOrFunction) {
TupleOrFunction other = (TupleOrFunction) o;
for (Integer i : other.types.keySet()) {
TLAType res;
if (this.types.containsKey(i)) {
TLAType res = other.types.get(i).unify(this.types.get(i));
if (res instanceof AbstractHasFollowers)
((AbstractHasFollowers) res).addFollower(this);
this.types.put(i, res);
res = other.types.get(i).unify(this.types.get(i));
} else {
TLAType res = other.types.get(i);
res = other.types.get(i);
}
if (res instanceof AbstractHasFollowers)
((AbstractHasFollowers) res).addFollower(this);
this.types.put(i, res);
}
}
other.setFollowersTo(this);
return this;
// if (isTupleOrFunction(this, other)) {
......@@ -295,33 +233,26 @@ public class TupleOrFunction extends AbstractHasFollowers {
// TupleType tuple2 = new TupleType(list2);
// return tuple1.unify(tuple2);
// }
}
throw new RuntimeException();
}
public void setNewType(AbstractHasFollowers oldType, TLAType newType) {
LinkedHashMap<Integer, TLAType> temp = new LinkedHashMap<>(
types);
for (Entry<Integer, TLAType> entry : temp.entrySet()) {
if (entry.getValue().equals(oldType)) {
types.put(entry.getKey(), newType);
new HashMap<>(types).forEach((key,value) -> {
if (value.equals(oldType)) {
types.put(key, newType);
if (newType instanceof AbstractHasFollowers) {
((AbstractHasFollowers) newType).addFollower(this);
}
}
}
});
update();
}
public TLAType getFinalType() {
List<TLAType> list = new ArrayList<>(this.types.values());
if (comparable(list)) {
FunctionType func = new FunctionType(IntType.getInstance(),
new UntypedType());
FunctionType func = new FunctionType(IntType.getInstance(), new UntypedType());
try {
func = (FunctionType) func.unify(this);
this.setFollowersTo(func);
......@@ -334,7 +265,6 @@ public class TupleOrFunction extends AbstractHasFollowers {
this.setFollowersTo(tuple);
return tuple;
}
}
private TLAType update() {
......
package de.tla2b.types;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.util.ASTBuilder;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.Collectors;
public class TupleType extends AbstractHasFollowers {
private List<TLAType> types;
......@@ -146,7 +148,7 @@ public class TupleType extends AbstractHasFollowers {
@Override
public PExpression getBNode() {
return BAstCreator.createNestedCouple(types);
return ASTBuilder.createNestedMultOrCard(types.stream().map(TLAType::getBNode).collect(Collectors.toList()));
}
public void apply(TypeVisitorInterface visitor) {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment