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