comparison lib/ur/list.ur @ 821:395a5d450cc0

Chars and more string operations
author Adam Chlipala <adamc@hcoop.net>
date Tue, 26 May 2009 12:25:06 -0400
parents 066493f7f008
children d4e811beb8eb
comparison
equal deleted inserted replaced
820:91f465ded07e 821:395a5d450cc0
18 | x :: ls => rev' (x :: acc) ls 18 | x :: ls => rev' (x :: acc) ls
19 in 19 in
20 rev' [] 20 rev' []
21 end 21 end
22 22
23 val revAppend (a ::: Type) =
24 let
25 fun ra (ls : list a) acc =
26 case ls of
27 [] => acc
28 | x :: ls => ra ls (x :: acc)
29 in
30 ra
31 end
32
33 fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
34
23 fun mp (a ::: Type) (b ::: Type) f = 35 fun mp (a ::: Type) (b ::: Type) f =
24 let 36 let
25 fun mp' acc ls = 37 fun mp' acc ls =
26 case ls of 38 case ls of
27 [] => rev acc 39 [] => rev acc
28 | x :: ls => mp' (f x :: acc) ls 40 | x :: ls => mp' (f x :: acc) ls
41 in
42 mp' []
43 end
44
45 fun mapPartial (a ::: Type) (b ::: Type) f =
46 let
47 fun mp' acc ls =
48 case ls of
49 [] => rev acc
50 | x :: ls => mp' (case f x of
51 None => acc
52 | Some y => y :: acc) ls
29 in 53 in
30 mp' [] 54 mp' []
31 end 55 end
32 56
33 fun mapX (a ::: Type) (ctx ::: {Unit}) f = 57 fun mapX (a ::: Type) (ctx ::: {Unit}) f =
47 [] => return (rev acc) 71 [] => return (rev acc)
48 | x :: ls => x' <- f x; mapM' (x' :: acc) ls 72 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
49 in 73 in
50 mapM' [] 74 mapM' []
51 end 75 end
76
77 fun filter (a ::: Type) f =
78 let
79 fun fil acc ls =
80 case ls of
81 [] => rev acc
82 | x :: ls => fil (if f x then x :: acc else acc) ls
83 in
84 fil []
85 end