Redefine restricted SequencesExt!Zip.

Addresses Github issue #78 #78 [Feature]
tlaplus · Oct 21, 2022 · c5708d0 · c5708d0
1 parent 51902eb
commit c5708d0
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 5 deletions.
diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla
@@ -320,7 +320,7 @@ FlattenSeq(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)                  *)
+  (*   t  in this order.                                                    *)
   (*                                                                        *)
   (* Examples:                                                              *)
   (*                                                                        *)
@@ -329,10 +329,9 @@ Zip(s, t) ==
   (*  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"
+  IF Len(s) < Len(t)
+  THEN FoldLeft(LAMBDA acc, e: Append(acc, << e, t[Len(acc)+1] >>), <<>>, s)
+  ELSE FoldLeft(LAMBDA acc, e: Append(acc, << s[Len(acc)+1], e >>), <<>>, t)
 
 Interleave(s, t) ==
   (**************************************************************************)

diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla
@@ -194,6 +194,13 @@ 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 Zip(<<1>>, <<>>) = << >>
+ASSUME Zip(<<>>, <<1>>) = << >>
+ASSUME Zip(<<2>>, <<2, 2>>) = << <<2, 2>> >>
+ASSUME Zip(<<2, 3>>, <<3>>) = << <<2, 3>> >>
+ASSUME Zip(<<2,3,3>>, <<2, 2>>) = << <<2, 2>>, <<3, 2>> >>
+ASSUME Zip(<<2, 3>>, <<3,3,3>>) = << <<2, 3>>, <<3, 3>> >>
+
 -----------------------------------------------------------------------------
 
 ASSUME SubSeqs(<<>>) = {<<>>}