comparison lib/ur/top.ur @ 1405:8631e9ed0ee8

queryXI and queryX1I
author Adam Chlipala <adam@chlipala.net>
date Thu, 20 Jan 2011 12:43:12 -0500
parents d328983dc5a6
children e8bea46f8eda
comparison
equal deleted inserted replaced
1404:82b204f20026 1405:8631e9ed0ee8
253 -> xml ctx inp []) = 253 -> xml ctx inp []) =
254 query q 254 query q
255 (fn fs acc => return <xml>{acc}{f fs}</xml>) 255 (fn fs acc => return <xml>{acc}{f fs}</xml>)
256 <xml/> 256 <xml/>
257 257
258 fun rev [a] (ls : list a) : list a =
259 let
260 fun rev' ls acc =
261 case ls of
262 [] => acc
263 | x :: ls => rev' ls (x :: acc)
264 in
265 rev' ls []
266 end
267
268 fun queryXI [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
269 [tables ~ exps] (q : sql_query [] [] tables exps)
270 (f : int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
271 -> xml ctx inp []) =
272 let
273 fun qxi ls i =
274 case ls of
275 [] => <xml/>
276 | x :: ls => <xml>{f i x}{qxi ls (i+1)}</xml>
277 in
278 ls <- queryL q;
279 return (qxi ls 0)
280 end
281
258 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] 282 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
259 (q : sql_query [] [] [nm = fs] []) 283 (q : sql_query [] [] [nm = fs] [])
260 (f : $fs -> xml ctx inp []) = 284 (f : $fs -> xml ctx inp []) =
261 query q 285 query q
262 (fn fs acc => return <xml>{acc}{f fs.nm}</xml>) 286 (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
263 <xml/> 287 <xml/>
288
289 fun queryX1I [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
290 (q : sql_query [] [] [nm = fs] [])
291 (f : int -> $fs -> xml ctx inp []) =
292 let
293 fun qx1i ls i =
294 case ls of
295 [] => <xml/>
296 | x :: ls => <xml>{f i x.nm}{qx1i ls (i+1)}</xml>
297 in
298 ls <- queryL q;
299 return (qx1i ls 0)
300 end
264 301
265 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] 302 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
266 [tables ~ exps] (q : sql_query [] [] tables exps) 303 [tables ~ exps] (q : sql_query [] [] tables exps)
267 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) 304 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
268 -> transaction (xml ctx inp [])) = 305 -> transaction (xml ctx inp [])) =