Mercurial > urweb

comparison demo/more/dlist.ur @ 1304:f0afe61a6f8b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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