From 3af6c283c504e7e85d9e127f64a5eb72abe583ee Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Thu, 6 Nov 2008 18:49:38 -0500
Subject: Tree demo works

---
 lib/basis.urs |  5 +++++
 lib/top.ur    | 13 +++++++++++++
 lib/top.urs   | 12 ++++++++++++
 3 files changed, 30 insertions(+)

(limited to 'lib')

diff --git a/lib/basis.urs b/lib/basis.urs
index daefe954..656c5b91 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -197,6 +197,11 @@ val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
                  -> t ::: Type
                  -> sql_injectable t -> t -> sql_exp tables agg exps t
 
+val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+                  -> t ::: Type
+                  -> sql_exp tables agg exps (option t)
+                  -> sql_exp tables agg exps bool
+
 con sql_unary :: Type -> Type -> Type
 val sql_not : sql_unary bool bool
 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
diff --git a/lib/top.ur b/lib/top.ur
index abc70e53..5d00282c 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -226,3 +226,16 @@ fun oneRow (tables ::: {{Type}}) (exps ::: {Type})
                 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)
diff --git a/lib/top.urs b/lib/top.urs
index 6653db07..d6315b92 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -169,3 +169,15 @@ val oneRow : tables ::: {{Type}} -> exps ::: {Type}
                                             [[nm] ~ acc] =>
                                          [nm = $fields] ++ acc)
                                          [] tables)
+
+val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+                 -> t ::: Type -> sql_injectable (option t)
+                 -> sql_exp tables agg exps (option t)
+                 -> sql_exp tables agg exps (option t)
+                 -> sql_exp tables agg exps bool
+
+val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+                  -> t ::: Type -> sql_injectable (option t)
+                  -> sql_exp tables agg exps (option t)
+                  -> option t
+                  -> sql_exp tables agg exps bool
-- 
cgit v1.2.3