diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-09-19 13:55:37 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-09-19 13:55:37 -0400 |
commit | ea30827e1977b1d1d028aa7701519bf95b976a3a (patch) | |
tree | 01b86deb0a5b412de199989ae743ac05b0574544 /demo/more/dlist.ur | |
parent | 41c93b49de08da17c1ea0d4c32481aaf8b6faa57 (diff) |
Testing Dlist MaxLength with constant value
Diffstat (limited to 'demo/more/dlist.ur')
-rw-r--r-- | demo/more/dlist.ur | 77 |
1 files changed, 51 insertions, 26 deletions
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur index 3bec8077..1a5be7e3 100644 --- a/demo/more/dlist.ur +++ b/demo/more/dlist.ur @@ -66,29 +66,33 @@ fun replace [t] dl ls = set dl (Nonempty {Head = Cons (x, hd), Tail = tlS}) end -fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos dl = <xml> +fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos len dl = <xml> <dyn signal={dl' <- signal dl; case dl' of Empty => return <xml/> | Nonempty {Head = hd, Tail = tlTop} => let - fun render' prev dl'' = - case dl'' of - Nil => <xml/> - | Cons (v, tl) => - let - val pos = case prev of - None => headPos dl - | Some prev => tailPos prev tl tlTop - in - <xml><dyn signal={b <- filter v; - return (if b then - f v pos - else - <xml/>)}/> - <dyn signal={tl' <- signal tl; - return (render' (Some tl) tl')}/></xml> - end + fun render' prev dl'' len = + case len of + Some 0 => <xml/> + | _ => + case dl'' of + Nil => <xml/> + | Cons (v, tl) => + let + val pos = case prev of + None => headPos dl + | Some prev => tailPos prev tl tlTop + val len = Option.mp (fn n => n - 1) len + in + <xml><dyn signal={b <- filter v; + return (if b then + f v pos + else + <xml/>)}/> + <dyn signal={tl' <- signal tl; + return (render' (Some tl) tl' len)}/></xml> + end fun skip pos hd = case pos of @@ -101,15 +105,33 @@ fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] skip (pos-1) tl' in case pos of - None => return (render' None hd) + None => return (render' None hd len) | Some pos => hd <- skip pos hd; - return (render' None hd) + return (render' None hd len) end}/> </xml> -fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls = - List.mapX (fn p => f p.1 p.2) ls +fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter = + let + fun renderFlat' len ls = + case len of + Some 0 => <xml/> + | _ => + case ls of + [] => <xml/> + | p :: ls => + let + val len = + case len of + None => None + | Some n => Some (n - 1) + in + <xml>{f p.1 p.2}{renderFlat' len ls}</xml> + end + in + renderFlat' + end val split [t] = let @@ -158,11 +180,14 @@ fun sort [t] (cmp : t -> t -> signal bool) = fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool, Sort : signal (option (t -> t -> signal bool)), - StartPosition : signal (option int)}) dl = <xml> - <dyn signal={cmp <- r.Sort; + StartPosition : signal (option int), + MaxLength : signal (option int)}) dl = <xml> + <dyn signal={len <- r.MaxLength; + cmp <- r.Sort; pos <- r.StartPosition; + case cmp of - None => return (renderDyn f r.Filter pos dl) + None => return (renderDyn f r.Filter pos len dl) | Some cmp => dl' <- signal dl; elems <- (case dl' of @@ -201,7 +226,7 @@ fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool, None => elems | Some pos => skip pos elems in - return (renderFlat f r.Filter elems) + return (renderFlat f r.Filter len elems) end}/> </xml> |