Mercurial > urweb
changeset 602:1d34d916c206
Combine lib* directories
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 13 Jan 2009 15:23:48 -0500 |
| parents | 7c3c21eb5b4c |
| children | b1064de2b1f9 |
| files | Makefile.in clib/.dir jslib/urweb.js lib/basis.urs lib/c/.dir lib/js/urweb.js lib/top.ur lib/top.urs lib/ur/basis.urs lib/ur/top.ur lib/ur/top.urs |
| diffstat | 9 files changed, 977 insertions(+), 977 deletions(-) [+] |
line wrap: on
line diff
--- a/Makefile.in Tue Jan 13 15:17:11 2009 -0500 +++ b/Makefile.in Tue Jan 13 15:23:48 2009 -0500 @@ -13,19 +13,19 @@ smlnj: src/urweb.cm mlton: bin/urweb -c: clib/urweb.o clib/driver.o +c: lib/c/urweb.o lib/c/driver.o clean: rm -f src/*.mlton.grm.* src/*.mlton.lex.* \ src/urweb.cm src/urweb.mlb \ - clib/*.o + lib/c/*.o rm -rf .cm src/.cm -clib/urweb.o: src/c/urweb.c include/*.h - gcc -O3 -I include -c src/c/urweb.c -o clib/urweb.o $(CFLAGS) +lib/c/urweb.o: src/c/urweb.c include/*.h + gcc -O3 -I include -c src/c/urweb.c -o lib/c/urweb.o $(CFLAGS) -clib/driver.o: src/c/driver.c include/*.h - gcc -O3 -I include -c src/c/driver.c -o clib/driver.o $(CFLAGS) +lib/c/driver.o: src/c/driver.c include/*.h + gcc -O3 -I include -c src/c/driver.c -o lib/c/driver.o $(CFLAGS) src/urweb.cm: src/prefix.cm src/sources cat src/prefix.cm src/sources \ @@ -67,12 +67,12 @@ mkdir -p $(BIN) cp bin/urweb $(BIN)/ mkdir -p $(LIB_UR) - cp lib/*.urs $(LIB_UR)/ - cp lib/*.ur $(LIB_UR)/ + cp lib/ur/*.urs $(LIB_UR)/ + cp lib/ur/*.ur $(LIB_UR)/ mkdir -p $(LIB_C) - cp clib/*.o $(LIB_C)/ + cp lib/c/*.o $(LIB_C)/ mkdir -p $(LIB_JS) - cp jslib/*.js $(LIB_JS)/ + cp lib/js/*.js $(LIB_JS)/ mkdir -p $(INCLUDE) cp include/*.h $(INCLUDE)/ mkdir -p $(SITELISP)
--- a/jslib/urweb.js Tue Jan 13 15:17:11 2009 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,72 +0,0 @@ -function cons(v, ls) { - return { n : ls, v : v }; -} -function callAll(ls) { - for (; ls; ls = ls.n) - ls.v(); -} - -function sc(v) { - return {v : v, h : null}; -} -function sv(s, v) { - s.v = v; - callAll(s.h); -} -function sg(s) { - return s.v; -} - -function ss(s) { - return s; -} -function sr(v) { - return {v : v, h : null}; -} -function sb(x,y) { - var z = y(x.v); - var s = {v : z.v, h : null}; - - function reZ() { - z.h = cons(function() { s.v = z.v; callAll(s.h); }, z.h); - } - - x.h = cons(function() { z = y(x.v); reZ(); s.v = z.v; callAll(s.h); }, x.h); - reZ(); - - return s; -} - -function myParent() { - var pos = document; - - while (pos.lastChild && pos.lastChild.nodeType == 1) - pos = pos.lastChild; - - return pos.parentNode; -} - -function dyn(s) { - var x = document.createElement("span"); - x.innerHTML = s.v; - myParent().appendChild(x); - s.h = cons(function() { x.innerHTML = s.v }, s.h); -} - -function inp(t, s) { - var x = document.createElement(t); - x.value = s.v; - myParent().appendChild(x); - s.h = cons(function() { x.value = s.v }, s.h); - x.onkeyup = function() { sv(s, x.value) }; -} - -function eh(x) { - return x.split("&").join("&").split("<").join("<").split(">").join(">"); -} - -function ts(x) { return x.toString() } -function bs(b) { return (b ? "True" : "False") } - -function pf() { alert("Pattern match failure") } -
--- a/lib/basis.urs Tue Jan 13 15:17:11 2009 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,471 +0,0 @@ -type int -type float -type string -type time - -type unit = {} - -datatype bool = False | True - -datatype option t = None | Some of t - - -(** Basic type classes *) - -class eq -val eq : t ::: Type -> eq t -> t -> t -> bool -val ne : t ::: Type -> eq t -> t -> t -> bool -val eq_int : eq int -val eq_float : eq float -val eq_string : eq string -val eq_bool : eq bool -val eq_time : eq time -val mkEq : t ::: Type -> (t -> t -> bool) -> eq t - -class num -val zero : t ::: Type -> num t -> t -val neg : t ::: Type -> num t -> t -> t -val plus : t ::: Type -> num t -> t -> t -> t -val minus : t ::: Type -> num t -> t -> t -> t -val times : t ::: Type -> num t -> t -> t -> t -val div : t ::: Type -> num t -> t -> t -> t -val mod : t ::: Type -> num t -> t -> t -> t -val num_int : num int -val num_float : num float - -class ord -val lt : t ::: Type -> ord t -> t -> t -> bool -val le : t ::: Type -> ord t -> t -> t -> bool -val gt : t ::: Type -> ord t -> t -> t -> bool -val ge : t ::: Type -> ord t -> t -> t -> bool -val ord_int : ord int -val ord_float : ord float -val ord_string : ord string -val ord_bool : ord bool -val ord_time : ord time - - -(** String operations *) - -val strcat : string -> string -> string - -class show -val show : t ::: Type -> show t -> t -> string -val show_int : show int -val show_float : show float -val show_string : show string -val show_bool : show bool -val show_time : show time -val mkShow : t ::: Type -> (t -> string) -> show t - -class read -val read : t ::: Type -> read t -> string -> option t -val readError : t ::: Type -> read t -> string -> t -(* [readError] calls [error] if the input is malformed. *) -val read_int : read int -val read_float : read float -val read_string : read string -val read_bool : read bool -val read_time : read time - - -(** * Monads *) - -class monad :: Type -> Type -val return : m ::: (Type -> Type) -> t ::: Type - -> monad m - -> t -> m t -val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type - -> monad m - -> m t1 -> (t1 -> m t2) - -> m t2 - -con transaction :: Type -> Type -val transaction_monad : monad transaction - -con source :: Type -> Type -val source : t ::: Type -> t -> transaction (source t) -val set : t ::: Type -> source t -> t -> transaction unit -val get : t ::: Type -> source t -> transaction t - -con signal :: Type -> Type -val signal_monad : monad signal -val signal : t ::: Type -> source t -> signal t - - -(** HTTP operations *) - -val requestHeader : string -> transaction (option string) - -con http_cookie :: Type -> Type -val getCookie : t ::: Type -> http_cookie t -> transaction (option t) -val setCookie : t ::: Type -> http_cookie t -> t -> transaction unit - - -(** JavaScript-y gadgets *) - -val alert : string -> transaction unit - - -(** 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 (fields :: ({Type} * {Type})) - acc [[nm] ~ acc] - [fields.1 ~ fields.2] => - [nm = fields.1 ++ fields.2] - ++ acc) [] keep_drop) - (fold (fn nm (fields :: ({Type} * {Type})) - 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 (fields :: {Type}) 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 (t :: Type) 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 : tables1 ::: {{Type}} - -> tables2 ::: {{Type}} - -> selectedFields ::: {{Type}} - -> selectedExps ::: {Type} - -> sql_relop - -> 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_direction - -> 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_time : sql_injectable time -val sql_option_bool : sql_injectable (option bool) -val sql_option_int : sql_injectable (option int) -val sql_option_float : sql_injectable (option float) -val sql_option_string : sql_injectable (option string) -val sql_option_time : sql_injectable (option time) -val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_injectable t -> t -> sql_exp tables agg exps t - -val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps bool - -class sql_arith -val sql_int_arith : sql_arith int -val sql_float_arith : sql_arith float - -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 - -val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t - -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 - -val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t -val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t -val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t -val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t -val sql_mod : sql_binary int int int - -val sql_eq : t ::: Type -> sql_binary t t bool -val sql_ne : t ::: Type -> sql_binary t t bool -val sql_lt : t ::: Type -> sql_binary t t bool -val sql_le : t ::: Type -> sql_binary t t bool -val sql_gt : t ::: Type -> sql_binary t t bool -val sql_ge : t ::: Type -> sql_binary t t bool - -val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> 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_maxable_time : sql_maxable time -val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t -val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t - -con sql_nfunc :: Type -> Type -val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_nfunc t -> sql_exp tables agg exps t -val sql_current_timestamp : sql_nfunc time - - -(*** Executing queries *) - -val query : tables ::: {{Type}} -> exps ::: {Type} - -> fn [tables ~ exps] => - state ::: Type - -> sql_query tables exps - -> ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) - -> state - -> transaction state) - -> state - -> transaction state - - -(*** Database mutators *) - -type dml -val dml : dml -> transaction unit - -val insert : fields ::: {Type} - -> sql_table fields - -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => - [nm = sql_exp [] [] [] t] ++ acc) - [] fields) - -> dml - -val update : unchanged ::: {Type} -> changed :: {Type} -> - fn [changed ~ unchanged] => - $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => - [nm = sql_exp [T = changed ++ unchanged] [] [] t] - ++ acc) - [] changed) - -> sql_table (changed ++ unchanged) - -> sql_exp [T = changed ++ unchanged] [] [] bool - -> dml - -val delete : fields ::: {Type} - -> sql_table fields - -> sql_exp [T = fields] [] [] bool - -> dml - -(*** Sequences *) - -type sql_sequence -val nextval : sql_sequence -> transaction int - - -(** 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} - -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit} - -> useOuter ::: {Type} -> useInner ::: {Type} - -> bindOuter ::: {Type} -> bindInner ::: {Type} - -> fn [attrsGiven ~ attrsAbsent] - [useOuter ~ useInner] - [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} - -> fn [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} - -> fn [use1 ~ use2] => - xml ctx use1 bind - -> xml ctx (use1 ++ use2) bind - -con xhtml = xml [Html] -con page = xhtml [] [] -con xbody = xml [Body] [] [] -con xtr = xml [Body, Tr] [] [] -con xform = xml [Body, Form] [] [] - -(*** HTML details *) - -con html = [Html] -con head = [Head] -con body = [Body] -con form = [Body, Form] -con tabl = [Body, Table] -con tr = [Body, Tr] - -val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> unit - -> tag [Signal = signal (xml ctx use bind)] ctx [] use bind - -val head : unit -> tag [] html head [] [] -val title : unit -> tag [] head [] [] [] - -val body : unit -> tag [] html body [] [] -con bodyTag = fn (attrs :: {Type}) => - ctx ::: {Unit} -> - fn [[Body] ~ ctx] => - unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] -con bodyTagStandalone = fn (attrs :: {Type}) => - ctx ::: {Unit} - -> fn [[Body] ~ ctx] => - unit -> tag attrs ([Body] ++ ctx) [] [] [] - -val br : bodyTagStandalone [] - -val p : bodyTag [] -val b : bodyTag [] -val i : bodyTag [] -val tt : bodyTag [] -val font : bodyTag [Size = int, Face = string] - -val h1 : bodyTag [] -val h2 : bodyTag [] -val h3 : bodyTag [] -val h4 : bodyTag [] - -val li : bodyTag [] -val ol : bodyTag [] -val ul : bodyTag [] - -val hr : bodyTag [] - -val a : bodyTag [Link = transaction page, Onclick = transaction unit] - -val form : ctx ::: {Unit} -> bind ::: {Type} - -> fn [[Body] ~ ctx] => - xml form [] bind - -> xml ([Body] ++ ctx) [] [] -con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) => - ctx ::: {Unit} - -> fn [[Form] ~ ctx] => - nm :: Name -> unit - -> tag attrs ([Form] ++ ctx) inner [] [nm = ty] -val textbox : formTag string [] [Value = string, Size = int, Source = source string] -val password : formTag string [] [Value = string, Size = int] -val textarea : formTag string [] [Rows = int, Cols = int] - -val checkbox : formTag bool [] [Checked = bool] - -con radio = [Body, Radio] -val radio : formTag string radio [] -val radioOption : unit -> tag [Value = string] radio [] [] [] - -con select = [Select] -val select : formTag string select [] -val option : unit -> tag [Value = string, Selected = bool] select [] [] [] - -val submit : ctx ::: {Unit} -> use ::: {Type} - -> fn [[Form] ~ ctx] => - unit - -> tag [Value = string, Action = $use -> transaction page] - ([Form] ++ ctx) ([Form] ++ ctx) use [] - -(*** AJAX-oriented widgets *) - -con cformTag = fn (attrs :: {Type}) => - ctx ::: {Unit} - -> fn [[Body] ~ ctx] => - unit -> tag attrs ([Body] ++ ctx) [] [] [] - -val ctextbox : cformTag [Value = string, Size = int, Source = source string] -val button : cformTag [Value = string, Onclick = transaction unit] - -(*** Tables *) - -val tabl : other ::: {Unit} -> fn [other ~ [Body, Table]] => - unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] [] -val tr : other ::: {Unit} -> fn [other ~ [Body, Table, Tr]] => - unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] [] -val th : other ::: {Unit} -> fn [other ~ [Body, Tr]] => - unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] -val td : other ::: {Unit} -> fn [other ~ [Body, Tr]] => - unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] - - -(** Aborting *) - -val error : t ::: Type -> xml [Body] [] [] -> t
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/js/urweb.js Tue Jan 13 15:23:48 2009 -0500 @@ -0,0 +1,72 @@ +function cons(v, ls) { + return { n : ls, v : v }; +} +function callAll(ls) { + for (; ls; ls = ls.n) + ls.v(); +} + +function sc(v) { + return {v : v, h : null}; +} +function sv(s, v) { + s.v = v; + callAll(s.h); +} +function sg(s) { + return s.v; +} + +function ss(s) { + return s; +} +function sr(v) { + return {v : v, h : null}; +} +function sb(x,y) { + var z = y(x.v); + var s = {v : z.v, h : null}; + + function reZ() { + z.h = cons(function() { s.v = z.v; callAll(s.h); }, z.h); + } + + x.h = cons(function() { z = y(x.v); reZ(); s.v = z.v; callAll(s.h); }, x.h); + reZ(); + + return s; +} + +function myParent() { + var pos = document; + + while (pos.lastChild && pos.lastChild.nodeType == 1) + pos = pos.lastChild; + + return pos.parentNode; +} + +function dyn(s) { + var x = document.createElement("span"); + x.innerHTML = s.v; + myParent().appendChild(x); + s.h = cons(function() { x.innerHTML = s.v }, s.h); +} + +function inp(t, s) { + var x = document.createElement(t); + x.value = s.v; + myParent().appendChild(x); + s.h = cons(function() { x.value = s.v }, s.h); + x.onkeyup = function() { sv(s, x.value) }; +} + +function eh(x) { + return x.split("&").join("&").split("<").join("<").split(">").join(">"); +} + +function ts(x) { return x.toString() } +function bs(b) { return (b ? "True" : "False") } + +function pf() { alert("Pattern match failure") } +
--- a/lib/top.ur Tue Jan 13 15:17:11 2009 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,241 +0,0 @@ -fun not b = if b then False else True - -con idT (t :: Type) = t -con record (t :: {Type}) = $t -con fstTT (t :: (Type * Type)) = t.1 -con sndTT (t :: (Type * Type)) = t.2 -con fstTTT (t :: (Type * Type * Type)) = t.1 -con sndTTT (t :: (Type * Type * Type)) = t.2 -con thdTTT (t :: (Type * Type * Type)) = t.3 - -con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f] ++ acc) [] - -con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapT3T (f :: (Type * Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con ex = fn tf :: (Type -> Type) => - res ::: Type -> (choice :: Type -> tf choice -> res) -> res - -fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf = - fn (res ::: Type) (f : choice :: Type -> tf choice -> res) => - f [choice] body - -fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) - (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) - -fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) = - cdata (show v) - -fun foldUR (tf :: Type) (tr :: {Unit} -> Type) - (f : nm :: Name -> rest :: {Unit} - -> fn [[nm] ~ rest] => - tf -> tr rest -> tr ([nm] ++ rest)) - (i : tr []) = - fold [fn r :: {Unit} => $(mapUT tf r) -> tr r] - (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc - [[nm] ~ rest] r => - f [nm] [rest] r.nm (acc (r -- nm))) - (fn _ => i) - -fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type) - (f : nm :: Name -> rest :: {Unit} - -> fn [[nm] ~ rest] => - tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) - (i : tr []) = - fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r] - (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc - [[nm] ~ rest] r1 r2 => - f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) - (f : nm :: Name -> rest :: {Unit} - -> fn [[nm] ~ rest] => - tf1 -> tf2 -> xml ctx [] []) = - foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc => - <xml>{f [nm] [rest] v1 v2}{acc}</xml>) - <xml/> - -fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) - (f : nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {Type} => $(mapTT tf r) -> tr r] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) - [[nm] ~ rest] r => - f [nm] [t] [rest] r.nm (acc (r -- nm))) - (fn _ => i) - -fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - (acc : _ -> tr rest) [[nm] ~ rest] r => - f [nm] [t] [rest] r.nm (acc (r -- nm))) - (fn _ => i) - -fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - (acc : _ -> tr rest) [[nm] ~ rest] r => - f [nm] [t] [rest] r.nm (acc (r -- nm))) - (fn _ => i) - -fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) - (f : nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) - (tr :: {(Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) - (tr :: {(Type * Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldTRX (tf :: Type -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) = - foldTR [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc => - <xml>{f [nm] [t] [rest] r}{acc}</xml>) - <xml/> - -fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) = - foldT2R [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - [[nm] ~ rest] r acc => - <xml>{f [nm] [t] [rest] r}{acc}</xml>) - <xml/> - -fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) = - foldT3R [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - [[nm] ~ rest] r acc => - <xml>{f [nm] [t] [rest] r}{acc}</xml>) - <xml/> - -fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) = - foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] - r1 r2 acc => - <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) - <xml/> - -fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) - (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) = - foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - [[nm] ~ rest] r1 r2 acc => - <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) - <xml/> - -fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) - (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) = - foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - [[nm] ~ rest] r1 r2 acc => - <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) - <xml/> - -fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) - (q : sql_query tables exps) [tables ~ exps] - (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) - -> xml ctx [] []) = - query q - (fn fs acc => return <xml>{acc}{f fs}</xml>) - <xml/> - -fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) - (q : sql_query tables exps) [tables ~ exps] - (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) - -> transaction (xml ctx [] [])) = - query q - (fn fs acc => - r <- f fs; - return <xml>{acc}{r}</xml>) - <xml/> - -fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type}) - (q : sql_query tables exps) [tables ~ exps] = - query q - (fn fs _ => return (Some fs)) - None - -fun oneRow (tables ::: {{Type}}) (exps ::: {Type}) - (q : sql_query tables exps) [tables ~ exps] = - o <- oneOrNoRows q; - return (case o of - None => error <xml>Query returned no rows</xml> - | Some r => r) - -fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) - (t ::: Type) (_ : sql_injectable (option t)) - (e1 : sql_exp tables agg exps (option t)) - (e2 : sql_exp tables agg exps (option t)) = - (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) - -fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) - (t ::: Type) (_ : sql_injectable (option t)) - (e1 : sql_exp tables agg exps (option t)) - (e2 : option t) = - case e2 of - None => (SQL {e1} IS NULL) - | Some _ => sql_binary sql_eq e1 (sql_inject e2)
--- a/lib/top.urs Tue Jan 13 15:17:11 2009 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,183 +0,0 @@ -val not : bool -> bool - -con idT = fn t :: Type => t -con record = fn t :: {Type} => $t -con fstTT = fn t :: (Type * Type) => t.1 -con sndTT = fn t :: (Type * Type) => t.2 -con fstTTT = fn t :: (Type * Type * Type) => t.1 -con sndTTT = fn t :: (Type * Type * Type) => t.2 -con thdTTT = fn t :: (Type * Type * Type) => t.3 - -con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f] ++ acc) [] - -con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con ex = fn tf :: (Type -> Type) => - res ::: Type -> (choice :: Type -> tf choice -> res) -> res - -val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf - -val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type - -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) - -val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t - -> xml ctx use [] - -val foldUR : tf :: Type -> tr :: ({Unit} -> Type) - -> (nm :: Name -> rest :: {Unit} - -> fn [[nm] ~ rest] => - tf -> tr rest -> tr ([nm] ++ rest)) - -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r - -val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) - -> (nm :: Name -> rest :: {Unit} - -> fn [[nm] ~ rest] => - tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) - -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r - -val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} - -> (nm :: Name -> rest :: {Unit} - -> fn [[nm] ~ rest] => - tf1 -> tf2 -> xml ctx [] []) - -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] - -val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r - -val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r - -val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r - -val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) - -> tr :: ({Type} -> Type) - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] - -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r - -val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) - -> tr :: ({(Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type)} - -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r - -val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) - -> tr :: ({(Type * Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type * Type)} - -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r - -val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] [] - -val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] - -val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] [] - -val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {Type} - -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] - -val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) - -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {(Type * Type)} - -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] - - -val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) - -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {(Type * Type * Type)} - -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] [] - -val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} - -> sql_query tables exps - -> fn [tables ~ exps] => - ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) - -> xml ctx [] []) - -> transaction (xml ctx [] []) - -val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} - -> sql_query tables exps - -> fn [tables ~ exps] => - ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) - -> transaction (xml ctx [] [])) - -> transaction (xml ctx [] []) - -val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} - -> sql_query tables exps - -> fn [tables ~ exps] => - transaction - (option - $(exps - ++ fold (fn nm (fields :: {Type}) acc - [[nm] ~ acc] => - [nm = $fields] ++ acc) - [] tables)) - -val oneRow : tables ::: {{Type}} -> exps ::: {Type} - -> sql_query tables exps - -> fn [tables ~ exps] => - transaction - $(exps - ++ fold (fn nm (fields :: {Type}) acc - [[nm] ~ acc] => - [nm = $fields] ++ acc) - [] tables) - -val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type -> sql_injectable (option t) - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps bool - -val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type -> sql_injectable (option t) - -> sql_exp tables agg exps (option t) - -> option t - -> sql_exp tables agg exps bool
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ur/basis.urs Tue Jan 13 15:23:48 2009 -0500 @@ -0,0 +1,471 @@ +type int +type float +type string +type time + +type unit = {} + +datatype bool = False | True + +datatype option t = None | Some of t + + +(** Basic type classes *) + +class eq +val eq : t ::: Type -> eq t -> t -> t -> bool +val ne : t ::: Type -> eq t -> t -> t -> bool +val eq_int : eq int +val eq_float : eq float +val eq_string : eq string +val eq_bool : eq bool +val eq_time : eq time +val mkEq : t ::: Type -> (t -> t -> bool) -> eq t + +class num +val zero : t ::: Type -> num t -> t +val neg : t ::: Type -> num t -> t -> t +val plus : t ::: Type -> num t -> t -> t -> t +val minus : t ::: Type -> num t -> t -> t -> t +val times : t ::: Type -> num t -> t -> t -> t +val div : t ::: Type -> num t -> t -> t -> t +val mod : t ::: Type -> num t -> t -> t -> t +val num_int : num int +val num_float : num float + +class ord +val lt : t ::: Type -> ord t -> t -> t -> bool +val le : t ::: Type -> ord t -> t -> t -> bool +val gt : t ::: Type -> ord t -> t -> t -> bool +val ge : t ::: Type -> ord t -> t -> t -> bool +val ord_int : ord int +val ord_float : ord float +val ord_string : ord string +val ord_bool : ord bool +val ord_time : ord time + + +(** String operations *) + +val strcat : string -> string -> string + +class show +val show : t ::: Type -> show t -> t -> string +val show_int : show int +val show_float : show float +val show_string : show string +val show_bool : show bool +val show_time : show time +val mkShow : t ::: Type -> (t -> string) -> show t + +class read +val read : t ::: Type -> read t -> string -> option t +val readError : t ::: Type -> read t -> string -> t +(* [readError] calls [error] if the input is malformed. *) +val read_int : read int +val read_float : read float +val read_string : read string +val read_bool : read bool +val read_time : read time + + +(** * Monads *) + +class monad :: Type -> Type +val return : m ::: (Type -> Type) -> t ::: Type + -> monad m + -> t -> m t +val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type + -> monad m + -> m t1 -> (t1 -> m t2) + -> m t2 + +con transaction :: Type -> Type +val transaction_monad : monad transaction + +con source :: Type -> Type +val source : t ::: Type -> t -> transaction (source t) +val set : t ::: Type -> source t -> t -> transaction unit +val get : t ::: Type -> source t -> transaction t + +con signal :: Type -> Type +val signal_monad : monad signal +val signal : t ::: Type -> source t -> signal t + + +(** HTTP operations *) + +val requestHeader : string -> transaction (option string) + +con http_cookie :: Type -> Type +val getCookie : t ::: Type -> http_cookie t -> transaction (option t) +val setCookie : t ::: Type -> http_cookie t -> t -> transaction unit + + +(** JavaScript-y gadgets *) + +val alert : string -> transaction unit + + +(** 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 (fields :: ({Type} * {Type})) + acc [[nm] ~ acc] + [fields.1 ~ fields.2] => + [nm = fields.1 ++ fields.2] + ++ acc) [] keep_drop) + (fold (fn nm (fields :: ({Type} * {Type})) + 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 (fields :: {Type}) 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 (t :: Type) 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 : tables1 ::: {{Type}} + -> tables2 ::: {{Type}} + -> selectedFields ::: {{Type}} + -> selectedExps ::: {Type} + -> sql_relop + -> 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_direction + -> 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_time : sql_injectable time +val sql_option_bool : sql_injectable (option bool) +val sql_option_int : sql_injectable (option int) +val sql_option_float : sql_injectable (option float) +val sql_option_string : sql_injectable (option string) +val sql_option_time : sql_injectable (option time) +val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type + -> sql_injectable t -> t -> sql_exp tables agg exps t + +val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type + -> sql_exp tables agg exps (option t) + -> sql_exp tables agg exps bool + +class sql_arith +val sql_int_arith : sql_arith int +val sql_float_arith : sql_arith float + +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 + +val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t + +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 + +val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t +val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t +val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t +val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t +val sql_mod : sql_binary int int int + +val sql_eq : t ::: Type -> sql_binary t t bool +val sql_ne : t ::: Type -> sql_binary t t bool +val sql_lt : t ::: Type -> sql_binary t t bool +val sql_le : t ::: Type -> sql_binary t t bool +val sql_gt : t ::: Type -> sql_binary t t bool +val sql_ge : t ::: Type -> sql_binary t t bool + +val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> 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_maxable_time : sql_maxable time +val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t +val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t + +con sql_nfunc :: Type -> Type +val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type + -> sql_nfunc t -> sql_exp tables agg exps t +val sql_current_timestamp : sql_nfunc time + + +(*** Executing queries *) + +val query : tables ::: {{Type}} -> exps ::: {Type} + -> fn [tables ~ exps] => + state ::: Type + -> sql_query tables exps + -> ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => + [nm = $fields] ++ acc) [] tables) + -> state + -> transaction state) + -> state + -> transaction state + + +(*** Database mutators *) + +type dml +val dml : dml -> transaction unit + +val insert : fields ::: {Type} + -> sql_table fields + -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => + [nm = sql_exp [] [] [] t] ++ acc) + [] fields) + -> dml + +val update : unchanged ::: {Type} -> changed :: {Type} -> + fn [changed ~ unchanged] => + $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => + [nm = sql_exp [T = changed ++ unchanged] [] [] t] + ++ acc) + [] changed) + -> sql_table (changed ++ unchanged) + -> sql_exp [T = changed ++ unchanged] [] [] bool + -> dml + +val delete : fields ::: {Type} + -> sql_table fields + -> sql_exp [T = fields] [] [] bool + -> dml + +(*** Sequences *) + +type sql_sequence +val nextval : sql_sequence -> transaction int + + +(** 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} + -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit} + -> useOuter ::: {Type} -> useInner ::: {Type} + -> bindOuter ::: {Type} -> bindInner ::: {Type} + -> fn [attrsGiven ~ attrsAbsent] + [useOuter ~ useInner] + [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} + -> fn [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} + -> fn [use1 ~ use2] => + xml ctx use1 bind + -> xml ctx (use1 ++ use2) bind + +con xhtml = xml [Html] +con page = xhtml [] [] +con xbody = xml [Body] [] [] +con xtr = xml [Body, Tr] [] [] +con xform = xml [Body, Form] [] [] + +(*** HTML details *) + +con html = [Html] +con head = [Head] +con body = [Body] +con form = [Body, Form] +con tabl = [Body, Table] +con tr = [Body, Tr] + +val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> unit + -> tag [Signal = signal (xml ctx use bind)] ctx [] use bind + +val head : unit -> tag [] html head [] [] +val title : unit -> tag [] head [] [] [] + +val body : unit -> tag [] html body [] [] +con bodyTag = fn (attrs :: {Type}) => + ctx ::: {Unit} -> + fn [[Body] ~ ctx] => + unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] +con bodyTagStandalone = fn (attrs :: {Type}) => + ctx ::: {Unit} + -> fn [[Body] ~ ctx] => + unit -> tag attrs ([Body] ++ ctx) [] [] [] + +val br : bodyTagStandalone [] + +val p : bodyTag [] +val b : bodyTag [] +val i : bodyTag [] +val tt : bodyTag [] +val font : bodyTag [Size = int, Face = string] + +val h1 : bodyTag [] +val h2 : bodyTag [] +val h3 : bodyTag [] +val h4 : bodyTag [] + +val li : bodyTag [] +val ol : bodyTag [] +val ul : bodyTag [] + +val hr : bodyTag [] + +val a : bodyTag [Link = transaction page, Onclick = transaction unit] + +val form : ctx ::: {Unit} -> bind ::: {Type} + -> fn [[Body] ~ ctx] => + xml form [] bind + -> xml ([Body] ++ ctx) [] [] +con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) => + ctx ::: {Unit} + -> fn [[Form] ~ ctx] => + nm :: Name -> unit + -> tag attrs ([Form] ++ ctx) inner [] [nm = ty] +val textbox : formTag string [] [Value = string, Size = int, Source = source string] +val password : formTag string [] [Value = string, Size = int] +val textarea : formTag string [] [Rows = int, Cols = int] + +val checkbox : formTag bool [] [Checked = bool] + +con radio = [Body, Radio] +val radio : formTag string radio [] +val radioOption : unit -> tag [Value = string] radio [] [] [] + +con select = [Select] +val select : formTag string select [] +val option : unit -> tag [Value = string, Selected = bool] select [] [] [] + +val submit : ctx ::: {Unit} -> use ::: {Type} + -> fn [[Form] ~ ctx] => + unit + -> tag [Value = string, Action = $use -> transaction page] + ([Form] ++ ctx) ([Form] ++ ctx) use [] + +(*** AJAX-oriented widgets *) + +con cformTag = fn (attrs :: {Type}) => + ctx ::: {Unit} + -> fn [[Body] ~ ctx] => + unit -> tag attrs ([Body] ++ ctx) [] [] [] + +val ctextbox : cformTag [Value = string, Size = int, Source = source string] +val button : cformTag [Value = string, Onclick = transaction unit] + +(*** Tables *) + +val tabl : other ::: {Unit} -> fn [other ~ [Body, Table]] => + unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] [] +val tr : other ::: {Unit} -> fn [other ~ [Body, Table, Tr]] => + unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] [] +val th : other ::: {Unit} -> fn [other ~ [Body, Tr]] => + unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] +val td : other ::: {Unit} -> fn [other ~ [Body, Tr]] => + unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] + + +(** Aborting *) + +val error : t ::: Type -> xml [Body] [] [] -> t
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ur/top.ur Tue Jan 13 15:23:48 2009 -0500 @@ -0,0 +1,241 @@ +fun not b = if b then False else True + +con idT (t :: Type) = t +con record (t :: {Type}) = $t +con fstTT (t :: (Type * Type)) = t.1 +con sndTT (t :: (Type * Type)) = t.2 +con fstTTT (t :: (Type * Type * Type)) = t.1 +con sndTTT (t :: (Type * Type * Type)) = t.2 +con thdTTT (t :: (Type * Type * Type)) = t.3 + +con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + +con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => + [nm = f] ++ acc) [] + +con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + +con mapT3T (f :: (Type * Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + +con ex = fn tf :: (Type -> Type) => + res ::: Type -> (choice :: Type -> tf choice -> res) -> res + +fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf = + fn (res ::: Type) (f : choice :: Type -> tf choice -> res) => + f [choice] body + +fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) + (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) + +fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) = + cdata (show v) + +fun foldUR (tf :: Type) (tr :: {Unit} -> Type) + (f : nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf -> tr rest -> tr ([nm] ++ rest)) + (i : tr []) = + fold [fn r :: {Unit} => $(mapUT tf r) -> tr r] + (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc + [[nm] ~ rest] r => + f [nm] [rest] r.nm (acc (r -- nm))) + (fn _ => i) + +fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type) + (f : nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) + (i : tr []) = + fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r] + (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc + [[nm] ~ rest] r1 r2 => + f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) + +fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) + (f : nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf1 -> tf2 -> xml ctx [] []) = + foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc => + <xml>{f [nm] [rest] v1 v2}{acc}</xml>) + <xml/> + +fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) + (f : nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {Type} => $(mapTT tf r) -> tr r] + (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) + [[nm] ~ rest] r => + f [nm] [t] [rest] r.nm (acc (r -- nm))) + (fn _ => i) + +fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) + (acc : _ -> tr rest) [[nm] ~ rest] r => + f [nm] [t] [rest] r.nm (acc (r -- nm))) + (fn _ => i) + +fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type) + (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r] + (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) + (acc : _ -> tr rest) [[nm] ~ rest] r => + f [nm] [t] [rest] r.nm (acc (r -- nm))) + (fn _ => i) + +fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) + (f : nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r] + (fn (nm :: Name) (t :: Type) (rest :: {Type}) + (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => + f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) + +fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) + (tr :: {(Type * Type)} -> Type) + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) + (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => + f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) + +fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) + (tr :: {(Type * Type * Type)} -> Type) + (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r] + (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) + (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => + f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) + +fun foldTRX (tf :: Type -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) = + foldTR [tf] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc => + <xml>{f [nm] [t] [rest] r}{acc}</xml>) + <xml/> + +fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) = + foldT2R [tf] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) + [[nm] ~ rest] r acc => + <xml>{f [nm] [t] [rest] r}{acc}</xml>) + <xml/> + +fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) = + foldT3R [tf] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) + [[nm] ~ rest] r acc => + <xml>{f [nm] [t] [rest] r}{acc}</xml>) + <xml/> + +fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) = + foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] + r1 r2 acc => + <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) + <xml/> + +fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) + (ctx :: {Unit}) + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) = + foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) + [[nm] ~ rest] r1 r2 acc => + <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) + <xml/> + +fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) + (ctx :: {Unit}) + (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) = + foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) + [[nm] ~ rest] r1 r2 acc => + <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) + <xml/> + +fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) + (q : sql_query tables exps) [tables ~ exps] + (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => + [nm = $fields] ++ acc) [] tables) + -> xml ctx [] []) = + query q + (fn fs acc => return <xml>{acc}{f fs}</xml>) + <xml/> + +fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) + (q : sql_query tables exps) [tables ~ exps] + (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => + [nm = $fields] ++ acc) [] tables) + -> transaction (xml ctx [] [])) = + query q + (fn fs acc => + r <- f fs; + return <xml>{acc}{r}</xml>) + <xml/> + +fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type}) + (q : sql_query tables exps) [tables ~ exps] = + query q + (fn fs _ => return (Some fs)) + None + +fun oneRow (tables ::: {{Type}}) (exps ::: {Type}) + (q : sql_query tables exps) [tables ~ exps] = + o <- oneOrNoRows q; + return (case o of + None => error <xml>Query returned no rows</xml> + | Some r => r) + +fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) + (t ::: Type) (_ : sql_injectable (option t)) + (e1 : sql_exp tables agg exps (option t)) + (e2 : sql_exp tables agg exps (option t)) = + (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) + +fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) + (t ::: Type) (_ : sql_injectable (option t)) + (e1 : sql_exp tables agg exps (option t)) + (e2 : option t) = + case e2 of + None => (SQL {e1} IS NULL) + | Some _ => sql_binary sql_eq e1 (sql_inject e2)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ur/top.urs Tue Jan 13 15:23:48 2009 -0500 @@ -0,0 +1,183 @@ +val not : bool -> bool + +con idT = fn t :: Type => t +con record = fn t :: {Type} => $t +con fstTT = fn t :: (Type * Type) => t.1 +con sndTT = fn t :: (Type * Type) => t.2 +con fstTTT = fn t :: (Type * Type * Type) => t.1 +con sndTTT = fn t :: (Type * Type * Type) => t.2 +con thdTTT = fn t :: (Type * Type * Type) => t.3 + +con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + +con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => + [nm = f] ++ acc) [] + +con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + +con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + +con ex = fn tf :: (Type -> Type) => + res ::: Type -> (choice :: Type -> tf choice -> res) -> res + +val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf + +val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type + -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) + +val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t + -> xml ctx use [] + +val foldUR : tf :: Type -> tr :: ({Unit} -> Type) + -> (nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf -> tr rest -> tr ([nm] ++ rest)) + -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r + +val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) + -> (nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) + -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r + +val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} + -> (nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf1 -> tf2 -> xml ctx [] []) + -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] + +val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) + -> (nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r + +val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r + +val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r + +val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) + -> tr :: ({Type} -> Type) + -> (nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] + -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r + +val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) + -> tr :: ({(Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type)} + -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r + +val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) + -> tr :: ({(Type * Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type * Type)} + -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r + +val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] [] + +val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] + +val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] [] + +val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) + -> r :: {Type} + -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] + +val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) + -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) + -> r :: {(Type * Type)} + -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] + + +val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) + -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) + -> r :: {(Type * Type * Type)} + -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] [] + +val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} + -> sql_query tables exps + -> fn [tables ~ exps] => + ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => + [nm = $fields] ++ acc) [] tables) + -> xml ctx [] []) + -> transaction (xml ctx [] []) + +val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} + -> sql_query tables exps + -> fn [tables ~ exps] => + ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => + [nm = $fields] ++ acc) [] tables) + -> transaction (xml ctx [] [])) + -> transaction (xml ctx [] []) + +val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} + -> sql_query tables exps + -> fn [tables ~ exps] => + transaction + (option + $(exps + ++ fold (fn nm (fields :: {Type}) acc + [[nm] ~ acc] => + [nm = $fields] ++ acc) + [] tables)) + +val oneRow : tables ::: {{Type}} -> exps ::: {Type} + -> sql_query tables exps + -> fn [tables ~ exps] => + transaction + $(exps + ++ fold (fn nm (fields :: {Type}) acc + [[nm] ~ acc] => + [nm = $fields] ++ acc) + [] tables) + +val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type -> sql_injectable (option t) + -> sql_exp tables agg exps (option t) + -> sql_exp tables agg exps (option t) + -> sql_exp tables agg exps bool + +val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type -> sql_injectable (option t) + -> sql_exp tables agg exps (option t) + -> option t + -> sql_exp tables agg exps bool