Mercurial > urweb

comparison lib/ur/list.ur @ 826:78504d97410b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix EDLet elab_util bug
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 12:40:55 -0400
parents d4e811beb8eb
children d07980bf1444
comparison
equal deleted inserted replaced
825:7f871c03e3a1 826:78504d97410b
1 datatype t = datatype Basis.list 1 datatype t = datatype Basis.list
2 2
3 val show (a ::: Type) (_ : show a) = 3 val show = fn [a] (_ : show a) =>
4 let 4 let
5 fun show' (ls : list a) = 5 fun show' (ls : list a) =
6 case ls of 6 case ls of
7 [] => "[]" 7 [] => "[]"
8 | x :: ls => show x ^ " :: " ^ show' ls 8 | x :: ls => show x ^ " :: " ^ show' ls
9 in 9 in
10 mkShow show' 10 mkShow show'
11 end 11 end
12 12
13 val rev (a ::: Type) = 13 val rev = fn [a] =>
14 let 14 let
15 fun rev' acc (ls : list a) = 15 fun rev' acc (ls : list a) =
16 case ls of 16 case ls of
17 [] => acc 17 [] => acc
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) = 23 val revAppend = fn [a] =>
24 let 24 let
25 fun ra (ls : list a) acc = 25 fun ra (ls : list a) acc =
26 case ls of 26 case ls of
27 [] => acc 27 [] => acc
28 | x :: ls => ra ls (x :: acc) 28 | x :: ls => ra ls (x :: acc)
29 in 29 in
30 ra 30 ra
31 end 31 end
32 32
33 fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2 33 fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
34 34
35 fun mp (a ::: Type) (b ::: Type) f = 35 fun mp [a] [b] f =
36 let 36 let
37 fun mp' acc ls = 37 fun mp' acc ls =
38 case ls of 38 case ls of
39 [] => rev acc 39 [] => rev acc
40 | x :: ls => mp' (f x :: acc) ls 40 | x :: ls => mp' (f x :: acc) ls
41 in 41 in
42 mp' [] 42 mp' []
43 end 43 end
44 44
45 fun mapPartial (a ::: Type) (b ::: Type) f = 45 fun mapPartial [a] [b] f =
46 let 46 let
47 fun mp' acc ls = 47 fun mp' acc ls =
48 case ls of 48 case ls of
49 [] => rev acc 49 [] => rev acc
50 | x :: ls => mp' (case f x of 50 | x :: ls => mp' (case f x of
52 | Some y => y :: acc) ls 52 | Some y => y :: acc) ls
53 in 53 in
54 mp' [] 54 mp' []
55 end 55 end
56 56
57 fun mapX (a ::: Type) (ctx ::: {Unit}) f = 57 fun mapX [a] [ctx ::: {Unit}] f =
58 let 58 let
59 fun mapX' ls = 59 fun mapX' ls =
60 case ls of 60 case ls of
61 [] => <xml/> 61 [] => <xml/>
62 | x :: ls => <xml>{f x}{mapX' ls}</xml> 62 | x :: ls => <xml>{f x}{mapX' ls}</xml>
63 in 63 in
64 mapX' 64 mapX'
65 end 65 end
66 66
67 fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f = 67 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
68 let 68 let
69 fun mapM' acc ls = 69 fun mapM' acc ls =
70 case ls of 70 case ls of
71 [] => return (rev acc) 71 [] => return (rev acc)
72 | x :: ls => x' <- f x; mapM' (x' :: acc) ls 72 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
73 in 73 in
74 mapM' [] 74 mapM' []
75 end 75 end
76 76
77 fun filter (a ::: Type) f = 77 fun filter [a] f =
78 let 78 let
79 fun fil acc ls = 79 fun fil acc ls =
80 case ls of 80 case ls of
81 [] => rev acc 81 [] => rev acc
82 | x :: ls => fil (if f x then x :: acc else acc) ls 82 | x :: ls => fil (if f x then x :: acc else acc) ls
83 in 83 in
84 fil [] 84 fil []
85 end 85 end
86 86
87 fun exists (a ::: Type) f = 87 fun exists [a] f =
88 let 88 let
89 fun ex ls = 89 fun ex ls =
90 case ls of 90 case ls of
91 [] => False 91 [] => False
92 | x :: ls => 92 | x :: ls =>
96 ex ls 96 ex ls
97 in 97 in
98 ex 98 ex
99 end 99 end
100 100
101 fun foldlMap (a ::: Type) (b ::: Type) (c ::: Type) f = 101 fun foldlMap [a] [b] [c] f =
102 let 102 let
103 fun fold ls' st ls = 103 fun fold ls' st ls =
104 case ls of 104 case ls of
105 [] => (rev ls', st) 105 [] => (rev ls', st)
106 | x :: ls => 106 | x :: ls =>