From 447b60afccc89ef18d8f92a260dd1fcdf735898e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 31 Aug 2008 08:32:18 -0400 Subject: Laconic -> Ur --- lib/basis.lig | 249 ---------------------------------------------------------- 1 file changed, 249 deletions(-) delete mode 100644 lib/basis.lig (limited to 'lib/basis.lig') diff --git a/lib/basis.lig b/lib/basis.lig deleted file mode 100644 index f9fc23d5..00000000 --- a/lib/basis.lig +++ /dev/null @@ -1,249 +0,0 @@ -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 [] -- cgit v1.2.3