SequencesExt!Fold[Left|Right]Domain over domain of sequence.

#101 [Feature] Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlaplus · Mar 7, 2024 · 3fb30f5 · 3fb30f5
1 parent 2cee5a3
commit 3fb30f5
Show file tree

Hide file tree

Showing 3 changed files with 56 additions and 0 deletions.
diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla
@@ -332,6 +332,20 @@ FoldRight(op(_, _), seq, base) ==
                  LAMBDA S : Min(S),
                  DOMAIN seq)
 
+FoldLeftDomain(op(_, _), base, seq) == 
+  (***************************************************************************)
+  (* FoldLeftDomain folds op on the domain of seq, i.e., the seq's indices,  *)
+  (* starting at the lowest index.                                           *) 
+  (***************************************************************************)
+  FoldLeft(op, base, [i \in DOMAIN seq |-> i])
+
+FoldRightDomain(op(_, _), seq, base) == 
+  (***************************************************************************)
+  (* FoldRightDomain folds op on the domain of seq, i.e., the seq's indices, *)
+  (* starting at the highest index.                                          *) 
+  (***************************************************************************)
+  FoldRight(op, [i \in DOMAIN seq |-> i], base)
+
 -----------------------------------------------------------------------------
 
 FlattenSeq(seqs) ==

diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java
@@ -304,6 +304,44 @@ public static Value foldRight(final OpValue op, final Value val, final Value bas
 
 		return args[1];
 	}
+
+	@TLAPlusOperator(identifier = "FoldLeftDomain", module = "SequencesExt", warn = false)
+	public static Value foldLeftDomain(final OpValue op, final Value base, final Value val) {
+		final TupleValue tv = (TupleValue) val.toTuple();
+		if (tv == null) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "third", "FoldLeftDomain", "sequence", Values.ppr(val.toString()) });
+		}
+
+		final Value[] args = new Value[2];
+		args[0] = base;
+
+		for (int i = 0; i < tv.size(); i++) {
+			args[1] = IntValue.gen(i+1);
+			args[0] = op.eval(args, EvalControl.Clear);
+		}
+
+		return args[0];
+	}
+
+	@TLAPlusOperator(identifier = "FoldRightDomain", module = "SequencesExt", warn = false)
+	public static Value foldRightDomain(final OpValue op, final Value val, final Value base) {
+		final TupleValue tv = (TupleValue) val.toTuple();
+		if (tv == null) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "second", "FoldRightDomain", "sequence", Values.ppr(val.toString()) });
+		}
+
+		final Value[] args = new Value[2];
+		args[1] = base;
+
+		for (int i = tv.size() - 1; i >= 0; i--) {
+			args[0] = IntValue.gen(i+1);
+			args[1] = op.eval(args, EvalControl.Clear);
+		}
+
+		return args[1];
+	}
 
 	@Evaluation(definition = "ReplaceFirstSubSeq", module = "SequencesExt", warn = false, silent = true)
 	public static Value replaceFirstSubSeq(final Tool tool, final ExprOrOpArgNode[] args, final Context c,

diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla
@@ -407,4 +407,8 @@ ASSUME AssertEq(RemoveFirstMatch(<<1,2>>, LAMBDA e: e = 1), <<2>>)
 ASSUME AssertEq(RemoveFirstMatch(<<1,2,1>>, LAMBDA e: e = 1), <<2,1>>)
 ASSUME AssertEq(RemoveFirstMatch(<<1,2,1,2>>, LAMBDA e: e = 2), <<1,1,2>>)
 
+-----------------------------------------------------------------------------
+
+ASSUME LET seq == <<"a","b","c","d","e">> IN AssertEq(FoldLeftDomain (LAMBDA acc, idx : acc \o seq[idx], "", seq), "abcde")
+ASSUME LET seq == <<"a","b","c","d","e">> IN AssertEq(FoldRightDomain(LAMBDA idx, acc : acc \o seq[idx], seq, ""), "edcba")
 =============================================================================