comparison demo/more/dlist.ur @ 964:fbc3a0eef45a

Paging mostly working; just need to get it working properly with filtering
author Adam Chlipala <adamc@hcoop.net>
date Sat, 19 Sep 2009 14:21:25 -0400
parents 6f9d1565de56
children e9c5992bc9bc
comparison
equal deleted inserted replaced
963:6f9d1565de56 964:fbc3a0eef45a
244 dl' <- signal dl; 244 dl' <- signal dl;
245 case dl' of 245 case dl' of
246 Empty => return [] 246 Empty => return []
247 | Nonempty {Head = hd, ...} => elements' hd 247 | Nonempty {Head = hd, ...} => elements' hd
248 248
249 fun size' [t] (dl'' : dlist'' t) =
250 case dl'' of
251 Nil => return 0
252 | Cons (x, dl'') =>
253 dl'' <- signal dl'';
254 n <- size' dl'';
255 return (n + 1)
256
257 fun size [t] (dl : dlist t) =
258 dl' <- signal dl;
259 case dl' of
260 Empty => return 0
261 | Nonempty {Head = hd, ...} => size' hd
262
249 fun foldl [t] [acc] (f : t -> acc -> signal acc) = 263 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
250 let 264 let
251 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc = 265 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
252 case dl of 266 case dl of
253 Nil => return i 267 Nil => return i