Mercurial > urweb

annotate 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
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 val len = Option.mp (fn n => n - 1) len
adamc@963 87 in
adamc@963 88 <xml><dyn signal={b <- filter v;
adamc@963 89 return (if b then
adamc@963 90 f v pos
adamc@963 91 else
adamc@963 92 <xml/>)}/>
adamc@963 93 <dyn signal={tl' <- signal tl;
adamc@963 94 return (render' (Some tl) tl' len)}/></xml>
adamc@963 95 end
adamc@962 96
adamc@962 97 fun skip pos hd =
adamc@962 98 case pos of
adamc@962 99 0 => return hd
adamc@962 100 | _ =>
adamc@962 101 case hd of
adamc@962 102 Nil => return hd
adamc@962 103 | Cons (_, tl) =>
adamc@962 104 tl' <- signal tl;
adamc@962 105 skip (pos-1) tl'
adamc@962 106 in
adamc@962 107 case pos of
adamc@963 108 None => return (render' None hd len)
adamc@962 109 | Some pos =>
adamc@962 110 hd <- skip pos hd;
adamc@963 111 return (render' None hd len)
adamc@962 112 end}/>
adamc@915 113 </xml>
adamc@915 114
adamc@963 115 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter =
adamc@963 116 let
adamc@963 117 fun renderFlat' len ls =
adamc@963 118 case len of
adamc@963 119 Some 0 => <xml/>
adamc@963 120 | _ =>
adamc@963 121 case ls of
adamc@963 122 [] => <xml/>
adamc@963 123 | p :: ls =>
adamc@963 124 let
adamc@963 125 val len =
adamc@963 126 case len of
adamc@963 127 None => None
adamc@963 128 | Some n => Some (n - 1)
adamc@963 129 in
adamc@963 130 <xml>{f p.1 p.2}{renderFlat' len ls}</xml>
adamc@963 131 end
adamc@963 132 in
adamc@963 133 renderFlat'
adamc@963 134 end
adamc@952 135
adamc@953 136 val split [t] =
adamc@953 137 let
adamc@953 138 fun split' acc (ls : list t) =
adamc@953 139 case ls of
adamc@953 140 [] => acc
adamc@953 141 | x1 :: [] => (x1 :: acc.1, acc.2)
adamc@953 142 | x1 :: x2 :: ls => split' (x1 :: acc.1, x2 :: acc.2) ls
adamc@953 143 in
adamc@953 144 split' ([], [])
adamc@953 145 end
adamc@953 146
adamc@953 147 fun merge [t] (cmp : t -> t -> signal bool) =
adamc@953 148 let
adamc@953 149 fun merge' acc (ls1 : list t) (ls2 : list t) =
adamc@953 150 case (ls1, ls2) of
adamc@953 151 ([], _) => return (List.revAppend acc ls2)
adamc@953 152 | (_, []) => return (List.revAppend acc ls1)
adamc@953 153 | (x1 :: ls1', x2 :: ls2') =>
adamc@953 154 b <- cmp x1 x2;
adamc@953 155 if b then
adamc@953 156 merge' (x1 :: acc) ls1' ls2
adamc@953 157 else
adamc@953 158 merge' (x2 :: acc) ls1 ls2'
adamc@953 159 in
adamc@953 160 merge' []
adamc@953 161 end
adamc@953 162
adamc@953 163 fun sort [t] (cmp : t -> t -> signal bool) =
adamc@953 164 let
adamc@953 165 fun sort' (ls : list t) =
adamc@953 166 case ls of
adamc@953 167 [] => return ls
adamc@953 168 | _ :: [] => return ls
adamc@953 169 | _ =>
adamc@953 170 let
adamc@953 171 val (ls1, ls2) = split ls
adamc@953 172 in
adamc@953 173 ls1' <- sort' ls1;
adamc@953 174 ls2' <- sort' ls2;
adamc@953 175 merge cmp ls1' ls2'
adamc@953 176 end
adamc@953 177 in
adamc@953 178 sort'
adamc@953 179 end
adamc@953 180
adamc@953 181 fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
adamc@962 182 Sort : signal (option (t -> t -> signal bool)),
adamc@963 183 StartPosition : signal (option int),
adamc@963 184 MaxLength : signal (option int)}) dl = <xml>
adamc@963 185 <dyn signal={len <- r.MaxLength;
adamc@963 186 cmp <- r.Sort;
adamc@962 187 pos <- r.StartPosition;
adamc@963 188
adamc@953 189 case cmp of
adamc@963 190 None => return (renderDyn f r.Filter pos len dl)
adamc@953 191 | Some cmp =>
adamc@952 192 dl' <- signal dl;
adamc@952 193 elems <- (case dl' of
adamc@952 194 Empty => return []
adamc@952 195 | Nonempty {Head = hd, Tail = tlTop} =>
adamc@952 196 let
adamc@952 197 fun listOut prev dl'' acc =
adamc@952 198 case dl'' of
adamc@952 199 Nil => return acc
adamc@952 200 | Cons (v, tl) =>
adamc@952 201 let
adamc@952 202 val pos = case prev of
adamc@952 203 None => headPos dl
adamc@952 204 | Some prev => tailPos prev tl tlTop
adamc@952 205 in
adamc@958 206 b <- r.Filter v;
adamc@952 207 tl' <- signal tl;
adamc@958 208 listOut (Some tl) tl' (if b then
adamc@958 209 (v, pos) :: acc
adamc@958 210 else
adamc@958 211 acc)
adamc@952 212 end
adamc@952 213 in
adamc@952 214 listOut None hd []
adamc@952 215 end);
adamc@953 216 elems <- sort (fn v1 v2 => cmp v1.1 v2.1) elems;
adamc@962 217 let
adamc@962 218 fun skip n ls =
adamc@962 219 case (n, ls) of
adamc@962 220 (0, _) => ls
adamc@962 221 | (n, _ :: ls) => skip (n-1) ls
adamc@962 222 | (_, []) => []
adamc@962 223
adamc@962 224 val elems =
adamc@962 225 case pos of
adamc@962 226 None => elems
adamc@962 227 | Some pos => skip pos elems
adamc@962 228 in
adamc@963 229 return (renderFlat f r.Filter len elems)
adamc@962 230 end}/>
adamc@952 231 </xml>
adamc@952 232
adamc@915 233 fun delete pos = pos
adamc@915 234
adamc@915 235 fun elements' [t] (dl'' : dlist'' t) =
adamc@915 236 case dl'' of
adamc@915 237 Nil => return []
adamc@915 238 | Cons (x, dl'') =>
adamc@915 239 dl'' <- signal dl'';
adamc@915 240 tl <- elements' dl'';
adamc@915 241 return (x :: tl)
adamc@915 242
adamc@915 243 fun elements [t] (dl : dlist t) =
adamc@951 244 dl' <- signal dl;
adamc@915 245 case dl' of
adamc@915 246 Empty => return []
adamc@915 247 | Nonempty {Head = hd, ...} => elements' hd
adamc@937 248
adamc@937 249 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
adamc@937 250 let
adamc@937 251 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
adamc@937 252 case dl of
adamc@937 253 Nil => return i
adamc@937 254 | Cons (v, dl') =>
adamc@937 255 dl' <- signal dl';
adamc@937 256 i' <- f v i;
adamc@937 257 foldl'' i' dl'
adamc@937 258
adamc@937 259 fun foldl' (i : acc) (dl : dlist t) : signal acc =
adamc@951 260 dl <- signal dl;
adamc@937 261 case dl of
adamc@937 262 Empty => return i
adamc@937 263 | Nonempty {Head = dl, ...} => foldl'' i dl
adamc@937 264 in
adamc@937 265 foldl'
adamc@937 266 end