Allow subqueries to reference aggregate-only columns of free tables; treat non-COUNT aggregate functions as possibly returning NULL

10 files changed, 145 insertions, 121 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index a91fd498..8ca2e81c 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -291,8 +291,8 @@ val check : fs ::: {Type}
 
 (*** Queries *)
 
-con sql_query :: {{Type}} -> {{Type}} -> {Type} -> Type
-con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
+con sql_query :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
+con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
 
 con sql_subset :: {{Type}} -> {{Type}} -> Type
 val sql_subset : keep_drop :: {({Type} * {Type})}
@@ -314,7 +314,7 @@ val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
                      -> fieldsOf t fs -> name :: Name
                      -> t -> sql_from_items free [name = fs]
 val sql_from_query : free ::: {{Type}} -> fs ::: {Type} -> name :: Name
-                     -> sql_query free [] fs
+                     -> sql_query free [] [] fs
                      -> sql_from_items free [name = fs]
 val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
                      -> [tabs1 ~ tabs2]
@@ -353,6 +353,7 @@ val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::
        -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
 
 val sql_query1 : free ::: {{Type}}
+                 -> afree ::: {{Type}}
                  -> tables ::: {{Type}}
                  -> grouped ::: {{Type}}
                  -> selectedFields ::: {{Type}}
@@ -360,33 +361,35 @@ val sql_query1 : free ::: {{Type}}
                  -> empties :: {Unit}
                  -> [free ~ tables]
                  => [free ~ grouped]
+                 => [afree ~ tables]
                  => [empties ~ selectedFields]
                  => {Distinct : bool,
                      From : sql_from_items free tables,
-                     Where : sql_exp (free ++ tables) [] [] bool,
+                     Where : sql_exp (free ++ tables) afree [] bool,
                      GroupBy : sql_subset tables grouped,
-                     Having : sql_exp (free ++ grouped) tables [] bool,
+                     Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool,
                      SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
-                     SelectExps : $(map (sql_exp (free ++ grouped) tables [])
+                     SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [])
                                             selectedExps) }
-                 -> sql_query1 free tables selectedFields selectedExps
+                 -> sql_query1 free afree tables selectedFields selectedExps
 
 type sql_relop 
 val sql_union : sql_relop
 val sql_intersect : sql_relop
 val sql_except : sql_relop
 val sql_relop : free ::: {{Type}}
+                -> afree ::: {{Type}}
                 -> tables1 ::: {{Type}}
                 -> tables2 ::: {{Type}}
                 -> selectedFields ::: {{Type}}
                 -> selectedExps ::: {Type}
                 -> sql_relop
-                -> sql_query1 free tables1 selectedFields selectedExps
-                -> sql_query1 free tables2 selectedFields selectedExps
-                -> sql_query1 free [] selectedFields selectedExps
-val sql_forget_tables : free ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
-                        -> sql_query1 free tables selectedFields selectedExps
-                        -> sql_query1 free [] selectedFields selectedExps
+                -> sql_query1 free afree tables1 selectedFields selectedExps
+                -> sql_query1 free afree tables2 selectedFields selectedExps
+                -> sql_query1 free afree [] selectedFields selectedExps
+val sql_forget_tables : free ::: {{Type}} -> afree ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
+                        -> sql_query1 free afree tables selectedFields selectedExps
+                        -> sql_query1 free afree [] selectedFields selectedExps
 
 type sql_direction
 val sql_asc : sql_direction
@@ -408,15 +411,16 @@ val sql_no_offset : sql_offset
 val sql_offset : int -> sql_offset
 
 val sql_query : free ::: {{Type}}
+                -> afree ::: {{Type}}
                 -> tables ::: {{Type}}
                 -> selectedFields ::: {{Type}}
                 -> selectedExps ::: {Type}
                 -> [free ~ tables]
-                => {Rows : sql_query1 free tables selectedFields selectedExps,
+                => {Rows : sql_query1 free afree tables selectedFields selectedExps,
                     OrderBy : sql_order_by (free ++ tables) selectedExps,
                     Limit : sql_limit,
                     Offset : sql_offset}
-                -> sql_query free selectedFields selectedExps
+                -> sql_query free afree selectedFields selectedExps
 
 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
                 -> fieldType ::: Type -> agg ::: {{Type}}
@@ -493,8 +497,8 @@ class sql_summable
 val sql_summable_int : sql_summable int
 val sql_summable_float : sql_summable float
 val sql_summable_option : t ::: Type -> sql_summable t -> sql_summable (option t)
-val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t t
-val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t t
+val sql_avg : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
+val sql_sum : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
 
 class sql_maxable
 val sql_maxable_int : sql_maxable int
@@ -502,8 +506,8 @@ val sql_maxable_float : sql_maxable float
 val sql_maxable_string : sql_maxable string
 val sql_maxable_time : sql_maxable time
 val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t)
