# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1325364594 18000
# Node ID 875221eee9879ac1cca67d951a4732069c747288
# Parent  6cd839818393a557eb4b9fd62681421a64f89bbb
Sql.lookup

diff -r 6cd839818393 -r 875221eee987 sql.ur
--- a/sql.ur	Thu Dec 29 14:15:02 2011 -0500
+++ b/sql.ur	Sat Dec 31 15:49:54 2011 -0500
@@ -50,3 +50,13 @@
     (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
     (vs : $keyCols) =
     dml (delete t (@selector [#T] ! kfl kinj vs))
+
+fun lookup [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
+           [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
+           (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
+           (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
+           (vs : $keyCols)
+    : transaction (option $otherCols) =
+      oneOrNoRows1 (SELECT t.{{otherCols}}
+                    FROM t
+                    WHERE {@selector [#T] ! kfl kinj (vs --- _)})
diff -r 6cd839818393 -r 875221eee987 sql.urs
--- a/sql.urs	Thu Dec 29 14:15:02 2011 -0500
+++ b/sql.urs	Sat Dec 31 15:49:54 2011 -0500
@@ -32,3 +32,10 @@
                   -> $keyCols
                   -> transaction {}
 (* Delete a row from a table by matching its primary key against a given record. *)
+
+val lookup : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
+             -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
+             => folder keyCols -> $(map sql_injectable keyCols)
+             -> sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
+             -> $keyCols -> transaction (option $otherCols)
+(* Get the further columns associated with a table key. *)