Add SequencesExt!RemoveFirst and RemoveFirstMatch.

tlaplus · Oct 11, 2023 · 065e7b7 · 065e7b7
1 parent 580efdc
commit 065e7b7
Show file tree

Hide file tree

Showing 3 changed files with 91 additions and 0 deletions.
diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla
@@ -169,6 +169,24 @@ RemoveAt(s, i) ==
   (**************************************************************************)
   SubSeq(s, 1, i-1) \o SubSeq(s, i+1, Len(s))
 
+RemoveFirst(s, e) ==
+    (************************************************************************)
+    (* The sequence s with the first occurrence of e removed or s           *)
+    (* iff e \notin Range(s)                                                *)
+    (************************************************************************)
+    IF \E i \in 1..Len(s): s[i] = e
+    THEN RemoveAt(s, SelectInSeq(s, LAMBDA v: v = e))
+    ELSE s
+
+RemoveFirstMatch(s, Test(_)) ==
+    (************************************************************************)
+    (* The sequence s with the first element removed s.t. Test(e) or s      *)
+    (* iff e \notin Range(s)                                                *)
+    (************************************************************************)
+    IF \E i \in 1..Len(s): Test(s[i])
+    THEN RemoveAt(s, SelectInSeq(s, Test))
+    ELSE s
+
 -----------------------------------------------------------------------------
 
 Cons(elt, seq) == 

diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java
@@ -25,6 +25,8 @@
  *   Markus Alexander Kuppe - initial API and implementation
  ******************************************************************************/
 
+import java.util.ArrayList;
+
 import org.apache.commons.lang3.StringUtils;
 
 import tla2sany.semantic.ExprOrOpArgNode;
@@ -535,6 +537,64 @@ public static Value SelectLastInSubSeq(final Value s, final Value f, final Value
 		}
 		return IntValue.ValZero;
 	}
+
+	@TLAPlusOperator(identifier = "RemoveFirst", module = "SequencesExt", warn = false)
+	public static Value removeFirst(final Value s, final Value e) {
+		final TupleValue seq = (TupleValue) s.toTuple();
+		if (seq == null) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "first", "RemoveFirst", "sequence", Values.ppr(s.toString()) });
+		}
+
+		final ArrayList<Value> val = new ArrayList<>(seq.elems.length);
+
+		boolean found = false;
+		for (int i = 0; i < seq.elems.length; i++) {
+			if (!found && seq.elems[i].equals(e)) {
+				found = true;
+			} else {
+				val.add(seq.elems[i]);
+			}
+		}
+
+		return new TupleValue(val.toArray(Value[]::new));
+	}
+
+	@TLAPlusOperator(identifier = "RemoveFirstMatch", module = "SequencesExt", warn = false)
+	public static Value removeFirstMatch(final Value s, final Value test) {
+		final TupleValue seq = (TupleValue) s.toTuple();
+		if (seq == null) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "first", "RemoveFirstMatch", "sequence", Values.ppr(s.toString()) });
+		}
+		if (!(test instanceof Applicable)) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "second", "RemoveFirstMatch", "function", Values.ppr(test.toString()) });
+		}
+		final Applicable ftest = (Applicable) test;
+		final Value[] args = new Value[1];
+
+		final ArrayList<Value> val = new ArrayList<>(seq.elems.length);
+
+		boolean found = false;
+		for (int i = 0; i < seq.elems.length; i++) {
+			if (!found) {
+				args[0] = seq.elems[i];
+				final Value bval = ftest.apply(args, EvalControl.Clear);
+				if (!(bval instanceof IBoolValue)) {
+					throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "second", "RemoveFirstMatch",
+							"boolean-valued function", Values.ppr(test.toString()) });
+				}
+				if (((BoolValue) bval).val) {
+					found = true;
+					continue;
+				}
+			}
+			val.add(seq.elems[i]);
+		}
+
+		return new TupleValue(val.toArray(Value[]::new));
+	}
 
 	/*
 	   Suffixes(s) ==

diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla
@@ -369,5 +369,18 @@ ASSUME AssertEq(Suffixes(<<>>), {<<>>})
 ASSUME AssertEq(Suffixes(<<1>>), {<<>>, <<1>>})
 ASSUME AssertEq(Suffixes(<<1,2>>), {<<>>, <<1,2>>, <<2>>})
 ASSUME AssertEq(Suffixes(<<1,2,3>>), {<<>>, <<3>>, <<2,3>>, <<1,2,3>>})
+-----------------------------------------------------------------------------
+
+ASSUME AssertEq(RemoveFirst(<<>>, 1), <<>>)
+ASSUME AssertEq(RemoveFirst(<<1>>, 1), <<>>)
+ASSUME AssertEq(RemoveFirst(<<1,2>>, 1), <<2>>)
+ASSUME AssertEq(RemoveFirst(<<1,2,1>>, 1), <<2,1>>)
+ASSUME AssertEq(RemoveFirst(<<1,2,1,2>>, 2), <<1,1,2>>)
+
+ASSUME AssertEq(RemoveFirstMatch(<<>>, LAMBDA e: e = 1), <<>>)
+ASSUME AssertEq(RemoveFirstMatch(<<1>>, LAMBDA e: e = 1), <<>>)
+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>>)
 
 =============================================================================