diff sql.urs @ 19:875221eee987

Sql.lookup
author Adam Chlipala <adam@chlipala.net>
date Sat, 31 Dec 2011 15:49:54 -0500
parents 959583692166
children c1da0e3749b3
line wrap: on
line diff
--- 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. *)