annotate lib/ur/listPair.ur @ 1884:5c30eea7aa78
ListPair.map2, based on code by escalier@riseup.net
author |
Adam Chlipala <adam@chlipala.net> |
date |
Sun, 03 Nov 2013 19:27:30 -0500 |
parents |
1c2f335297b7 |
children |
8297968cf7ef |
rev |
line source |
adamc@850
|
1 fun foldlAbort [a] [b] [c] f =
|
adamc@846
|
2 let
|
adamc@850
|
3 fun foldlAbort' acc ls1 ls2 =
|
adamc@846
|
4 case (ls1, ls2) of
|
adamc@846
|
5 ([], []) => Some acc
|
adamc@846
|
6 | (x1 :: ls1, x2 :: ls2) =>
|
adamc@846
|
7 (case f x1 x2 acc of
|
adamc@846
|
8 None => None
|
adamc@850
|
9 | Some acc' => foldlAbort' acc' ls1 ls2)
|
adamc@846
|
10 | _ => None
|
adamc@846
|
11 in
|
adamc@850
|
12 foldlAbort'
|
adamc@846
|
13 end
|
adamc@846
|
14
|
adamc@826
|
15 fun mapX [a] [b] [ctx ::: {Unit}] f =
|
adamc@801
|
16 let
|
adamc@801
|
17 fun mapX' ls1 ls2 =
|
adamc@801
|
18 case (ls1, ls2) of
|
adamc@801
|
19 ([], []) => <xml/>
|
adamc@801
|
20 | (x1 :: ls1, x2 :: ls2) => <xml>{f x1 x2}{mapX' ls1 ls2}</xml>
|
adamc@801
|
21 | _ => error <xml>ListPair.mapX: Unequal list lengths</xml>
|
adamc@801
|
22 in
|
adamc@801
|
23 mapX'
|
adamc@801
|
24 end
|
adamc@844
|
25
|
adamc@844
|
26 fun all [a] [b] f =
|
adamc@844
|
27 let
|
adamc@844
|
28 fun all' ls1 ls2 =
|
adamc@844
|
29 case (ls1, ls2) of
|
adamc@844
|
30 ([], []) => True
|
adamc@844
|
31 | (x1 :: ls1, x2 :: ls2) => f x1 x2 && all' ls1 ls2
|
adamc@844
|
32 | _ => False
|
adamc@844
|
33 in
|
adamc@844
|
34 all'
|
adamc@844
|
35 end
|
adam@1884
|
36
|
adam@1884
|
37 fun map2 [a] [b] [c] (f : a -> b -> c) =
|
adam@1884
|
38 let
|
adam@1884
|
39 fun map2' ls1 ls2 =
|
adam@1884
|
40 case (ls1, ls2) of
|
adam@1884
|
41 ([], []) => []
|
adam@1884
|
42 | (x1 :: ls1, x2 :: ls2) => f x1 x2 :: map2' ls1 ls2
|
adam@1884
|
43 | _ => error <xml>ListPair.map2: Unequal list lengths</xml>
|
adam@1884
|
44 in
|
adam@1884
|
45 map2'
|
adam@1884
|
46 end
|