comparison lib/ur/top.ur @ 1191:61c3139eab12

Subquery expressions
author Adam Chlipala <adamc@hcoop.net>
date Thu, 25 Mar 2010 15:44:24 -0400
parents 26fed2c4f5be
children 4172863d049d
comparison
equal deleted inserted replaced
1190:899875315bde 1191:61c3139eab12
213 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 213 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
214 r1 r2 r3 acc => 214 r1 r2 r3 acc =>
215 <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>) 215 <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
216 <xml/> 216 <xml/>
217 217
218 fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [t = fs] []) 218 fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] [])
219 (f : $fs -> state -> transaction state) (i : state) = 219 (f : $fs -> state -> transaction state) (i : state) =
220 query q (fn r => f r.t) i 220 query q (fn r => f r.t) i
221 221
222 fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [t = fs] []) 222 fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] [])
223 (f : $fs -> state -> state) (i : state) = 223 (f : $fs -> state -> state) (i : state) =
224 query q (fn r s => return (f r.t s)) i 224 query q (fn r s => return (f r.t s)) i
225 225
226 fun queryL [tables] [exps] [tables ~ exps] (q : sql_query tables exps) = 226 fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] tables exps) =
227 query q 227 query q
228 (fn r ls => return (r :: ls)) 228 (fn r ls => return (r :: ls))
229 [] 229 []
230 230
231 fun queryI [tables ::: {{Type}}] [exps ::: {Type}] 231 fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
232 [tables ~ exps] (q : sql_query tables exps) 232 [tables ~ exps] (q : sql_query [] tables exps)
233 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) 233 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
234 -> transaction unit) = 234 -> transaction unit) =
235 query q 235 query q
236 (fn fs _ => f fs) 236 (fn fs _ => f fs)
237 () 237 ()
238 238
239 fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] 239 fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
240 [tables ~ exps] (q : sql_query tables exps) 240 [tables ~ exps] (q : sql_query [] tables exps)
241 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) 241 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
242 -> xml ctx inp []) = 242 -> xml ctx inp []) =
243 query q 243 query q
244 (fn fs acc => return <xml>{acc}{f fs}</xml>) 244 (fn fs acc => return <xml>{acc}{f fs}</xml>)
245 <xml/> 245 <xml/>
246 246
247 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] 247 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
248 (q : sql_query [nm = fs] []) 248 (q : sql_query [] [nm = fs] [])
249 (f : $fs -> xml ctx inp []) = 249 (f : $fs -> xml ctx inp []) =
250 query q 250 query q
251 (fn fs acc => return <xml>{acc}{f fs.nm}</xml>) 251 (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
252 <xml/> 252 <xml/>
253 253
254 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] 254 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
255 [tables ~ exps] (q : sql_query tables exps) 255 [tables ~ exps] (q : sql_query [] tables exps)
256 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) 256 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
257 -> transaction (xml ctx inp [])) = 257 -> transaction (xml ctx inp [])) =
258 query q 258 query q
259 (fn fs acc => 259 (fn fs acc =>
260 r <- f fs; 260 r <- f fs;
261 return <xml>{acc}{r}</xml>) 261 return <xml>{acc}{r}</xml>)
262 <xml/> 262 <xml/>
263 263
264 fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] 264 fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
265 (q : sql_query [nm = fs] []) 265 (q : sql_query [] [nm = fs] [])
266 (f : $fs -> transaction (xml ctx inp [])) = 266 (f : $fs -> transaction (xml ctx inp [])) =
267 query q 267 query q
268 (fn fs acc => 268 (fn fs acc =>
269 r <- f fs.nm; 269 r <- f fs.nm;
270 return <xml>{acc}{r}</xml>) 270 return <xml>{acc}{r}</xml>)
271 <xml/> 271 <xml/>
272 272
273 fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] 273 fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
274 (q : sql_query [] exps) 274 (q : sql_query [] [] exps)
275 (f : $exps -> transaction (xml ctx inp [])) = 275 (f : $exps -> transaction (xml ctx inp [])) =
276 query q 276 query q
277 (fn fs acc => 277 (fn fs acc =>
278 r <- f fs; 278 r <- f fs;
279 return <xml>{acc}{r}</xml>) 279 return <xml>{acc}{r}</xml>)
280 <xml/> 280 <xml/>
281 281
282 fun hasRows [tables ::: {{Type}}] [exps ::: {Type}] 282 fun hasRows [tables ::: {{Type}}] [exps ::: {Type}]
283 [tables ~ exps] 283 [tables ~ exps]
284 (q : sql_query tables exps) = 284 (q : sql_query [] tables exps) =
285 query q 285 query q
286 (fn _ _ => return True) 286 (fn _ _ => return True)
287 False 287 False
288 288
289 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}] 289 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
290 [tables ~ exps] 290 [tables ~ exps]
291 (q : sql_query tables exps) = 291 (q : sql_query [] tables exps) =
292 query q 292 query q
293 (fn fs _ => return (Some fs)) 293 (fn fs _ => return (Some fs))
294 None 294 None
295 295
296 fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) = 296 fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) =
297 query q 297 query q
298 (fn fs _ => return (Some fs.nm)) 298 (fn fs _ => return (Some fs.nm))
299 None 299 None
300 300
301 fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query (mapU [] tabs) [nm = t]) = 301 fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) =
302 query q 302 query q
303 (fn fs _ => return (Some fs.nm)) 303 (fn fs _ => return (Some fs.nm))
304 None 304 None
305 305
306 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}] 306 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
307 [tables ~ exps] (q : sql_query tables exps) = 307 [tables ~ exps] (q : sql_query [] tables exps) =
308 o <- oneOrNoRows q; 308 o <- oneOrNoRows q;
309 return (case o of 309 return (case o of
310 None => error <xml>Query returned no rows</xml> 310 None => error <xml>Query returned no rows</xml>
311 | Some r => r) 311 | Some r => r)
312 312
313 fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) = 313 fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) =
314 o <- oneOrNoRows q; 314 o <- oneOrNoRows q;
315 return (case o of 315 return (case o of
316 None => error <xml>Query returned no rows</xml> 316 None => error <xml>Query returned no rows</xml>
317 | Some r => r.nm) 317 | Some r => r.nm)
318 318
319 fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query (mapU [] tabs) [nm = t]) = 319 fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) =
320 o <- oneOrNoRows q; 320 o <- oneOrNoRows q;
321 return (case o of 321 return (case o of
322 None => error <xml>Query returned no rows</xml> 322 None => error <xml>Query returned no rows</xml>
323 | Some r => r.nm) 323 | Some r => r.nm)
324 324