Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- a/demo/more/dlist.ur Sun Oct 10 14:41:03 2010 -0400 +++ b/demo/more/dlist.ur Sun Oct 10 15:37:14 2010 -0400 @@ -119,7 +119,8 @@ end}/> </xml> -fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter = +fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) + : option int -> list (t * position) -> xml (ctx ++ body) [] [] = let fun renderFlat' len ls = case len of @@ -233,13 +234,13 @@ None => elems | Some pos => skip pos elems in - return (renderFlat f r.Filter len elems) + return (renderFlat f len elems) end}/> </xml> fun delete pos = pos -fun elements' [t] (dl'' : dlist'' t) = +fun elements' [t] (dl'' : dlist'' t) : signal (list t) = case dl'' of Nil => return [] | Cons (x, dl'') => @@ -247,13 +248,13 @@ tl <- elements' dl''; return (x :: tl) -fun elements [t] (dl : dlist t) = +fun elements [t] (dl : dlist t) : signal (list t) = dl' <- signal dl; case dl' of Empty => return [] | Nonempty {Head = hd, ...} => elements' hd -fun size' [t] (dl'' : dlist'' t) = +fun size' [t] (dl'' : dlist'' t) : signal int = case dl'' of Nil => return 0 | Cons (x, dl'') => @@ -261,13 +262,13 @@ n <- size' dl''; return (n + 1) -fun size [t] (dl : dlist t) = +fun size [t] (dl : dlist t) : signal int = dl' <- signal dl; case dl' of Empty => return 0 | Nonempty {Head = hd, ...} => size' hd -fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) = +fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) : signal int = case dl'' of Nil => return 0 | Cons (x, dl'') => @@ -276,7 +277,7 @@ n <- numPassing' f dl''; return (if b then n + 1 else n) -fun numPassing [t] (f : t -> signal bool) (dl : dlist t) = +fun numPassing [t] (f : t -> signal bool) (dl : dlist t) : signal int = dl' <- signal dl; case dl' of Empty => return 0