Mercurial > urweb

comparison lib/ur/top.ur @ 1778:818d4097e2ed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Lighter-weight encoding of window function use
author Adam Chlipala <adam@chlipala.net>
date Sun, 03 Jun 2012 11:29:31 -0400
parents 6bc2a8cb3a67
children 69daa6d70299
comparison
equal deleted inserted replaced
1777:59b07fdae1ff 1778:818d4097e2ed
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 [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t)) 379 [t ::: Type] (_ : sql_injectable (option t))
380 (e1 : sql_exp tables agg exps aw (option t)) 380 (e1 : sql_exp tables agg exps (option t))
381 (e2 : sql_exp tables agg exps aw (option t)) = 381 (e2 : sql_exp tables agg exps (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 [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t)) 385 [t ::: Type] (_ : sql_injectable (option t))
386 (e1 : sql_exp tables agg exps aw (option t)) 386 (e1 : sql_exp tables agg exps (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