diff options
author | 2008-08-31 08:32:18 -0400 | |
---|---|---|
committer | 2008-08-31 08:32:18 -0400 | |
commit | 447b60afccc89ef18d8f92a260dd1fcdf735898e (patch) | |
tree | 93d1ffca9832084286525896afc4c17eaf5d23f4 /lib/basis.urs | |
parent | 508290e29047e068b9db4b02485fefd9e3ced81c (diff) |
Laconic -> Ur
Diffstat (limited to 'lib/basis.urs')
-rw-r--r-- | lib/basis.urs | 249 |
1 files changed, 249 insertions, 0 deletions
diff --git a/lib/basis.urs b/lib/basis.urs new file mode 100644 index 00000000..f9fc23d5 --- /dev/null +++ b/lib/basis.urs @@ -0,0 +1,249 @@ +type int +type float +type string + +type unit = {} + +datatype bool = False | True + + +(** SQL *) + +con sql_table :: {Type} -> Type + +(*** Queries *) + +con sql_query :: {{Type}} -> {Type} -> Type +con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type +con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type + +con sql_subset :: {{Type}} -> {{Type}} -> Type +val sql_subset : keep_drop :: {({Type} * {Type})} + -> sql_subset + (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc => + [nm] ~ acc => fields.1 ~ fields.2 => + [nm = fields.1 ++ fields.2] ++ acc) [] keep_drop) + (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc => + [nm] ~ acc => + [nm = fields.1] ++ acc) [] keep_drop) +val sql_subset_all : tables :: {{Type}} + -> sql_subset tables tables + +val sql_query1 : tables ::: {{Type}} + -> grouped ::: {{Type}} + -> selectedFields ::: {{Type}} + -> selectedExps ::: {Type} + -> {From : $(fold (fn nm => fn fields :: {Type} => fn acc => + [nm] ~ acc => [nm = sql_table fields] ++ acc) [] tables), + Where : sql_exp tables [] [] bool, + GroupBy : sql_subset tables grouped, + Having : sql_exp grouped tables [] bool, + SelectFields : sql_subset grouped selectedFields, + SelectExps : $(fold (fn nm => fn t :: Type => fn acc => + [nm] ~ acc => [nm = sql_exp grouped tables [] t] ++ acc) [] selectedExps) } + -> sql_query1 tables selectedFields selectedExps + +type sql_relop +val sql_union : sql_relop +val sql_intersect : sql_relop +val sql_except : sql_relop +val sql_relop : sql_relop + -> tables1 ::: {{Type}} + -> tables2 ::: {{Type}} + -> selectedFields ::: {{Type}} + -> selectedExps ::: {Type} + -> sql_query1 tables1 selectedFields selectedExps + -> sql_query1 tables2 selectedFields selectedExps + -> sql_query1 selectedFields selectedFields selectedExps + +type sql_direction +val sql_asc : sql_direction +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_order_by tables exps + -> sql_order_by tables exps + +type sql_limit +val sql_no_limit : sql_limit +val sql_limit : int -> sql_limit + +type sql_offset +val sql_no_offset : sql_offset +val sql_offset : int -> sql_offset + +val sql_query : tables ::: {{Type}} + -> selectedFields ::: {{Type}} + -> selectedExps ::: {Type} + -> {Rows : sql_query1 tables selectedFields selectedExps, + OrderBy : sql_order_by tables selectedExps, + Limit : sql_limit, + Offset : sql_offset} + -> sql_query selectedFields selectedExps + +val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> agg ::: {{Type}} + -> exps ::: {Type} + -> tab :: Name -> field :: Name + -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) agg exps fieldType + +val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} -> nm :: Name + -> sql_exp tabs agg ([nm = t] ++ rest) t + +class sql_injectable +val sql_bool : sql_injectable bool +val sql_int : sql_injectable int +val sql_float : sql_injectable float +val sql_string : sql_injectable string +val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type + -> sql_injectable t -> t -> sql_exp tables agg exps 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 + +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 + +type sql_comparison +val sql_eq : sql_comparison +val sql_ne : sql_comparison +val sql_lt : sql_comparison +val sql_le : sql_comparison +val sql_gt : sql_comparison +val sql_ge : sql_comparison +val sql_comparison : sql_comparison + -> tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type + -> sql_exp tables agg exps t -> sql_exp tables agg exps t + -> sql_exp tables agg exps bool + +val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> unit -> sql_exp tables agg exps int + +con sql_aggregate :: Type -> Type +val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type + -> sql_aggregate t -> sql_exp agg agg exps t -> sql_exp tables agg exps t + +class sql_summable +val sql_summable_int : sql_summable int +val sql_summable_float : sql_summable float +val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t +val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t + +class sql_maxable +val sql_maxable_int : sql_maxable int +val sql_maxable_float : sql_maxable float +val sql_maxable_string : sql_maxable string +val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t +val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t + + +(*** Executing queries *) + +con transaction :: Type -> Type +val return : t ::: Type + -> t -> transaction t +val bind : t1 ::: Type -> t2 ::: Type + -> transaction t1 -> (t1 -> transaction t2) + -> transaction t2 + +val query : tables ::: {{Type}} -> exps ::: {Type} + -> sql_query tables exps + -> state ::: Type + -> ($(fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) + -> $exps + -> state + -> transaction state) + -> state + -> transaction state + + +(** XML *) + +con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type + + +con xml :: {Unit} -> {Type} -> {Type} -> Type +val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use [] +val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent + -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit} + -> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner + -> bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner + -> $attrsGiven + -> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter + -> xml ctxInner useInner bindInner + -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner) +val join : ctx ::: {Unit} + -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type} + -> use1 ~ bind1 -> bind1 ~ bind2 + -> xml ctx use1 bind1 + -> xml ctx (use1 ++ bind1) bind2 + -> xml ctx use1 (bind1 ++ bind2) +val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type} + -> use1 ~ use2 + -> xml ctx use1 bind + -> xml ctx (use1 ++ use2) bind + +con xhtml = xml [Html] +con page = xhtml [] [] + +(*** HTML details *) + +con html = [Html] +con head = [Head] +con body = [Body] +con lform = [Body, LForm] + +val head : unit -> tag [] html head [] [] +val title : unit -> tag [] head [] [] [] + +val body : unit -> tag [] html body [] [] +con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit + -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] +con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit + -> tag attrs ([Body] ++ ctx) [] [] [] + +val br : bodyTagStandalone [] + +val p : bodyTag [] +val b : bodyTag [] +val i : bodyTag [] +val font : bodyTag [Size = int, Face = string] + +val h1 : bodyTag [] +val li : bodyTag [] + +val a : bodyTag [Link = page] + +val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type} + -> xml lform [] bind + -> xml ([Body] ++ ctx) [] [] +con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} => + ctx ::: {Unit} -> [LForm] ~ ctx + -> nm :: Name -> unit + -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty] +val textbox : lformTag string [] [] +val password : lformTag string [] [] +val ltextarea : lformTag string [] [] + +val checkbox : lformTag bool [] [] + +con radio = [Body, Radio] +val radio : lformTag string radio [] +val radioOption : unit -> tag [Value = string] radio [] [] [] + +con select = [Select] +val lselect : lformTag string select [] +val loption : unit -> tag [Value = string] select [] [] [] + +val submit : ctx ::: {Unit} -> [LForm] ~ ctx + -> use ::: {Type} -> unit + -> tag [Action = $use -> page] ([LForm] ++ ctx) ([LForm] ++ ctx) use [] |