summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-06-02 15:35:58 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-06-02 15:35:58 -0400
commitf4dab2b31d11cc6957c1a64a3ffe6261816d96d4 (patch)
tree1e06ff6455bda35dc28fb3f9601270a7f91cdc2e /lib
parentb3dec3df4038cf76821f43717673456c7f691030 (diff)
Track whether SQL expressions may use window functions, in preparation for actual window function support
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/basis.urs122
-rw-r--r--lib/ur/top.ur10
-rw-r--r--lib/ur/top.urs14
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