Mercurial > urweb
comparison demo/more/dlist.ur @ 1304:f0afe61a6f8b
Tweaking unification fix to apply to demo/more
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 10 Oct 2010 15:37:14 -0400 |
parents | c2fe1dbaceb9 |
children | 68429cfce8db |
comparison
equal
deleted
inserted
replaced
1303:c7b9a33c26c8 | 1304:f0afe61a6f8b |
---|---|
117 hd <- skip pos hd; | 117 hd <- skip pos hd; |
118 return (render' None hd len) | 118 return (render' None hd len) |
119 end}/> | 119 end}/> |
120 </xml> | 120 </xml> |
121 | 121 |
122 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter = | 122 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) |
123 : option int -> list (t * position) -> xml (ctx ++ body) [] [] = | |
123 let | 124 let |
124 fun renderFlat' len ls = | 125 fun renderFlat' len ls = |
125 case len of | 126 case len of |
126 Some 0 => <xml/> | 127 Some 0 => <xml/> |
127 | _ => | 128 | _ => |
231 val elems = | 232 val elems = |
232 case pos of | 233 case pos of |
233 None => elems | 234 None => elems |
234 | Some pos => skip pos elems | 235 | Some pos => skip pos elems |
235 in | 236 in |
236 return (renderFlat f r.Filter len elems) | 237 return (renderFlat f len elems) |
237 end}/> | 238 end}/> |
238 </xml> | 239 </xml> |
239 | 240 |
240 fun delete pos = pos | 241 fun delete pos = pos |
241 | 242 |
242 fun elements' [t] (dl'' : dlist'' t) = | 243 fun elements' [t] (dl'' : dlist'' t) : signal (list t) = |
243 case dl'' of | 244 case dl'' of |
244 Nil => return [] | 245 Nil => return [] |
245 | Cons (x, dl'') => | 246 | Cons (x, dl'') => |
246 dl'' <- signal dl''; | 247 dl'' <- signal dl''; |
247 tl <- elements' dl''; | 248 tl <- elements' dl''; |
248 return (x :: tl) | 249 return (x :: tl) |
249 | 250 |
250 fun elements [t] (dl : dlist t) = | 251 fun elements [t] (dl : dlist t) : signal (list t) = |
251 dl' <- signal dl; | 252 dl' <- signal dl; |
252 case dl' of | 253 case dl' of |
253 Empty => return [] | 254 Empty => return [] |
254 | Nonempty {Head = hd, ...} => elements' hd | 255 | Nonempty {Head = hd, ...} => elements' hd |
255 | 256 |
256 fun size' [t] (dl'' : dlist'' t) = | 257 fun size' [t] (dl'' : dlist'' t) : signal int = |
257 case dl'' of | 258 case dl'' of |
258 Nil => return 0 | 259 Nil => return 0 |
259 | Cons (x, dl'') => | 260 | Cons (x, dl'') => |
260 dl'' <- signal dl''; | 261 dl'' <- signal dl''; |
261 n <- size' dl''; | 262 n <- size' dl''; |
262 return (n + 1) | 263 return (n + 1) |
263 | 264 |
264 fun size [t] (dl : dlist t) = | 265 fun size [t] (dl : dlist t) : signal int = |
265 dl' <- signal dl; | 266 dl' <- signal dl; |
266 case dl' of | 267 case dl' of |
267 Empty => return 0 | 268 Empty => return 0 |
268 | Nonempty {Head = hd, ...} => size' hd | 269 | Nonempty {Head = hd, ...} => size' hd |
269 | 270 |
270 fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) = | 271 fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) : signal int = |
271 case dl'' of | 272 case dl'' of |
272 Nil => return 0 | 273 Nil => return 0 |
273 | Cons (x, dl'') => | 274 | Cons (x, dl'') => |
274 b <- f x; | 275 b <- f x; |
275 dl'' <- signal dl''; | 276 dl'' <- signal dl''; |
276 n <- numPassing' f dl''; | 277 n <- numPassing' f dl''; |
277 return (if b then n + 1 else n) | 278 return (if b then n + 1 else n) |
278 | 279 |
279 fun numPassing [t] (f : t -> signal bool) (dl : dlist t) = | 280 fun numPassing [t] (f : t -> signal bool) (dl : dlist t) : signal int = |
280 dl' <- signal dl; | 281 dl' <- signal dl; |
281 case dl' of | 282 case dl' of |
282 Empty => return 0 | 283 Empty => return 0 |
283 | Nonempty {Head = hd, ...} => numPassing' f hd | 284 | Nonempty {Head = hd, ...} => numPassing' f hd |
284 | 285 |