comparison demo/more/dlist.ur @ 915:5e8b6fa5b48f

Start 'more' demo with dbgrid
author Adam Chlipala <adamc@hcoop.net>
date Tue, 08 Sep 2009 07:48:57 -0400
parents
children 37dd42935dad
comparison
equal deleted inserted replaced
914:782f0b4eea67 915:5e8b6fa5b48f
1 datatype dlist'' t =
2 Nil
3 | Cons of t * source (dlist'' t)
4
5 datatype dlist' t =
6 Empty
7 | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }
8
9 con dlist t = source (dlist' t)
10
11 type position = transaction unit
12
13 fun headPos [t] (dl : dlist t) =
14 dl' <- get dl;
15 case dl' of
16 Nonempty { Head = Cons (_, tl), Tail = tl' } =>
17 cur <- get tl;
18 set dl (case cur of
19 Nil => Empty
20 | _ => Nonempty {Head = cur, Tail = tl'})
21 | _ => return ()
22
23 fun tailPos [t] (cur : source (dlist'' t)) new tail =
24 new' <- get new;
25 set cur new';
26
27 case new' of
28 Nil => set tail cur
29 | _ => return ()
30
31 val create = fn [t] => source Empty
32
33 fun clear [t] (s : dlist t) = set s Empty
34
35 fun append [t] dl v =
36 dl' <- get dl;
37 case dl' of
38 Empty =>
39 tl <- source Nil;
40 tl' <- source tl;
41 set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
42 return (headPos dl)
43
44 | Nonempty {Tail = tl, ...} =>
45 cur <- get tl;
46 new <- source Nil;
47 set cur (Cons (v, new));
48 set tl new;
49 return (tailPos cur new tl)
50
51 fun render [ctx] [ctx ~ body] [t] f dl = <xml>
52 <dyn signal={dl' <- signal dl;
53 return (case dl' of
54 Empty => <xml/>
55 | Nonempty {Head = hd, Tail = tlTop} =>
56 let
57 fun render' prev dl'' =
58 case dl'' of
59 Nil => <xml/>
60 | Cons (v, tl) =>
61 let
62 val pos = case prev of
63 None => headPos dl
64 | Some prev => tailPos prev tl tlTop
65 in
66 <xml>{f v pos}<dyn signal={tl' <- signal tl;
67 return (render' (Some tl) tl')}/></xml>
68 end
69 in
70 render' None hd
71 end)}/>
72 </xml>
73
74 fun delete pos = pos
75
76 fun elements' [t] (dl'' : dlist'' t) =
77 case dl'' of
78 Nil => return []
79 | Cons (x, dl'') =>
80 dl'' <- signal dl'';
81 tl <- elements' dl'';
82 return (x :: tl)
83
84 fun elements [t] (dl : dlist t) =
85 dl' <- signal dl;
86 case dl' of
87 Empty => return []
88 | Nonempty {Head = hd, ...} => elements' hd