Align SequencesExt!Zip with the usual definition in PLs.

[Refactor]

Author: konnov

modules/SequencesExt.tla

@@ -283,6 +283,23 @@ FlattenSeq(seqs) ==
         IF i = 1 THEN seqs[i] ELSE flatten[i-1] \o seqs[i]
     IN flatten[Len(seqs)]
 
+Zip(s, t) ==
+  (**************************************************************************)
+  (* A sequence where the i-th tuple contains the i-th element of  s  and   *)
+  (*   t  in this order.  Not defined for  Len(s) # Len(t)                  *)
+  (*                                                                        *)
+  (* Examples:                                                              *)
+  (*                                                                        *)
+  (*  Zip(<< >>, << >>) = << >>                                             *)
+  (*  Zip(<<"a">>, <<"b">>) = <<"a", "b">>                                  *)
+  (*  Zip(<<1, 3>>, <<2, 4>>) = <<<<1, 2>>, <<3, 4>>>>                      *)
+  (*  FlattenSeq(Zip(<<1, 3>>, <<2, 4>>)) = <<1, 2, 3, 4>>>>                *)
+  (**************************************************************************)
+  CASE Len(s) = Len(t) /\ Len(s) > 0 ->
+        [ i \in DOMAIN s |-> <<s[i], t[i]>> ]
+    [] Len(s) = Len(t) /\ Len(s) = 0 -> << >>
+    \* error "Zip: sequences must have same length"
+
 Interleave(s, t) ==
   (**************************************************************************)
   (* A sequence where the i-th tuple contains the i-th element of  s  and   *)
@@ -303,7 +320,6 @@ Interleave(s, t) ==
     [] Len(s) = Len(t) /\ Len(s) = 0 -> << <<>>, <<>> >>
     \* error "Interleave: sequences must have same length"
 
-
 SubSeqs(s) ==
   (**************************************************************************)
   (* The set of all subsequences of the sequence  s  .  Note that the empty *)

tests/SequencesExtTests.tla

@@ -182,6 +182,20 @@ ASSUME AssertEq(FlattenSeq(Interleave(<<"a", "c">>, <<"b", "d">>)), <<"a", "b",
 
 -----------------------------------------------------------------------------
 
+ASSUME Zip(<<>>, <<>>) = << >>
+ASSUME Zip(<< <<>> >>, <<1>>) = << << <<>>, 1>> >>
+ASSUME Zip(<<1>>, << <<>>  >>) = << <<1, <<>> >> >>
+ASSUME Zip(<<2>>, <<2>>) = << <<2, 2>> >>
+ASSUME Zip(<<2>>, <<3>>) = << <<2, 3>> >>
+ASSUME Zip(<<2, 3>>, <<1, 4>>) = << <<2, 1>>, <<3, 4>> >>
+ASSUME Zip(<<2, 3>>, <<2, 3>>) = << <<2, 2>>, <<3, 3>> >>
+ASSUME Zip(<<1, 3>>, <<2, 4>>) = << <<1, 2>>, <<3, 4>> >>
+ASSUME AssertEq(FlattenSeq(Zip(<<1, 3>>, <<2, 4>>)), <<1, 2, 3, 4>>)
+ASSUME Zip(<<"a", "c">>, <<"b", "d">>) = << <<"a", "b">>, <<"c", "d">> >>
+ASSUME AssertEq(FlattenSeq(Zip(<<"a", "c">>, <<"b", "d">>)), <<"a", "b", "c", "d">>)
+
+-----------------------------------------------------------------------------
+
 ASSUME SubSeqs(<<>>) = {<<>>}
 ASSUME SubSeqs(<<1>>) = {<<>>, <<1>>}
 ASSUME SubSeqs(<<1,1>>) = {<<>>, <<1>>, <<1,1>>}