Mercurial > urweb

comparison lib/ur/top.ur @ 1775:6bc2a8cb3a67

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Track whether SQL expressions may use window functions, in preparation for actual window function support
author Adam Chlipala <adam@chlipala.net>
date Sat, 02 Jun 2012 15:35:58 -0400
parents 9253765d7724
children 818d4097e2ed
comparison
equal deleted inserted replaced
1774:27fdd78bd2f5 1775:6bc2a8cb3a67
374 374
375 fun nonempty [fs] [us] (t : sql_table fs us) = 375 fun nonempty [fs] [us] (t : sql_table fs us) =
376 oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t) 376 oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
377 377
378 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] 378 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
379 [t ::: Type] (_ : sql_injectable (option t)) 379 [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t))
380 (e1 : sql_exp tables agg exps (option t)) 380 (e1 : sql_exp tables agg exps aw (option t))
381 (e2 : sql_exp tables agg exps (option t)) = 381 (e2 : sql_exp tables agg exps aw (option t)) =
382 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) 382 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
383 383
384 fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] 384 fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
385 [t ::: Type] (_ : sql_injectable (option t)) 385 [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t))
386 (e1 : sql_exp tables agg exps (option t)) 386 (e1 : sql_exp tables agg exps aw (option t))
387 (e2 : option t) = 387 (e2 : option t) =
388 case e2 of 388 case e2 of
389 None => (SQL {e1} IS NULL) 389 None => (SQL {e1} IS NULL)
390 | Some _ => sql_binary sql_eq e1 (sql_inject e2) 390 | Some _ => sql_binary sql_eq e1 (sql_inject e2)
391 391