Mercurial > urweb

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