Handling extensible records.

src/main/java/de/tla2b/analysis/TypeChecker.java

@@ -961,19 +961,21 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
 			String fieldName = ((StringNode) n.getArgs()[1]).getRep()
 					.toString();
 			StructType r = (StructType) visitExprOrOpArgNode(n.getArgs()[0],
-					new StructType());
+					StructType.getIncompleteStruct());
 
-			StructType expectedStruct = new StructType();
+			StructType expectedStruct = StructType.getIncompleteStruct();
 			expectedStruct.add(fieldName, expected);
 
 			try {
 				r = r.unify(expectedStruct);
-				return r.getType(fieldName);
 			} catch (UnificationException e) {
 				throw new TypeErrorException(String.format(
 						"Struct has no field %s with type %s: %s\n%s",
 						fieldName, r.getType(fieldName), r, n.getLocation()));
 			}
+			n.setToolObject(TYPE_ID, r);
+			r.addFollower(n);
+			return r.getType(fieldName);
 		}
 
 		/***********************************************************************

src/main/java/de/tla2b/exceptions/NotImplementedException.java

@@ -2,7 +2,7 @@ package de.tla2b.exceptions;
 
 
 @SuppressWarnings("serial")
-public class NotImplementedException extends TLA2BException {
+public class NotImplementedException extends RuntimeException {
 	public NotImplementedException(String e){
 		super(e);
 	}

src/main/java/de/tla2b/types/StructOrFunction.java

@@ -172,7 +172,7 @@ public class StructOrFunction extends AbstractHasFollowers {
 			return found.unify(o);
 		}
 		if (o instanceof StructType) {
-			StructType res = new StructType();
+			StructType res = StructType.getIncompleteStruct();
 
 			for (String field : types.keySet()) {
 				res.add(field, this.types.get(field));

src/main/java/de/tla2b/types/StructType.java

@@ -7,6 +7,9 @@ import java.util.List;
 import java.util.Map.Entry;
 import java.util.Set;
 
+import de.be4.classicalb.core.parser.node.ABoolSetExpression;
+import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
+import de.be4.classicalb.core.parser.node.APowSubsetExpression;
 import de.be4.classicalb.core.parser.node.ARecEntry;
 import de.be4.classicalb.core.parser.node.AStructExpression;
 import de.be4.classicalb.core.parser.node.PExpression;
@@ -14,14 +17,26 @@ import de.be4.classicalb.core.parser.node.PRecEntry;
 import de.tla2b.exceptions.UnificationException;
 import de.tla2bAst.BAstCreator;
 
-
-
 public class StructType extends AbstractHasFollowers {
 	private LinkedHashMap<String, TLAType> types;
+	private boolean extensible;
+	private boolean incompleteStruct;
 
 	public StructType() {
 		super(STRUCT);
 		types = new LinkedHashMap<String, TLAType>();
+		extensible = false;
+		incompleteStruct = false;
+	}
+
+	public static StructType getIncompleteStruct() {
+		StructType s = new StructType();
+		s.incompleteStruct = true;
+		return s;
+	}
+
+	public boolean isExtensible() {
+		return extensible;
 	}
 
 	public TLAType getType(String fieldName) {
@@ -104,6 +119,27 @@ public class StructType extends AbstractHasFollowers {
 
 		if (o instanceof StructType) {
 			StructType s = (StructType) o;
+			boolean extendStruct = false;
+			
+			if (this.incompleteStruct && s.incompleteStruct) {
+				extendStruct = false;
+			} else if (this.incompleteStruct) {
+				if (s.types.keySet().containsAll(this.types.keySet())) {
+					extendStruct = false;
+				} else {
+					extendStruct = true;
+				}
+			} else if (s.incompleteStruct) {
+				if (this.types.keySet().containsAll(s.types.keySet())) {
+					extendStruct = false;
+				} else {
+					extendStruct = true;
+				}
+			} else {
+				extendStruct = !s.types.keySet().equals(this.types.keySet());
+			}
+			this.extensible = this.extensible || s.extensible || extendStruct;
+
 			Iterator<String> keys = s.types.keySet().iterator();
 			while (keys.hasNext()) {
 				String fieldName = (String) keys.next();
@@ -118,6 +154,7 @@ public class StructType extends AbstractHasFollowers {
 					}
 					this.types.put(fieldName, sType);
 				}
+				this.incompleteStruct = false;
 			}
 			return this;
 		}
@@ -184,7 +221,16 @@ public class StructType extends AbstractHasFollowers {
 		for (Entry<String, TLAType> entry : types.entrySet()) {
 			ARecEntry rec = new ARecEntry();
 			rec.setIdentifier(BAstCreator.createIdentifierNode(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);
 		}
 		return new AStructExpression(recList);

src/main/java/de/tla2bAst/BAstCreator.java

@@ -137,6 +137,7 @@ import de.tla2b.analysis.PredicateVsExpression.DefinitionType;
 import de.tla2b.analysis.UsedExternalFunctions.EXTERNAL_FUNCTIONS;
 import de.tla2b.config.ConfigfileEvaluator;
 import de.tla2b.config.ValueObj;
+import de.tla2b.exceptions.NotImplementedException;
 import de.tla2b.global.BBuildIns;
 import de.tla2b.global.BBuiltInOPs;
 import de.tla2b.global.Priorities;
@@ -238,8 +239,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 
 	}
 
-	
-	
 	private void createSetsClause() {
 		if (conEval == null || conEval.getEnumerationSet() == null
 				|| conEval.getEnumerationSet().size() == 0)
@@ -1200,7 +1199,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			AMemberPredicate member = new AMemberPredicate();
 			member.setLeft(createIdentifierNode("t_"));
 			AIntervalExpression interval = new AIntervalExpression();
-			interval.setLeftBorder(new AIntegerExpression(new TIntegerLiteral("1")));
+			interval.setLeftBorder(new AIntegerExpression(new TIntegerLiteral(
+					"1")));
 			AMinusOrSetSubtractExpression minus = new AMinusOrSetSubtractExpression();
 			minus.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
 			minus.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
@@ -1224,13 +1224,15 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			lambda.setExpression(func);
 			return lambda;
 
-//			ARestrictFrontExpression restrictFront = new ARestrictFrontExpression();
+			// ARestrictFrontExpression restrictFront = new
+			// ARestrictFrontExpression();
 			// restrictFront
 			// .setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
 			// restrictFront
 			// .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
 			//
-//			ARestrictTailExpression restrictTail = new ARestrictTailExpression();
+			// ARestrictTailExpression restrictTail = new
+			// ARestrictTailExpression();
 			// restrictTail.setLeft(restrictFront);
 			// restrictTail
 			// .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
@@ -1589,8 +1591,25 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 
 			}
 			List<PRecEntry> recList = new ArrayList<PRecEntry>();
+			if (struct.isExtensible()) {
+				for (int i = 0; i < struct.getFields().size(); i++) {
+					String fieldName = struct.getFields().get(i); 																// name
+					AIdentifierExpression field = createIdentifierNode(fieldName);
+					ARecEntry rec = new ARecEntry();
+					rec.setIdentifier(field);
+					AMultOrCartExpression cart = new AMultOrCartExpression();
+					cart.setLeft(new ABoolSetExpression());
+					if (pairTable.containsKey(fieldName)) {
+						cart.setRight(pairTable.get(fieldName));
+					} else {
+						cart.setRight(struct.getType(fieldName).getBNode());
+					}
+					rec.setValue(new APowSubsetExpression(cart));
+					recList.add(rec);
+				}
+			} else {
 				for (int i = 0; i < struct.getFields().size(); i++) {
-				String fieldName = struct.getFields().get(i); // renamed name
+					String fieldName = struct.getFields().get(i);
 					AIdentifierExpression field = createIdentifierNode(fieldName);
 					ARecEntry rec = new ARecEntry();
 					rec.setIdentifier(field);
@@ -1602,11 +1621,13 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 					recList.add(rec);
 				}
 
+			}
 			return new AStructExpression(recList);
 		}
 
 		case OPCODE_rc: { // [h_1 |-> 1, h_2 |-> 2]
 			StructType struct = (StructType) n.getToolObject(TYPE_ID);
+			if (struct.isExtensible()) {
 				Hashtable<String, PExpression> pairTable = new Hashtable<String, PExpression>();
 				ExprOrOpArgNode[] args = n.getArgs();
 				for (int i = 0; i < args.length; i++) {
@@ -1622,24 +1643,74 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 					ARecEntry rec = new ARecEntry();
 					rec.setIdentifier(field);
 					if (pairTable.containsKey(fieldName)) {
-					rec.setValue(pairTable.get(fieldName));
+
+						ACoupleExpression couple = new ACoupleExpression();
+						List<PExpression> coupleList = new ArrayList<PExpression>();
+						coupleList.add(new ABooleanTrueExpression());
+						coupleList.add(pairTable.get(fieldName));
+						couple.setList(coupleList);
+						ASetExtensionExpression set = new ASetExtensionExpression(
+								makePexpressionList(couple));
+						rec.setValue(set);
 					} else {
-					// insert null element
+						AEmptySetExpression emptySet = new AEmptySetExpression();
+						rec.setValue(emptySet);
 					}
 					recList.add(rec);
 				}
+				return new ARecExpression(recList);
 
+			} else {
+				Hashtable<String, PExpression> pairTable = new Hashtable<String, PExpression>();
+				ExprOrOpArgNode[] args = n.getArgs();
+				for (int i = 0; i < args.length; i++) {
+					OpApplNode pair = (OpApplNode) args[i];
+					StringNode stringNode = (StringNode) pair.getArgs()[0];
+					pairTable.put(stringNode.getRep().toString(),
+							visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
+				}
+				List<PRecEntry> recList = new ArrayList<PRecEntry>();
+				for (int i = 0; i < struct.getFields().size(); i++) {
+					String fieldName = struct.getFields().get(i);
+					AIdentifierExpression field = createIdentifierNode(fieldName);
+					ARecEntry rec = new ARecEntry();
+					rec.setIdentifier(field);
+					if (pairTable.containsKey(fieldName)) {
+						rec.setValue(pairTable.get(fieldName));
+					} else {
+						// this struct is extensible
+						throw new NotImplementedException("Missing case handling extensible structs.");
+					}
+					recList.add(rec);
+				}
 				return new ARecExpression(recList);
 			}
 
+		}
+
 		case OPCODE_rs: { // $RcdSelect r.c
+			StructType struct = (StructType) n.getToolObject(TYPE_ID);
+			if (struct.isExtensible()) {
 				ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
-			rcdSelect.setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+				rcdSelect
+						.setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
 				StringNode stringNode = (StringNode) n.getArgs()[1];
-			rcdSelect.setIdentifier(createIdentifierNode(stringNode.getRep()
-					.toString())); // TODO renamed
+				rcdSelect.setIdentifier(createIdentifierNode(stringNode
+						.getRep().toString()));
+				AFunctionExpression funcCall = new AFunctionExpression();
+				funcCall.setIdentifier(rcdSelect);
+				funcCall.setParameters(makePexpressionList(new ABooleanTrueExpression()));
+				return funcCall;
+			} else {
+				ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
+				rcdSelect
+						.setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+				StringNode stringNode = (StringNode) n.getArgs()[1];
+				rcdSelect.setIdentifier(createIdentifierNode(stringNode
+						.getRep().toString()));
 				return rcdSelect;
 			}
+		}
 
 		case OPCODE_prime: // prime
 		{
@@ -2190,4 +2261,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		return list;
 	}
 
+	public static List<PExpression> makePexpressionList(PExpression expr) {
+		ArrayList<PExpression> list = new ArrayList<PExpression>();
+		list.add(expr);
+		return list;
+	}
 }

src/test/java/de/tla2b/expression/TestComplexExpression.java → src/test/java/de/tla2b/expression/ComplexExpressionTest.java

@@ -8,7 +8,7 @@ import org.junit.Test;
 
 import static de.tla2b.util.TestUtil.compareExpr;
 
-public class TestComplexExpression {
+public class ComplexExpressionTest {
 
 	@Test
 	public void testExcept() throws Exception {

src/test/java/de/tla2b/prettyprintb/ExtensibleRecordTest.java

+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class ExtensibleRecordTest {
+
+	@Test
+	public void testRecord1() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME [a |-> 1] = [b |-> TRUE, a |-> 4] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES rec(b:{}, a:{(TRUE,1)}) = rec(b:{(TRUE,TRUE)}, a:{(TRUE,4)}) \n"
+				+ "END";
+		compare(expected, module);
+	}
+
+	@Test
+	public void testRecord2() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME [a |-> 1] = [b |-> TRUE] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES rec(b:{}, a:{(TRUE,1)}) = rec(b:{(TRUE,TRUE)}, a:{}) \n"
+				+ "END";
+		compare(expected, module);
+	}
+
+	@Test
+	public void testSelect() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [a |-> 1] /\\ k # [b |-> 1] /\\ k.a = 1 \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "ABSTRACT_CONSTANTS k \n"
+				+ "PROPERTIES k : struct(b:POW(BOOL * INTEGER), a:POW(BOOL * INTEGER)) & ((k = rec(b:{}, a:{(TRUE,1)}) & k /= rec(b:{(TRUE,1)}, a:{})) & (k'a)(TRUE) = 1) \n"
+				+ "END";
+		compare(expected, module);
+	}
+
+	@Test
+	public void testSelect2() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME [a |-> 1].b = TRUE \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES (rec(a:{(TRUE,1)}, b:{})'b)(TRUE) = TRUE \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testStructExpansion() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME [a: {2}] = [a : {1}, b : BOOLEAN] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES struct(a:POW(BOOL * {2}), b:POW(BOOL * BOOL)) = struct(a:POW(BOOL * {1}), b:POW(BOOL * BOOL)) \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testRecExpansion2() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [a |-> 1] /\\ TRUE = k.b \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "ABSTRACT_CONSTANTS k \n"
+				+ "PROPERTIES k : struct(a:POW(BOOL * INTEGER), b:POW(BOOL * BOOL)) & (k = rec(a:{(TRUE,1)}, b:{}) & TRUE = (k'b)(TRUE)) \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+}

src/test/java/de/tla2b/prettyprintb/RecordTest.java

@@ -34,18 +34,6 @@ public class RecordTest {
 	}
 	
 
-	@Test
-	public void testStructExpansion() throws Exception {
-		final String module = "-------------- MODULE Testing ----------------\n"
-				+ "ASSUME [a: {2}] = [a : {1}, b : BOOLEAN] \n"
-				+ "=================================";
-
-		final String expected = "MACHINE Testing\n"
-				+ "PROPERTIES struct(a : {2},b : BOOL) = struct(a : {1},b : BOOL) \n"
-				+ "END";
-		compare(expected, module);
-	}
-
 	/**********************************************************************
 	 * Record: [L1 |-> e1, L2 |-> e2]
 	 **********************************************************************/