Improve error-messages for bogus inputs to Fold operators.

[Feature]

Author: lemmy

modules/tlc2/overrides/Functions.java

@@ -107,12 +107,32 @@ public static Value antiFunction(final Value f) {
 	}
 
 	@TLAPlusOperator(identifier = "FoldFunction", module = "Functions", warn = false)
-	public static Value foldFunction(final OpValue op, final Value base, final Applicable fun) {
-		return foldFunctionOnSet(op, base, fun, (Enumerable) fun.getDomain());
+	public static Value foldFunction(final OpValue op, final Value base, final Value fun) {
+		// Can assume type of OpValue because tla2sany.semantic.Generator.java will
+		// make sure that the first parameter is a binary operator.
+		
+		if (!(fun instanceof Applicable)) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "third", "FoldFunction", "function", Values.ppr(fun.toString()) });
+		}
+		return foldFunctionOnSet(op, base, fun, ((Applicable) fun).getDomain());
 	}
 
 	@TLAPlusOperator(identifier = "FoldFunctionOnSet", module = "Functions", warn = false)
-	public static Value foldFunctionOnSet(final OpValue op, final Value base, final Applicable fun, final Enumerable subdomain) {
+	public static Value foldFunctionOnSet(final OpValue op, final Value base, final Value v3, final Value v4) {
+		// Can assume type of OpValue because tla2sany.semantic.Generator.java will
+		// make sure that the first parameter is a binary operator.
+
+		if (!(v3 instanceof Applicable)) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "third", "FoldFunctionOnSet", "function", Values.ppr(v3.toString()) });
+		}
+		final Applicable fun = (Applicable) v3;
+		if (!(v4 instanceof Enumerable)) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "fourth", "FoldFunctionOnSet", "set", Values.ppr(v4.toString()) });
+		}
+		final Enumerable subdomain = (Enumerable) v4;
 
 		// FoldFunction base is second operand.
 		final Value[] args = new Value[2];

modules/tlc2/overrides/SequencesExt.java

@@ -168,17 +168,19 @@ private static Value longestCommonPrefix(final StringValue first, final ValueVec
 	}
 
 	@TLAPlusOperator(identifier = "FoldSeq", module = "SequencesExt", warn = false)
-	public static Value foldSeq(final OpValue op, final Value base, final TupleValue tv) {
+	public static Value foldSeq(final OpValue op, final Value base, final Value tv) {
 		return Functions.foldFunction(op, base, tv);
 	}
 
 	@TLAPlusOperator(identifier = "FoldLeft", module = "SequencesExt", warn = false)
 	public static Value foldLeft(final OpValue op, final Value base, final Value val) {
-
+		// Can assume type of OpValue because tla2sany.semantic.Generator.java will
+		// make sure that the first parameter is a binary operator.
+		
 		final TupleValue tv = (TupleValue) val.toTuple();
 		if (tv == null) {
-			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
-					new String[] { "FoldLeft", "sequence", Values.ppr(val.toString()) });
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "third", "FoldLeft", "sequence", Values.ppr(val.toString()) });
 		}
 
 		// FoldLeft base is left (first) operand.
@@ -196,11 +198,13 @@ public static Value foldLeft(final OpValue op, final Value base, final Value val
 
 	@TLAPlusOperator(identifier = "FoldRight", module = "SequencesExt", warn = false)
 	public static Value foldRight(final OpValue op, final Value val, final Value base) {
-
+		// Can assume type of OpValue because tla2sany.semantic.Generator.java will
+		// make sure that the first parameter is a binary operator.
+		
 		final TupleValue tv = (TupleValue) val.toTuple();
 		if (tv == null) {
-			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
-					new String[] { "FoldRight", "sequence", Values.ppr(val.toString()) });
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "second", "FoldRight", "sequence", Values.ppr(val.toString()) });
 		}
 
 		// FoldRight base is right (second) operand.

tests/FunctionsTests.tla

@@ -43,6 +43,18 @@ ASSUME FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, [n \in 1..9999 |-> n], {})
 
 ASSUME FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, [n \in 1..9999 |-> n], 2..9998) = 2..9998
 
+ASSUME AssertError(
+           "The third argument of FoldFunction should be a function, but instead it is:\nTRUE",
+           FoldFunction(+, 23, TRUE))
+
+ASSUME AssertError(
+           "The fourth argument of FoldFunctionOnSet should be a set, but instead it is:\nTRUE",
+           FoldFunctionOnSet(+, 23, <<>>, TRUE))
+
+ASSUME AssertError(
+           "The third argument of FoldFunctionOnSet should be a function, but instead it is:\nTRUE",
+           FoldFunctionOnSet(+, 23, TRUE, {}))
+
 \* AntiFunction
 ASSUME AntiFunction(<<"a", "b", "c">>) = [a |-> 1, b |-> 2, c |-> 3]
 

tests/SequencesExtTests.tla

@@ -103,6 +103,19 @@ ASSUME FoldSeq(  LAMBDA e, acc: acc + 1, 0, <<1,1,1,1,1>>) = 5
 ASSUME FoldLeft( LAMBDA acc, e: acc + 1, 0, <<1,1,1,1,1>>) = 5
 ASSUME FoldRight(LAMBDA e, acc: acc + 1, <<1,1,1,1,1>>, 0) = 5
 
+ASSUME AssertError(
+           "The second argument of FoldRight should be a sequence, but instead it is:\nTRUE",
+           FoldRight(+, TRUE, 23))
+
+ASSUME AssertError(
+           "The third argument of FoldLeft should be a sequence, but instead it is:\nTRUE",
+           FoldLeft(+, 23, TRUE))
+
+\* Error comes from Functions!FoldFunctionOnSet
+ASSUME AssertError(
+           "The third argument of FoldFunction should be a function, but instead it is:\nTRUE",
+           FoldSeq(+, 23, TRUE))
+
 -----------------------------------------------------------------------------
 
 ASSUME LongestCommonPrefix({<<>>}) = <<>>