# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1323630274 18000
# Node ID 6ebc2ca594b783e92f169dcd8290c55b886c8bbf
# Parent  744bf911dcc6501c8de2b3abd4adb5eee1fe8751
Sql.insertIfMissing and deleteByKey (partly from Ron de Bruijn)

diff -r 744bf911dcc6 -r 6ebc2ca594b7 sql.ur
--- a/sql.ur	Tue Jun 14 08:55:15 2011 -0400
+++ b/sql.ur	Sun Dec 11 14:04:34 2011 -0500
@@ -3,7 +3,8 @@
      (fn [t] => @sql_inject)
      fl inj r
 
-fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs) =
+fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs)
+    : sql_exp [tn = ofs ++ fs] [] [] bool =
     @foldR2 [sql_injectable] [id]
      [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool]
      (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
@@ -15,7 +16,7 @@
      fl m r [_] !
 
 fun joiner [tn1 :: Name] [tn2 :: Name] [fs] [ofs1] [ofs2] [[tn1] ~ [tn2]] [fs ~ ofs1] [fs ~ ofs2]
-           (fl : folder fs) =
+           (fl : folder fs) : sql_exp [tn1 = ofs1 ++ fs, tn2 = ofs2 ++ fs] [] [] bool =
     @fold
      [fn key => rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool]
      (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
@@ -25,3 +26,26 @@
          (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2]}))
      (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE))
      fl [_] [_] ! !
+
+fun insertIfMissing [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
+                    [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
+                    (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
+                    (vs : $(keyCols ++ otherCols))
+                    (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
+                    (ofl : folder otherCols) (oinj : $(map sql_injectable otherCols))
+    : transaction bool =
+    alreadyThere <- oneRowE1 (SELECT COUNT( * ) > 0
+                              FROM t
+                              WHERE {@selector [#T] ! kfl kinj (vs --- _)});
+    if alreadyThere then
+        return False
+    else
+        dml (insert t (@sqexps kfl kinj (vs --- _)
+                        ++ @sqexps ofl oinj (vs --- _)));
+        return True
+
+fun deleteByKey [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
+    [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
+    (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
+    (vs : $keyCols) (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols)) =
+    dml (delete t (@selector [#T] ! kfl kinj vs))
diff -r 744bf911dcc6 -r 6ebc2ca594b7 sql.urs
--- a/sql.urs	Tue Jun 14 08:55:15 2011 -0400
+++ b/sql.urs	Sun Dec 11 14:04:34 2011 -0500
@@ -15,3 +15,19 @@
                => folder fs
                -> sql_exp [tn1 = ofs1 ++ fs, tn2 = ofs2 ++ fs] [] [] bool
 (* Declare equality of same-named columns from two tables. *)
+
+val insertIfMissing : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
+                      -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
+                      => sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
+                      -> $(keyCols ++ otherCols)
+                      -> folder keyCols -> $(map sql_injectable keyCols)
+                      -> folder otherCols -> $(map sql_injectable otherCols)
+                      -> transaction bool
+(* Insert a row into an SQL table if its key isn't already present, returning [False] iff the key was already present *)
+
+val deleteByKey : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
+                  -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
+                  => sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
+                  -> $keyCols -> folder keyCols -> $(map sql_injectable keyCols)
+                  -> transaction {}
+(* Delete a row from a table by matching its primary key against a given record. *)