Mercurial > urweb
diff lib/ur/basis.urs @ 1775:6bc2a8cb3a67
Track whether SQL expressions may use window functions, in preparation for actual window function support
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 02 Jun 2012 15:35:58 -0400 |
| parents | acadf9d1214a |
| children | 8f28c3295148 |
line wrap: on
line diff
--- a/lib/ur/basis.urs Sat Jun 02 10:54:49 2012 -0400 +++ b/lib/ur/basis.urs Sat Jun 02 15:35:58 2012 -0400 @@ -305,15 +305,23 @@ 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_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 @@ -> [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 @@ => $(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 @@ => [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 @@ 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 @@ -> 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 @@ 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 @@ 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_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 @@ 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 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 *)