From 3fb30f52426b45cda44541b906ad9ebe16ce07c4 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 7 Mar 2024 11:30:30 -0800 Subject: [PATCH] SequencesExt!Fold[Left|Right]Domain over domain of sequence. https://github.com/tlaplus/CommunityModules/issues/101 [Feature] Signed-off-by: Markus Alexander Kuppe --- modules/SequencesExt.tla | 14 +++++++++ modules/tlc2/overrides/SequencesExt.java | 38 ++++++++++++++++++++++++ tests/SequencesExtTests.tla | 4 +++ 3 files changed, 56 insertions(+) diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index 3facdde..60c3ef1 100644 --- 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 index b28a570..ef4d810 100644 --- 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 index 22e4b0d..e4bd246 100644 --- 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") =============================================================================