From 58ce95463f5c2a4090c294a02e262bf11eafbcd8 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Tue, 14 Jan 2025 19:56:32 +0100
Subject: [PATCH] simplifications in types
---
.../de/tla2b/types/AbstractHasFollowers.java | 4 -
src/main/java/de/tla2b/types/EnumType.java | 12 +-
.../de/tla2b/types/StructOrFunctionType.java | 18 +--
src/main/java/de/tla2b/types/StructType.java | 108 ++++---------
.../java/de/tla2b/types/TupleOrFunction.java | 148 +++++-------------
src/main/java/de/tla2b/types/TupleType.java | 4 +-
6 files changed, 78 insertions(+), 216 deletions(-)
diff --git a/src/main/java/de/tla2b/types/AbstractHasFollowers.java b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
index 295c4cf..9da88b8 100644
--- a/src/main/java/de/tla2b/types/AbstractHasFollowers.java
+++ b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
@@ -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;
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index 26e745a..583dd35 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -1,6 +1,7 @@
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) {
diff --git a/src/main/java/de/tla2b/types/StructOrFunctionType.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
index 89a9fbf..be4ec5b 100644
--- a/src/main/java/de/tla2b/types/StructOrFunctionType.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -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();
}
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index 18137a9..98e3455 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -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;
}
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index 3794538..396f87a 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -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++) {
- if (!types.get(i).compare(other.types.get(i))) {
- return false;
- }
+ 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,18 +186,15 @@ 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);
- if (res instanceof AbstractHasFollowers)
- ((AbstractHasFollowers) res).addFollower(this);
- this.types.put(i, res);
+ res = other.types.get(i);
}
-
+ if (res instanceof AbstractHasFollowers)
+ ((AbstractHasFollowers) res).addFollower(this);
+ this.types.put(i, res);
}
other.setFollowersTo(this);
return this;
@@ -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() {
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index 4a6500c..557c1b7 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -1,12 +1,14 @@
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) {
--
GitLab