Mercurial > urweb

comparison lib/ur/top.ur @ 1472:18d18a70821e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Implicit argument insertion for local variables
author Adam Chlipala <adam@chlipala.net>
date Tue, 14 Jun 2011 08:54:45 -0400
parents 44f78d6fec29
children 9253765d7724
comparison
equal deleted inserted replaced
1471:67ebd30a2283 1472:18d18a70821e
19 19
20 fun cons [K] [r ::: {K}] [nm :: Name] [v :: K] [[nm] ~ r] (fold : folder r) 20 fun cons [K] [r ::: {K}] [nm :: Name] [v :: K] [[nm] ~ r] (fold : folder r)
21 [tf :: {K} -> Type] 21 [tf :: {K} -> Type]
22 (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] => 22 (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
23 tf r -> tf ([nm = v] ++ r)) 23 tf r -> tf ([nm = v] ++ r))
24 (i : tf []) = f [nm] [v] [r] ! (fold [tf] f i) 24 (i : tf []) = f [nm] [v] [r] (fold [tf] f i)
25 25
26 fun concat [K] [r1 ::: {K}] [r2 ::: {K}] [r1 ~ r2] 26 fun concat [K] [r1 ::: {K}] [r2 ::: {K}] [r1 ~ r2]
27 (f1 : folder r1) (f2 : folder r2) 27 (f1 : folder r1) (f2 : folder r2)
28 [tf :: {K} -> Type] 28 [tf :: {K} -> Type]
29 (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] => 29 (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
31 (i : tf []) = 31 (i : tf []) =
32 f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)] 32 f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)]
33 (fn [nm :: Name] [v :: K] [r1' :: {K}] [[nm] ~ r1'] 33 (fn [nm :: Name] [v :: K] [r1' :: {K}] [[nm] ~ r1']
34 (acc : [r1' ~ r2] => tf (r1' ++ r2)) 34 (acc : [r1' ~ r2] => tf (r1' ++ r2))
35 [[nm = v] ++ r1' ~ r2] => 35 [[nm = v] ++ r1' ~ r2] =>
36 f [nm] [v] [r1' ++ r2] ! acc) 36 f [nm] [v] [r1' ++ r2] acc)
37 (fn [[] ~ r2] => f2 [tf] f i) ! 37 (fn [[] ~ r2] => f2 [tf] f i)
38 38
39 fun mp [K1] [K2] [f ::: K1 -> K2] [r ::: {K1}] 39 fun mp [K1] [K2] [f ::: K1 -> K2] [r ::: {K1}]
40 (fold : folder r) 40 (fold : folder r)
41 [tf :: {K2} -> Type] 41 [tf :: {K2} -> Type]
42 (f : nm :: Name -> v :: K2 -> r :: {K2} -> [[nm] ~ r] => 42 (f : nm :: Name -> v :: K2 -> r :: {K2} -> [[nm] ~ r] =>
43 tf r -> tf ([nm = v] ++ r)) 43 tf r -> tf ([nm = v] ++ r))
44 (i : tf []) = 44 (i : tf []) =
45 fold [fn r => tf (map f r)] 45 fold [fn r => tf (map f r)]
46 (fn [nm :: Name] [v :: K1] [rest :: {K1}] [[nm] ~ rest] (acc : tf (map f rest)) => 46 (fn [nm :: Name] [v :: K1] [rest :: {K1}] [[nm] ~ rest] (acc : tf (map f rest)) =>
47 f [nm] [f v] [map f rest] ! acc) 47 f [nm] [f v] [map f rest] acc)
48 i 48 i
49 end 49 end
50 50
51 51
52 fun not b = if b then False else True 52 fun not b = if b then False else True
125 -> [[nm] ~ rest] => 125 -> [[nm] ~ rest] =>
126 tf -> tr rest -> tr ([nm] ++ rest)) 126 tf -> tr rest -> tr ([nm] ++ rest))
127 (i : tr []) [r ::: {Unit}] (fl : folder r) = 127 (i : tr []) [r ::: {Unit}] (fl : folder r) =
128 fl [fn r :: {Unit} => $(mapU tf r) -> tr r] 128 fl [fn r :: {Unit} => $(mapU tf r) -> tr r]
129 (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r => 129 (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r =>
130 f [nm] [rest] ! r.nm (acc (r -- nm))) 130 f [nm] [rest] r.nm (acc (r -- nm)))
131 (fn _ => i) 131 (fn _ => i)
132 132
133 fun foldUR2 [tf1 :: Type] [tf2 :: Type] [tr :: {Unit} -> Type] 133 fun foldUR2 [tf1 :: Type] [tf2 :: Type] [tr :: {Unit} -> Type]
134 (f : nm :: Name -> rest :: {Unit} 134 (f : nm :: Name -> rest :: {Unit}
135 -> [[nm] ~ rest] => 135 -> [[nm] ~ rest] =>
136 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) 136 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
137 (i : tr []) [r ::: {Unit}] (fl : folder r) = 137 (i : tr []) [r ::: {Unit}] (fl : folder r) =
138 fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r] 138 fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r]
139 (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 => 139 (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 =>
140 f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 140 f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
141 (fn _ _ => i) 141 (fn _ _ => i)
142 142
143 fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type] 143 fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type]
144 (f : nm :: Name -> t :: K -> rest :: {K} 144 (f : nm :: Name -> t :: K -> rest :: {K}
145 -> [[nm] ~ rest] => 145 -> [[nm] ~ rest] =>
146 tf t -> tr rest -> tr ([nm = t] ++ rest)) 146 tf t -> tr rest -> tr ([nm = t] ++ rest))
147 (i : tr []) [r ::: {K}] (fl : folder r) = 147 (i : tr []) [r ::: {K}] (fl : folder r) =
148 fl [fn r :: {K} => $(map tf r) -> tr r] 148 fl [fn r :: {K} => $(map tf r) -> tr r]
149 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r => 149 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r =>
150 f [nm] [t] [rest] ! r.nm (acc (r -- nm))) 150 f [nm] [t] [rest] r.nm (acc (r -- nm)))
151 (fn _ => i) 151 (fn _ => i)
152 152
153 fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type] 153 fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
154 (f : nm :: Name -> t :: K -> rest :: {K} 154 (f : nm :: Name -> t :: K -> rest :: {K}
155 -> [[nm] ~ rest] => 155 -> [[nm] ~ rest] =>
156 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 156 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
157 (i : tr []) [r ::: {K}] (fl : folder r) = 157 (i : tr []) [r ::: {K}] (fl : folder r) =
158 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r] 158 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
159 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 159 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
160 (acc : _ -> _ -> tr rest) r1 r2 => 160 (acc : _ -> _ -> tr rest) r1 r2 =>
161 f [nm] [t] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 161 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
162 (fn _ _ => i) 162 (fn _ _ => i)
163 163
164 fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type] 164 fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
165 (f : nm :: Name -> t :: K -> rest :: {K} 165 (f : nm :: Name -> t :: K -> rest :: {K}
166 -> [[nm] ~ rest] => 166 -> [[nm] ~ rest] =>
167 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest)) 167 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
168 (i : tr []) [r ::: {K}] (fl : folder r) = 168 (i : tr []) [r ::: {K}] (fl : folder r) =
169 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r] 169 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r]
170 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 170 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
171 (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 => 171 (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
172 f [nm] [t] [rest] ! r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) 172 f [nm] [t] [rest] r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
173 (fn _ _ _ => i) 173 (fn _ _ _ => i)
174 174
175 fun mapUX [tf :: Type] [ctx :: {Unit}] 175 fun mapUX [tf :: Type] [ctx :: {Unit}]
176 (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) = 176 (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
177 @@foldR [fn _ => tf] [fn _ => xml ctx [] []] 177 @@foldR [fn _ => tf] [fn _ => xml ctx [] []]
178 (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc => 178 (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc =>
179 <xml>{f [nm] [rest] ! r}{acc}</xml>) 179 <xml>{f [nm] [rest] r}{acc}</xml>)
180 <xml/> 180 <xml/>
181 181
182 fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}] 182 fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}]
183 (f : nm :: Name -> t :: K -> rest :: {K} 183 (f : nm :: Name -> t :: K -> rest :: {K}
184 -> [[nm] ~ rest] => 184 -> [[nm] ~ rest] =>
185 tf t -> xml ctx [] []) = 185 tf t -> xml ctx [] []) =
186 @@foldR [tf] [fn _ => xml ctx [] []] 186 @@foldR [tf] [fn _ => xml ctx [] []]
187 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc => 187 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
188 <xml>{f [nm] [t] [rest] ! r}{acc}</xml>) 188 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
189 <xml/> 189 <xml/>
190 190
191 fun mapUX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}] 191 fun mapUX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}]
192 (f : nm :: Name -> rest :: {Unit} 192 (f : nm :: Name -> rest :: {Unit}
193 -> [[nm] ~ rest] => 193 -> [[nm] ~ rest] =>
194 tf1 -> tf2 -> xml ctx [] []) = 194 tf1 -> tf2 -> xml ctx [] []) =
195 @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] 195 @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
196 (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc => 196 (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
197 <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>) 197 <xml>{f [nm] [rest] v1 v2}{acc}</xml>)
198 <xml/> 198 <xml/>
199 199
200 fun mapX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}] 200 fun mapX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
201 (f : nm :: Name -> t :: K -> rest :: {K} 201 (f : nm :: Name -> t :: K -> rest :: {K}
202 -> [[nm] ~ rest] => 202 -> [[nm] ~ rest] =>
203 tf1 t -> tf2 t -> xml ctx [] []) = 203 tf1 t -> tf2 t -> xml ctx [] []) =
204 @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] 204 @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
205 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 205 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
206 r1 r2 acc => 206 r1 r2 acc =>
207 <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>) 207 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
208 <xml/> 208 <xml/>
209 209
210 fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}] 210 fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
211 (f : nm :: Name -> t :: K -> rest :: {K} 211 (f : nm :: Name -> t :: K -> rest :: {K}
212 -> [[nm] ~ rest] => 212 -> [[nm] ~ rest] =>
213 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) = 213 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
214 @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []] 214 @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
215 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 215 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
216 r1 r2 r3 acc => 216 r1 r2 r3 acc =>
217 <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>) 217 <xml>{f [nm] [t] [rest] r1 r2 r3}{acc}</xml>)
218 <xml/> 218 <xml/>
219 219
220 fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] []) 220 fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
221 (f : $fs -> state -> transaction state) (i : state) = 221 (f : $fs -> state -> transaction state) (i : state) =
222 query q (fn r => f r.t) i 222 query q (fn r => f r.t) i