Mercurial > urweb

annotate demo/more/dlist.ur @ 957:2831be2daf2e

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