-val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t t
-val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t t
+val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
+val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
 
 con sql_nfunc :: Type -> Type
 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
@@ -526,7 +530,7 @@ val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} ->
                    -> sql_exp tables agg exps (option t)
 
 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type
-                   -> sql_query tables [] [nm = t]
+                   -> sql_query tables agg [] [nm = t]
                    -> sql_exp tables agg exps t
 
 (*** Executing queries *)
@@ -534,7 +538,7 @@ val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} ->
 val query : tables ::: {{Type}} -> exps ::: {Type}
             -> [tables ~ exps] =>
                   state ::: Type
-                  -> sql_query [] tables exps
+                  -> sql_query [] [] tables exps
                   -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                       -> state
                       -> transaction state)
@@ -838,21 +842,21 @@ val periodic : int -> task_kind unit
 type sql_policy
 
 val sendClient : tables ::: {{Type}} -> exps ::: {Type}
-                 -> [tables ~ exps] => sql_query [] tables exps
+                 -> [tables ~ exps] => sql_query [] [] tables exps
                  -> sql_policy
 
 val sendOwnIds : sql_sequence -> sql_policy
 
 val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
-                => sql_query [] ([New = fs] ++ tables) []
+                => sql_query [] [] ([New = fs] ++ tables) []
                 -> sql_policy
 
 val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
-                => sql_query [] ([Old = fs] ++ tables) []
+                => sql_query [] [] ([Old = fs] ++ tables) []
                 -> sql_policy
 
 val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
-                => sql_query [] ([Old = fs, New = fs] ++ tables) []
+                => sql_query [] [] ([Old = fs, New = fs] ++ tables) []
                 -> sql_policy
 
 val also : sql_policy -> sql_policy -> sql_policy
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 3153cc32..d0c2e7a1 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -254,7 +254,7 @@ fun app [m] (_ : monad m) [a] f =
     end
 
 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
-             [tables ~ exps] (q : sql_query [] tables exps)
+             [tables ~ exps] (q : sql_query [] [] tables exps)
              (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
     ls <- query q
                 (fn fs acc => return (f fs :: acc))
@@ -262,7 +262,7 @@ fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
     return (rev ls)
 
 fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
-             [tables ~ exps] (q : sql_query [] tables exps)
+             [tables ~ exps] (q : sql_query [] [] tables exps)
              (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
     ls <- query q
                 (fn fs acc => v <- f fs; return (v :: acc))
@@ -270,7 +270,7 @@ fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
     return (rev ls)
 
 fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
-             [tables ~ exps] (q : sql_query [] tables exps)
+             [tables ~ exps] (q : sql_query [] [] tables exps)
              (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
     ls <- query q
                 (fn fs acc => v <- f fs;
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index 9ad738f1..8284510d 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -53,19 +53,19 @@ val app : m ::: (Type -> Type) -> monad m -> a ::: Type
 
 val mapQuery : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
                -> [tables ~ exps] =>
-    sql_query [] tables exps
+    sql_query [] [] tables exps
     -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> t)
     -> transaction (list t)
 
 val mapQueryM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
                -> [tables ~ exps] =>
-    sql_query [] tables exps
+    sql_query [] [] tables exps
     -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t)
     -> transaction (list t)
 
 val mapQueryPartialM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
                -> [tables ~ exps] =>
-    sql_query [] tables exps
+    sql_query [] [] tables exps
     -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t))
     -> transaction (list t)
 
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 83d5b6af..0fdbae7a 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -215,40 +215,40 @@ fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {
           <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
       <xml/>
 
-fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] [])
+fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
            (f : $fs -> state -> transaction state) (i : state) =
     query q (fn r => f r.t) i
 
-fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] [])
+fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
             (f : $fs -> state -> state) (i : state) =
     query q (fn r s => return (f r.t s)) i
 
-fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] tables exps) =
+fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] [] tables exps) =
     query q
     (fn r ls => return (r :: ls))
     []
 
-fun queryL1 [t ::: Name] [fs ::: {Type}] (q : sql_query [] [t = fs] []) =
+fun queryL1 [t ::: Name] [fs ::: {Type}] (q : sql_query [] [] [t = fs] []) =
     query q
     (fn r ls => return (r.t :: ls))
     []
 
 fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
