Mercurial > urweb
comparison demo/more/dlist.ur @ 965:e9c5992bc9bc
Progress on sorting + filtering
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 19 Sep 2009 14:42:36 -0400 |
parents | fbc3a0eef45a |
children | c2fe1dbaceb9 |
comparison
equal
deleted
inserted
replaced
964:fbc3a0eef45a | 965:e9c5992bc9bc |
---|---|
258 dl' <- signal dl; | 258 dl' <- signal dl; |
259 case dl' of | 259 case dl' of |
260 Empty => return 0 | 260 Empty => return 0 |
261 | Nonempty {Head = hd, ...} => size' hd | 261 | Nonempty {Head = hd, ...} => size' hd |
262 | 262 |
263 fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) = | |
264 case dl'' of | |
265 Nil => return 0 | |
266 | Cons (x, dl'') => | |
267 b <- f x; | |
268 dl'' <- signal dl''; | |
269 n <- numPassing' f dl''; | |
270 return (if b then n + 1 else n) | |
271 | |
272 fun numPassing [t] (f : t -> signal bool) (dl : dlist t) = | |
273 dl' <- signal dl; | |
274 case dl' of | |
275 Empty => return 0 | |
276 | Nonempty {Head = hd, ...} => numPassing' f hd | |
277 | |
263 fun foldl [t] [acc] (f : t -> acc -> signal acc) = | 278 fun foldl [t] [acc] (f : t -> acc -> signal acc) = |
264 let | 279 let |
265 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc = | 280 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc = |
266 case dl of | 281 case dl of |
267 Nil => return i | 282 Nil => return i |