comparison lib/ur/list.ur @ 845:6725d73c3c31

Mark current as effectful; add List functions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Jun 2009 11:12:34 -0400
parents 74a1e3bdf430
children 0d30e6338c65
comparison
equal deleted inserted replaced
844:74a1e3bdf430 845:6725d73c3c31
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 fun foldl [a] [b] f =
14 let
15 fun foldl' acc ls =
16 case ls of
17 [] => acc
18 | x :: ls => foldl' (f x acc) ls
19 in
20 foldl'
21 end
22
13 val rev = fn [a] => 23 val rev = fn [a] =>
14 let 24 let
15 fun rev' acc (ls : list a) = 25 fun rev' acc (ls : list a) =
16 case ls of 26 case ls of
17 [] => acc 27 [] => acc
121 (y, st) => fold (y :: ls') st ls 131 (y, st) => fold (y :: ls') st ls
122 in 132 in
123 fold [] 133 fold []
124 end 134 end
125 135
136 fun search [a] [b] f =
137 let
138 fun search' ls =
139 case ls of
140 [] => None
141 | x :: ls =>
142 case f x of
143 None => search' ls
144 | v => v
145 in
146 search'
147 end
148
149 fun foldlM [m] (_ : monad m) [a] [b] f =
150 let
151 fun foldlM' acc ls =
152 case ls of
153 [] => return acc
154 | x :: ls =>
155 acc <- f x acc;
156 foldlM' acc ls
157 in
158 foldlM'
159 end
160
161 fun all [m] f =
162 let
163 fun all' ls =
164 case ls of
165 [] => True
166 | x :: ls => f x && all' ls
167 in
168 all'
169 end
170
171 fun app [m] (_ : monad m) [a] f =
172 let
173 fun app' ls =
174 case ls of
175 [] => return ()
176 | x :: ls =>
177 f x;
178 app' ls
179 in
180 app'
181 end
182
126 fun assoc [a] [b] (_ : eq a) (x : a) = 183 fun assoc [a] [b] (_ : eq a) (x : a) =
127 let 184 let
128 fun assoc' ls = 185 fun assoc' (ls : list (a * b)) =
129 case ls of 186 case ls of
130 [] => None 187 [] => None
131 | (y, z) :: ls => 188 | (y, z) :: ls =>
132 if x = y then 189 if x = y then
133 Some z 190 Some z
135 assoc' ls 192 assoc' ls
136 in 193 in
137 assoc' 194 assoc'
138 end 195 end
139 196
140 fun search [a] [b] f = 197 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
141 let 198 case assoc x ls of
142 fun search' ls = 199 None => (x, y) :: ls
143 case ls of 200 | Some _ => ls
144 [] => None
145 | x :: ls =>
146 case f x of
147 None => search' ls
148 | v => v
149 in
150 search'
151 end
152
153 fun foldlM [m] (_ : monad m) [a] [b] f =
154 let
155 fun foldlM' acc ls =
156 case ls of
157 [] => return acc
158 | x :: ls =>
159 acc <- f x acc;
160 foldlM' acc ls
161 in
162 foldlM'
163 end
164
165 fun all [m] f =
166 let
167 fun all' ls =
168 case ls of
169 [] => True
170 | x :: ls => f x && all' ls
171 in
172 all'
173 end
174
175 fun app [m] (_ : monad m) [a] f =
176 let
177 fun app' ls =
178 case ls of
179 [] => return ()
180 | x :: ls =>
181 f x;
182 app' ls
183 in
184 app'
185 end