-           [tables ~ exps] (q : sql_query [] tables exps)
+           [tables ~ exps] (q : sql_query [] [] tables exps)
            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                 -> transaction unit) =
     query q
           (fn fs _ => f fs)
           ()
 
-fun queryI1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] [])
+fun queryI1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] [])
             (f : $fs -> transaction unit) =
     query q
           (fn fs _ => f fs.nm)
           ()
 
 fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-           [tables ~ exps] (q : sql_query [] tables exps)
+           [tables ~ exps] (q : sql_query [] [] tables exps)
            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                 -> xml ctx inp []) =
     query q
@@ -256,14 +256,14 @@ fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Ty
           <xml/>
 
 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-            (q : sql_query [] [nm = fs] [])
+            (q : sql_query [] [] [nm = fs] [])
             (f : $fs -> xml ctx inp []) =
     query q
           (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
           <xml/>
 
 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-            [tables ~ exps] (q : sql_query [] tables exps)
+            [tables ~ exps] (q : sql_query [] [] tables exps)
             (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> transaction (xml ctx inp [])) =
     query q
@@ -273,7 +273,7 @@ fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {T
           <xml/>
 
 fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-             (q : sql_query [] [nm = fs] [])
+             (q : sql_query [] [] [nm = fs] [])
              (f : $fs -> transaction (xml ctx inp [])) =
     query q
           (fn fs acc =>
@@ -282,7 +282,7 @@ fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
           <xml/>
 
 fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-             (q : sql_query [] [] exps)
+             (q : sql_query [] [] [] exps)
              (f : $exps -> transaction (xml ctx inp [])) =
     query q
           (fn fs acc =>
@@ -292,42 +292,42 @@ fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
 
 fun hasRows [tables ::: {{Type}}] [exps ::: {Type}]
             [tables ~ exps]
-            (q : sql_query [] tables exps) =
+            (q : sql_query [] [] tables exps) =
     query q
           (fn _ _ => return True)
           False
 
 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
                 [tables ~ exps]
-                (q : sql_query [] tables exps) =
+                (q : sql_query [] [] tables exps) =
     query q
           (fn fs _ => return (Some fs))
           None
 
-fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) =
+fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) =
     query q
           (fn fs _ => return (Some fs.nm))
           None
 
-fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) =
+fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) =
     query q
           (fn fs _ => return (Some fs.nm))
           None
 
 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
-           [tables ~ exps] (q : sql_query [] tables exps) =
+           [tables ~ exps] (q : sql_query [] [] tables exps) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
               | Some r => r)
 
-fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) =
+fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
               | Some r => r.nm)
 
-fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) =
+fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index d86ae553..ed3b4c14 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -126,100 +126,100 @@ val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
 
 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 queryL1 : t ::: Name -> fs ::: {Type}
-              -> sql_query [] [t = fs] []
+              -> sql_query [] [] [t = fs] []
               -> transaction (list $fs)
 
 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 queryI1 : nm ::: Name -> fs ::: {Type}
