Commit 0098b5f8b0efe9d42e883771f6aebdaf924293c1

Authored by HerrmannM
1 parent 6730102e

maj list

Showing 1 changed file with 12 additions and 2 deletions   Show diff stats
anubis_dev/library/tools/list.anubis
@@ -825,7 +825,7 @@ public define List($A) unfold($B item, $B -> Result($A, ($A, $B)) unspool) = if @@ -825,7 +825,7 @@ public define List($A) unfold($B item, $B -> Result($A, ($A, $B)) unspool) = if
825 *** Zip 825 *** Zip
826 ================================================================================================================== 826 ==================================================================================================================
827 827
828 -define Maybe(List(($T,$T))) zip(List($T) lg, List($T) ld, List(($T,$T)) acc) = 828 +define Maybe(List(($T1, $T2))) zip(List($T1) lg, List($T2) ld, List(($T1, $T2)) acc) =
829 if lg is 829 if lg is
830 { 830 {
831 [ ] then if ld is [ ] then success(reverse(acc)) else failure, 831 [ ] then if ld is [ ] then success(reverse(acc)) else failure,
@@ -835,7 +835,17 @@ define Maybe(List(($T,$T))) zip(List($T) lg, List($T) ld, List(($T,$T)) acc) = @@ -835,7 +835,17 @@ define Maybe(List(($T,$T))) zip(List($T) lg, List($T) ld, List(($T,$T)) acc) =
835 }. 835 }.
836 836
837 Zip two lists into a list of tuples. Returns failure if the two lists have different length. 837 Zip two lists into a list of tuples. Returns failure if the two lists have different length.
838 -public define Maybe(List(($T,$T))) zip(List($T) lg, List($T) ld) = zip(lg, ld, []). 838 +public define Maybe(List(($T1,$T2))) zip(List($T1) lg, List($T2) ld) = zip(lg, ld, []).
  839 +
  840 + Note: The list is pre-reversed in the public interface.
  841 +define (List($T1), List($T2)) unzip(List(($T1, $T2)) list, List($T1) accl, List($T2) accr) =
  842 + if list is
  843 + {
  844 + [ ] then (accl, accr),
  845 + [h . t] then unzip(t, [p1(h) . accl], [p2(h) . accr])
  846 + }.
  847 +
  848 +public define (List($T1), List($T2)) unzip(List(($T1, $T2)) l) = unzip(reverse(l), [], []).
839 849
840 850
841 851