diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-09-19 13:44:12 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-09-19 13:44:12 -0400 |
commit | df4c988ff8d326d0e6c94d9d31712c3bd3a53eb0 (patch) | |
tree | da7d19f0f8711523ec52bc98419c70d410b0ea69 /demo/more | |
parent | 04b98841de74bdf38e905729a501b34913902db7 (diff) |
Testing Dlist StartPosition with constant offset
Diffstat (limited to 'demo/more')
-rw-r--r-- | demo/more/dlist.ur | 87 | ||||
-rw-r--r-- | demo/more/dlist.urs | 3 | ||||
-rw-r--r-- | demo/more/grid.ur | 3 |
3 files changed, 61 insertions, 32 deletions
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur index 3d2cb49e..3bec8077 100644 --- a/demo/more/dlist.ur +++ b/demo/more/dlist.ur @@ -66,32 +66,46 @@ 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 dl = <xml> +fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos dl = <xml> <dyn signal={dl' <- signal dl; - return (case dl' of - Empty => <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 - in - render' None hd - end)}/> + 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 skip pos hd = + case pos of + 0 => return hd + | _ => + case hd of + Nil => return hd + | Cons (_, tl) => + tl' <- signal tl; + skip (pos-1) tl' + in + case pos of + None => return (render' None hd) + | Some pos => + hd <- skip pos hd; + return (render' None hd) + end}/> </xml> fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls = @@ -143,10 +157,12 @@ fun sort [t] (cmp : t -> t -> signal bool) = end fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool, - Sort : signal (option (t -> t -> signal bool))}) dl = <xml> + Sort : signal (option (t -> t -> signal bool)), + StartPosition : signal (option int)}) dl = <xml> <dyn signal={cmp <- r.Sort; + pos <- r.StartPosition; case cmp of - None => return (renderDyn f r.Filter dl) + None => return (renderDyn f r.Filter pos dl) | Some cmp => dl' <- signal dl; elems <- (case dl' of @@ -173,10 +189,21 @@ fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool, listOut None hd [] end); elems <- sort (fn v1 v2 => cmp v1.1 v2.1) elems; - return (renderFlat f r.Filter elems)}/> + let + fun skip n ls = + case (n, ls) of + (0, _) => ls + | (n, _ :: ls) => skip (n-1) ls + | (_, []) => [] + + val elems = + case pos of + None => elems + | Some pos => skip pos elems + in + return (renderFlat f r.Filter elems) + end}/> </xml> - - fun delete pos = pos diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs index b25e41a1..cd42f9ee 100644 --- a/demo/more/dlist.urs +++ b/demo/more/dlist.urs @@ -12,7 +12,8 @@ val foldl : t ::: Type -> acc ::: Type -> (t -> acc -> signal acc) -> acc -> dli val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type -> (t -> position -> xml (ctx ++ body) [] []) - -> {Filter : t -> signal bool, + -> {StartPosition : signal (option int), + Filter : t -> signal bool, Sort : signal (option (t -> t -> signal bool)) (* <= *)} -> dlist t -> xml (ctx ++ body) [] [] diff --git a/demo/more/grid.ur b/demo/more/grid.ur index 7cd16d72..dbaca7db 100644 --- a/demo/more/grid.ur +++ b/demo/more/grid.ur @@ -216,7 +216,8 @@ functor Make(M : sig [_] M.folder grid.Cols M.cols cols)}/> </tr></xml> end) - {Filter = fn all => + {StartPosition = return (Some 1), + Filter = fn all => row <- signal all.Row; foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool] (fn [nm :: Name] [p :: (Type * Type * Type)] |