Mercurial > urweb

annotate demo/more/dlist.ur @ 2117:f1c4edf0a655

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New release
author Adam Chlipala <adam@chlipala.net>
date Sat, 14 Feb 2015 08:17:36 -0500
parents 68429cfce8db
children
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
adam@1641 69 fun renderDyn [ctx] [ctx ~ [Dyn]] [t] (f : t -> position -> xml (ctx ++ [Dyn]) [] []) 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
adam@1641 122 fun renderFlat [ctx] [ctx ~ [Dyn]] [t] (f : t -> position -> xml (ctx ++ [Dyn]) [] [])
adam@1641 123 : option int -> list (t * position) -> xml (ctx ++ [Dyn]) [] [] =
adamc@963 124 let
adamc@963 125 fun renderFlat' len ls =
adamc@963 126 case len of
adamc@963 127 Some 0 => <xml/>
adamc@963 128 | _ =>
adamc@963 129 case ls of
adamc@963 130 [] => <xml/>
adamc@963 131 | p :: ls =>
adamc@963 132 let
adamc@963 133 val len =
adamc@963 134 case len of
adamc@963 135 None => None
adamc@963 136 | Some n => Some (n - 1)
adamc@963 137 in
adamc@963 138 <xml>{f p.1 p.2}{renderFlat' len ls}</xml>
adamc@963 139 end
adamc@963 140 in
adamc@963 141 renderFlat'
adamc@963 142 end
adamc@952 143
adamc@953 144 val split [t] =
adamc@953 145 let
adamc@953 146 fun split' acc (ls : list t) =
adamc@953 147 case ls of
adamc@953 148 [] => acc
adamc@953 149 | x1 :: [] => (x1 :: acc.1, acc.2)
adamc@953 150 | x1 :: x2 :: ls => split' (x1 :: acc.1, x2 :: acc.2) ls
adamc@953 151 in
adamc@953 152 split' ([], [])
adamc@953 153 end
adamc@953 154
adamc@953 155 fun merge [t] (cmp : t -> t -> signal bool) =
adamc@953 156 let
adamc@953 157 fun merge' acc (ls1 : list t) (ls2 : list t) =
adamc@953 158 case (ls1, ls2) of
adamc@953 159 ([], _) => return (List.revAppend acc ls2)
adamc@953 160 | (_, []) => return (List.revAppend acc ls1)
adamc@953 161 | (x1 :: ls1', x2 :: ls2') =>
adamc@953 162 b <- cmp x1 x2;
adamc@953 163 if b then
adamc@953 164 merge' (x1 :: acc) ls1' ls2
adamc@953 165 else
adamc@953 166 merge' (x2 :: acc) ls1 ls2'
adamc@953 167 in
adamc@953 168 merge' []
adamc@953 169 end
adamc@953 170
adamc@953 171 fun sort [t] (cmp : t -> t -> signal bool) =
adamc@953 172 let
adamc@953 173 fun sort' (ls : list t) =
adamc@953 174 case ls of
adamc@953 175 [] => return ls
adamc@953 176 | _ :: [] => return ls
adamc@953 177 | _ =>
adamc@953 178 let
adamc@953 179 val (ls1, ls2) = split ls
adamc@953 180 in
adamc@953 181 ls1' <- sort' ls1;
adamc@953 182 ls2' <- sort' ls2;
adamc@953 183 merge cmp ls1' ls2'
adamc@953 184 end
adamc@953 185 in
adamc@953 186 sort'
adamc@953 187 end
adamc@953 188
adam@1641 189 fun render [ctx] [ctx ~ [Dyn]] [t] f (r : {Filter : t -> signal bool,
adam@1641 190 Sort : signal (option (t -> t -> signal bool)),
adam@1641 191 StartPosition : signal (option int),
adam@1641 192 MaxLength : signal (option int)}) dl = <xml>
adamc@963 193 <dyn signal={len <- r.MaxLength;
adamc@963 194 cmp <- r.Sort;
adamc@962 195 pos <- r.StartPosition;
adamc@963 196
adamc@953 197 case cmp of
adamc@963 198 None => return (renderDyn f r.Filter pos len dl)
adamc@953 199 | Some cmp =>
adamc@952 200 dl' <- signal dl;
adamc@952 201 elems <- (case dl' of
adamc@952 202 Empty => return []
adamc@952 203 | Nonempty {Head = hd, Tail = tlTop} =>
adamc@952 204 let
adamc@952 205 fun listOut prev dl'' acc =
adamc@952 206 case dl'' of
adamc@952 207 Nil => return acc
adamc@952 208 | Cons (v, tl) =>
adamc@952 209 let
adamc@952 210 val pos = case prev of
adamc@952 211 None => headPos dl
adamc@952 212 | Some prev => tailPos prev tl tlTop
adamc@952 213 in
adamc@958 214 b <- r.Filter v;
adamc@952 215 tl' <- signal tl;
adamc@958 216 listOut (Some tl) tl' (if b then
adamc@958 217 (v, pos) :: acc
adamc@958 218 else
adamc@958 219 acc)
adamc@952 220 end
adamc@952 221 in
adamc@952 222 listOut None hd []
adamc@952 223 end);
adamc@953 224 elems <- sort (fn v1 v2 => cmp v1.1 v2.1) elems;
adamc@962 225 let
adamc@962 226 fun skip n ls =
adamc@962 227 case (n, ls) of
adamc@962 228 (0, _) => ls
adamc@962 229 | (n, _ :: ls) => skip (n-1) ls
adamc@962 230 | (_, []) => []
adamc@962 231
adamc@962 232 val elems =
adamc@962 233 case pos of
adamc@962 234 None => elems
adamc@962 235 | Some pos => skip pos elems
adamc@962 236 in
adam@1304 237 return (renderFlat f len elems)
adamc@962 238 end}/>
adamc@952 239 </xml>
adamc@952 240
adamc@915 241 fun delete pos = pos
adamc@915 242
adam@1304 243 fun elements' [t] (dl'' : dlist'' t) : signal (list t) =
adamc@915 244 case dl'' of
adamc@915 245 Nil => return []
adamc@915 246 | Cons (x, dl'') =>
adamc@915 247 dl'' <- signal dl'';
adamc@915 248 tl <- elements' dl'';
adamc@915 249 return (x :: tl)
adamc@915 250
adam@1304 251 fun elements [t] (dl : dlist t) : signal (list t) =
adamc@951 252 dl' <- signal dl;
adamc@915 253 case dl' of
adamc@915 254 Empty => return []
adamc@915 255 | Nonempty {Head = hd, ...} => elements' hd
adamc@937 256
adam@1304 257 fun size' [t] (dl'' : dlist'' t) : signal int =
adamc@964 258 case dl'' of
adamc@964 259 Nil => return 0
adamc@964 260 | Cons (x, dl'') =>
adamc@964 261 dl'' <- signal dl'';
adamc@964 262 n <- size' dl'';
adamc@964 263 return (n + 1)
adamc@964 264
adam@1304 265 fun size [t] (dl : dlist t) : signal int =
adamc@964 266 dl' <- signal dl;
adamc@964 267 case dl' of
adamc@964 268 Empty => return 0
adamc@964 269 | Nonempty {Head = hd, ...} => size' hd
adamc@964 270
adam@1304 271 fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) : signal int =
adamc@965 272 case dl'' of
adamc@965 273 Nil => return 0
adamc@965 274 | Cons (x, dl'') =>
adamc@965 275 b <- f x;
adamc@965 276 dl'' <- signal dl'';
adamc@965 277 n <- numPassing' f dl'';
adamc@965 278 return (if b then n + 1 else n)
adamc@965 279
adam@1304 280 fun numPassing [t] (f : t -> signal bool) (dl : dlist t) : signal int =
adamc@965 281 dl' <- signal dl;
adamc@965 282 case dl' of
adamc@965 283 Empty => return 0
adamc@965 284 | Nonempty {Head = hd, ...} => numPassing' f hd
adamc@965 285
adamc@937 286 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
adamc@937 287 let
adamc@937 288 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
adamc@937 289 case dl of
adamc@937 290 Nil => return i
adamc@937 291 | Cons (v, dl') =>
adamc@937 292 dl' <- signal dl';
adamc@937 293 i' <- f v i;
adamc@937 294 foldl'' i' dl'
adamc@937 295
adamc@937 296 fun foldl' (i : acc) (dl : dlist t) : signal acc =
adamc@951 297 dl <- signal dl;
adamc@937 298 case dl of
adamc@937 299 Empty => return i
adamc@937 300 | Nonempty {Head = dl, ...} => foldl'' i dl
adamc@937 301 in
adamc@937 302 foldl'
adamc@937 303 end