adamc@915
|
1 datatype dlist'' t =
|
adamc@915
|
2 Nil
|
adamc@915
|
3 | Cons of t * source (dlist'' t)
|
adamc@915
|
4
|
adamc@915
|
5 datatype dlist' t =
|
adamc@915
|
6 Empty
|
adamc@915
|
7 | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }
|
adamc@915
|
8
|
adamc@951
|
9 con dlist t = source (dlist' t)
|
adamc@915
|
10
|
adamc@915
|
11 type position = transaction unit
|
adamc@915
|
12
|
adamc@915
|
13 fun headPos [t] (dl : dlist t) =
|
adamc@951
|
14 dl' <- get dl;
|
adamc@915
|
15 case dl' of
|
adamc@915
|
16 Nonempty { Head = Cons (_, tl), Tail = tl' } =>
|
adamc@915
|
17 cur <- get tl;
|
adamc@951
|
18 set dl (case cur of
|
adamc@951
|
19 Nil => Empty
|
adamc@951
|
20 | _ => Nonempty {Head = cur, Tail = tl'})
|
adamc@915
|
21 | _ => return ()
|
adamc@915
|
22
|
adamc@915
|
23 fun tailPos [t] (cur : source (dlist'' t)) new tail =
|
adamc@915
|
24 new' <- get new;
|
adamc@915
|
25 set cur new';
|
adamc@915
|
26
|
adamc@915
|
27 case new' of
|
adamc@915
|
28 Nil => set tail cur
|
adamc@915
|
29 | _ => return ()
|
adamc@915
|
30
|
adamc@951
|
31 val create [t] = source Empty
|
adamc@915
|
32
|
adamc@951
|
33 fun clear [t] (s : dlist t) = set s Empty
|
adamc@915
|
34
|
adamc@915
|
35 fun append [t] dl v =
|
adamc@951
|
36 dl' <- get dl;
|
adamc@915
|
37 case dl' of
|
adamc@915
|
38 Empty =>
|
adamc@915
|
39 tl <- source Nil;
|
adamc@915
|
40 tl' <- source tl;
|
adamc@951
|
41 set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
|
adamc@915
|
42 return (headPos dl)
|
adamc@915
|
43
|
adamc@915
|
44 | Nonempty {Tail = tl, ...} =>
|
adamc@915
|
45 cur <- get tl;
|
adamc@915
|
46 new <- source Nil;
|
adamc@915
|
47 set cur (Cons (v, new));
|
adamc@915
|
48 set tl new;
|
adamc@915
|
49 return (tailPos cur new tl)
|
adamc@915
|
50
|
adamc@951
|
51 fun render [ctx] [ctx ~ body] [t] f {Filter = filter, ...} dl = <xml>
|
adamc@951
|
52 <dyn signal={dl' <- signal dl;
|
adamc@915
|
53 return (case dl' of
|
adamc@915
|
54 Empty => <xml/>
|
adamc@915
|
55 | Nonempty {Head = hd, Tail = tlTop} =>
|
adamc@915
|
56 let
|
adamc@915
|
57 fun render' prev dl'' =
|
adamc@915
|
58 case dl'' of
|
adamc@915
|
59 Nil => <xml/>
|
adamc@915
|
60 | Cons (v, tl) =>
|
adamc@915
|
61 let
|
adamc@915
|
62 val pos = case prev of
|
adamc@915
|
63 None => headPos dl
|
adamc@915
|
64 | Some prev => tailPos prev tl tlTop
|
adamc@915
|
65 in
|
adamc@951
|
66 <xml><dyn signal={b <- filter v;
|
adamc@944
|
67 return (if b then
|
adamc@944
|
68 f v pos
|
adamc@944
|
69 else
|
adamc@944
|
70 <xml/>)}/>
|
adamc@944
|
71 <dyn signal={tl' <- signal tl;
|
adamc@944
|
72 return (render' (Some tl) tl')}/></xml>
|
adamc@915
|
73 end
|
adamc@915
|
74 in
|
adamc@915
|
75 render' None hd
|
adamc@915
|
76 end)}/>
|
adamc@915
|
77 </xml>
|
adamc@915
|
78
|
adamc@915
|
79 fun delete pos = pos
|
adamc@915
|
80
|
adamc@915
|
81 fun elements' [t] (dl'' : dlist'' t) =
|
adamc@915
|
82 case dl'' of
|
adamc@915
|
83 Nil => return []
|
adamc@915
|
84 | Cons (x, dl'') =>
|
adamc@915
|
85 dl'' <- signal dl'';
|
adamc@915
|
86 tl <- elements' dl'';
|
adamc@915
|
87 return (x :: tl)
|
adamc@915
|
88
|
adamc@915
|
89 fun elements [t] (dl : dlist t) =
|
adamc@951
|
90 dl' <- signal dl;
|
adamc@915
|
91 case dl' of
|
adamc@915
|
92 Empty => return []
|
adamc@915
|
93 | Nonempty {Head = hd, ...} => elements' hd
|
adamc@937
|
94
|
adamc@937
|
95 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
|
adamc@937
|
96 let
|
adamc@937
|
97 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
|
adamc@937
|
98 case dl of
|
adamc@937
|
99 Nil => return i
|
adamc@937
|
100 | Cons (v, dl') =>
|
adamc@937
|
101 dl' <- signal dl';
|
adamc@937
|
102 i' <- f v i;
|
adamc@937
|
103 foldl'' i' dl'
|
adamc@937
|
104
|
adamc@937
|
105 fun foldl' (i : acc) (dl : dlist t) : signal acc =
|
adamc@951
|
106 dl <- signal dl;
|
adamc@937
|
107 case dl of
|
adamc@937
|
108 Empty => return i
|
adamc@937
|
109 | Nonempty {Head = dl, ...} => foldl'' i dl
|
adamc@937
|
110 in
|
adamc@937
|
111 foldl'
|
adamc@937
|
112 end
|