annotate sql.urs @ 29:7530b2b54353

Update for Ur/Web's new type class handling
author Adam Chlipala <adam@chlipala.net>
date Sun, 29 Jul 2012 12:27:36 -0400
parents c1da0e3749b3
children
rev   line source
adam@6 1 (** Common metaprogramming patterns for SQL syntax construction *)
adam@6 2
adam@6 3 val sqexps : env ::: {{Type}} -> fields ::: {Type} -> folder fields -> $(map sql_injectable fields)
adam@6 4 -> $fields -> $(map (sql_exp env [] []) fields)
adam@6 5 (* Convert a record of Ur values into a record of SQL expressions *)
adam@6 6
adam@6 7 val selector : tn :: Name -> fs ::: {Type} -> ofs ::: {Type} -> [fs ~ ofs]
adam@6 8 => folder fs -> $(map sql_injectable fs) -> $fs
adam@6 9 -> sql_exp [tn = ofs ++ fs] [] [] bool
adam@6 10 (* Build a boolean SQL expression expressing equality of some fields of a table
adam@6 11 * row with a record of Ur values *)
adam@13 12
adam@13 13 val joiner : tn1 :: Name -> tn2 :: Name -> fs ::: {Type} -> ofs1 ::: {Type} -> ofs2 ::: {Type}
adam@13 14 -> [[tn1] ~ [tn2]] => [fs ~ ofs1] => [fs ~ ofs2]
adam@13 15 => folder fs
adam@13 16 -> sql_exp [tn1 = ofs1 ++ fs, tn2 = ofs2 ++ fs] [] [] bool
adam@13 17 (* Declare equality of same-named columns from two tables. *)
adam@15 18
adam@15 19 val insertIfMissing : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
adam@15 20 -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
adam@16 21 => folder keyCols -> $(map sql_injectable keyCols)
adam@16 22 -> folder otherCols -> $(map sql_injectable otherCols)
adam@16 23 -> sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
adam@15 24 -> $(keyCols ++ otherCols)
adam@15 25 -> transaction bool
adam@15 26 (* Insert a row into an SQL table if its key isn't already present, returning [False] iff the key was already present *)
adam@15 27
adam@15 28 val deleteByKey : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
adam@15 29 -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
adam@16 30 => folder keyCols -> $(map sql_injectable keyCols)
adam@16 31 -> sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
adam@16 32 -> $keyCols
adam@15 33 -> transaction {}
adam@15 34 (* Delete a row from a table by matching its primary key against a given record. *)
adam@19 35
adam@19 36 val lookup : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
adam@19 37 -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
adam@19 38 => folder keyCols -> $(map sql_injectable keyCols)
adam@19 39 -> sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
adam@19 40 -> $keyCols -> transaction (option $otherCols)
adam@19 41 (* Get the further columns associated with a table key. *)
adam@26 42
adam@26 43 val listify : lead :: Name -> cols ::: {Type} -> rest ::: {{Type}} -> [[lead] ~ rest]
adam@26 44 => folder cols -> $(map eq cols)
adam@26 45 -> sql_query [] [] ([lead = cols] ++ rest) []
adam@26 46 -> transaction (list ($cols * list $(map (fn ts => $ts) rest)))
adam@26 47 (* Shrink a set of table rows by summarizing into lists, keyed off of a lead table *)