SequencesExt!ReplaceFirstSubSeq

[Feature]

Author: lemmy

modules/SequencesExt.tla

@@ -288,4 +288,34 @@ SubSeqs(s) ==
   (**************************************************************************)
   { SubSeq(s, i+1, j) : i, j \in 0..Len(s) }
 
+
+IndexFirstSubSeq(s, t) ==
+  (**************************************************************************)
+  (* The (1-based) index of the beginning of the subsequence  s  of the     *)
+  (* sequence  t  .  If  s  appears in  t  multiple times, this equals the  *)
+  (* lowest index.                                                          *)
+  (* For example:  IndexFirstSubSeq(<<1>>, <<1,1,1>>) = 1                   *)
+  (**************************************************************************)
+  LET last == CHOOSE i \in 0..Len(t) :
+                /\ s \in SubSeqs(SubSeq(t, 1, i))
+                /\ \A j \in 0..i-1 : s \notin SubSeqs(SubSeq(t, 1, j))
+  IN last - (Len(s) - 1)
+
+ReplaceSubSeqAt(i, r, s, t) ==
+  (**************************************************************************)
+  (* The sequence  t  with its subsequence  s  at position  i  replaced by  *)
+  (* the sequence  r  .                                                     *)
+  (**************************************************************************)
+  LET prefix == SubSeq(t, 1, i - 1)
+      suffix == SubSeq(t, i + Len(s), Len(t))
+  IN prefix \o r \o suffix 
+
+ReplaceFirstSubSeq(r, s, t) ==
+  (**************************************************************************)
+  (* The sequence  t  with its subsequence  s  replaced by the sequence  r  *)
+  (**************************************************************************)
+  IF s \in SubSeqs(t)
+  THEN ReplaceSubSeqAt(IndexFirstSubSeq(s, t), r, s, t)
+  ELSE t
+
 =============================================================================

modules/tlc2/overrides/SequencesExt.java

@@ -25,9 +25,17 @@
  *   Markus Alexander Kuppe - initial API and implementation
  ******************************************************************************/
 
+import java.util.regex.Pattern;
+
+import tla2sany.semantic.ExprOrOpArgNode;
 import tlc2.output.EC;
 import tlc2.tool.EvalControl;
 import tlc2.tool.EvalException;
+import tlc2.tool.TLCState;
+import tlc2.tool.coverage.CostModel;
+import tlc2.tool.impl.Tool;
+import tlc2.util.Context;
+import tlc2.value.IValue;
 import tlc2.value.Values;
 import tlc2.value.impl.Applicable;
 import tlc2.value.impl.BoolValue;
@@ -231,4 +239,22 @@ public static Value foldRight(final OpValue op, final Value val, final Value bas
 
 		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,
+			final TLCState s0, final TLCState s1, final int control, final CostModel cm) {
+		final IValue r = tool.eval(args[0], c, s0, s1, control, cm);
+		final IValue s = tool.eval(args[1], c, s0, s1, control, cm);
+		final IValue t = tool.eval(args[2], c, s0, s1, control, cm);
+		
+		if (r instanceof StringValue && s instanceof StringValue && t instanceof StringValue) {
+			final String st = ((StringValue) t).toUnquotedString();
+			final String ss = ((StringValue) s).toUnquotedString();
+			final String sr = ((StringValue) r).toUnquotedString();
+			
+			return new StringValue(st.replaceFirst(Pattern.quote(ss), sr));
+		}
+		
+		return null; // Non-string functions handled by pure TLA+ definition of operator.
+	}
 }

tests/SequencesExtTests.tla

@@ -192,4 +192,39 @@ ASSUME \A seq \in BoundedSeq(1..5, 5) :
                    /\ Len(s) <= Len(seq)
                    /\ Range(s) \subseteq Range(seq)
 
+-----------------------------------------------------------------------------
+
+ASSUME ReplaceFirstSubSeq(<<>>,<<>>,<<>>) = <<>>
+ASSUME ReplaceFirstSubSeq(<<4>>,<<>>,<<>>) = <<4>>
+ASSUME ReplaceFirstSubSeq(<<4>>,<<4>>,<<>>) = <<>>
+ASSUME ReplaceFirstSubSeq(<<>>,<<>>,<<3,2,3,4>>) = <<3,2,3,4>>
+ASSUME ReplaceFirstSubSeq(<<4,4>>,<<3,2,3,4>>,<<3,2,3,4>>) = <<4,4>>
+ASSUME ReplaceFirstSubSeq(<<4,4>>,<<>>,<<3,2,3,4>>) = <<4,4,3,2,3,4>>
+
+ASSUME ReplaceFirstSubSeq(<<4,4>>,<<4>>,<<3,2,3,4>>) = <<3,2,3,4,4>>
+ASSUME ReplaceFirstSubSeq(<<>>,<<4>>,<<3,2,3,4>>) = <<3,2,3>>
+ASSUME ReplaceFirstSubSeq(<<>>,<<4>>,<<3,2,3,4,4>>) = <<3,2,3,4>>
+ASSUME ReplaceFirstSubSeq(<<4,4>>,<<3>>,<<3,2,3,4>>) = <<4,4,2,3,4>>
+ASSUME ReplaceFirstSubSeq(<<4>>, <<1,2>>, <<1,2,1,2>>) = <<4,1,2>>
+ASSUME ReplaceFirstSubSeq(<<4,4>>, <<1,2>>, <<1,2,1,2>>) = <<4,4,1,2>>
+ASSUME ReplaceFirstSubSeq(<<4,4,4>>, <<1,2>>, <<1,2,1,2>>) = <<4,4,4,1,2>>
+
+ASSUME ReplaceFirstSubSeq(<<1,2>>, <<1,2>>, <<1,2,2,1>>) = <<1,2,2,1>>
+ASSUME ReplaceFirstSubSeq(<<2,1>>, <<1,2>>, <<1,2,2,1>>) = <<2,1,2,1>>
+
+ASSUME \A seq \in (BoundedSeq(1..5, 5) \ {<<>>}):
+    /\ ReplaceFirstSubSeq(<<6>>, <<>>, seq) = <<6>> \o seq
+    /\ ReplaceFirstSubSeq(<<6>>, <<Head(seq)>>, seq) = <<6>> \o Tail(seq)
+
+ASSUME ReplaceFirstSubSeq("", "", "") = ""
+ASSUME ReplaceFirstSubSeq("a", "", "") = "a"
+ASSUME ReplaceFirstSubSeq("a", "b", "") = ""
+ASSUME ReplaceFirstSubSeq("a", "d", "abc") = "abc"
+ASSUME ReplaceFirstSubSeq("ddd", "ab", "abab") = "dddab"
+ASSUME ReplaceFirstSubSeq("ddd", "aa", "aaa") = "ddda"
+ASSUME ReplaceFirstSubSeq("ddd", "abab", "abab") = "ddd"
+
+ASSUME ReplaceFirstSubSeq("\\\\", "\\", "Properly escape the \\quotes") = "Properly escape the \\\\quotes"
+ASSUME ReplaceFirstSubSeq("replaces", "%pattern%", "This %pattern% the pattern") = "This replaces the pattern"
+
 =============================================================================