comparison lib/ur/top.ur @ 1003:61c30f0742d7

Registering for Conference1
author Adam Chlipala <adamc@hcoop.net>
date Tue, 20 Oct 2009 11:05:58 -0400
parents 10114d7b7477
children a87495bcaeec
comparison
equal deleted inserted replaced
1002:bb3fc575cfe7 1003:61c30f0742d7
234 return <xml>{acc}{r}</xml>) 234 return <xml>{acc}{r}</xml>)
235 <xml/> 235 <xml/>
236 236
237 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}] 237 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
238 [tables ~ exps] 238 [tables ~ exps]
239 (q : sql_query tables exps) = 239 (q : sql_query tables exps) =
240 query q 240 query q
241 (fn fs _ => return (Some fs)) 241 (fn fs _ => return (Some fs))
242 None
243
244 fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) =
245 query q
246 (fn fs _ => return (Some fs.nm))
242 None 247 None
243 248
244 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}] 249 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
245 [tables ~ exps] (q : sql_query tables exps) = 250 [tables ~ exps] (q : sql_query tables exps) =
246 o <- oneOrNoRows q; 251 o <- oneOrNoRows q;
247 return (case o of 252 return (case o of
248 None => error <xml>Query returned no rows</xml> 253 None => error <xml>Query returned no rows</xml>
249 | Some r => r) 254 | Some r => r)
255
256 fun oneRowE1 [tab ::: Name] [nm ::: Name] [t ::: Type] [[tab] ~ [nm]] (q : sql_query [tab = []] [nm = t]) =
257 o <- oneOrNoRows q;
258 return (case o of
259 None => error <xml>Query returned no rows</xml>
260 | Some r => r.nm)
250 261
251 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] 262 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
252 [t ::: Type] (_ : sql_injectable (option t)) 263 [t ::: Type] (_ : sql_injectable (option t))
253 (e1 : sql_exp tables agg exps (option t)) 264 (e1 : sql_exp tables agg exps (option t))
254 (e2 : sql_exp tables agg exps (option t)) = 265 (e2 : sql_exp tables agg exps (option t)) =