Track whether SQL expressions may use window functions, in preparation for actual window function support

3 files changed, 77 insertions, 69 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 760cc4d2..27b6393b 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -305,15 +305,23 @@ val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused :::
            OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
        -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
 
-con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
-val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+con allow_window :: {Unit}
+con disallow_window :: {Unit}
+
+con sql_exp :: {{Type}} (* Free tables, for normal use *)
+    -> {{Type}}         (* Free tables, for use in arguments to aggregate functions *)
+    -> {Type}           (* Free ad-hoc variables *)
+    -> {Unit}           (* Allow window functions here?  ([allow_window] indicates yes.) *)
+    -> Type             (* SQL type of this expression *)
+    -> Type
+val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type
                      -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type}
                      -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] =>
-                     sql_exp fs agg exps t
-                     -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t
+                     sql_exp fs agg exps aw t
+                     -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') aw t
 
 val check : fs ::: {Type}
-            -> sql_exp [] [] fs bool
+            -> sql_exp [] [] fs disallow_window bool
             -> sql_constraint fs []
 
 
@@ -351,7 +359,7 @@ val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type
 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
                      -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
     => sql_from_items free tabs1 -> sql_from_items free tabs2
-       -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
+       -> sql_exp (free ++ tabs1 ++ tabs2) [] [] disallow_window bool
        -> sql_from_items free (tabs1 ++ tabs2)
 
 class nullify :: Type -> Type -> Type
@@ -362,14 +370,14 @@ val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type
                      -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
     => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
        -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
-       -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
+       -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] disallow_window bool
        -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
 
 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
                      -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
     => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
        -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
-       -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
+       -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] disallow_window bool
        -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
 
 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
@@ -377,7 +385,7 @@ val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::
     => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
        -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
        -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
-       -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
+       -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] disallow_window bool
        -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
 
 val sql_query1 : free ::: {{Type}}
@@ -393,11 +401,11 @@ val sql_query1 : free ::: {{Type}}
                  => [empties ~ selectedFields]
                  => {Distinct : bool,
                      From : sql_from_items free tables,
-                     Where : sql_exp (free ++ tables) afree [] bool,
+                     Where : sql_exp (free ++ tables) afree [] disallow_window bool,
                      GroupBy : sql_subset tables grouped,
-                     Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool,
+                     Having : sql_exp (free ++ grouped) (afree ++ tables) [] disallow_window bool,
                      SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
-                     SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [])
+                     SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [] allow_window)
                                             selectedExps) }
                  -> sql_query1 free afree tables selectedFields selectedExps
 
@@ -427,7 +435,7 @@ val sql_desc : sql_direction
 con sql_order_by :: {{Type}} -> {Type} -> Type
 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
-                        -> sql_exp tables [] exps t -> sql_direction
+                        -> sql_exp tables [] exps allow_window t -> sql_direction
                         -> sql_order_by tables exps
                         -> sql_order_by tables exps
 val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type}
@@ -454,42 +462,42 @@ val sql_query : free ::: {{Type}}
                 -> sql_query free afree selectedFields selectedExps
 
 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
-                -> fieldType ::: Type -> agg ::: {{Type}}
+                -> aw ::: {Unit} -> fieldType ::: Type -> agg ::: {{Type}}
                 -> exps ::: {Type}
                 -> tab :: Name -> field :: Name
                 -> sql_exp
                        ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
-                       agg exps fieldType
+                       agg exps aw fieldType
 
-val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
+val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> aw ::: {Unit} -> t ::: Type -> rest ::: {Type}
               -> nm :: Name
-              -> sql_exp tabs agg ([nm = t] ++ rest) t
+              -> sql_exp tabs agg ([nm = t] ++ rest) aw t
 
 class sql_injectable
 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
 
 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                 -> t ::: Type
-                 -> sql_injectable t -> t -> sql_exp tables agg exps t
+                 -> aw ::: {Unit} -> t ::: Type
+                 -> sql_injectable t -> t -> sql_exp tables agg exps aw t
 
 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                  -> t ::: Type
-                  -> sql_exp tables agg exps (option t)
-                  -> sql_exp tables agg exps bool
+                  -> aw ::: {Unit} -> t ::: Type
+                  -> sql_exp tables agg exps aw (option t)
+                  -> sql_exp tables agg exps aw bool
 
 val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                  -> t ::: Type
-                  -> sql_exp tables agg exps (option t)
-                  -> sql_exp tables agg exps t
-                  -> sql_exp tables agg exps t
+                  -> aw ::: {Unit} -> t ::: Type
+                  -> sql_exp tables agg exps aw (option t)
+                  -> sql_exp tables agg exps aw t
+                  -> sql_exp tables agg exps aw t
 
 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                       -> t ::: Type
-                       -> sql_exp tables agg exps bool
-                       -> sql_exp tables agg exps t
-                       -> sql_exp tables agg exps t
-                       -> sql_exp tables agg exps t
+                       -> aw ::: {Unit} -> t ::: Type
+                       -> sql_exp tables agg exps aw bool
+                       -> sql_exp tables agg exps aw t
+                       -> sql_exp tables agg exps aw t
+                       -> sql_exp tables agg exps aw t
 
 class sql_arith
 val sql_arith_int : sql_arith int
@@ -499,9 +507,9 @@ val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
 con sql_unary :: Type -> Type -> Type
 val sql_not : sql_unary bool bool
 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                -> arg ::: Type -> res ::: Type
