comparison demo/more/dlist.ur @ 962:7e7edfb6fe82

Testing Dlist StartPosition with constant offset
author Adam Chlipala <adamc@hcoop.net>
date Sat, 19 Sep 2009 13:44:12 -0400
parents 3aaac251a5af
children 6f9d1565de56
comparison
equal deleted inserted replaced
961:8c37699de273 962:7e7edfb6fe82
64 hd <- build (List.rev ls) tl; 64 hd <- build (List.rev ls) tl;
65 tlS <- source tl; 65 tlS <- source tl;
66 set dl (Nonempty {Head = Cons (x, hd), Tail = tlS}) 66 set dl (Nonempty {Head = Cons (x, hd), Tail = tlS})
67 end 67 end
68 68
69 fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter dl = <xml> 69 fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos dl = <xml>
70 <dyn signal={dl' <- signal dl; 70 <dyn signal={dl' <- signal dl;
71 return (case dl' of 71 case dl' of
72 Empty => <xml/> 72 Empty => return <xml/>
73 | Nonempty {Head = hd, Tail = tlTop} => 73 | Nonempty {Head = hd, Tail = tlTop} =>
74 let 74 let
75 fun render' prev dl'' = 75 fun render' prev dl'' =
76 case dl'' of 76 case dl'' of
77 Nil => <xml/> 77 Nil => <xml/>
78 | Cons (v, tl) => 78 | Cons (v, tl) =>
79 let 79 let
80 val pos = case prev of 80 val pos = case prev of
81 None => headPos dl 81 None => headPos dl
82 | Some prev => tailPos prev tl tlTop 82 | Some prev => tailPos prev tl tlTop
83 in 83 in
84 <xml><dyn signal={b <- filter v; 84 <xml><dyn signal={b <- filter v;
85 return (if b then 85 return (if b then
86 f v pos 86 f v pos
87 else 87 else
88 <xml/>)}/> 88 <xml/>)}/>
89 <dyn signal={tl' <- signal tl; 89 <dyn signal={tl' <- signal tl;
90 return (render' (Some tl) tl')}/></xml> 90 return (render' (Some tl) tl')}/></xml>
91 end 91 end
92 in 92
93 render' None hd 93 fun skip pos hd =
94 end)}/> 94 case pos of
95 0 => return hd
96 | _ =>
97 case hd of
98 Nil => return hd
99 | Cons (_, tl) =>
100 tl' <- signal tl;
101 skip (pos-1) tl'
102 in
103 case pos of
104 None => return (render' None hd)
105 | Some pos =>
106 hd <- skip pos hd;
107 return (render' None hd)
108 end}/>
95 </xml> 109 </xml>
96 110
97 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls = 111 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls =
98 List.mapX (fn p => f p.1 p.2) ls 112 List.mapX (fn p => f p.1 p.2) ls
99 113
141 in 155 in
142 sort' 156 sort'
143 end 157 end
144 158
145 fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool, 159 fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
146 Sort : signal (option (t -> t -> signal bool))}) dl = <xml> 160 Sort : signal (option (t -> t -> signal bool)),
161 StartPosition : signal (option int)}) dl = <xml>
147 <dyn signal={cmp <- r.Sort; 162 <dyn signal={cmp <- r.Sort;
163 pos <- r.StartPosition;
148 case cmp of 164 case cmp of
149 None => return (renderDyn f r.Filter dl) 165 None => return (renderDyn f r.Filter pos dl)
150 | Some cmp => 166 | Some cmp =>
151 dl' <- signal dl; 167 dl' <- signal dl;
152 elems <- (case dl' of 168 elems <- (case dl' of
153 Empty => return [] 169 Empty => return []
154 | Nonempty {Head = hd, Tail = tlTop} => 170 | Nonempty {Head = hd, Tail = tlTop} =>
171 end 187 end
172 in 188 in
173 listOut None hd [] 189 listOut None hd []
174 end); 190 end);
175 elems <- sort (fn v1 v2 => cmp v1.1 v2.1) elems; 191 elems <- sort (fn v1 v2 => cmp v1.1 v2.1) elems;
176 return (renderFlat f r.Filter elems)}/> 192 let
193 fun skip n ls =
194 case (n, ls) of
195 (0, _) => ls
196 | (n, _ :: ls) => skip (n-1) ls
197 | (_, []) => []
198
199 val elems =
200 case pos of
201 None => elems
202 | Some pos => skip pos elems
203 in
204 return (renderFlat f r.Filter elems)
205 end}/>
177 </xml> 206 </xml>
178
179
180 207
181 fun delete pos = pos 208 fun delete pos = pos
182 209
183 fun elements' [t] (dl'' : dlist'' t) = 210 fun elements' [t] (dl'' : dlist'' t) =
184 case dl'' of 211 case dl'' of