diff lib/top.ur @ 470:7cb418e9714f

Tree demo works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 18:49:38 -0500
parents b393c2fc80f8
children 20fab0e96217
line wrap: on
line diff
--- a/lib/top.ur	Thu Nov 06 17:09:53 2008 -0500
+++ b/lib/top.ur	Thu Nov 06 18:49:38 2008 -0500
@@ -226,3 +226,16 @@
                 None => error <xml>Query returned no rows</xml>
               | Some r => r)
 
+fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
+    (t ::: Type) (_ : sql_injectable (option t))
+    (e1 : sql_exp tables agg exps (option t))
+    (e2 : sql_exp tables agg exps (option t)) =
+    (SQL ({[e1]} IS NULL AND {[e2]} IS NULL) OR {[e1]} = {[e2]})
+
+fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
+    (t ::: Type) (inj : sql_injectable (option t))
+    (e1 : sql_exp tables agg exps (option t))
+    (e2 : option t) =
+    case e2 of
+        None => (SQL {[e1]} IS NULL)
+      | Some _ => sql_comparison sql_eq e1 (@sql_inject inj e2)