Mercurial > urweb

annotate demo/more/dlist.ur @ 962:7e7edfb6fe82

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Testing Dlist StartPosition with constant offset
author Adam Chlipala <adamc@hcoop.net>
date Sat, 19 Sep 2009 13:44:12 -0400
parents 3aaac251a5af
children 6f9d1565de56
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@962 69 fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos 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@962 75 fun render' prev dl'' =
adamc@962 76 case dl'' of
adamc@962 77 Nil => <xml/>
adamc@962 78 | Cons (v, tl) =>
adamc@962 79 let
adamc@962 80 val pos = case prev of
adamc@962 81 None => headPos dl
adamc@962 82 | Some prev => tailPos prev tl tlTop
adamc@962 83 in
adamc@962 84 <xml><dyn signal={b <- filter v;
adamc@962 85 return (if b then
adamc@962 86 f v pos
adamc@962 87 else
adamc@962 88 <xml/>)}/>
adamc@962 89 <dyn signal={tl' <- signal tl;
adamc@962 90 return (render' (Some tl) tl')}/></xml>
adamc@962 91 end
adamc@962 92
adamc@962 93 fun skip pos hd =
adamc@962 94 case pos of
adamc@962 95 0 => return hd
adamc@962 96 | _ =>
adamc@962 97 case hd of
adamc@962 98 Nil => return hd
adamc@962 99 | Cons (_, tl) =>
adamc@962 100 tl' <- signal tl;
adamc@962 101 skip (pos-1) tl'
adamc@962 102 in
adamc@962 103 case pos of
adamc@962 104 None => return (render' None hd)
adamc@962 105 | Some pos =>
adamc@962 106 hd <- skip pos hd;
adamc@962 107 return (render' None hd)
adamc@962 108 end}/>
adamc@915 109 </xml>
adamc@915 110
adamc@952 111 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls =
adamc@952 112 List.mapX (fn p => f p.1 p.2) ls
adamc@952 113
adamc@953 114 val split [t] =
adamc@953 115 let
adamc@953 116 fun split' acc (ls : list t) =
adamc@953 117 case ls of
adamc@953 118 [] => acc
adamc@953 119 | x1 :: [] => (x1 :: acc.1, acc.2)
adamc@953 120 | x1 :: x2 :: ls => split' (x1 :: acc.1, x2 :: acc.2) ls
adamc@953 121 in
adamc@953 122 split' ([], [])
adamc@953 123 end
adamc@953 124
adamc@953 125 fun merge [t] (cmp : t -> t -> signal bool) =
adamc@953 126 let
adamc@953 127 fun merge' acc (ls1 : list t) (ls2 : list t) =
adamc@953 128 case (ls1, ls2) of
adamc@953 129 ([], _) => return (List.revAppend acc ls2)
adamc@953 130 | (_, []) => return (List.revAppend acc ls1)
adamc@953 131 | (x1 :: ls1', x2 :: ls2') =>
adamc@953 132 b <- cmp x1 x2;
adamc@953 133 if b then
adamc@953 134 merge' (x1 :: acc) ls1' ls2
adamc@953 135 else
adamc@953 136 merge' (x2 :: acc) ls1 ls2'
adamc@953 137 in
adamc@953 138 merge' []
adamc@953 139 end
adamc@953 140
adamc@953 141 fun sort [t] (cmp : t -> t -> signal bool) =
adamc@953 142 let
adamc@953 143 fun sort' (ls : list t) =
adamc@953 144 case ls of
adamc@953 145 [] => return ls
adamc@953 146 | _ :: [] => return ls
adamc@953 147 | _ =>
adamc@953 148 let
adamc@953 149 val (ls1, ls2) = split ls
adamc@953 150 in
adamc@953 151 ls1' <- sort' ls1;
adamc@953 152 ls2' <- sort' ls2;
adamc@953 153 merge cmp ls1' ls2'
adamc@953 154 end
adamc@953 155 in
adamc@953 156 sort'
adamc@953 157 end
adamc@953 158
adamc@953 159 fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
adamc@962 160 Sort : signal (option (t -> t -> signal bool)),
adamc@962 161 StartPosition : signal (option int)}) dl = <xml>
adamc@953 162 <dyn signal={cmp <- r.Sort;
adamc@962 163 pos <- r.StartPosition;
adamc@953 164 case cmp of
adamc@962 165 None => return (renderDyn f r.Filter pos dl)
adamc@953 166 | Some cmp =>
adamc@952 167 dl' <- signal dl;
adamc@952 168 elems <- (case dl' of
adamc@952 169 Empty => return []
adamc@952 170 | Nonempty {Head = hd, Tail = tlTop} =>
adamc@952 171 let
adamc@952 172 fun listOut prev dl'' acc =
adamc@952 173 case dl'' of
adamc@952 174 Nil => return acc
adamc@952 175 | Cons (v, tl) =>
adamc@952 176 let
adamc@952 177 val pos = case prev of
adamc@952 178 None => headPos dl
adamc@952 179 | Some prev => tailPos prev tl tlTop
adamc@952 180 in
adamc@958 181 b <- r.Filter v;
adamc@952 182 tl' <- signal tl;
adamc@958 183 listOut (Some tl) tl' (if b then
adamc@958 184 (v, pos) :: acc
adamc@958 185 else
adamc@958 186 acc)
adamc@952 187 end
adamc@952 188 in
adamc@952 189 listOut None hd []
adamc@952 190 end);
adamc@953 191 elems <- sort (fn v1 v2 => cmp v1.1 v2.1) elems;
adamc@962 192 let
adamc@962 193 fun skip n ls =
adamc@962 194 case (n, ls) of
adamc@962 195 (0, _) => ls
adamc@962 196 | (n, _ :: ls) => skip (n-1) ls
adamc@962 197 | (_, []) => []
adamc@962 198
adamc@962 199 val elems =
adamc@962 200 case pos of
adamc@962 201 None => elems
adamc@962 202 | Some pos => skip pos elems
adamc@962 203 in
adamc@962 204 return (renderFlat f r.Filter elems)
adamc@962 205 end}/>
adamc@952 206 </xml>
adamc@952 207
adamc@915 208 fun delete pos = pos
adamc@915 209
adamc@915 210 fun elements' [t] (dl'' : dlist'' t) =
adamc@915 211 case dl'' of
adamc@915 212 Nil => return []
adamc@915 213 | Cons (x, dl'') =>
adamc@915 214 dl'' <- signal dl'';
adamc@915 215 tl <- elements' dl'';
adamc@915 216 return (x :: tl)
adamc@915 217
adamc@915 218 fun elements [t] (dl : dlist t) =
adamc@951 219 dl' <- signal dl;
adamc@915 220 case dl' of
adamc@915 221 Empty => return []
adamc@915 222 | Nonempty {Head = hd, ...} => elements' hd
adamc@937 223
adamc@937 224 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
adamc@937 225 let
adamc@937 226 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
adamc@937 227 case dl of
adamc@937 228 Nil => return i
adamc@937 229 | Cons (v, dl') =>
adamc@937 230 dl' <- signal dl';
adamc@937 231 i' <- f v i;
adamc@937 232 foldl'' i' dl'
adamc@937 233
adamc@937 234 fun foldl' (i : acc) (dl : dlist t) : signal acc =
adamc@951 235 dl <- signal dl;
adamc@937 236 case dl of
adamc@937 237 Empty => return i
adamc@937 238 | Nonempty {Head = dl, ...} => foldl'' i dl
adamc@937 239 in
adamc@937 240 foldl'
adamc@937 241 end