comparison demo/more/dlist.ur @ 951:103ac1792c41

Make filter argument to render, not create
author Adam Chlipala <adamc@hcoop.net>
date Thu, 17 Sep 2009 14:27:00 -0400
parents da3ec6014d2f
children 07569af40069
comparison
equal deleted inserted replaced
950:5be3d19b59f3 951:103ac1792c41
4 4
5 datatype dlist' t = 5 datatype dlist' t =
6 Empty 6 Empty
7 | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) } 7 | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }
8 8
9 con dlist t = {Filter: t -> signal bool, 9 con dlist t = source (dlist' t)
10 Elements : source (dlist' t)}
11 10
12 type position = transaction unit 11 type position = transaction unit
13 12
14 fun headPos [t] (dl : dlist t) = 13 fun headPos [t] (dl : dlist t) =
15 dl' <- get dl.Elements; 14 dl' <- get dl;
16 case dl' of 15 case dl' of
17 Nonempty { Head = Cons (_, tl), Tail = tl' } => 16 Nonempty { Head = Cons (_, tl), Tail = tl' } =>
18 cur <- get tl; 17 cur <- get tl;
19 set dl.Elements (case cur of 18 set dl (case cur of
20 Nil => Empty 19 Nil => Empty
21 | _ => Nonempty {Head = cur, Tail = tl'}) 20 | _ => Nonempty {Head = cur, Tail = tl'})
22 | _ => return () 21 | _ => return ()
23 22
24 fun tailPos [t] (cur : source (dlist'' t)) new tail = 23 fun tailPos [t] (cur : source (dlist'' t)) new tail =
25 new' <- get new; 24 new' <- get new;
26 set cur new'; 25 set cur new';
27 26
28 case new' of 27 case new' of
29 Nil => set tail cur 28 Nil => set tail cur
30 | _ => return () 29 | _ => return ()
31 30
32 fun create [t] r = 31 val create [t] = source Empty
33 s <- source Empty;
34 return {Filter = r.Filter,
35 Elements = s}
36 32
37 fun clear [t] (s : dlist t) = set s.Elements Empty 33 fun clear [t] (s : dlist t) = set s Empty
38 34
39 fun append [t] dl v = 35 fun append [t] dl v =
40 dl' <- get dl.Elements; 36 dl' <- get dl;
41 case dl' of 37 case dl' of
42 Empty => 38 Empty =>
43 tl <- source Nil; 39 tl <- source Nil;
44 tl' <- source tl; 40 tl' <- source tl;
45 set dl.Elements (Nonempty {Head = Cons (v, tl), Tail = tl'}); 41 set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
46 return (headPos dl) 42 return (headPos dl)
47 43
48 | Nonempty {Tail = tl, ...} => 44 | Nonempty {Tail = tl, ...} =>
49 cur <- get tl; 45 cur <- get tl;
50 new <- source Nil; 46 new <- source Nil;
51 set cur (Cons (v, new)); 47 set cur (Cons (v, new));
52 set tl new; 48 set tl new;
53 return (tailPos cur new tl) 49 return (tailPos cur new tl)
54 50
55 fun render [ctx] [ctx ~ body] [t] f dl = <xml> 51 fun render [ctx] [ctx ~ body] [t] f {Filter = filter, ...} dl = <xml>
56 <dyn signal={dl' <- signal dl.Elements; 52 <dyn signal={dl' <- signal dl;
57 return (case dl' of 53 return (case dl' of
58 Empty => <xml/> 54 Empty => <xml/>
59 | Nonempty {Head = hd, Tail = tlTop} => 55 | Nonempty {Head = hd, Tail = tlTop} =>
60 let 56 let
61 fun render' prev dl'' = 57 fun render' prev dl'' =
65 let 61 let
66 val pos = case prev of 62 val pos = case prev of
67 None => headPos dl 63 None => headPos dl
68 | Some prev => tailPos prev tl tlTop 64 | Some prev => tailPos prev tl tlTop
69 in 65 in
70 <xml><dyn signal={b <- dl.Filter v; 66 <xml><dyn signal={b <- filter v;
71 return (if b then 67 return (if b then
72 f v pos 68 f v pos
73 else 69 else
74 <xml/>)}/> 70 <xml/>)}/>
75 <dyn signal={tl' <- signal tl; 71 <dyn signal={tl' <- signal tl;
89 dl'' <- signal dl''; 85 dl'' <- signal dl'';
90 tl <- elements' dl''; 86 tl <- elements' dl'';
91 return (x :: tl) 87 return (x :: tl)
92 88
93 fun elements [t] (dl : dlist t) = 89 fun elements [t] (dl : dlist t) =
94 dl' <- signal dl.Elements; 90 dl' <- signal dl;
95 case dl' of 91 case dl' of
96 Empty => return [] 92 Empty => return []
97 | Nonempty {Head = hd, ...} => elements' hd 93 | Nonempty {Head = hd, ...} => elements' hd
98 94
99 fun foldl [t] [acc] (f : t -> acc -> signal acc) = 95 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
105 dl' <- signal dl'; 101 dl' <- signal dl';
106 i' <- f v i; 102 i' <- f v i;
107 foldl'' i' dl' 103 foldl'' i' dl'
108 104
109 fun foldl' (i : acc) (dl : dlist t) : signal acc = 105 fun foldl' (i : acc) (dl : dlist t) : signal acc =
110 dl <- signal dl.Elements; 106 dl <- signal dl;
111 case dl of 107 case dl of
112 Empty => return i 108 Empty => return i
113 | Nonempty {Head = dl, ...} => foldl'' i dl 109 | Nonempty {Head = dl, ...} => foldl'' i dl
114 in 110 in
115 foldl' 111 foldl'