Mercurial > urweb

annotate demo/more/dlist.ur @ 1841:184d00f7be74

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add more HTML singleton tags, anticipating that others may make them available via the FFI
author Adam Chlipala <adam@chlipala.net>
date Mon, 31 Dec 2012 09:04:35 -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