-              -> sql_query [] [nm = fs] []
+              -> sql_query [] [] [nm = fs] []
               -> ($fs -> 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
diff --git a/src/compiler.sml b/src/compiler.sml
index c8bb036a..61fa23b1 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -1311,9 +1311,15 @@ fun compileC {cname, oname, ename, libs, profile, debug, link = link'} =
                 (compile, link)
 
         val link = foldl (fn (s, link) => link ^ " " ^ s) link link'
+
+        fun system s =
+            (if debug then
+                 print (s ^ "\n")
+             else
+                 ();
+             OS.Process.isSuccess (OS.Process.system s))
     in
-        OS.Process.isSuccess (OS.Process.system compile)
-        andalso OS.Process.isSuccess (OS.Process.system link)
+        system compile andalso system link
     end
 
 fun compile job =
diff --git a/src/mono_env.sig b/src/mono_env.sig
index c5ca7c0b..97d7d9ea 100644
--- a/src/mono_env.sig
+++ b/src/mono_env.sig
@@ -50,5 +50,6 @@ signature MONO_ENV = sig
     val patBindsN : Mono.pat -> int
 
     val liftExpInExp : int -> Mono.exp -> Mono.exp
-                                                 
+    val subExpInExp : (int * Mono.exp) -> Mono.exp -> Mono.exp
+
 end
diff --git a/src/mono_env.sml b/src/mono_env.sml
index 1df38db3..7f9a6e62 100644
--- a/src/mono_env.sml
+++ b/src/mono_env.sml
@@ -85,6 +85,19 @@ val liftExpInExp =
                 bind = fn (bound, U.Exp.RelE _) => bound + 1
                         | (bound, _) => bound}
 
+val subExpInExp =
+    U.Exp.mapB {typ = fn t => t,
+                exp = fn (xn, rep) => fn e =>
+                                  case e of
+                                      ERel xn' =>
+                                      (case Int.compare (xn', xn) of
+                                           EQUAL => #1 rep
+                                         | GREATER=> ERel (xn' - 1)
+                                         | LESS => e)
+                                    | _ => e,
+                bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
+                        | (ctx, _) => ctx}
+
 fun pushERel (env : env) x t eo =
     {datatypes = #datatypes env,
      constructors = #constructors env,
diff --git a/src/mono_reduce.sml b/src/mono_reduce.sml
index e61ed237..82d0a63d 100644
--- a/src/mono_reduce.sml
+++ b/src/mono_reduce.sml
@@ -57,7 +57,6 @@ fun simpleImpure (tsyms, syms) =
                               | ERecv _ => true
                               | ESleep _ => true
                               | ENamed n => IS.member (syms, n)
-                              | EError _ => true
                               | ERel n =>
                                 let
                                     val (_, t, _) = E.lookupERel env n
@@ -398,7 +397,10 @@ fun reduce file =
                         summarize d e @ [ReadCookie]
                       | EFfiApp (m, x, es) =>
                         if Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x) then
-                            List.concat (map (summarize d) es) @ [Unsure]
+                            List.concat (map (summarize d) es) @ [if m = "Basis" andalso String.isSuffix "_w" x then
+                                                                      WritePage
+                                                                  else
+                                                                      Unsure]
                         else
                             List.concat (map (summarize d) es)
                       | EApp ((EFfi _, _), e) => summarize d e
@@ -429,6 +431,7 @@ fun reduce file =
                                   | EApp (f, x) =>
                                     unravel (#1 f, passed + 1, List.revAppend (summarize d x,
                                                                                ls))
+                                  | EError _ => [Abort]
                                   | _ => [Unsure]
                         in
                             unravel (e, 0, [])
@@ -445,17 +448,25 @@ fun reduce file =
                       | ECase (e, pes, _) =>
                         let
                             val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes
+
+                            fun splitRel ls acc =
+                                case ls of
+                                    [] => (acc, false, ls)
+                                  | UseRel :: ls  => (acc, true, ls)
+                                  | v :: ls => splitRel ls (v :: acc)
+
+                            val (pre, used, post) = foldl (fn (ls, (pre, used, post)) =>
+                                                              let
+                                                                  val (pre', used', post') = splitRel ls []
+                                                              in
+                                                                  (pre' @ pre, used' orelse used, post' @ post)
+                                                              end)
+                                                    ([], false, []) lss
                         in
-                            case lss of
-                                [] => summarize d e
-                              | ls :: lss =>
-                                summarize d e
-                                @ (if List.all (fn ls' => ls' = ls) lss then
-                                       ls
-                                   else if length (List.filter (not o List.null) (ls :: lss)) <= 1 then
-                                       valOf (List.find (not o List.null) (ls :: lss))
-                                   else
-                                       [Unsure])
+                            summarize d e
+                            @ pre
+                            @ (if used then [UseRel] else [])
+                            @ post
                         end
                       | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
 
@@ -534,8 +545,8 @@ fun reduce file =
                                 val effs_e' = List.filter (fn x => x <> UseRel) effs_e'
                                 val effs_b = summarize 0 b
 
-                                (*val () = Print.prefaces "Try"
-                                                        [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan)),
+                                (*val () = Print.fprefaces outf "Try"
+                                                        [(*("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan)),*)
                                                          ("e'", MonoPrint.p_exp env e'),
                                                          ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
                                                          ("e'_eff", p_events effs_e'),
diff --git a/src/monoize.sml b/src/monoize.sml
index 30dfdd46..4295811a 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -236,9 +236,9 @@ fun monoType env =
                     (L'.TFfi ("Basis", "string"), loc)
                   | L.CFfi ("Basis", "sql_sequence") =>
                     (L'.TFfi ("Basis", "string"), loc)
-                  | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_query"), _), _), _), _), _), _) =>
+                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_query"), _), _), _), _), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
-                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_query1"), _), _), _), _), _), _), _), _) =>
+                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_query1"), _), _), _), _), _), _), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
                   | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_from_items"), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
@@ -1908,7 +1908,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                  end
                | _ => poly ())
 
-          | L.ECApp ((L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_query"), _), _), _), _), _), _), _), _) =>
+          | L.ECApp ((L.ECApp ((L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_query"), _), _), _), _), _), _), _), _), _), _) =>
             let
                 fun sc s = (L'.EPrim (Prim.String s), loc)
                 val s = (L'.TFfi ("Basis", "string"), loc)
@@ -1934,7 +1934,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
               (L.ECApp (
                (L.ECApp (
                 (L.ECApp (
-                 (L.EFfi ("Basis", "sql_query1"), _),
+                 (L.ECApp (
+                  (L.EFfi ("Basis", "sql_query1"), _),
+                  _), _),
                  _), _),
                 (L.CRecord (_, tables), _)), _),
                (L.CRecord (_, grouped), _)), _),
@@ -2592,7 +2594,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             (L.ECApp (
              (L.ECApp (
               (L.ECApp (
-               (L.EFfi ("Basis", "sql_forget_tables"), _),
+               (L.ECApp (
+                (L.EFfi ("Basis", "sql_forget_tables"), _),
+                _), _),
                _), _),
               _), _),
              _), _),
@@ -2625,7 +2629,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
               (L.EFfi ("Basis", "sql_count"), _),
               _), _),
              _), _),
-            _) => ((L'.EPrim (Prim.String "COALESCE(COUNT(*),0)"), loc),
+            _) => ((L'.EPrim (Prim.String "COUNT(*)"), loc),
                    fm)
 
           | L.ECApp (
@@ -2640,18 +2644,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
              _), _),
             t) =>
             let
-                val default =
-                    case #1 t of
-                        L.CFfi ("Basis", s) =>
-                        SOME (case s of
-                             "int" => "0"
-                           | "float" => "0.0"
-                           | "string" => "''"
-                           | "time" => "0"
-                           | _ => raise Fail "Illegal type of sql_aggregate [1]")
-                      | L.CApp ((L.CFfi ("Basis", "option"), _), _) => NONE
-                      | _ => raise Fail "Illegal type of sql_aggregate [2]"
-
                 val s = (L'.TFfi ("Basis", "string"), loc)
                 fun sc s = (L'.EPrim (Prim.String s), loc)
 
@@ -2659,13 +2651,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                                    sc "(",
                                    (L'.ERel 0, loc),
                                    sc ")"]
-
-                val main = case default of
-                               NONE => main
-                             | SOME default =>
-                               strcat [sc "COALESCE(",
-                                       main,
-                                       sc ("," ^ default ^ ")")]
             in
                 ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
                            (L'.EAbs ("e1", s, (L'.TFun (s, s), loc), main), loc)), loc),
@@ -2682,13 +2667,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TRecord [], loc),
                        (L'.ERecord [], loc)), loc),
              fm)
-          | L.ECApp ((L.EFfi ("Basis", "sql_avg"), _), _) =>
-            ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
-                       (L'.EPrim (Prim.String "AVG"), loc)), loc),
+          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_avg"), _), _), _), _) =>
+            ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun ((L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc)), loc),
+                       (L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+                                 (L'.EPrim (Prim.String "AVG"), loc)), loc)), loc),
              fm)
-          | L.ECApp ((L.EFfi ("Basis", "sql_sum"), _), _) =>
-            ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
-                       (L'.EPrim (Prim.String "SUM"), loc)), loc),
+          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_sum"), _), _), _), _) =>
+            ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun ((L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc)), loc),
+                       (L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+                                 (L'.EPrim (Prim.String "SUM"), loc)), loc)), loc),
              fm)
 
           | L.EFfi ("Basis", "sql_arith_int") => ((L'.ERecord [], loc), fm)
@@ -2701,13 +2688,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TRecord [], loc),
                        (L'.ERecord [], loc)), loc),
              fm)
-          | L.ECApp ((L.EFfi ("Basis", "sql_max"), _), _) =>
-            ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
-                       (L'.EPrim (Prim.String "MAX"), loc)), loc),
+          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_max"), _), _), _), _) =>
+            ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun ((L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc)), loc),
+                       (L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+                                 (L'.EPrim (Prim.String "MAX"), loc)), loc)), loc),
              fm)
-          | L.ECApp ((L.EFfi ("Basis", "sql_min"), _), _) =>
-            ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
-                       (L'.EPrim (Prim.String "MIN"), loc)), loc),
+          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_min"), _), _), _), _) =>
+            ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun ((L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc)), loc),
+                       (L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc),
+                                 (L'.EPrim (Prim.String "MIN"), loc)), loc)), loc),
              fm)
 
           | L.EFfi ("Basis", "sql_asc") => ((L'.EPrim (Prim.String ""), loc), fm)