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