Mercurial > urweb

annotate demo/more/dlist.ur @ 944:da3ec6014d2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Filters implementation type-checking
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 15:48:53 -0400
parents 37dd42935dad
children 103ac1792c41
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@944 9 con dlist t = {Filter: t -> signal bool,
adamc@944 10 Elements : source (dlist' t)}
adamc@915 11
adamc@915 12 type position = transaction unit
adamc@915 13
adamc@915 14 fun headPos [t] (dl : dlist t) =
adamc@944 15 dl' <- get dl.Elements;
adamc@915 16 case dl' of
adamc@915 17 Nonempty { Head = Cons (_, tl), Tail = tl' } =>
adamc@915 18 cur <- get tl;
adamc@944 19 set dl.Elements (case cur of
adamc@944 20 Nil => Empty
adamc@944 21 | _ => Nonempty {Head = cur, Tail = tl'})
adamc@915 22 | _ => return ()
adamc@915 23
adamc@915 24 fun tailPos [t] (cur : source (dlist'' t)) new tail =
adamc@915 25 new' <- get new;
adamc@915 26 set cur new';
adamc@915 27
adamc@915 28 case new' of
adamc@915 29 Nil => set tail cur
adamc@915 30 | _ => return ()
adamc@915 31
adamc@944 32 fun create [t] r =
adamc@944 33 s <- source Empty;
adamc@944 34 return {Filter = r.Filter,
adamc@944 35 Elements = s}
adamc@915 36
adamc@944 37 fun clear [t] (s : dlist t) = set s.Elements Empty
adamc@915 38
adamc@915 39 fun append [t] dl v =
adamc@944 40 dl' <- get dl.Elements;
adamc@915 41 case dl' of
adamc@915 42 Empty =>
adamc@915 43 tl <- source Nil;
adamc@915 44 tl' <- source tl;
adamc@944 45 set dl.Elements (Nonempty {Head = Cons (v, tl), Tail = tl'});
adamc@915 46 return (headPos dl)
adamc@915 47
adamc@915 48 | Nonempty {Tail = tl, ...} =>
adamc@915 49 cur <- get tl;
adamc@915 50 new <- source Nil;
adamc@915 51 set cur (Cons (v, new));
adamc@915 52 set tl new;
adamc@915 53 return (tailPos cur new tl)
adamc@915 54
adamc@915 55 fun render [ctx] [ctx ~ body] [t] f dl = <xml>
adamc@944 56 <dyn signal={dl' <- signal dl.Elements;
adamc@915 57 return (case dl' of
adamc@915 58 Empty => <xml/>
adamc@915 59 | Nonempty {Head = hd, Tail = tlTop} =>
adamc@915 60 let
adamc@915 61 fun render' prev dl'' =
adamc@915 62 case dl'' of
adamc@915 63 Nil => <xml/>
adamc@915 64 | Cons (v, tl) =>
adamc@915 65 let
adamc@915 66 val pos = case prev of
adamc@915 67 None => headPos dl
adamc@915 68 | Some prev => tailPos prev tl tlTop
adamc@915 69 in
adamc@944 70 <xml><dyn signal={b <- dl.Filter v;
adamc@944 71 return (if b then
adamc@944 72 f v pos
adamc@944 73 else
adamc@944 74 <xml/>)}/>
adamc@944 75 <dyn signal={tl' <- signal tl;
adamc@944 76 return (render' (Some tl) tl')}/></xml>
adamc@915 77 end
adamc@915 78 in
adamc@915 79 render' None hd
adamc@915 80 end)}/>
adamc@915 81 </xml>
adamc@915 82
adamc@915 83 fun delete pos = pos
adamc@915 84
adamc@915 85 fun elements' [t] (dl'' : dlist'' t) =
adamc@915 86 case dl'' of
adamc@915 87 Nil => return []
adamc@915 88 | Cons (x, dl'') =>
adamc@915 89 dl'' <- signal dl'';
adamc@915 90 tl <- elements' dl'';
adamc@915 91 return (x :: tl)
adamc@915 92
adamc@915 93 fun elements [t] (dl : dlist t) =
adamc@944 94 dl' <- signal dl.Elements;
adamc@915 95 case dl' of
adamc@915 96 Empty => return []
adamc@915 97 | Nonempty {Head = hd, ...} => elements' hd
adamc@937 98
adamc@937 99 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
adamc@937 100 let
adamc@937 101 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
adamc@937 102 case dl of
adamc@937 103 Nil => return i
adamc@937 104 | Cons (v, dl') =>
adamc@937 105 dl' <- signal dl';
adamc@937 106 i' <- f v i;
adamc@937 107 foldl'' i' dl'
adamc@937 108
adamc@937 109 fun foldl' (i : acc) (dl : dlist t) : signal acc =
adamc@944 110 dl <- signal dl.Elements;
adamc@937 111 case dl of
adamc@937 112 Empty => return i
adamc@937 113 | Nonempty {Head = dl, ...} => foldl'' i dl
adamc@937 114 in
adamc@937 115 foldl'
adamc@937 116 end