summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/basis.urs54
-rw-r--r--lib/ur/list.ur6
-rw-r--r--lib/ur/list.urs6
-rw-r--r--lib/ur/top.ur36
-rw-r--r--lib/ur/top.urs36
5 files changed, 71 insertions, 67 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