Mercurial > urweb
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 |