Mercurial > urweb

annotate demo/more/dlist.ur @ 937:37dd42935dad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Summary row with aggregates
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 10:18:56 -0400
parents 5e8b6fa5b48f
children da3ec6014d2f
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@915 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@915 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@915 18 set dl (case cur of
adamc@915 19 Nil => Empty
adamc@915 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@915 31 val create = fn [t] => source Empty
adamc@915 32
adamc@915 33 fun clear [t] (s : dlist t) = set s Empty
adamc@915 34
adamc@915 35 fun append [t] dl v =
adamc@915 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@915 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@915 51 fun render [ctx] [ctx ~ body] [t] f dl = <xml>
adamc@915 52 <dyn signal={dl' <- signal dl;
adamc@915 53 return (case dl' of
adamc@915 54 Empty => <xml/>
adamc@915 55 | Nonempty {Head = hd, Tail = tlTop} =>
adamc@915 56 let
adamc@915 57 fun render' prev dl'' =
adamc@915 58 case dl'' of
adamc@915 59 Nil => <xml/>
adamc@915 60 | Cons (v, tl) =>
adamc@915 61 let
adamc@915 62 val pos = case prev of
adamc@915 63 None => headPos dl
adamc@915 64 | Some prev => tailPos prev tl tlTop
adamc@915 65 in
adamc@915 66 <xml>{f v pos}<dyn signal={tl' <- signal tl;
adamc@915 67 return (render' (Some tl) tl')}/></xml>
adamc@915 68 end
adamc@915 69 in
adamc@915 70 render' None hd
adamc@915 71 end)}/>
adamc@915 72 </xml>
adamc@915 73
adamc@915 74 fun delete pos = pos
adamc@915 75
adamc@915 76 fun elements' [t] (dl'' : dlist'' t) =
adamc@915 77 case dl'' of
adamc@915 78 Nil => return []
adamc@915 79 | Cons (x, dl'') =>
adamc@915 80 dl'' <- signal dl'';
adamc@915 81 tl <- elements' dl'';
adamc@915 82 return (x :: tl)
adamc@915 83
adamc@915 84 fun elements [t] (dl : dlist t) =
adamc@915 85 dl' <- signal dl;
adamc@915 86 case dl' of
adamc@915 87 Empty => return []
adamc@915 88 | Nonempty {Head = hd, ...} => elements' hd
adamc@937 89
adamc@937 90 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
adamc@937 91 let
adamc@937 92 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
adamc@937 93 case dl of
adamc@937 94 Nil => return i
adamc@937 95 | Cons (v, dl') =>
adamc@937 96 dl' <- signal dl';
adamc@937 97 i' <- f v i;
adamc@937 98 foldl'' i' dl'
adamc@937 99
adamc@937 100 fun foldl' (i : acc) (dl : dlist t) : signal acc =
adamc@937 101 dl <- signal dl;
adamc@937 102 case dl of
adamc@937 103 Empty => return i
adamc@937 104 | Nonempty {Head = dl, ...} => foldl'' i dl
adamc@937 105 in
adamc@937 106 foldl'
adamc@937 107 end