From 065e7b74225c58062b7ee77a8dddb70673aa24f1 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Wed, 11 Oct 2023 14:04:17 -0700
Subject: [PATCH] Add SequencesExt!RemoveFirst and RemoveFirstMatch.

---
 modules/SequencesExt.tla                 | 18 +++++++
 modules/tlc2/overrides/SequencesExt.java | 60 ++++++++++++++++++++++++
 tests/SequencesExtTests.tla              | 13 +++++
 3 files changed, 91 insertions(+)

diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla
index e67d636..9fb13b0 100644
--- 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
index cda42aa..a01e6c0 100644
--- 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
index bac46fe..1ac478e 100644
--- 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>>)
 
 =============================================================================