Mercurial > urweb
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 |