adamc@56: type int adamc@56: type float adamc@56: type string adamc@436: type time adamc@91: adamc@119: type unit = {} adamc@119: adamc@186: datatype bool = False | True adamc@186: adamc@288: datatype option t = None | Some of t adamc@284: adamc@91: adamc@256: (** Basic type classes *) adamc@256: adamc@256: class eq adamc@256: val eq : t ::: Type -> eq t -> t -> t -> bool adamc@257: val ne : t ::: Type -> eq t -> t -> t -> bool adamc@256: val eq_int : eq int adamc@394: val eq_float : eq float adamc@256: val eq_string : eq string adamc@256: val eq_bool : eq bool adamc@437: val eq_time : eq time adamc@422: val mkEq : t ::: Type -> (t -> t -> bool) -> eq t adamc@256: adamc@389: class num adamc@417: val zero : t ::: Type -> num t -> t adamc@389: val neg : t ::: Type -> num t -> t -> t adamc@389: val plus : t ::: Type -> num t -> t -> t -> t adamc@389: val minus : t ::: Type -> num t -> t -> t -> t adamc@389: val times : t ::: Type -> num t -> t -> t -> t adamc@389: val div : t ::: Type -> num t -> t -> t -> t adamc@389: val mod : t ::: Type -> num t -> t -> t -> t adamc@389: val num_int : num int adamc@390: val num_float : num float adamc@389: adamc@391: class ord adamc@391: val lt : t ::: Type -> ord t -> t -> t -> bool adamc@391: val le : t ::: Type -> ord t -> t -> t -> bool adamc@391: val gt : t ::: Type -> ord t -> t -> t -> bool adamc@391: val ge : t ::: Type -> ord t -> t -> t -> bool adamc@391: val ord_int : ord int adamc@394: val ord_float : ord float adamc@394: val ord_string : ord string adamc@394: val ord_bool : ord bool adamc@437: val ord_time : ord time adamc@391: adamc@256: adamc@283: (** String operations *) adamc@283: adamc@283: val strcat : string -> string -> string adamc@283: adamc@286: class show adamc@286: val show : t ::: Type -> show t -> t -> string adamc@286: val show_int : show int adamc@286: val show_float : show float adamc@286: val show_string : show string adamc@286: val show_bool : show bool adamc@436: val show_time : show time adamc@452: val mkShow : t ::: Type -> (t -> string) -> show t adamc@286: adamc@290: class read adamc@290: val read : t ::: Type -> read t -> string -> option t adamc@292: val readError : t ::: Type -> read t -> string -> t adamc@292: (* [readError] calls [error] if the input is malformed. *) adamc@290: val read_int : read int adamc@290: val read_float : read float adamc@290: val read_string : read string adamc@290: val read_bool : read bool adamc@436: val read_time : read time adamc@288: adamc@283: adamc@564: (** * Monads *) adamc@564: adamc@564: class monad :: Type -> Type adamc@564: val return : m ::: (Type -> Type) -> t ::: Type adamc@564: -> monad m adamc@564: -> t -> m t adamc@564: val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type adamc@564: -> monad m adamc@564: -> m t1 -> (t1 -> m t2) adamc@564: -> m t2 adamc@564: adamc@456: con transaction :: Type -> Type adamc@564: val transaction_monad : monad transaction adamc@456: adamc@565: con source :: Type -> Type adamc@565: val source : t ::: Type -> t -> transaction (source t) adamc@575: val set : t ::: Type -> source t -> t -> transaction unit adamc@601: val get : t ::: Type -> source t -> transaction t adamc@565: adamc@565: con signal :: Type -> Type adamc@565: val signal_monad : monad signal adamc@565: val signal : t ::: Type -> source t -> signal t adamc@456: adamc@456: adamc@456: (** HTTP operations *) adamc@456: adamc@456: val requestHeader : string -> transaction (option string) adamc@456: adamc@459: con http_cookie :: Type -> Type adamc@459: val getCookie : t ::: Type -> http_cookie t -> transaction (option t) adamc@459: val setCookie : t ::: Type -> http_cookie t -> t -> transaction unit adamc@459: adamc@456: adamc@566: (** JavaScript-y gadgets *) adamc@566: adamc@566: val alert : string -> transaction unit adamc@694: val spawn : transaction unit -> transaction unit adamc@695: val sleep : int -> transaction unit adamc@566: adamc@566: adamc@678: (** Channels *) adamc@678: adamc@678: con channel :: Type -> Type adamc@678: val channel : t ::: Type -> transaction (channel t) adamc@678: val send : t ::: Type -> channel t -> t -> transaction unit adamc@678: val recv : t ::: Type -> channel t -> transaction t adamc@678: adamc@682: type client adamc@682: val self : transaction client adamc@682: adamc@678: adamc@203: (** SQL *) adamc@203: adamc@705: con sql_table :: {Type} -> {{Unit}} -> Type adamc@203: adamc@704: (*** Constraints *) adamc@704: adamc@705: con sql_constraints :: {Type} -> {{Unit}} -> Type adamc@705: (* Arguments: column types, uniqueness implications of constraints *) adamc@704: adamc@705: con sql_constraint :: {Type} -> {Unit} -> Type adamc@704: adamc@705: val no_constraint : fs ::: {Type} -> sql_constraints fs [] adamc@705: val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name adamc@705: -> sql_constraint fs unique adamc@705: -> sql_constraints fs [name = unique] adamc@705: val join_constraints : fs ::: {Type} adamc@705: -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2] adamc@705: => sql_constraints fs uniques1 -> sql_constraints fs uniques2 adamc@705: -> sql_constraints fs (uniques1 ++ uniques2) adamc@705: adamc@705: val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type} adamc@705: -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest] adamc@705: => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique) adamc@704: adamc@704: adamc@204: (*** Queries *) adamc@204: adamc@233: con sql_query :: {{Type}} -> {Type} -> Type adamc@233: con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type adamc@234: con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type adamc@204: adamc@223: con sql_subset :: {{Type}} -> {{Type}} -> Type adamc@223: val sql_subset : keep_drop :: {({Type} * {Type})} adamc@354: -> sql_subset adamc@621: (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop) adamc@621: (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop) adamc@354: val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables adamc@223: adamc@705: val sql_query1 : tables ::: {({Type} * {{Unit}})} adamc@354: -> grouped ::: {{Type}} adamc@354: -> selectedFields ::: {{Type}} adamc@354: -> selectedExps ::: {Type} adamc@705: -> {From : $(map (fn p :: ({Type} * {{Unit}}) => sql_table p.1 p.2) tables), adamc@705: Where : sql_exp (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] [] bool, adamc@705: GroupBy : sql_subset (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) grouped, adamc@705: Having : sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] bool, adamc@354: SelectFields : sql_subset grouped selectedFields, adamc@705: SelectExps : $(map (sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) []) adamc@705: selectedExps) } adamc@705: -> sql_query1 (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) selectedFields selectedExps adamc@229: adamc@229: type sql_relop adamc@229: val sql_union : sql_relop adamc@229: val sql_intersect : sql_relop adamc@229: val sql_except : sql_relop adamc@260: val sql_relop : tables1 ::: {{Type}} adamc@354: -> tables2 ::: {{Type}} adamc@354: -> selectedFields ::: {{Type}} adamc@354: -> selectedExps ::: {Type} adamc@354: -> sql_relop adamc@354: -> sql_query1 tables1 selectedFields selectedExps adamc@354: -> sql_query1 tables2 selectedFields selectedExps adamc@354: -> sql_query1 selectedFields selectedFields selectedExps adamc@229: adamc@230: type sql_direction adamc@230: val sql_asc : sql_direction adamc@230: val sql_desc : sql_direction adamc@230: adamc@234: con sql_order_by :: {{Type}} -> {Type} -> Type adamc@234: val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps adamc@234: val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type adamc@354: -> sql_exp tables [] exps t -> sql_direction adamc@354: -> sql_order_by tables exps adamc@354: -> sql_order_by tables exps adamc@230: adamc@231: type sql_limit adamc@231: val sql_no_limit : sql_limit adamc@231: val sql_limit : int -> sql_limit adamc@354: adamc@232: type sql_offset adamc@232: val sql_no_offset : sql_offset adamc@232: val sql_offset : int -> sql_offset adamc@232: adamc@229: val sql_query : tables ::: {{Type}} adamc@354: -> selectedFields ::: {{Type}} adamc@354: -> selectedExps ::: {Type} adamc@354: -> {Rows : sql_query1 tables selectedFields selectedExps, adamc@354: OrderBy : sql_order_by tables selectedExps, adamc@354: Limit : sql_limit, adamc@354: Offset : sql_offset} adamc@354: -> sql_query selectedFields selectedExps adamc@204: adamc@354: val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} adamc@354: -> fieldType ::: Type -> agg ::: {{Type}} adamc@354: -> exps ::: {Type} adamc@354: -> tab :: Name -> field :: Name adamc@354: -> sql_exp adamc@354: ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) adamc@354: agg exps fieldType adamc@234: adamc@354: val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} adamc@354: -> nm :: Name adamc@354: -> sql_exp tabs agg ([nm = t] ++ rest) t adamc@209: adamc@676: class sql_injectable_prim adamc@676: val sql_bool : sql_injectable_prim bool adamc@676: val sql_int : sql_injectable_prim int adamc@676: val sql_float : sql_injectable_prim float adamc@676: val sql_string : sql_injectable_prim string adamc@676: val sql_time : sql_injectable_prim time adamc@683: val sql_channel : t ::: Type -> sql_injectable_prim (channel t) adamc@683: val sql_client : sql_injectable_prim client adamc@678: adamc@221: class sql_injectable adamc@676: val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t adamc@676: val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t) adamc@676: adamc@354: val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} adamc@354: -> t ::: Type adamc@354: -> sql_injectable t -> t -> sql_exp tables agg exps t adamc@209: adamc@470: val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} adamc@470: -> t ::: Type adamc@470: -> sql_exp tables agg exps (option t) adamc@470: -> sql_exp tables agg exps bool adamc@470: adamc@559: class sql_arith adamc@559: val sql_int_arith : sql_arith int adamc@559: val sql_float_arith : sql_arith float adamc@559: adamc@220: con sql_unary :: Type -> Type -> Type adamc@220: val sql_not : sql_unary bool bool adamc@354: val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} adamc@354: -> arg ::: Type -> res ::: Type adamc@354: -> sql_unary arg res -> sql_exp tables agg exps arg adamc@354: -> sql_exp tables agg exps res adamc@220: adamc@559: val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t adamc@559: adamc@220: con sql_binary :: Type -> Type -> Type -> Type adamc@220: val sql_and : sql_binary bool bool bool adamc@220: val sql_or : sql_binary bool bool bool adamc@234: val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} adamc@354: -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type adamc@354: -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 adamc@354: -> sql_exp tables agg exps arg2 adamc@354: -> sql_exp tables agg exps res adamc@220: adamc@559: val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t adamc@559: val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t adamc@559: val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t adamc@559: val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t adamc@559: val sql_mod : sql_binary int int int adamc@559: adamc@559: val sql_eq : t ::: Type -> sql_binary t t bool adamc@559: val sql_ne : t ::: Type -> sql_binary t t bool adamc@559: val sql_lt : t ::: Type -> sql_binary t t bool adamc@559: val sql_le : t ::: Type -> sql_binary t t bool adamc@559: val sql_gt : t ::: Type -> sql_binary t t bool adamc@559: val sql_ge : t ::: Type -> sql_binary t t bool adamc@203: adamc@235: val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} adamc@544: -> sql_exp tables agg exps int adamc@235: adamc@236: con sql_aggregate :: Type -> Type adamc@354: val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} adamc@354: -> t ::: Type adamc@354: -> sql_aggregate t -> sql_exp agg agg exps t adamc@354: -> sql_exp tables agg exps t adamc@236: adamc@236: class sql_summable adamc@236: val sql_summable_int : sql_summable int adamc@236: val sql_summable_float : sql_summable float adamc@236: val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t adamc@236: val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t adamc@236: adamc@236: class sql_maxable adamc@236: val sql_maxable_int : sql_maxable int adamc@236: val sql_maxable_float : sql_maxable float adamc@236: val sql_maxable_string : sql_maxable string adamc@437: val sql_maxable_time : sql_maxable time adamc@236: val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t adamc@236: val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t adamc@236: adamc@441: con sql_nfunc :: Type -> Type adamc@441: val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} adamc@441: -> t ::: Type adamc@441: -> sql_nfunc t -> sql_exp tables agg exps t adamc@441: val sql_current_timestamp : sql_nfunc time adamc@441: adamc@235: adamc@243: (*** Executing queries *) adamc@243: adamc@354: val query : tables ::: {{Type}} -> exps ::: {Type} adamc@629: -> [tables ~ exps] => adamc@354: state ::: Type adamc@354: -> sql_query tables exps adamc@621: -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) adamc@354: -> state adamc@354: -> transaction state) adamc@354: -> state adamc@354: -> transaction state adamc@243: adamc@243: adamc@299: (*** Database mutators *) adamc@299: adamc@299: type dml adamc@299: val dml : dml -> transaction unit adamc@299: adamc@705: val insert : fields ::: {Type} -> uniques ::: {{Unit}} adamc@705: -> sql_table fields uniques adamc@621: -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) adamc@354: -> dml adamc@299: adamc@705: val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} -> adamc@629: [changed ~ unchanged] => adamc@621: $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) adamc@705: -> sql_table (changed ++ unchanged) uniques adamc@354: -> sql_exp [T = changed ++ unchanged] [] [] bool adamc@354: -> dml adamc@299: adamc@705: val delete : fields ::: {Type} -> uniques ::: {{Unit}} adamc@705: -> sql_table fields uniques adamc@354: -> sql_exp [T = fields] [] [] bool adamc@354: -> dml adamc@299: adamc@338: (*** Sequences *) adamc@338: adamc@338: type sql_sequence adamc@338: val nextval : sql_sequence -> transaction int adamc@338: adamc@299: adamc@203: (** XML *) adamc@203: adamc@139: con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type adamc@91: adamc@91: adamc@139: con xml :: {Unit} -> {Type} -> {Type} -> Type adamc@141: val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use [] adamc@354: val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} adamc@354: -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit} adamc@354: -> useOuter ::: {Type} -> useInner ::: {Type} adamc@354: -> bindOuter ::: {Type} -> bindInner ::: {Type} adamc@629: -> [attrsGiven ~ attrsAbsent] => adamc@629: [useOuter ~ useInner] => adamc@629: [bindOuter ~ bindInner] => adamc@629: $attrsGiven adamc@629: -> tag (attrsGiven ++ attrsAbsent) adamc@629: ctxOuter ctxInner useOuter bindOuter adamc@629: -> xml ctxInner useInner bindInner adamc@629: -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner) adamc@140: val join : ctx ::: {Unit} adamc@139: -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type} adamc@629: -> [use1 ~ bind1] => [bind1 ~ bind2] => adamc@354: xml ctx use1 bind1 adamc@354: -> xml ctx (use1 ++ bind1) bind2 adamc@354: -> xml ctx use1 (bind1 ++ bind2) adamc@354: val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} adamc@354: -> bind ::: {Type} adamc@629: -> [use1 ~ use2] => adamc@354: xml ctx use1 bind adamc@354: -> xml ctx (use1 ++ use2) bind adamc@91: adamc@110: con xhtml = xml [Html] adamc@139: con page = xhtml [] [] adamc@325: con xbody = xml [Body] [] [] adamc@326: con xtr = xml [Body, Tr] [] [] adamc@361: con xform = xml [Body, Form] [] [] adamc@110: adamc@204: (*** HTML details *) adamc@204: adamc@140: con html = [Html] adamc@140: con head = [Head] adamc@140: con body = [Body] adamc@361: con form = [Body, Form] adamc@332: con tabl = [Body, Table] adamc@332: con tr = [Body, Tr] adamc@93: adamc@691: val dyn : use ::: {Type} -> bind ::: {Type} -> unit adamc@691: -> tag [Signal = signal (xml body use bind)] body [] use bind adamc@568: adamc@140: val head : unit -> tag [] html head [] [] adamc@140: val title : unit -> tag [] head [] [] [] adamc@110: adamc@668: val body : unit -> tag [Onload = transaction unit] html body [] [] adamc@354: con bodyTag = fn (attrs :: {Type}) => adamc@354: ctx ::: {Unit} -> adamc@629: [[Body] ~ ctx] => adamc@354: unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] adamc@354: con bodyTagStandalone = fn (attrs :: {Type}) => adamc@354: ctx ::: {Unit} adamc@629: -> [[Body] ~ ctx] => adamc@354: unit -> tag attrs ([Body] ++ ctx) [] [] [] adamc@141: adamc@141: val br : bodyTagStandalone [] adamc@119: adamc@691: val span : bodyTag [] adamc@691: adamc@140: val p : bodyTag [] adamc@140: val b : bodyTag [] adamc@140: val i : bodyTag [] adamc@407: val tt : bodyTag [] adamc@140: val font : bodyTag [Size = int, Face = string] adamc@140: adamc@140: val h1 : bodyTag [] adamc@443: val h2 : bodyTag [] adamc@443: val h3 : bodyTag [] adamc@443: val h4 : bodyTag [] adamc@469: adamc@140: val li : bodyTag [] adamc@469: val ol : bodyTag [] adamc@469: val ul : bodyTag [] adamc@140: adamc@410: val hr : bodyTag [] adamc@410: adamc@566: val a : bodyTag [Link = transaction page, Onclick = transaction unit] adamc@140: adamc@361: val form : ctx ::: {Unit} -> bind ::: {Type} adamc@629: -> [[Body] ~ ctx] => adamc@354: xml form [] bind adamc@354: -> xml ([Body] ++ ctx) [] [] adamc@361: con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) => adamc@354: ctx ::: {Unit} adamc@629: -> [[Form] ~ ctx] => adamc@354: nm :: Name -> unit adamc@361: -> tag attrs ([Form] ++ ctx) inner [] [nm = ty] adamc@598: val textbox : formTag string [] [Value = string, Size = int, Source = source string] adamc@444: val password : formTag string [] [Value = string, Size = int] adamc@444: val textarea : formTag string [] [Rows = int, Cols = int] adamc@153: adamc@361: val checkbox : formTag bool [] [Checked = bool] adamc@190: adamc@153: con radio = [Body, Radio] adamc@361: val radio : formTag string radio [] adamc@153: val radioOption : unit -> tag [Value = string] radio [] [] [] adamc@142: adamc@154: con select = [Select] adamc@361: val select : formTag string select [] adamc@422: val option : unit -> tag [Value = string, Selected = bool] select [] [] [] adamc@154: adamc@568: val submit : ctx ::: {Unit} -> use ::: {Type} adamc@629: -> [[Form] ~ ctx] => adamc@354: unit adamc@406: -> tag [Value = string, Action = $use -> transaction page] adamc@361: ([Form] ++ ctx) ([Form] ++ ctx) use [] adamc@283: adamc@601: (*** AJAX-oriented widgets *) adamc@601: adamc@601: con cformTag = fn (attrs :: {Type}) => adamc@601: ctx ::: {Unit} adamc@629: -> [[Body] ~ ctx] => adamc@601: unit -> tag attrs ([Body] ++ ctx) [] [] [] adamc@601: adamc@601: val ctextbox : cformTag [Value = string, Size = int, Source = source string] adamc@601: val button : cformTag [Value = string, Onclick = transaction unit] adamc@601: adamc@325: (*** Tables *) adamc@325: adamc@629: val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => adamc@406: unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] [] adamc@629: val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] => adamc@406: unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] [] adamc@629: val th : other ::: {Unit} -> [other ~ [Body, Tr]] => adamc@406: unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] adamc@629: val td : other ::: {Unit} -> [other ~ [Body, Tr]] => adamc@406: unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] adamc@325: adamc@283: adamc@283: (** Aborting *) adamc@283: adamc@283: val error : t ::: Type -> xml [Body] [] [] -> t adamc@668: adamc@668: