SequencesExt!ReplaceAllSubSeqs

[Feature]

Author: lemmy

modules/SequencesExt.tla

@@ -318,4 +318,43 @@ ReplaceFirstSubSeq(r, s, t) ==
   THEN ReplaceSubSeqAt(IndexFirstSubSeq(s, t), r, s, t)
   ELSE t
 
+ReplaceAllSubSeqs(r, s, t) ==
+  (**************************************************************************)
+  (* The sequence  t  with all subsequences  s  replaced by the sequence  r *)
+  (* Overlapping replacements are disambiguated by choosing the occurrence  *)
+  (* closer to the beginning of the sequence.                               *)
+  (*                                                                        *)
+  (* Examples:                                                              *)
+  (*                                                                        *)
+  (*  ReplaceAllSubSeqs(<<>>,<<>>,<<>>) = <<>>                              *)
+  (*  ReplaceAllSubSeqs(<<4>>,<<>>,<<>>) = <<4>>                            *)
+  (*  ReplaceAllSubSeqs(<<2>>,<<3>>,<<1,3>>) = <<1,2>>                      *)
+  (*  ReplaceAllSubSeqs(<<2,2>>,<<1,1>>,<<1,1,1>>) = <<2,2,1>>              *)
+  (**************************************************************************)
+  CASE s = t -> r
+    [] r = s -> t  \* TLC optimization
+    [] s # t /\ Len(s) = 0 ->
+        LET z == Zip([i \in 1..Len(t) |-> r], [i \in 1..Len(t) |-> <<t[i]>>])
+        IN FlattenSeq(FlattenSeq(z))
+    [] s # t /\ Len(s) > 0 /\ s \in SubSeqs(t) ->
+        \* Not defined recursively to avoid infinite loops.
+        LET match(f) == { i \in 1..Len(f) : s = f[i] }
+            comp(p, q) == \A i \in 1..Len(p) : p[i] <= q[i]
+            \* TODO: Replace with Seq(Seq(Range(t))) once *total* Java module
+            \*       override in place. The current override handles only the
+            \*       case where the parameters are strings (hence Range("abc") 
+            \*       not a problem with TLC).
+            R == BoundedSeq(BoundedSeq(Range(t), Len(t)), Len(t))
+            \* A) Matches the input t.
+            S == { f \in R : FlattenSeq(f) = t }
+            \* B) Has the max number of matches...
+            T == { f \in S : \A g \in S : 
+                    Cardinality(match(g)) <= Cardinality(match(f)) }
+            \* C) ...of min (leftmost) matches.
+            u == CHOOSE f \in T : 
+                    \A g \in T : comp(
+                        SetToSortSeq(match(f), <), SetToSortSeq(match(g), <))
+        IN FlattenSeq([i \in 1..Len(u) |-> IF s = u[i] THEN r ELSE u[i]])
+    [] OTHER -> t
+
 =============================================================================

modules/tlc2/overrides/SequencesExt.java

@@ -257,4 +257,22 @@ public static Value replaceFirstSubSeq(final Tool tool, final ExprOrOpArgNode[]
 
 		return null; // Non-string functions handled by pure TLA+ definition of operator.
 	}
+
+	@Evaluation(definition = "ReplaceAllSubSeqs", module = "SequencesExt", warn = false, silent = true)
+	public static Value replaceAllSubSeq(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.replaceAll(Pattern.quote(ss), sr));
+		}
+		
+		return null; // Non-string functions handled by pure TLA+ definition of operator.
+	}
 }

tests/SequencesExtTests.tla

@@ -227,4 +227,44 @@ 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"
 
+-----------------------------------------------------------------------------
+
+ASSUME AssertEq(ReplaceAllSubSeqs(<<4>>,<<1>>,<<>>), <<>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<4>>,<<2>>,<<1>>), <<1>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<4>>,<<2>>,<<1,1>>), <<1,1>>)
+
+ASSUME AssertEq(ReplaceAllSubSeqs(<<>>,<<>>,<<>>), <<>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<4>>,<<>>,<<>>), <<4>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<4,4>>,<<>>,<<>>), <<4,4>>)
+
+ASSUME AssertEq(ReplaceAllSubSeqs(<<1>>, <<1>>, <<1>>), <<1>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<2>>, <<3>>, <<1,3>>), <<1,2>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<1,1>>, <<1>>, <<1,1>>), <<1,1,1,1>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<1,1>>, <<1,1>>, <<1,1>>), <<1,1>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<2,2>>, <<1,1>>, <<1,1,1>>), <<2,2,1>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<>>, <<1,1>>, <<1,1,1>>), <<1>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<2,2>>, <<1,1,1>>, <<1,1,1>>), <<2,2>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<>>, <<1,1,1>>, <<1,1,1>>), <<>>)
+ASSUME AssertEq(ReplaceAllSubSeqs(<<2,2>>, <<1,1,1>>, <<1,1,1,1>>), <<2,2,1>>)
+
+ASSUME AssertEq(ReplaceAllSubSeqs(<<1,1>>, <<>>, <<2,2>>), <<1,1,2,1,1,2>>)
+
+ASSUME ReplaceAllSubSeqs("dd", "d", "dd") = "dddd"
+
+ASSUME ReplaceAllSubSeqs("ddd", "a", "") = ""
+ASSUME ReplaceAllSubSeqs("ddd", "", "") = "ddd"
+ASSUME ReplaceAllSubSeqs("ddd", "ab", "abab") = "dddddd"
+ASSUME ReplaceAllSubSeqs("ddd", "abab", "abab") = "ddd"
+
+ASSUME ReplaceAllSubSeqs("ddd", "aa", "aaa") = "ddda"
+ASSUME ReplaceAllSubSeqs("a", "a", "a") = "a"
+ASSUME ReplaceAllSubSeqs("aa", "aa", "aa") = "aa"
+ASSUME ReplaceAllSubSeqs("aa", "aa", "aaaa") = "aaaa"
+ASSUME ReplaceAllSubSeqs("aa", "aa", "bbbb") = "bbbb"
+
+ASSUME ReplaceAllSubSeqs("ddd", "", "abab") = "dddadddbdddadddbddd"
+
+ASSUME AssertEq(ReplaceAllSubSeqs("replaces", "%pattern%", "This %pattern% the pattern %pattern% multipe times"), "This replaces the pattern replaces multipe times")
+ASSUME AssertEq(ReplaceAllSubSeqs("\\\\", "\\", "Properly escape the \\quotes"), "Properly escape the \\\\quotes")
+
 =============================================================================