comparison lib/ur/top.ur @ 1074:d89f98f0b4bb

Fixing a bug in DInitializer elaboration
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Dec 2009 14:34:18 -0500
parents 9001966ae1c8
children dcf98ae3c48d
comparison
equal deleted inserted replaced
1073:b2311dfb3158 1074:d89f98f0b4bb
269 o <- oneOrNoRows q; 269 o <- oneOrNoRows q;
270 return (case o of 270 return (case o of
271 None => error <xml>Query returned no rows</xml> 271 None => error <xml>Query returned no rows</xml>
272 | Some r => r.nm) 272 | Some r => r.nm)
273 273
274 fun nonempty [fs] [us] (t : sql_table fs us) =
275 oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
276
274 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] 277 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
275 [t ::: Type] (_ : sql_injectable (option t)) 278 [t ::: Type] (_ : sql_injectable (option t))
276 (e1 : sql_exp tables agg exps (option t)) 279 (e1 : sql_exp tables agg exps (option t))
277 (e2 : sql_exp tables agg exps (option t)) = 280 (e2 : sql_exp tables agg exps (option t)) =
278 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) 281 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})