aboutsummaryrefslogtreecommitdiffhomepage
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-09-19 13:44:12 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-09-19 13:44:12 -0400
commitdf4c988ff8d326d0e6c94d9d31712c3bd3a53eb0 (patch)
treeda7d19f0f8711523ec52bc98419c70d410b0ea69 /demo
parent04b98841de74bdf38e905729a501b34913902db7 (diff)
Testing Dlist StartPosition with constant offset
Diffstat (limited to 'demo')
-rw-r--r--demo/more/dlist.ur87
-rw-r--r--demo/more/dlist.urs3
-rw-r--r--demo/more/grid.ur3
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)]