Mercurial > urweb

comparison demo/more/dlist.ur @ 963:6f9d1565de56

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Testing Dlist MaxLength with constant value
author Adam Chlipala <adamc@hcoop.net>
date Sat, 19 Sep 2009 13:55:37 -0400
parents 7e7edfb6fe82
children fbc3a0eef45a
comparison
equal deleted inserted replaced
962:7e7edfb6fe82 963:6f9d1565de56
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 pos dl = <xml> 69 fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos len dl = <xml>
70 <dyn signal={dl' <- signal dl; 70 <dyn signal={dl' <- signal dl;
71 case dl' of 71 case dl' of
72 Empty => return <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'' len =
76 case dl'' of 76 case len of
77 Nil => <xml/> 77 Some 0 => <xml/>
78 | Cons (v, tl) => 78 | _ =>
79 let 79 case dl'' of
80 val pos = case prev of 80 Nil => <xml/>
81 None => headPos dl 81 | Cons (v, tl) =>
82 | Some prev => tailPos prev tl tlTop 82 let
83 in 83 val pos = case prev of
84 <xml><dyn signal={b <- filter v; 84 None => headPos dl
85 return (if b then 85 | Some prev => tailPos prev tl tlTop
86 f v pos 86 val len = Option.mp (fn n => n - 1) len
87 else 87 in
88 <xml/>)}/> 88 <xml><dyn signal={b <- filter v;
89 <dyn signal={tl' <- signal tl; 89 return (if b then
90 return (render' (Some tl) tl')}/></xml> 90 f v pos
91 end 91 else
92 <xml/>)}/>
93 <dyn signal={tl' <- signal tl;
94 return (render' (Some tl) tl' len)}/></xml>
95 end
92 96
93 fun skip pos hd = 97 fun skip pos hd =
94 case pos of 98 case pos of
95 0 => return hd 99 0 => return hd
96 | _ => 100 | _ =>
99 | Cons (_, tl) => 103 | Cons (_, tl) =>
100 tl' <- signal tl; 104 tl' <- signal tl;
101 skip (pos-1) tl' 105 skip (pos-1) tl'
102 in 106 in
103 case pos of 107 case pos of
104 None => return (render' None hd) 108 None => return (render' None hd len)
105 | Some pos => 109 | Some pos =>
106 hd <- skip pos hd; 110 hd <- skip pos hd;
107 return (render' None hd) 111 return (render' None hd len)
108 end}/> 112 end}/>
109 </xml> 113 </xml>
110 114
111 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls = 115 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter =
112 List.mapX (fn p => f p.1 p.2) ls 116 let
117 fun renderFlat' len ls =
118 case len of
119 Some 0 => <xml/>
120 | _ =>
121 case ls of
122 [] => <xml/>
123 | p :: ls =>
124 let
125 val len =
126 case len of
127 None => None
128 | Some n => Some (n - 1)
129 in
130 <xml>{f p.1 p.2}{renderFlat' len ls}</xml>
131 end
132 in
133 renderFlat'
134 end
113 135
114 val split [t] = 136 val split [t] =
115 let 137 let
116 fun split' acc (ls : list t) = 138 fun split' acc (ls : list t) =
117 case ls of 139 case ls of
156 sort' 178 sort'
157 end 179 end
158 180
159 fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool, 181 fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
160 Sort : signal (option (t -> t -> signal bool)), 182 Sort : signal (option (t -> t -> signal bool)),
161 StartPosition : signal (option int)}) dl = <xml> 183 StartPosition : signal (option int),
162 <dyn signal={cmp <- r.Sort; 184 MaxLength : signal (option int)}) dl = <xml>
185 <dyn signal={len <- r.MaxLength;
186 cmp <- r.Sort;
163 pos <- r.StartPosition; 187 pos <- r.StartPosition;
188
164 case cmp of 189 case cmp of
165 None => return (renderDyn f r.Filter pos dl) 190 None => return (renderDyn f r.Filter pos len dl)
166 | Some cmp => 191 | Some cmp =>
167 dl' <- signal dl; 192 dl' <- signal dl;
168 elems <- (case dl' of 193 elems <- (case dl' of
169 Empty => return [] 194 Empty => return []
170 | Nonempty {Head = hd, Tail = tlTop} => 195 | Nonempty {Head = hd, Tail = tlTop} =>
199 val elems = 224 val elems =
200 case pos of 225 case pos of
201 None => elems 226 None => elems
202 | Some pos => skip pos elems 227 | Some pos => skip pos elems
203 in 228 in
204 return (renderFlat f r.Filter elems) 229 return (renderFlat f r.Filter len elems)
205 end}/> 230 end}/>
206 </xml> 231 </xml>
207 232
208 fun delete pos = pos 233 fun delete pos = pos
209 234