Mercurial > urweb

annotate demo/more/dlist.ur @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
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