Delegate from SequencesExt!FoldSeq to Functions!FoldFunction instead

of `SequencesExt!FoldLeft`.

The difference is that the base element is the second and not the
first operand of the operation op(_,_).  The (iteration) order is
determined by the order of the sequence's (seq) domain, which is
1..Len(seq) in both cases.

[Bug]

Author: lemmy

modules/tlc2/overrides/Functions.java

@@ -114,6 +114,7 @@ public static Value foldFunction(final OpValue op, final Value base, final Appli
 	@TLAPlusOperator(identifier = "FoldFunctionOnSet", module = "Functions", warn = false)
 	public static Value foldFunctionOnSet(final OpValue op, final Value base, final Applicable fun, final Enumerable subdomain) {
 
+		// FoldFunction base is second operand.
 		final Value[] args = new Value[2];
 		args[1] = base;
 

modules/tlc2/overrides/SequencesExt.java

@@ -37,15 +37,12 @@
 import tlc2.util.Context;
 import tlc2.value.IValue;
 import tlc2.value.Values;
-import tlc2.value.impl.Applicable;
 import tlc2.value.impl.BoolValue;
-import tlc2.value.impl.Enumerable;
 import tlc2.value.impl.OpValue;
 import tlc2.value.impl.SetEnumValue;
 import tlc2.value.impl.StringValue;
 import tlc2.value.impl.TupleValue;
 import tlc2.value.impl.Value;
-import tlc2.value.impl.ValueEnumeration;
 import tlc2.value.impl.ValueVec;
 
 public final class SequencesExt {
@@ -97,29 +94,6 @@ public String longestCommonPrefix(String[] strs) {
 		        }        
 		    return prefix;
 		}
-	/*
-	 */
-		@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());
-		}
-
-		@TLAPlusOperator(identifier = "FoldFunctionOnSet", module = "Functions", warn = false)
-		public static Value foldFunctionOnSet(final OpValue op, final Value base, final Applicable fun, final Enumerable subdomain) {
-			
-			final Value[] args = new Value[2];
-			args[1] = base;
-
-			final ValueEnumeration ve = subdomain.elements();
-
-			Value v = null;
-			while ((v = ve.nextElement()) != null) {
-				args[0] = fun.select(v);
-				args[1] = op.apply(args, EvalControl.Clear);
-			}
-			
-			return args[1];
-		}
 
 	@TLAPlusOperator(identifier = "LongestCommonPrefix", module = "SequencesExt", warn = false)
 	public static Value longestCommonPrefix(final Value val) {
@@ -195,7 +169,7 @@ 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) {
-		return foldLeft(op, base, tv);
+		return Functions.foldFunction(op, base, tv);
 	}
 
 	@TLAPlusOperator(identifier = "FoldLeft", module = "SequencesExt", warn = false)
@@ -207,6 +181,7 @@ public static Value foldLeft(final OpValue op, final Value base, final Value val
 					new String[] { "FoldLeft", "sequence", Values.ppr(val.toString()) });
 		}
 
+		// FoldLeft base is left (first) operand.
 		final Value[] args = new Value[2];
 		args[0] = base;
 
@@ -228,6 +203,7 @@ public static Value foldRight(final OpValue op, final Value val, final Value bas
 					new String[] { "FoldRight", "sequence", Values.ppr(val.toString()) });
 		}
 
+		// FoldRight base is right (second) operand.
 		final Value[] args = new Value[2];
 		args[1] = base;
 

tests/SequencesExtTests.tla

@@ -99,6 +99,10 @@ ASSUME FoldRight(-, [n \in 1..25 |-> n], 1) =  12
 ASSUME FoldRight(+, [n \in 1..250 |-> n], 1) = 31376
 ASSUME FoldRight(-, [n \in 1..250 |-> n], 1) =  -124
 
+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 LongestCommonPrefix({<<>>}) = <<>>