Fix typechecking of user defined operators when they are used multiple times with different types

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

@@ -278,49 +278,28 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
 
 			case UserDefinedOpKind: {
 				OpDefNode def = (OpDefNode) n.getOperator();
+				ExprOrOpArgNode[] args = n.getArgs();
+				FormalParamNode[] params = def.getParams();
 
 				// Definition is a BBuilt-in definition
 				if (BBuiltInOPs.isBBuiltInOp(def)) {
 					return evalBBuiltIns(n, expected);
 				}
 
-				TLAType found = getType(def);
-				if (found == null) {
-					found = new UntypedType();
-					// throw new RuntimeException(def.getName() + " has no type yet!");
-				}
-				if (n.getArgs().length != 0) {
-					found = found.cloneTLAType();
+				// the definition might be generic, so we have to re-evaluate
+				// the definition body with the concrete types we have here as args
+
+				// set param types
+				assert params.length == args.length;
+				for (int i = 0; i < args.length; i++) {
+					TLAType argType = visitExprOrOpArgNode(args[i], new UntypedType());
+					setType(params[i], argType.cloneTLAType(), TEMP_TYPE_ID);
 				}
-				found = unify(found, expected, def.getName().toString(), def);
 
-				boolean untyped = false;
-				FormalParamNode[] params = def.getParams();
-				for (int i = 0; i < n.getArgs().length; i++) {
-					// clone the parameter type, because the parameter type is not
-					// set/changed at a definition call
-					FormalParamNode p = params[i];
-					TLAType pType = getType(p);
-					if (pType == null) {
-						pType = new UntypedType();
-						// throw new RuntimeException("Parameter " + p.getName() + " has no type yet!%n" + p.getLocation());
-					}
-					pType = pType.cloneTLAType();
-					if (pType.isUntyped())
-						untyped = true;
-
-					pType = visitExprOrOpArgNode(n.getArgs()[i], pType);
-					// unify both types,
-					// set types of the arguments of the definition call to the parameters for reevaluation the def body
-					setType(p, pType, TEMP_TYPE_ID);
-				}
-
-				if (found.isUntyped() || untyped || !def.getInRecursive()) {
-					// evaluate the body of the definition again
+				// re-evaluate definition body
 				paramId = TEMP_TYPE_ID;
-					found = visitExprNode(def.getBody(), found);
+				TLAType found = visitExprNode(def.getBody(), expected);
 				paramId = TYPE_ID;
-				}
 
 				setType(n, found);
 				return found;

src/test/java/de/tla2b/typechecking/standardmodules/TestModuleTLC.java

+package de.tla2b.typechecking.standardmodules;
+
+import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.util.TestTypeChecker;
+import de.tla2b.util.TestUtil;
+import org.junit.Test;
+
+import static org.junit.Assert.assertEquals;
+
+
+public class TestModuleTLC {
+
+	/*
+	 * a :> b : The function [x \in {a} |-> b]
+	 */
+	@Test
+	public void testSingleton() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Naturals, TLC \n"
+			+ "CONSTANTS k \n"
+			+ "ASSUME k = 1 :> 2 \n"
+			+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k"));
+	}
+
+	/*
+	 * func1 @@ func2 : Function merge. If two functions share the same key, uses the value from func1 (NOT func2).
+	 */
+	@Test
+	public void testMerge() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Naturals, TLC \n"
+			+ "CONSTANTS k1, k2, k3 \n"
+			+ "ASSUME k1 = 1 :> 2 /\\ k2 = 1 :> 3 /\\ k3 = k1 @@ k2 \n"
+			+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k1"));
+		assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k2"));
+		assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k3"));
+	}
+
+	/*
+	 * Combination of the previous operators to override one value of a function
+	 */
+	@Test
+	public void testOverride() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Naturals, TLC \n"
+			+ "CONSTANTS k1, k2 \n"
+			+ "FuncAssign(f, d, e) ==  d :> e @@ f \n"
+			+ "ASSUME k1 = 1 :> 2 /\\ k2 = FuncAssign(k1, 1, 3) \n"
+			+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k1"));
+		assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k2"));
+	}
+}

src/test/resources/regression/NeedhamSchroederFixed/Functions.tla

+----------------------------- MODULE Functions -----------------------------
+EXTENDS TLC
+
+FuncAssign(f, d, e) ==  d :> e @@ f
+ \* [x \in (DOMAIN f) \cup {d} |-> IF x = d THEN e ELSE f[x]]
+ \* Overwriting the function f at index d with value e
+
+ParFunc(S, T) ==  UNION{[x -> T] :x \in SUBSET S}
+ \* The set of all partial functions
+
+=============================================================================

src/test/resources/regression/NeedhamSchroederFixed/NeedhamSchroederFixed.cfg

+INIT Init
+NEXT Next
+INVARIANT Invariant1
+CONSTANTS
+initiator = initiator
+responder = responder
+responder_2_generate = responder_2_generate
+responder_1_receive = responder_1_receive
+initiator_3_receive = initiator_3_receive
+initiator_4_send = initiator_4_send
+initiator_2_send = initiator_2_send
+initiator_1_generate = initiator_1_generate
+responder_4_receive = responder_4_receive
+responder_3_send = responder_3_send

src/test/resources/regression/NeedhamSchroederFixed/NeedhamSchroederFixed.tla

+---- MODULE NeedhamSchroederFixed ----
+EXTENDS Naturals, Sequences, TLC, Functions
+CONSTANTS initiator, responder, responder_2_generate, responder_1_receive, initiator_3_receive, initiator_4_send, initiator_2_send, initiator_1_generate, responder_4_receive, responder_3_send
+VARIABLES threads
+
+ROLE == {initiator, responder}
+ACTION_1 == {responder_2_generate, responder_1_receive, initiator_3_receive, initiator_4_send, initiator_2_send, initiator_1_generate, responder_4_receive, responder_3_send}
+MaxThreads == TLCEval(2)
+Protocol == TLCEval((responder:><<responder_1_receive, responder_2_generate, responder_3_send, responder_4_receive>> @@ initiator:><<initiator_1_generate, initiator_2_send, initiator_3_receive, initiator_4_send>>))
+AGENT == TLCEval({1, 4, 3, 2})
+ValidSubs == TLCEval({(initiator:>1 @@ responder:>3), (responder:>4 @@ initiator:>3), (responder:>2 @@ initiator:>1), (initiator:>3 @@ responder:>1)})
+
+Invariant1 == threads \in Seq([role : DOMAIN Protocol, sub : ParFunc(DOMAIN Protocol, AGENT)])
+
+Init == threads = <<>>
+
+create(tid, role, sub) == (tid =< MaxThreads /\ threads' = FuncAssign(threads, tid, [role |-> role, sub |-> sub]))
+
+Next == \E tid \in {Len(threads) + 1}, role \in DOMAIN Protocol, sub \in ValidSubs : create(tid, role, sub)
+====