Mercurial > urweb
changeset 963:6f9d1565de56
Testing Dlist MaxLength with constant value
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 19 Sep 2009 13:55:37 -0400 |
| parents | 7e7edfb6fe82 |
| children | fbc3a0eef45a |
| files | demo/more/dlist.ur demo/more/dlist.urs demo/more/grid.ur |
| diffstat | 3 files changed, 53 insertions(+), 26 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/more/dlist.ur Sat Sep 19 13:44:12 2009 -0400 +++ b/demo/more/dlist.ur Sat Sep 19 13:55:37 2009 -0400 @@ -66,29 +66,33 @@ 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 @@ 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 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 @@ None => elems | Some pos => skip pos elems in - return (renderFlat f r.Filter elems) + return (renderFlat f r.Filter len elems) end}/> </xml>
--- a/demo/more/dlist.urs Sat Sep 19 13:44:12 2009 -0400 +++ b/demo/more/dlist.urs Sat Sep 19 13:55:37 2009 -0400 @@ -13,6 +13,7 @@ val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type -> (t -> position -> xml (ctx ++ body) [] []) -> {StartPosition : signal (option int), + MaxLength : signal (option int), Filter : t -> signal bool, Sort : signal (option (t -> t -> signal bool)) (* <= *)} -> dlist t
--- a/demo/more/grid.ur Sat Sep 19 13:44:12 2009 -0400 +++ b/demo/more/grid.ur Sat Sep 19 13:55:37 2009 -0400 @@ -217,6 +217,7 @@ </tr></xml> end) {StartPosition = return (Some 1), + MaxLength = return (Some 2), Filter = fn all => row <- signal all.Row; foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]