Mercurial > meta
changeset 19:875221eee987
Sql.lookup
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 31 Dec 2011 15:49:54 -0500 |
| parents | 6cd839818393 |
| children | 296807a9fd50 |
| files | sql.ur sql.urs |
| diffstat | 2 files changed, 17 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- 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 --- _)})
--- 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. *)