-                -> sql_unary arg res -> sql_exp tables agg exps arg
-                -> sql_exp tables agg exps res
+                -> aw ::: {Unit} -> arg ::: Type -> res ::: Type
+                -> sql_unary arg res -> sql_exp tables agg exps aw arg
+                -> sql_exp tables agg exps aw res
 
 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
 
@@ -509,10 +517,10 @@ con sql_binary :: Type -> Type -> Type -> Type
 val sql_and : sql_binary bool bool bool
 val sql_or : sql_binary bool bool bool
 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
-                 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
-                 -> sql_exp tables agg exps arg2
-                 -> sql_exp tables agg exps res
+                 -> aw ::: {Unit} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
+                 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps aw arg1
+                 -> sql_exp tables agg exps aw arg2
+                 -> sql_exp tables agg exps aw res
 
 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
@@ -529,14 +537,14 @@ val sql_ge : t ::: Type -> sql_binary t t bool
 
 val sql_like : sql_binary string string bool
 
-val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                -> sql_exp tables agg exps int
+val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit}
+                -> sql_exp tables agg exps aw int
 
 con sql_aggregate :: Type -> Type -> Type
 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                    -> dom ::: Type -> ran ::: Type
-                    -> sql_aggregate dom ran -> sql_exp agg agg exps dom
-                    -> sql_exp tables agg exps ran
+                    -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type
+                    -> sql_aggregate dom ran -> sql_exp agg agg exps aw dom
+                    -> sql_exp tables agg exps aw ran
 
 val sql_count_col : t ::: Type -> sql_aggregate (option t) int
 
@@ -558,29 +566,29 @@ val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_
 
 con sql_nfunc :: Type -> Type
 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                -> t ::: Type
-                -> sql_nfunc t -> sql_exp tables agg exps t
+                -> aw ::: {Unit} -> t ::: Type
+                -> sql_nfunc t -> sql_exp tables agg exps aw t
 val sql_current_timestamp : sql_nfunc time
 
 con sql_ufunc :: Type -> Type -> Type
 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                -> dom ::: Type -> ran ::: Type
-                -> sql_ufunc dom ran -> sql_exp tables agg exps dom
-                -> sql_exp tables agg exps ran
+                -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type
+                -> sql_ufunc dom ran -> sql_exp tables agg exps aw dom
+                -> sql_exp tables agg exps aw ran
 val sql_octet_length : sql_ufunc blob int
 val sql_known : t ::: Type -> sql_ufunc t bool
 val sql_lower : sql_ufunc string string
 val sql_upper : sql_ufunc string string
 
-val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type
                    -> sql_injectable_prim t
-                   -> sql_exp tables agg exps t
-                   -> sql_exp tables agg exps (option t)
+                   -> sql_exp tables agg exps aw t
+                   -> sql_exp tables agg exps aw (option t)
 
-val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type
+val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> aw ::: {Unit} -> t ::: Type -> nt ::: Type
                    -> nullify t nt
                    -> sql_query tables agg [] [nm = t]
-                   -> sql_exp tables agg exps nt
+                   -> sql_exp tables agg exps aw nt
 
 (*** Executing queries *)
 
@@ -604,19 +612,19 @@ val tryDml : dml -> transaction (option string)
 
 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
              -> sql_table fields uniques
-             -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
+             -> $(map (fn t :: Type => sql_exp [] [] [] disallow_window t) fields)
              -> dml
 
 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
              [changed ~ unchanged] =>
-                $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
+                $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] disallow_window t) changed)
                 -> sql_table (changed ++ unchanged) uniques
-                -> sql_exp [T = changed ++ unchanged] [] [] bool
+                -> sql_exp [T = changed ++ unchanged] [] [] disallow_window bool
                 -> dml
 
 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
              -> sql_table fields uniques
-             -> sql_exp [T = fields] [] [] bool
+             -> sql_exp [T = fields] [] [] disallow_window bool
              -> dml
 
 (*** Sequences *)
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index e504204e..60774ba5 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -376,14 +376,14 @@ fun nonempty [fs] [us] (t : sql_table fs us) =
     oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
 
 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
-    [t ::: Type] (_ : sql_injectable (option t))
-    (e1 : sql_exp tables agg exps (option t))
-    (e2 : sql_exp tables agg exps (option t)) =
+    [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t))
+    (e1 : sql_exp tables agg exps aw (option t))
+    (e2 : sql_exp tables agg exps aw (option t)) =
     (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
 
 fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
-    [t ::: Type] (_ : sql_injectable (option t))
-    (e1 : sql_exp tables agg exps (option t))
+    [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t))
+    (e1 : sql_exp tables agg exps aw (option t))
     (e2 : option t) =
     case e2 of
         None => (SQL {e1} IS NULL)
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 489e744d..def3bc63 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -269,15 +269,15 @@ val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
                -> transaction bool
 
 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                 -> t ::: Type -> sql_injectable (option t)
-                 -> sql_exp tables agg exps (option t)
-                 -> sql_exp tables agg exps (option t)
-                 -> sql_exp tables agg exps bool
+                 -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t)
+                 -> sql_exp tables agg exps aw (option t)
+                 -> sql_exp tables agg exps aw (option t)
+                 -> sql_exp tables agg exps aw bool
 
 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                  -> t ::: Type -> sql_injectable (option t)
-                  -> sql_exp tables agg exps (option t)
+                  -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t)
+                  -> sql_exp tables agg exps aw (option t)
                   -> option t
-                  -> sql_exp tables agg exps bool
+                  -> sql_exp tables agg exps aw bool
 
 val mkRead' : t ::: Type -> (string -> option t) -> string -> read t