Mercurial > urweb

annotate demo/more/dlist.ur @ 995:166ea3944b91

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Versioned1 demo working
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Oct 2009 17:36:45 -0400
parents c2fe1dbaceb9
children f0afe61a6f8b
rev   line source
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@954 51 fun replace [t] dl ls =
adamc@954 52 case ls of
adamc@954 53 [] => set dl Empty
adamc@954 54 | x :: ls =>
adamc@954 55 tl <- source Nil;
adamc@954 56 let
adamc@954 57 fun build ls acc =
adamc@954 58 case ls of
adamc@954 59 [] => return acc
adamc@954 60 | x :: ls =>
adamc@957 61 this <- source (Cons (x, acc));
adamc@954 62 build ls this
adamc@954 63 in
adamc@954 64 hd <- build (List.rev ls) tl;
adamc@954 65 tlS <- source tl;
adamc@954 66 set dl (Nonempty {Head = Cons (x, hd), Tail = tlS})
adamc@954 67 end
adamc@954 68
adamc@963 69 fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos len dl = <xml>
adamc@951 70 <dyn signal={dl' <- signal dl;
adamc@962 71 case dl' of
adamc@962 72 Empty => return <xml/>
adamc@962 73 | Nonempty {Head = hd, Tail = tlTop} =>
adamc@962 74 let
adamc@963 75 fun render' prev dl'' len =
adamc@963 76 case len of
adamc@963 77 Some 0 => <xml/>
adamc@963 78 | _ =>
adamc@963 79 case dl'' of
adamc@963 80 Nil => <xml/>
adamc@963 81 | Cons (v, tl) =>
adamc@963 82 let
adamc@963 83 val pos = case prev of
adamc@963 84 None => headPos dl
adamc@963 85 | Some prev => tailPos prev tl tlTop
adamc@963 86 in
adamc@966 87 <xml>
adamc@966 88 <dyn signal={b <- filter v;
adamc@966 89 return <xml>
adamc@966 90 {if b then
adamc@966 91 f v pos
adamc@966 92 else
adamc@966 93 <xml/>}
adamc@966 94 <dyn signal={tl' <- signal tl;
adamc@966 95 return (render' (Some tl) tl'
adamc@966 96 (if b then
adamc@966 97 Option.mp (fn n => n - 1) len
adamc@966 98 else
adamc@966 99 len))}/>
adamc@966 100 </xml>}/>
adamc@966 101 </xml>
adamc@963 102 end
adamc@962 103
adamc@962 104 fun skip pos hd =
adamc@962 105 case pos of
adamc@962 106 0 => return hd
adamc@962 107 | _ =>
adamc@962 108 case hd of
adamc@962 109 Nil => return hd
adamc@962 110 | Cons (_, tl) =>
adamc@962 111 tl' <- signal tl;
adamc@962 112 skip (pos-1) tl'
adamc@962 113 in
adamc@962 114 case pos of
adamc@963 115 None => return (render' None hd len)
adamc@962 116 | Some pos =>
adamc@962 117 hd <- skip pos hd;
adamc@963 118 return (render' None hd len)
adamc@962 119 end}/>
adamc@915 120 </xml>
adamc@915 121
adamc@963 122 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter =
adamc@963 123 let
adamc@963 124 fun renderFlat' len ls =
adamc@963 125 case len of
adamc@963 126 Some 0 => <xml/>
adamc@963 127 | _ =>
adamc@963 128 case ls of
adamc@963 129 [] => <xml/>
adamc@963 130 | p :: ls =>
adamc@963 131 let
adamc@963 132 val len =
adamc@963 133 case len of
adamc@963 134 None => None
adamc@963 135 | Some n => Some (n - 1)
adamc@963 136 in
adamc@963 137 <xml>{f p.1 p.2}{renderFlat' len ls}</xml>
adamc@963 138 end
adamc@963 139 in
adamc@963 140 renderFlat'
adamc@963 141 end
adamc@952 142
adamc@953 143 val split [t] =
adamc@953 144 let
adamc@953 145 fun split' acc (ls : list t) =
adamc@953 146 case ls of
adamc@953 147 [] => acc
adamc@953 148 | x1 :: [] => (x1 :: acc.1, acc.2)
adamc@953 149 | x1 :: x2 :: ls => split' (x1 :: acc.1, x2 :: acc.2) ls
adamc@953 150 in
adamc@953 151 split' ([], [])
adamc@953 152 end
adamc@953 153
adamc@953 154 fun merge [t] (cmp : t -> t -> signal bool) =
adamc@953 155 let
adamc@953 156 fun merge' acc (ls1 : list t) (ls2 : list t) =
adamc@953 157 case (ls1, ls2) of
adamc@953 158 ([], _) => return (List.revAppend acc ls2)
adamc@953 159 | (_, []) => return (List.revAppend acc ls1)
adamc@953 160 | (x1 :: ls1', x2 :: ls2') =>
adamc@953 161 b <- cmp x1 x2;
adamc@953 162 if b then
adamc@953 163 merge' (x1 :: acc) ls1' ls2
adamc@953 164 else
adamc@953 165 merge' (x2 :: acc) ls1 ls2'
adamc@953 166 in
adamc@953 167 merge' []
adamc@953 168 end
adamc@953 169
adamc@953 170 fun sort [t] (cmp : t -> t -> signal bool) =
adamc@953 171 let
adamc@953 172 fun sort' (ls : list t) =
adamc@953 173 case ls of
adamc@953 174 [] => return ls
adamc@953 175 | _ :: [] => return ls
adamc@953 176 | _ =>
adamc@953 177 let
adamc@953 178 val (ls1, ls2) = split ls
adamc@953 179 in
adamc@953 180 ls1' <- sort' ls1;
adamc@953 181 ls2' <- sort' ls2;
adamc@953 182 merge cmp ls1' ls2'
adamc@953 183 end
adamc@953 184 in
adamc@953 185 sort'
adamc@953 186 end
adamc@953 187
adamc@953 188 fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
adamc@962 189 Sort : signal (option (t -> t -> signal bool)),
adamc@963 190 StartPosition : signal (option int),
adamc@963 191 MaxLength : signal (option int)}) dl = <xml>
adamc@963 192 <dyn signal={len <- r.MaxLength;
adamc@963 193 cmp <- r.Sort;
adamc@962 194 pos <- r.StartPosition;
adamc@963 195
adamc@953 196 case cmp of
adamc@963 197 None => return (renderDyn f r.Filter pos len dl)
adamc@953 198 | Some cmp =>
adamc@952 199 dl' <- signal dl;
adamc@952 200 elems <- (case dl' of
adamc@952 201 Empty => return []
adamc@952 202 | Nonempty {Head = hd, Tail = tlTop} =>
adamc@952 203 let
adamc@952 204 fun listOut prev dl'' acc =
adamc@952 205 case dl'' of
adamc@952 206 Nil => return acc
adamc@952 207 | Cons (v, tl) =>
adamc@952 208 let
adamc@952 209 val pos = case prev of
adamc@952 210 None => headPos dl
adamc@952 211 | Some prev => tailPos prev tl tlTop
adamc@952 212 in
adamc@958 213 b <- r.Filter v;
adamc@952 214 tl' <- signal tl;
adamc@958 215 listOut (Some tl) tl' (if b then
adamc@958 216 (v, pos) :: acc
adamc@958 217 else
adamc@958 218 acc)
adamc@952 219 end
adamc@952 220 in
adamc@952 221 listOut None hd []
adamc@952 222 end);
adamc@953 223 elems <- sort (fn v1 v2 => cmp v1.1 v2.1) elems;
adamc@962 224 let
adamc@962 225 fun skip n ls =
adamc@962 226 case (n, ls) of
adamc@962 227 (0, _) => ls
adamc@962 228 | (n, _ :: ls) => skip (n-1) ls
adamc@962 229 | (_, []) => []
adamc@962 230
adamc@962 231 val elems =
adamc@962 232 case pos of
adamc@962 233 None => elems
adamc@962 234 | Some pos => skip pos elems
adamc@962 235 in
adamc@963 236 return (renderFlat f r.Filter len elems)
adamc@962 237 end}/>
adamc@952 238 </xml>
adamc@952 239
adamc@915 240 fun delete pos = pos
adamc@915 241
adamc@915 242 fun elements' [t] (dl'' : dlist'' t) =
adamc@915 243 case dl'' of
adamc@915 244 Nil => return []
adamc@915 245 | Cons (x, dl'') =>
adamc@915 246 dl'' <- signal dl'';
adamc@915 247 tl <- elements' dl'';
adamc@915 248 return (x :: tl)
adamc@915 249
adamc@915 250 fun elements [t] (dl : dlist t) =
adamc@951 251 dl' <- signal dl;
adamc@915 252 case dl' of
adamc@915 253 Empty => return []
adamc@915 254 | Nonempty {Head = hd, ...} => elements' hd
adamc@937 255
adamc@964 256 fun size' [t] (dl'' : dlist'' t) =
adamc@964 257 case dl'' of
adamc@964 258 Nil => return 0
adamc@964 259 | Cons (x, dl'') =>
adamc@964 260 dl'' <- signal dl'';
adamc@964 261 n <- size' dl'';
adamc@964 262 return (n + 1)
adamc@964 263
adamc@964 264 fun size [t] (dl : dlist t) =
adamc@964 265 dl' <- signal dl;
adamc@964 266 case dl' of
adamc@964 267 Empty => return 0
adamc@964 268 | Nonempty {Head = hd, ...} => size' hd
adamc@964 269
adamc@965 270 fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) =
adamc@965 271 case dl'' of
adamc@965 272 Nil => return 0
adamc@965 273 | Cons (x, dl'') =>
adamc@965 274 b <- f x;
adamc@965 275 dl'' <- signal dl'';
adamc@965 276 n <- numPassing' f dl'';
adamc@965 277 return (if b then n + 1 else n)
adamc@965 278
adamc@965 279 fun numPassing [t] (f : t -> signal bool) (dl : dlist t) =
adamc@965 280 dl' <- signal dl;
adamc@965 281 case dl' of
adamc@965 282 Empty => return 0
adamc@965 283 | Nonempty {Head = hd, ...} => numPassing' f hd
adamc@965 284
adamc@937 285 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
adamc@937 286 let
adamc@937 287 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
adamc@937 288 case dl of
adamc@937 289 Nil => return i
adamc@937 290 | Cons (v, dl') =>
adamc@937 291 dl' <- signal dl';
adamc@937 292 i' <- f v i;
adamc@937 293 foldl'' i' dl'
adamc@937 294
adamc@937 295 fun foldl' (i : acc) (dl : dlist t) : signal acc =
adamc@951 296 dl <- signal dl;
adamc@937 297 case dl of
adamc@937 298 Empty => return i
adamc@937 299 | Nonempty {Head = dl, ...} => foldl'' i dl
adamc@937 300 in
adamc@937 301 foldl'
adamc@937 302 end