diff lib/ur/top.urs @ 1191:61c3139eab12

Subquery expressions
author Adam Chlipala <adamc@hcoop.net>
date Thu, 25 Mar 2010 15:44:24 -0400
parents 26fed2c4f5be
children 4172863d049d
line wrap: on
line diff
--- a/lib/ur/top.urs	Thu Mar 25 13:04:49 2010 -0400
+++ b/lib/ur/top.urs	Thu Mar 25 15:44:24 2010 -0400
@@ -126,91 +126,91 @@
 
 val queryL : tables ::: {{Type}} -> exps ::: {Type}
              -> [tables ~ exps] =>
-                  sql_query tables exps
+                  sql_query [] tables exps
                   -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables))
 
 val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
-             -> sql_query [t = fs] []
+             -> sql_query [] [t = fs] []
              -> ($fs -> state -> transaction state)
              -> state
              -> transaction state
 
 val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type
-              -> sql_query [t = fs] []
+              -> sql_query [] [t = fs] []
               -> ($fs -> state -> state)
               -> state
               -> transaction state
 
 val queryI : tables ::: {{Type}} -> exps ::: {Type}
              -> [tables ~ exps] =>
-             sql_query tables exps
+             sql_query [] tables exps
              -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> transaction unit)
              -> transaction unit
 
 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
              -> [tables ~ exps] =>
-             sql_query tables exps
+             sql_query [] tables exps
              -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> xml ctx inp [])
              -> transaction (xml ctx inp [])
 
 val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
-              -> sql_query [nm = fs] []
+              -> sql_query [] [nm = fs] []
               -> ($fs -> xml ctx inp [])
               -> transaction (xml ctx inp [])
 
 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
               -> [tables ~ exps] =>
-              sql_query tables exps
+              sql_query [] tables exps
               -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                   -> transaction (xml ctx inp []))
               -> transaction (xml ctx inp [])
 val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
-              -> sql_query [nm = fs] []
+              -> sql_query [] [nm = fs] []
               -> ($fs -> transaction (xml ctx inp []))
               -> transaction (xml ctx inp [])
 val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
-              -> sql_query [] exps
+              -> sql_query [] [] exps
               -> ($exps -> transaction (xml ctx inp []))
               -> transaction (xml ctx inp [])
 
 val hasRows : tables ::: {{Type}} -> exps ::: {Type}
               -> [tables ~ exps] =>
-    sql_query tables exps
+    sql_query [] tables exps
     -> transaction bool
 
 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
                   -> [tables ~ exps] =>
-                  sql_query tables exps
+                  sql_query [] tables exps
                   -> transaction
                          (option
                               $(exps
                                     ++ map (fn fields :: {Type} => $fields) tables))
 
 val oneOrNoRows1 : nm ::: Name -> fs ::: {Type}
-                   -> sql_query [nm = fs] []
+                   -> sql_query [] [nm = fs] []
                    -> transaction (option $fs)
 
 val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
                     -> [tabs ~ [nm]] =>
-    sql_query (mapU [] tabs) [nm = t]
+    sql_query [] (mapU [] tabs) [nm = t]
     -> transaction (option t)
 
 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
              -> [tables ~ exps] =>
-             sql_query tables exps
+             sql_query [] tables exps
              -> transaction
                     $(exps
                           ++ map (fn fields :: {Type} => $fields) tables)
 
 val oneRow1 : nm ::: Name -> fs ::: {Type}
-    -> sql_query [nm = fs] []
+    -> sql_query [] [nm = fs] []
     -> transaction $fs
 
 val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
                -> [tabs ~ [nm]] =>
-    sql_query (mapU [] tabs) [nm = t]
+    sql_query [] (mapU [] tabs) [nm = t]
     -> transaction t
 
 val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us