summaryrefslogtreecommitdiff
path: root/lib/ur/basis.urs
diff options
context:
space:
mode:
Diffstat (limited to 'lib/ur/basis.urs')
-rw-r--r--lib/ur/basis.urs106
1 files changed, 58 insertions, 48 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 98e620df..98390555 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -274,8 +274,8 @@ val check : fs ::: {Type}
(*** Queries *)
-con sql_query :: {{Type}} -> {Type} -> Type
-con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
+con sql_query :: {{Type}} -> {{Type}} -> {Type} -> Type
+con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
con sql_subset :: {{Type}} -> {{Type}} -> Type
val sql_subset : keep_drop :: {({Type} * {Type})}
@@ -290,78 +290,82 @@ val sql_subset_concat : big1 ::: {{Type}} -> little1 ::: {{Type}}
-> sql_subset big2 little2
-> sql_subset (big1 ++ big2) (little1 ++ little2)
-con sql_from_items :: {{Type}} -> Type
+con sql_from_items :: {{Type}} -> {{Type}} -> Type
-val sql_from_table : t ::: Type -> fs ::: {Type}
+val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
-> fieldsOf t fs -> name :: Name
- -> t -> sql_from_items [name = fs]
-val sql_from_comma : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
+ -> t -> sql_from_items free [name = fs]
+val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
-> [tabs1 ~ tabs2]
- => sql_from_items tabs1 -> sql_from_items tabs2
- -> sql_from_items (tabs1 ++ tabs2)
-val sql_inner_join : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
- -> [tabs1 ~ tabs2]
- => sql_from_items tabs1 -> sql_from_items tabs2
- -> sql_exp (tabs1 ++ tabs2) [] [] bool
- -> sql_from_items (tabs1 ++ tabs2)
+ => sql_from_items free tabs1 -> sql_from_items free tabs2
+ -> sql_from_items free (tabs1 ++ tabs2)
+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_from_items free (tabs1 ++ tabs2)
class nullify :: Type -> Type -> Type
val nullify_option : t ::: Type -> nullify (option t) (option t)
val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
-val sql_left_join : tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
- -> [tabs1 ~ tabs2]
+val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * 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 tabs1 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
- -> sql_exp (tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
- -> sql_from_items (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) 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_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
-val sql_right_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
- -> [tabs1 ~ 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 (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items tabs2
- -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
- -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
+ -> 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_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
-val sql_full_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
- -> [tabs1 ~ tabs2]
+val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
+ -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
=> $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
- -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1)
- -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
- -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
- -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) (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_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
-val sql_query1 : tables ::: {{Type}}
+val sql_query1 : free ::: {{Type}}
+ -> tables ::: {{Type}}
-> grouped ::: {{Type}}
-> selectedFields ::: {{Type}}
-> selectedExps ::: {Type}
-> empties :: {Unit}
- -> [empties ~ selectedFields]
+ -> [free ~ tables]
+ => [free ~ grouped]
+ => [empties ~ selectedFields]
=> {Distinct : bool,
- From : sql_from_items tables,
- Where : sql_exp tables [] [] bool,
+ From : sql_from_items free tables,
+ Where : sql_exp (free ++ tables) [] [] bool,
GroupBy : sql_subset tables grouped,
- Having : sql_exp grouped tables [] bool,
+ Having : sql_exp (free ++ grouped) tables [] bool,
SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
- SelectExps : $(map (sql_exp grouped tables [])
+ SelectExps : $(map (sql_exp (free ++ grouped) tables [])
selectedExps) }
- -> sql_query1 tables selectedFields selectedExps
+ -> sql_query1 free tables selectedFields selectedExps
type sql_relop
val sql_union : sql_relop
val sql_intersect : sql_relop
val sql_except : sql_relop
-val sql_relop : tables1 ::: {{Type}}
+val sql_relop : free ::: {{Type}}
+ -> tables1 ::: {{Type}}
-> tables2 ::: {{Type}}
-> selectedFields ::: {{Type}}
-> selectedExps ::: {Type}
-> sql_relop
- -> sql_query1 tables1 selectedFields selectedExps
- -> sql_query1 tables2 selectedFields selectedExps
- -> sql_query1 [] selectedFields selectedExps
-val sql_forget_tables : tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
- -> sql_query1 tables selectedFields selectedExps
- -> sql_query1 [] selectedFields selectedExps
+ -> 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
type sql_direction
val sql_asc : sql_direction
@@ -382,14 +386,16 @@ type sql_offset
val sql_no_offset : sql_offset
val sql_offset : int -> sql_offset
-val sql_query : tables ::: {{Type}}
+val sql_query : free ::: {{Type}}
+ -> tables ::: {{Type}}
-> selectedFields ::: {{Type}}
-> selectedExps ::: {Type}
- -> {Rows : sql_query1 tables selectedFields selectedExps,
- OrderBy : sql_order_by tables selectedExps,
+ -> [free ~ tables]
+ => {Rows : sql_query1 free tables selectedFields selectedExps,
+ OrderBy : sql_order_by (free ++ tables) selectedExps,
Limit : sql_limit,
Offset : sql_offset}
- -> sql_query selectedFields selectedExps
+ -> sql_query free selectedFields selectedExps
val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
-> fieldType ::: Type -> agg ::: {{Type}}
@@ -495,12 +501,16 @@ val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} ->
-> sql_exp tables agg exps t
-> 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_exp tables agg exps t
+
(*** Executing queries *)
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)