From 794a3ad4e4713e74d2118d8f24b09ef4d35bd34f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 27 Oct 2008 08:16:19 -0400 Subject: Switch exit(1) call to uw_error() --- CHANGELOG | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 CHANGELOG (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 index 00000000..6b62d606 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,12 @@ +======== +20081027 +======== + +- On missing inputs, print an error message, but don't exit the web server. + +======== +20081026 +======== + +- Change 'sed' call to work on OSX. +- Avoid including or linking libpq files on apps that don't use SQL. -- cgit v1.2.3 From 5d118aafe9b7cecdb429836b61bb9fdf6e8fc24e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 27 Oct 2008 08:27:45 -0400 Subject: Remove need for '() <-' notation --- CHANGELOG | 1 + demo/crud.ur | 44 ++++++++++++++++++++++---------------------- demo/ref.ur | 8 ++++---- demo/refFun.ur | 2 +- demo/sql.ur | 8 ++++---- src/urweb.grm | 30 ++++++++++++++++++------------ 6 files changed, 50 insertions(+), 43 deletions(-) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 6b62d606..1c20780e 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -3,6 +3,7 @@ ======== - On missing inputs, print an error message, but don't exit the web server. +- Remove need for "() <-" notation. ======== 20081026 diff --git a/demo/crud.ur b/demo/crud.ur index 472de6d4..77fccf16 100644 --- a/demo/crud.ur +++ b/demo/crud.ur @@ -94,15 +94,15 @@ functor Make(M : sig and create (inputs : $(mapT2T sndTT M.cols)) = id <- nextval seq; - () <- dml (insert tab - (foldT2R2 [sndTT] [colMeta] - [fn cols => $(mapT2T (fn t :: (Type * Type) => - sql_exp [] [] [] t.1) cols)] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - [[nm] ~ rest] => - fn input col acc => acc with nm = @sql_inject col.Inject (col.Parse input)) - {} [M.cols] inputs M.cols - with #Id = (SQL {id}))); + dml (insert tab + (foldT2R2 [sndTT] [colMeta] + [fn cols => $(mapT2T (fn t :: (Type * Type) => + sql_exp [] [] [] t.1) cols)] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) + [[nm] ~ rest] => + fn input col acc => acc with nm = @sql_inject col.Inject (col.Parse input)) + {} [M.cols] inputs M.cols + with #Id = (SQL {id}))); ls <- list (); return

Inserted with ID {[id]}.

@@ -111,18 +111,18 @@ functor Make(M : sig and save (id : int) (inputs : $(mapT2T sndTT M.cols)) = - () <- dml (update [mapT2T fstTT M.cols] - (foldT2R2 [sndTT] [colMeta] - [fn cols => $(mapT2T (fn t :: (Type * Type) => - sql_exp [T = [Id = int] - ++ mapT2T fstTT M.cols] - [] [] t.1) cols)] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - [[nm] ~ rest] => - fn input col acc => acc with nm = - @sql_inject col.Inject (col.Parse input)) - {} [M.cols] inputs M.cols) - tab (WHERE T.Id = {id})); + dml (update [mapT2T fstTT M.cols] + (foldT2R2 [sndTT] [colMeta] + [fn cols => $(mapT2T (fn t :: (Type * Type) => + sql_exp [T = [Id = int] + ++ mapT2T fstTT M.cols] + [] [] t.1) cols)] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) + [[nm] ~ rest] => + fn input col acc => acc with nm = + @sql_inject col.Inject (col.Parse input)) + {} [M.cols] inputs M.cols) + tab (WHERE T.Id = {id})); ls <- list (); return

Saved!

@@ -150,7 +150,7 @@ functor Make(M : sig and delete (id : int) = - () <- dml (DELETE FROM tab WHERE Id = {id}); + dml (DELETE FROM tab WHERE Id = {id}); ls <- list (); return

The deed is done.

diff --git a/demo/ref.ur b/demo/ref.ur index 089529e3..4030b6fa 100644 --- a/demo/ref.ur +++ b/demo/ref.ur @@ -13,15 +13,15 @@ fun main () = ir' <- IR.new 7; sr <- SR.new "hi"; - () <- IR.write ir' 10; + IR.write ir' 10; iv <- IR.read ir; iv' <- IR.read ir'; sv <- SR.read sr; - () <- IR.delete ir; - () <- IR.delete ir'; - () <- SR.delete sr; + IR.delete ir; + IR.delete ir'; + SR.delete sr; return {[iv]}, {[iv']}, {[sv]} diff --git a/demo/refFun.ur b/demo/refFun.ur index a090b297..d648f31e 100644 --- a/demo/refFun.ur +++ b/demo/refFun.ur @@ -10,7 +10,7 @@ functor Make(M : sig fun new d = id <- nextval s; - () <- dml (INSERT INTO t (Id, Data) VALUES ({id}, {d})); + dml (INSERT INTO t (Id, Data) VALUES ({id}, {d})); return id fun read r = diff --git a/demo/sql.ur b/demo/sql.ur index 9e9effff..43a69573 100644 --- a/demo/sql.ur +++ b/demo/sql.ur @@ -26,8 +26,8 @@ fun list () = and add r = - () <- dml (INSERT INTO t (A, B, C, D) - VALUES ({readError r.A}, {readError r.B}, {r.C}, {r.D})); + dml (INSERT INTO t (A, B, C, D) + VALUES ({readError r.A}, {readError r.B}, {r.C}, {r.D})); xml <- list (); return

Row added.

@@ -36,8 +36,8 @@ and add r = and delete a = - () <- dml (DELETE FROM t - WHERE t.A = {a}); + dml (DELETE FROM t + WHERE t.A = {a}); xml <- list (); return

Row deleted.

diff --git a/src/urweb.grm b/src/urweb.grm index 9a9081a3..4f470fa0 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -263,6 +263,7 @@ fun tagIn bt = | xmlOne of exp | tag of string * exp | tagHead of string * exp + | bind of string * con option * exp | earg of exp * con -> exp * con | eargp of exp * con -> exp * con @@ -668,20 +669,13 @@ eexp : eapps (eapps) (ECase (eexp1, [((PCon (["Basis"], "True", NONE), loc), eexp2), ((PCon (["Basis"], "False", NONE), loc), eexp3)]), loc) end) - | SYMBOL LARROW eexp SEMI eexp (let - val loc = s (SYMBOLleft, eexp2right) + | bind SEMI eexp (let + val loc = s (bindleft, eexpright) + val (v, to, e1) = bind val e = (EVar (["Basis"], "bind", Infer), loc) - val e = (EApp (e, eexp1), loc) + val e = (EApp (e, e1), loc) in - (EApp (e, (EAbs (SYMBOL, NONE, eexp2), loc)), loc) - end) - | UNIT LARROW eexp SEMI eexp (let - val loc = s (UNITleft, eexp2right) - val e = (EVar (["Basis"], "bind", Infer), loc) - val e = (EApp (e, eexp1), loc) - val t = (TRecord (CRecord [], loc), loc) - in - (EApp (e, (EAbs ("_", SOME t, eexp2), loc)), loc) + (EApp (e, (EAbs (v, to, eexp), loc)), loc) end) | eexp EQ eexp (native_op ("eq", eexp1, eexp2, s (eexp1left, eexp2right))) | eexp NE eexp (native_op ("ne", eexp1, eexp2, s (eexp1left, eexp2right))) @@ -699,6 +693,18 @@ eexp : eapps (eapps) | eexp WITH cterm EQ eexp (EWith (eexp1, cterm, eexp2), s (eexp1left, eexp2right)) +bind : SYMBOL LARROW eapps (SYMBOL, NONE, eapps) + | UNIT LARROW eapps (let + val loc = s (UNITleft, eappsright) + in + ("_", SOME (TRecord (CRecord [], loc), loc), eapps) + end) + | eapps (let + val loc = s (eappsleft, eappsright) + in + ("_", SOME (TRecord (CRecord [], loc), loc), eapps) + end) + eargs : earg (earg) | eargl (eargl) -- cgit v1.2.3 From e0f5b40bb999cf78e9ad479d8004cf00ed7b3059 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 28 Oct 2008 15:05:16 -0400 Subject: GCCARGS configure option --- CHANGELOG | 6 ++++++ configure | 6 +++++- configure.ac | 2 ++ src/compiler.sml | 2 +- src/config.sig | 2 ++ src/config.sml.in | 2 ++ 6 files changed, 18 insertions(+), 2 deletions(-) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 1c20780e..aca01ea7 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,9 @@ +======== +20081028 +======== + +- Add GCCARGS configure option + ======== 20081027 ======== diff --git a/configure b/configure index e205575b..e34c6b57 100755 --- a/configure +++ b/configure @@ -618,6 +618,7 @@ BIN LIB INCLUDE SITELISP +GCCARGS do_not_edit LIBOBJS LTLIBOBJS' @@ -1665,6 +1666,7 @@ do_not_edit="Do not edit this file. It was generated automatically from" + # finish the configure script and generate various files; ./configure # will apply variable substitutions to .in to generate ; # I find it useful to mark generated files as read-only so I don't @@ -2365,12 +2367,13 @@ BIN!$BIN$ac_delim LIB!$LIB$ac_delim INCLUDE!$INCLUDE$ac_delim SITELISP!$SITELISP$ac_delim +GCCARGS!$GCCARGS$ac_delim do_not_edit!$do_not_edit$ac_delim LIBOBJS!$LIBOBJS$ac_delim LTLIBOBJS!$LTLIBOBJS$ac_delim _ACEOF - if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 44; then + if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 45; then break elif $ac_last_try; then { { echo "$as_me:$LINENO: error: could not make $CONFIG_STATUS" >&5 @@ -2712,4 +2715,5 @@ Ur/Web configuration: lib directory: LIB $LIB include directory: INCLUDE $INCLUDE site-lisp directory: SITELISP $SITELISP + Extra GCC args: GCCARGS $GCCARGS EOF diff --git a/configure.ac b/configure.ac index dee2bc1b..25196f76 100644 --- a/configure.ac +++ b/configure.ac @@ -56,6 +56,7 @@ AC_SUBST(BIN) AC_SUBST(LIB) AC_SUBST(INCLUDE) AC_SUBST(SITELISP) +AC_SUBST(GCCARGS) AC_SUBST(do_not_edit) # finish the configure script and generate various files; ./configure @@ -98,4 +99,5 @@ Ur/Web configuration: lib directory: LIB $LIB include directory: INCLUDE $INCLUDE site-lisp directory: SITELISP $SITELISP + Extra GCC args: GCCARGS $GCCARGS EOF diff --git a/src/compiler.sml b/src/compiler.sml index 5d48287b..1f88705c 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -511,7 +511,7 @@ fun compileC {cname, oname, ename, libs} = val urweb_o = clibFile "urweb.o" val driver_o = clibFile "driver.o" - val compile = "gcc -Wstrict-prototypes -Werror -O3 -I include -c " ^ cname ^ " -o " ^ oname + val compile = "gcc " ^ Config.gccArgs ^ " -Wstrict-prototypes -Werror -O3 -I include -c " ^ cname ^ " -o " ^ oname val link = "gcc -Werror -O3 -lm -pthread " ^ libs ^ " " ^ urweb_o ^ " " ^ oname ^ " " ^ driver_o ^ " -o " ^ ename in if not (OS.Process.isSuccess (OS.Process.system compile)) then diff --git a/src/config.sig b/src/config.sig index 890bd9ab..6075482e 100644 --- a/src/config.sig +++ b/src/config.sig @@ -6,4 +6,6 @@ signature CONFIG = sig val libUr : string val libC : string + + val gccArgs : string end diff --git a/src/config.sml.in b/src/config.sml.in index d1eb5025..9e53986b 100644 --- a/src/config.sml.in +++ b/src/config.sml.in @@ -10,4 +10,6 @@ val libUr = OS.Path.joinDirFile {dir = lib, val libC = OS.Path.joinDirFile {dir = lib, file = "c"} +val gccArgs = "@GCCARGS@" + end -- cgit v1.2.3 From 0a10b5b7d2bbdcbfec723176b2a31d6b4c6d34d1 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 6 Nov 2008 15:37:38 -0500 Subject: Inserted a NULL value --- CHANGELOG | 9 +++++ include/urweb.h | 6 +++ lib/basis.urs | 5 +++ src/c/urweb.c | 35 ++++++++++++++++++ src/cjr_print.sml | 101 +++++++++++++++++++++++++++++++++++++++++---------- src/elab_env.sml | 31 ++++++++++++++-- src/elaborate.sml | 47 ++++++++++++++++-------- src/mono_opt.sml | 5 +++ src/monoize.sml | 24 ++++++++++-- src/urweb.grm | 5 ++- src/urweb.lex | 1 + tests/sql_option.ur | 22 +++++++++++ tests/sql_option.urp | 5 +++ 13 files changed, 252 insertions(+), 44 deletions(-) create mode 100644 tests/sql_option.ur create mode 100644 tests/sql_option.urp (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index aca01ea7..0f8d0f09 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,12 @@ +======== +NEXT +======== + +- Nested function definitions +- Primitive "time" type +- Nullable SQL columns (via "option") +- Cookies + ======== 20081028 ======== diff --git a/include/urweb.h b/include/urweb.h index 7db66ed4..7e16fd40 100644 --- a/include/urweb.h +++ b/include/urweb.h @@ -80,6 +80,12 @@ uw_Basis_string uw_Basis_sqlifyString(uw_context, uw_Basis_string); uw_Basis_string uw_Basis_sqlifyBool(uw_context, uw_Basis_bool); uw_Basis_string uw_Basis_sqlifyTime(uw_context, uw_Basis_time); +uw_Basis_string uw_Basis_sqlifyIntN(uw_context, uw_Basis_int*); +uw_Basis_string uw_Basis_sqlifyFloatN(uw_context, uw_Basis_float*); +uw_Basis_string uw_Basis_sqlifyStringN(uw_context, uw_Basis_string); +uw_Basis_string uw_Basis_sqlifyBoolN(uw_context, uw_Basis_bool*); +uw_Basis_string uw_Basis_sqlifyTimeN(uw_context, uw_Basis_time*); + char *uw_Basis_ensqlBool(uw_Basis_bool); uw_Basis_string uw_Basis_intToString(uw_context, uw_Basis_int); diff --git a/lib/basis.urs b/lib/basis.urs index 84fb4e4c..f68bedee 100644 --- a/lib/basis.urs +++ b/lib/basis.urs @@ -188,6 +188,11 @@ 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 diff --git a/src/c/urweb.c b/src/c/urweb.c index 638fbb16..1530c138 100644 --- a/src/c/urweb.c +++ b/src/c/urweb.c @@ -872,6 +872,13 @@ char *uw_Basis_sqlifyInt(uw_context ctx, uw_Basis_int n) { return r; } +char *uw_Basis_sqlifyIntN(uw_context ctx, uw_Basis_int *n) { + if (n == NULL) + return "NULL"; + else + return uw_Basis_sqlifyInt(ctx, *n); +} + char *uw_Basis_sqlifyFloat(uw_context ctx, uw_Basis_float n) { int len; char *r; @@ -883,6 +890,13 @@ char *uw_Basis_sqlifyFloat(uw_context ctx, uw_Basis_float n) { return r; } +char *uw_Basis_sqlifyFloatN(uw_context ctx, uw_Basis_float *n) { + if (n == NULL) + return "NULL"; + else + return uw_Basis_sqlifyFloat(ctx, *n); +} + uw_Basis_string uw_Basis_sqlifyString(uw_context ctx, uw_Basis_string s) { char *r, *s2; @@ -920,6 +934,13 @@ uw_Basis_string uw_Basis_sqlifyString(uw_context ctx, uw_Basis_string s) { return r; } +uw_Basis_string uw_Basis_sqlifyStringN(uw_context ctx, uw_Basis_string s) { + if (s == NULL) + return "NULL"; + else + return uw_Basis_sqlifyString(ctx, s); +} + char *uw_Basis_sqlifyBool(uw_context ctx, uw_Basis_bool b) { if (b == uw_Basis_False) return "FALSE"; @@ -927,6 +948,13 @@ char *uw_Basis_sqlifyBool(uw_context ctx, uw_Basis_bool b) { return "TRUE"; } +char *uw_Basis_sqlifyBoolN(uw_context ctx, uw_Basis_bool *b) { + if (b == NULL) + return "NULL"; + else + return uw_Basis_sqlifyBool(ctx, *b); +} + char *uw_Basis_sqlifyTime(uw_context ctx, uw_Basis_time t) { size_t len; char *r; @@ -942,6 +970,13 @@ char *uw_Basis_sqlifyTime(uw_context ctx, uw_Basis_time t) { return ""; } +char *uw_Basis_sqlifyTimeN(uw_context ctx, uw_Basis_time *t) { + if (t == NULL) + return "NULL"; + else + return uw_Basis_sqlifyTime(ctx, *t); +} + char *uw_Basis_ensqlBool(uw_Basis_bool b) { static uw_Basis_int true = 1; static uw_Basis_int false = 0; diff --git a/src/cjr_print.sml b/src/cjr_print.sml index 06154b91..d7e426c3 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -408,24 +408,61 @@ fun p_unsql wontLeakStrings env (tAll as (t, loc)) e = box [string "uw_Basis_strdup(ctx, ", e, string ")"] | TFfi ("Basis", "bool") => box [string "uw_Basis_stringToBool_error(ctx, ", e, string ")"] | TFfi ("Basis", "time") => box [string "uw_Basis_stringToTime_error(ctx, ", e, string ")"] + | _ => (ErrorMsg.errorAt loc "Don't know how to unmarshal type from SQL"; Print.eprefaces' [("Type", p_typ env tAll)]; string "ERROR") +fun p_getcol wontLeakStrings env (tAll as (t, loc)) i = + case t of + TOption t => + box [string "(PQgetisnull (res, i, ", + string (Int.toString i), + string ") ? NULL : ", + case t of + (TFfi ("Basis", "string"), _) => p_getcol wontLeakStrings env t i + | _ => box [string "({", + newline, + p_typ env t, + space, + string "*tmp = uw_malloc(ctx, sizeof(", + p_typ env t, + string "));", + newline, + string "*tmp = ", + p_getcol wontLeakStrings env t i, + string ";", + newline, + string "tmp;", + newline, + string "})"], + string ")"] + + | _ => + p_unsql wontLeakStrings env tAll + (box [string "PQgetvalue(res, i, ", + string (Int.toString i), + string ")"]) + datatype sql_type = Int | Float | String | Bool | Time + | Nullable of sql_type + +fun p_sql_type' t = + case t of + Int => "uw_Basis_int" + | Float => "uw_Basis_float" + | String => "uw_Basis_string" + | Bool => "uw_Basis_bool" + | Time => "uw_Basis_time" + | Nullable String => "uw_Basis_string" + | Nullable t => p_sql_type' t ^ "*" -fun p_sql_type t = - string (case t of - Int => "uw_Basis_int" - | Float => "uw_Basis_float" - | String => "uw_Basis_string" - | Bool => "uw_Basis_bool" - | Time => "uw_Basis_time") +fun p_sql_type t = string (p_sql_type' t) fun getPargs (e, _) = case e of @@ -448,6 +485,12 @@ fun p_ensql t e = | String => e | Bool => box [string "(", e, string " ? \"TRUE\" : \"FALSE\")"] | Time => box [string "uw_Basis_sqlifyTime(ctx, ", e, string ")"] + | Nullable String => e + | Nullable t => box [string "(", + e, + string " == NULL ? NULL : ", + p_ensql t (box [string "*", e]), + string ")"] fun notLeaky env allowHeapAllocated = let @@ -1169,10 +1212,7 @@ fun p_exp' par env (e, loc) = space, string "=", space, - p_unsql wontLeakStrings env t - (box [string "PQgetvalue(res, i, ", - string (Int.toString i), - string ")"]), + p_getcol wontLeakStrings env t i, string ";", newline]) outputs, @@ -1660,7 +1700,10 @@ fun p_decl env (dAll as (d, _) : decl) = string "}", newline] - | DPreparedStatements [] => box [] + | DPreparedStatements [] => + box [string "static void uw_db_prepare(uw_context ctx) {", + newline, + string "}"] | DPreparedStatements ss => box [string "static void uw_db_prepare(uw_context ctx) {", newline, @@ -1708,7 +1751,7 @@ datatype 'a search = | NotFound | Error -fun p_sqltype' env (tAll as (t, loc)) = +fun p_sqltype'' env (tAll as (t, loc)) = case t of TFfi ("Basis", "int") => "int8" | TFfi ("Basis", "float") => "float8" @@ -1719,8 +1762,25 @@ fun p_sqltype' env (tAll as (t, loc)) = Print.eprefaces' [("Type", p_typ env tAll)]; "ERROR") +fun p_sqltype' env (tAll as (t, loc)) = + case t of + (TOption t, _) => p_sqltype'' env t + | _ => p_sqltype'' env t ^ " NOT NULL" + fun p_sqltype env t = string (p_sqltype' env t) +fun p_sqltype_base' env t = + case t of + (TOption t, _) => p_sqltype'' env t + | _ => p_sqltype'' env t + +fun p_sqltype_base env t = string (p_sqltype_base' env t) + +fun is_not_null t = + case t of + (TOption _, _) => false + | _ => true + fun p_file env (ds, ps) = let val (pds, env) = ListUtil.foldlMap (fn (d, env) => @@ -1997,8 +2057,13 @@ fun p_file env (ds, ps) = Char.toLower (ident x), "' AND atttypid = (SELECT oid FROM pg_type", " WHERE typname = '", - p_sqltype' env t, - "'))"]) xts), + p_sqltype_base' env t, + "') AND attnotnull = ", + if is_not_null t then + "TRUE" + else + "FALSE", + ")"]) xts), ")"] val q'' = String.concat ["SELECT COUNT(*) FROM pg_attribute WHERE attrelid = (SELECT oid FROM pg_class WHERE relname = '", @@ -2295,11 +2360,7 @@ fun p_sql env (ds, _) = box [string "uw_", string (CharVector.map Char.toLower x), space, - p_sqltype env t, - space, - string "NOT", - space, - string "NULL"]) xts, + p_sqltype env (t, ErrorMsg.dummySpan)]) xts, string ");", newline, newline] diff --git a/src/elab_env.sml b/src/elab_env.sml index b14cd06c..46f62727 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -150,12 +150,14 @@ datatype class_key = CkNamed of int | CkRel of int | CkProj of int * string list * string + | CkApp of class_key * class_key fun ck2s ck = case ck of CkNamed n => "Named(" ^ Int.toString n ^ ")" | CkRel n => "Rel(" ^ Int.toString n ^ ")" | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" + | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")" fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")" @@ -176,6 +178,12 @@ fun compare x = join (Int.compare (m1, m2), fn () => join (joinL String.compare (ms1, ms2), fn () => String.compare (x1, x2))) + | (CkProj _, _) => LESS + | (_, CkProj _) => GREATER + + | (CkApp (f1, x1), CkApp (f2, x2)) => + join (compare (f1, f2), + fn () => compare (x1, x2)) end structure KM = BinaryMapFn(KK) @@ -251,6 +259,7 @@ fun liftClassKey ck = CkNamed _ => ck | CkRel n => CkRel (n + 1) | CkProj _ => ck + | CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2) fun pushCRel (env : env) x k = let @@ -411,6 +420,10 @@ fun class_key_in (c, _) = | CNamed n => SOME (CkNamed n) | CModProj x => SOME (CkProj x) | CUnif (_, _, _, ref (SOME c)) => class_key_in c + | CApp (c1, c2) => + (case (class_key_in c1, class_key_in c2) of + (SOME k1, SOME k2) => SOME (CkApp (k1, k2)) + | _ => NONE) | _ => NONE fun class_pair_in (c, _) = @@ -653,7 +666,7 @@ fun sgnS_con (str, (sgns, strs, cons)) c = end) | _ => c -fun sgnS_con' (m1, ms', (sgns, strs, cons)) c = +fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c = case c of CModProj (m1, ms, x) => (case IM.find (strs, m1) of @@ -663,6 +676,8 @@ fun sgnS_con' (m1, ms', (sgns, strs, cons)) c = (case IM.find (cons, n) of NONE => c | SOME nx => CModProj (m1, ms', nx)) + | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1), + (sgnS_con' arg (#1 c2), #2 c2)) | _ => c fun sgnS_sgn (str, (sgns, strs, cons)) sgn = @@ -1033,13 +1048,21 @@ fun projectVal env {sgn, str, field} = ListUtil.search (fn (x, _, to) => if x = field then SOME (let + val base = (CNamed n, #2 sgn) + val nxs = length xs + val base = ListUtil.foldli (fn (i, _, base) => + (CApp (base, + (CRel (nxs - i - 1), #2 sgn)), + #2 sgn)) + base xs + val t = case to of - NONE => (CNamed n, #2 sgn) - | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn) + NONE => base + | SOME t => (TFun (t, base), #2 sgn) val k = (KType, #2 sgn) in - foldr (fn (x, t) => (TCFun (Explicit, x, k, t), #2 sgn)) + foldr (fn (x, t) => (TCFun (Implicit, x, k, t), #2 sgn)) t xs end) else diff --git a/src/elaborate.sml b/src/elaborate.sml index 3b70c623..a6edc0ed 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1389,17 +1389,32 @@ fun unmodCon env (c, loc) = end | _ => (c, loc) -fun normClassConstraint envs (c, loc) = +fun normClassKey envs c = + let + val c = ElabOps.hnormCon envs c + in + case #1 c of + L'.CApp (c1, c2) => + let + val c1 = normClassKey envs c1 + val c2 = normClassKey envs c2 + in + (L'.CApp (c1, c2), #2 c) + end + | _ => c + end + +fun normClassConstraint env (c, loc) = case c of L'.CApp (f, x) => let - val f = unmodCon (#1 envs) f - val (x, gs) = hnormCon envs x + val f = unmodCon env f + val x = normClassKey env x in - ((L'.CApp (f, x), loc), gs) + (L'.CApp (f, x), loc) end - | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint envs c - | _ => ((c, loc), []) + | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c + | _ => (c, loc) val makeInstantiable = @@ -1491,12 +1506,12 @@ fun elabExp (env, denv) (eAll as (e, loc)) = checkKind env t' tk ktype; (t', gs) end - val (dom, gs2) = normClassConstraint (env, denv) t' - val (e', et, gs3) = elabExp (E.pushERel env x dom, denv) e + val dom = normClassConstraint env t' + val (e', et, gs2) = elabExp (E.pushERel env x dom, denv) e in ((L'.EAbs (x, t', et, e'), loc), (L'.TFun (t', et), loc), - enD gs1 @ enD gs2 @ gs3) + enD gs1 @ gs2) end | L.ECApp (e, c) => let @@ -1708,11 +1723,11 @@ and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = val (e', et, gs2) = elabExp (env, denv) e val gs3 = checkCon (env, denv) e' et c' - val (c', gs4) = normClassConstraint (env, denv) c' + val c' = normClassConstraint env c' val env' = E.pushERel env x c' val c' = makeInstantiable c' in - ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) + ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ gs)) end | L.EDValRec vis => let @@ -1884,12 +1899,12 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = val (c', ck, gs') = elabCon (env, denv) c val (env', n) = E.pushENamed env x c' - val (c', gs'') = normClassConstraint (env, denv) c' + val c' = normClassConstraint env c' in (unifyKinds ck ktype handle KUnify ue => strError env (NotType (ck, ue))); - ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs'' @ gs)) + ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) end | L.SgiStr (x, sgn) => @@ -2875,13 +2890,13 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = val (e', et, gs2) = elabExp (env, denv) e val gs3 = checkCon (env, denv) e' et c' - val (c', gs4) = normClassConstraint (env, denv) c' + val c = normClassConstraint env c' val (env', n) = E.pushENamed env x c' val c' = makeInstantiable c' in (*prefaces "DVal" [("x", Print.PD.string x), ("c'", p_con env c')];*) - ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) + ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ gs)) end | L.DValRec vis => let @@ -3404,7 +3419,7 @@ fun elabFile basis topStr topSgn env file = ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) | TypeClass (env, c, r, loc) => let - val c = ElabOps.hnormCon env c + val c = normClassKey env c in case E.resolveClass env c of SOME e => r := SOME e diff --git a/src/mono_opt.sml b/src/mono_opt.sml index b22f053b..93cb888b 100644 --- a/src/mono_opt.sml +++ b/src/mono_opt.sml @@ -268,6 +268,11 @@ fun exp e = | EFfiApp ("Basis", "sqlifyInt", [(EPrim (Prim.Int n), _)]) => EPrim (Prim.String (sqlifyInt n)) + | EFfiApp ("Basis", "sqlifyIntN", [(ENone _, _)]) => + EPrim (Prim.String "NULL") + | EFfiApp ("Basis", "sqlifyIntN", [(ESome (_, (EPrim (Prim.Int n), _)), _)]) => + EPrim (Prim.String (sqlifyInt n)) + | EFfiApp ("Basis", "sqlifyFloat", [(EPrim (Prim.Float n), _)]) => EPrim (Prim.String (sqlifyFloat n)) | EFfiApp ("Basis", "sqlifyBool", [b as (_, loc)]) => diff --git a/src/monoize.sml b/src/monoize.sml index c4c296bd..83da382b 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -982,10 +982,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | L.EFfiApp ("Basis", "dml", [e]) => let val (e, fm) = monoExp (env, st, fm) e - val un = (L'.TRecord [], loc) in - ((L'.EAbs ("_", un, un, - (L'.EDml (liftExpInExp 0 e), loc)), loc), + ((L'.EDml (liftExpInExp 0 e), loc), fm) end @@ -1274,6 +1272,26 @@ fun monoExp (env, st, fm) (all as (e, loc)) = ((L'.EAbs ("x", (L'.TFfi ("Basis", "time"), loc), (L'.TFfi ("Basis", "string"), loc), (L'.EFfiApp ("Basis", "sqlifyTime", [(L'.ERel 0, loc)]), loc)), loc), fm) + | L.EFfi ("Basis", "sql_option_int") => + ((L'.EAbs ("x", (L'.TOption (L'.TFfi ("Basis", "int"), loc), loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EFfiApp ("Basis", "sqlifyIntN", [(L'.ERel 0, loc)]), loc)), loc), + fm) + | L.EFfi ("Basis", "sql_option_float") => + ((L'.EAbs ("x", (L'.TOption (L'.TFfi ("Basis", "float"), loc), loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EFfiApp ("Basis", "sqlifyFloatN", [(L'.ERel 0, loc)]), loc)), loc), + fm) + | L.EFfi ("Basis", "sql_option_bool") => + ((L'.EAbs ("x", (L'.TOption (L'.TFfi ("Basis", "bool"), loc), loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EFfiApp ("Basis", "sqlifyBoolN", [(L'.ERel 0, loc)]), loc)), loc), + fm) + | L.EFfi ("Basis", "sql_option_string") => + ((L'.EAbs ("x", (L'.TOption (L'.TFfi ("Basis", "string"), loc), loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EFfiApp ("Basis", "sqlifyStringN", [(L'.ERel 0, loc)]), loc)), loc), + fm) + | L.EFfi ("Basis", "sql_option_time") => + ((L'.EAbs ("x", (L'.TOption (L'.TFfi ("Basis", "time"), loc), loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EFfiApp ("Basis", "sqlifyTimeN", [(L'.ERel 0, loc)]), loc)), loc), + fm) | L.ECApp ((L.EFfi ("Basis", "sql_subset"), _), _) => ((L'.ERecord [], loc), fm) diff --git a/src/urweb.grm b/src/urweb.grm index b2f2d486..2482be1b 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -214,7 +214,7 @@ fun tagIn bt = | TRUE | FALSE | CAND | OR | NOT | COUNT | AVG | SUM | MIN | MAX | ASC | DESC - | INSERT | INTO | VALUES | UPDATE | SET | DELETE + | INSERT | INTO | VALUES | UPDATE | SET | DELETE | NULL | CURRENT_TIMESTAMP | NE | LT | LE | GT | GE @@ -1251,6 +1251,9 @@ sqlexp : TRUE (sql_inject (EVar (["Basis"], "True", In s (LBRACEleft, RBRACEright))) | LPAREN sqlexp RPAREN (sqlexp) + | NULL (sql_inject ((EVar (["Basis"], "None", Infer), + s (NULLleft, NULLright)))) + | COUNT LPAREN STAR RPAREN (let val loc = s (COUNTleft, RPARENright) in diff --git a/src/urweb.lex b/src/urweb.lex index f5ea558a..f4ae3a85 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -357,6 +357,7 @@ notags = [^<{\n]+; "UPDATE" => (Tokens.UPDATE (pos yypos, pos yypos + size yytext)); "SET" => (Tokens.SET (pos yypos, pos yypos + size yytext)); "DELETE" => (Tokens.DELETE (pos yypos, pos yypos + size yytext)); + "NULL" => (Tokens.NULL (pos yypos, pos yypos + size yytext)); "CURRENT_TIMESTAMP" => (Tokens.CURRENT_TIMESTAMP (pos yypos, pos yypos + size yytext)); diff --git a/tests/sql_option.ur b/tests/sql_option.ur new file mode 100644 index 00000000..257f8c55 --- /dev/null +++ b/tests/sql_option.ur @@ -0,0 +1,22 @@ +table t : { O : option int } + +fun addNull () = + dml (INSERT INTO t (O) VALUES (NULL)); + return Done + +(*fun add42 () = + dml (INSERT INTO t (O) VALUES (42)); + return Done*) + +fun main () : transaction page = + xml <- queryX (SELECT * FROM t) + (fn r => case r.T.O of + None => Nada
+ | Some n => Num: {[n]}
); + return + {xml} + + Add a null
+ + +(* Add a 42
*) diff --git a/tests/sql_option.urp b/tests/sql_option.urp new file mode 100644 index 00000000..543c32a8 --- /dev/null +++ b/tests/sql_option.urp @@ -0,0 +1,5 @@ +debug +database dbname=option +sql option.sql + +sql_option -- cgit v1.2.3 From 68efe8d483e8d1e9f138c1388f737aa0ab68ace8 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 18 Nov 2008 13:27:33 -0500 Subject: Mention Especialize in CHANGELOG --- CHANGELOG | 1 + 1 file changed, 1 insertion(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 0f8d0f09..3bc58f47 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -6,6 +6,7 @@ NEXT - Primitive "time" type - Nullable SQL columns (via "option") - Cookies +- Compiler: Specialization of functions to known arguments (especially of function type) ======== 20081028 -- cgit v1.2.3 From 398bf05eb87aa7e4a5ece16c938719325eb304d8 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 18 Nov 2008 13:28:44 -0500 Subject: Tag CHANGELOG with release number --- CHANGELOG | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 3bc58f47..4ce8e4c2 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,5 +1,5 @@ ======== -NEXT +20081118 ======== - Nested function definitions -- cgit v1.2.3 From 1e6547284fbe62b1604d12b651a161709b30851f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 20 Nov 2008 14:51:14 -0500 Subject: Update CHANGELOG for 20081120 --- CHANGELOG | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 4ce8e4c2..a9cc96db 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,12 @@ +======== +20081120 +======== + +- Fix bug that sometimes led to omission of initial "" in pages +- Take advantage of nested functions in some demos +- "profile" option that may appear in .urp files, to enable gprof profiling +- "-guided-demo" option that works like "-demo" but uses less screen space for prose + ======== 20081118 ======== -- cgit v1.2.3 From 940865b04fa534983982b261386a3b1926bd5531 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 25 Nov 2008 10:05:44 -0500 Subject: Fusing writes with recursive function calls --- CHANGELOG | 5 +++ src/compiler.sig | 4 ++ src/compiler.sml | 13 +++++- src/fuse.sig | 32 ++++++++++++++ src/fuse.sml | 130 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ src/mono_opt.sig | 1 + src/mono_opt.sml | 2 + src/mono_util.sig | 7 +++ src/mono_util.sml | 21 ++++++++- src/sources | 3 ++ 10 files changed, 216 insertions(+), 2 deletions(-) create mode 100644 src/fuse.sig create mode 100644 src/fuse.sml (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index a9cc96db..cbd67118 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,8 @@ +======== +======== + +- Optimization: Fusing page writes with calls to recursive functions + ======== 20081120 ======== diff --git a/src/compiler.sig b/src/compiler.sig index af086675..8c52ea32 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -76,6 +76,7 @@ signature COMPILER = sig val untangle : (Mono.file, Mono.file) phase val mono_reduce : (Mono.file, Mono.file) phase val mono_shake : (Mono.file, Mono.file) phase + val fuse : (Mono.file, Mono.file) phase val pathcheck : (Mono.file, Mono.file) phase val cjrize : (Mono.file, Cjr.file) phase val prepare : (Cjr.file, Cjr.file) phase @@ -104,6 +105,9 @@ signature COMPILER = sig val toMono_reduce : (string, Mono.file) transform val toMono_shake : (string, Mono.file) transform val toMono_opt2 : (string, Mono.file) transform + val toFuse : (string, Mono.file) transform + val toUntangle2 : (string, Mono.file) transform + val toMono_shake2 : (string, Mono.file) transform val toPathcheck : (string, Mono.file) transform val toCjrize : (string, Cjr.file) transform val toPrepare : (string, Cjr.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index 6a6c4391..aac4a924 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -523,12 +523,23 @@ val toMono_shake = transform mono_shake "mono_shake1" o toMono_reduce val toMono_opt2 = transform mono_opt "mono_opt2" o toMono_shake +val fuse = { + func = Fuse.fuse, + print = MonoPrint.p_file MonoEnv.empty +} + +val toFuse = transform fuse "fuse" o toMono_opt2 + +val toUntangle2 = transform untangle "untangle2" o toFuse + +val toMono_shake2 = transform mono_shake "mono_shake2" o toUntangle2 + val pathcheck = { func = (fn file => (PathCheck.check file; file)), print = MonoPrint.p_file MonoEnv.empty } -val toPathcheck = transform pathcheck "pathcheck" o toMono_opt2 +val toPathcheck = transform pathcheck "pathcheck" o toMono_shake2 val cjrize = { func = Cjrize.cjrize, diff --git a/src/fuse.sig b/src/fuse.sig new file mode 100644 index 00000000..3ad45ac9 --- /dev/null +++ b/src/fuse.sig @@ -0,0 +1,32 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +signature FUSE = sig + + val fuse : Mono.file -> Mono.file + +end diff --git a/src/fuse.sml b/src/fuse.sml new file mode 100644 index 00000000..b6bd6b47 --- /dev/null +++ b/src/fuse.sml @@ -0,0 +1,130 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +structure Fuse :> FUSE = struct + +open Mono +structure U = MonoUtil + +structure IM = IntBinaryMap + +fun returnsString (t, loc) = + let + fun rs (t, loc) = + case t of + TFfi ("Basis", "string") => SOME ([], (TRecord [], loc)) + | TFun (dom, ran) => + (case rs ran of + NONE => NONE + | SOME (args, ran') => SOME (dom :: args, (TFun (dom, ran'), loc))) + | _ => NONE + in + case t of + TFun (dom, ran) => + (case rs ran of + NONE => NONE + | SOME (args, ran') => SOME (dom :: args, (TFun (dom, ran'), loc))) + | _ => NONE + end + +fun fuse file = + let + fun doDecl (d as (_, loc), (funcs, maxName)) = + let + val (d, funcs, maxName) = + case #1 d of + DValRec vis => + let + val (vis', funcs, maxName) = + foldl (fn ((x, n, t, e, s), (vis', funcs, maxName)) => + case returnsString t of + NONE => (vis', funcs, maxName) + | SOME (args, t') => + let + fun getBody (e, args) = + case (#1 e, args) of + (_, []) => (e, []) + | (EAbs (x, t, _, e), _ :: args) => + let + val (body, args') = getBody (e, args) + in + (body, (x, t) :: args') + end + | _ => raise Fail "Fuse: getBody" + + val (body, args) = getBody (e, args) + val body = MonoOpt.optExp (EWrite body, loc) + val (body, _) = foldl (fn ((x, dom), (body, ran)) => + ((EAbs (x, dom, ran, body), loc), + (TFun (dom, ran), loc))) + (body, (TRecord [], loc)) args + in + ((x, maxName, t', body, s) :: vis', + IM.insert (funcs, n, maxName), + maxName + 1) + end) + ([], funcs, maxName) vis + in + ((DValRec (vis @ vis'), loc), funcs, maxName) + end + | _ => (d, funcs, maxName) + + fun exp e = + case e of + EWrite e' => + let + fun unravel (e, loc) = + case e of + ENamed n => + (case IM.find (funcs, n) of + NONE => NONE + | SOME n' => SOME (ENamed n', loc)) + | EApp (e1, e2) => + (case unravel e1 of + NONE => NONE + | SOME e1 => SOME (EApp (e1, e2), loc)) + | _ => NONE + in + case unravel e' of + NONE => e + | SOME (e', _) => e' + end + | _ => e + in + (U.Decl.map {typ = fn x => x, + exp = exp, + decl = fn x => x} + d, + (funcs, maxName)) + end + + val (file, _) = ListUtil.foldlMap doDecl (IM.empty, U.File.maxName file + 1) file + in + file + end + +end diff --git a/src/mono_opt.sig b/src/mono_opt.sig index d147e7bc..d0268087 100644 --- a/src/mono_opt.sig +++ b/src/mono_opt.sig @@ -28,5 +28,6 @@ signature MONO_OPT = sig val optimize : Mono.file -> Mono.file + val optExp : Mono.exp -> Mono.exp end diff --git a/src/mono_opt.sml b/src/mono_opt.sml index b56372c7..6c0e6e21 100644 --- a/src/mono_opt.sml +++ b/src/mono_opt.sml @@ -366,4 +366,6 @@ and optExp e = #1 (U.Exp.map {typ = typ, exp = exp} e) val optimize = U.File.map {typ = typ, exp = exp, decl = decl} +val optExp = U.Exp.map {typ = typ, exp = exp} + end diff --git a/src/mono_util.sig b/src/mono_util.sig index 4e9d5d91..32a83855 100644 --- a/src/mono_util.sig +++ b/src/mono_util.sig @@ -90,6 +90,11 @@ structure Decl : sig exp : Mono.exp' * 'state -> 'state, decl : Mono.decl' * 'state -> 'state} -> 'state -> Mono.decl -> 'state + + val map : {typ : Mono.typ' -> Mono.typ', + exp : Mono.exp' -> Mono.exp', + decl : Mono.decl' -> Mono.decl'} + -> Mono.decl -> Mono.decl end structure File : sig @@ -121,6 +126,8 @@ structure File : sig exp : Mono.exp' * 'state -> 'state, decl : Mono.decl' * 'state -> 'state} -> 'state -> Mono.file -> 'state + + val maxName : Mono.file -> int end end diff --git a/src/mono_util.sml b/src/mono_util.sml index 14ab1674..2b2476e7 100644 --- a/src/mono_util.sml +++ b/src/mono_util.sml @@ -422,6 +422,13 @@ fun fold {typ, exp, decl} s d = S.Continue (_, s) => s | S.Return _ => raise Fail "MonoUtil.Decl.fold: Impossible" +fun map {typ, exp, decl} e = + case mapfold {typ = fn c => fn () => S.Continue (typ c, ()), + exp = fn e => fn () => S.Continue (exp e, ()), + decl = fn d => fn () => S.Continue (decl d, ())} e () of + S.Return () => raise Fail "MonoUtil.Decl.map: Impossible" + | S.Continue (e, ()) => e + end structure File = struct @@ -490,7 +497,7 @@ fun map {typ, exp, decl} e = case mapfold {typ = fn c => fn () => S.Continue (typ c, ()), exp = fn e => fn () => S.Continue (exp e, ()), decl = fn d => fn () => S.Continue (decl d, ())} e () of - S.Return () => raise Fail "Mono_util.File.map" + S.Return () => raise Fail "MonoUtil.File.map: Impossible" | S.Continue (e, ()) => e fun fold {typ, exp, decl} s d = @@ -500,6 +507,18 @@ fun fold {typ, exp, decl} s d = S.Continue (_, s) => s | S.Return _ => raise Fail "MonoUtil.File.fold: Impossible" +val maxName = foldl (fn ((d, _) : decl, count) => + case d of + DDatatype (_, n, ns) => + foldl (fn ((_, n', _), m) => Int.max (n', m)) + (Int.max (n, count)) ns + | DVal (_, n, _, _, _) => Int.max (n, count) + | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis + | DExport _ => count + | DTable _ => count + | DSequence _ => count + | DDatabase _ => count) 0 + end end diff --git a/src/sources b/src/sources index bddcac67..13f505d0 100644 --- a/src/sources +++ b/src/sources @@ -140,6 +140,9 @@ mono_shake.sml pathcheck.sig pathcheck.sml +fuse.sig +fuse.sml + cjr.sml cjr_env.sig -- cgit v1.2.3 From df08dfc3be26b2cf829a1ea31b63f4aaecf1f3bf Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 27 Nov 2008 13:43:15 -0500 Subject: Note optimizations in changelog --- CHANGELOG | 1 + 1 file changed, 1 insertion(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index cbd67118..a620eb3c 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,6 +2,7 @@ ======== - Optimization: Fusing page writes with calls to recursive functions +- Optimization of bottleneck compiler phases ======== 20081120 -- cgit v1.2.3 From 61bd40e1af8c3f7ace2a09068557ac7c05662b69 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 27 Nov 2008 14:38:53 -0500 Subject: Start of manual --- .hgignore | 7 ++++- CHANGELOG | 1 + doc/Makefile | 23 ++++++++++++++++ doc/manual.tex | 85 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 115 insertions(+), 1 deletion(-) create mode 100644 doc/Makefile create mode 100644 doc/manual.tex (limited to 'CHANGELOG') diff --git a/.hgignore b/.hgignore index b388b26a..fe5b6659 100644 --- a/.hgignore +++ b/.hgignore @@ -13,7 +13,7 @@ src/urweb.mlb *.grm.* *.o -Makefile +./Makefile src/config.sml *.exe @@ -27,3 +27,8 @@ demo/demo.* *.sql *mlmon.out + +*.aux +*.dvi +*.pdf +*.ps diff --git a/CHANGELOG b/CHANGELOG index a620eb3c..7ba7088e 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -3,6 +3,7 @@ - Optimization: Fusing page writes with calls to recursive functions - Optimization of bottleneck compiler phases +- Start of manual ======== 20081120 diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 00000000..777c5bf7 --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,23 @@ +PAPERS=manual + +FIGURES= + +all: $(PAPERS:%=%.dvi) $(PAPERS:%=%.ps) $(PAPERS:%=%.pdf) + +%.dvi: %.tex $(FIGURES:%=%.eps) + latex $< + latex $< + +%.ps: %.dvi + dvips $< -o $@ + +%.pdf: %.dvi $(FIGURES:%=%.pdf) + pdflatex $(<:%.dvi=%) + +%.pdf: %.eps + epstopdf $< + +clean: + rm -f *.aux *.bbl *.blg *.dvi *.log *.pdf *.ps + +.PHONY: all clean diff --git a/doc/manual.tex b/doc/manual.tex new file mode 100644 index 00000000..8517206a --- /dev/null +++ b/doc/manual.tex @@ -0,0 +1,85 @@ +\documentclass{article} +\usepackage{fullpage,amsmath,amssymb,proof} + +\newcommand{\cd}[1]{\texttt{#1}} +\newcommand{\mt}[1]{\mathsf{#1}} + +\newcommand{\rc}{+ \hspace{-.075in} + \;} + +\begin{document} + +\title{The Ur/Web Manual} +\author{Adam Chlipala} + +\maketitle + +\section{Syntax} + +\subsection{Lexical Conventions} + +We give the Ur language definition in \LaTeX $\;$ math mode, since that is prettier than monospaced ASCII. The corresponding ASCII syntax can be read off directly. Here is the key for mapping math symbols to ASCII character sequences. + +\begin{center} + \begin{tabular}{rl} + \textbf{\LaTeX} & \textbf{ASCII} \\ + $\to$ & \cd{->} \\ + $\times$ & \cd{*} \\ + $\lambda$ & \cd{fn} \\ + $\Rightarrow$ & \cd{=>} \\ + $\rc$ & \cd{++} \\ + \\ + $x$ & Normal textual identifier, not beginning with an uppercase letter \\ + $\alpha$ & Normal textual identifier, not beginning with an uppercase letter \\ + $f$ & Normal textual identifier, beginning with an uppercase letter \\ + \end{tabular} +\end{center} + +We often write syntax like $N, \cdots, N$ to stand for the non-terminal $N$ repeated 0 or more times. That is, the $\cdots$ symbol is not translated literally to ASCII. + +\subsection{Core Syntax} + +\emph{Kinds} classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies. +$$\begin{array}{rrcll} + \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\ + &&& \mid \mt{Unit} & \textrm{the trivial constructor} \\ + &&& \mid \mt{Name} & \textrm{field names} \\ + &&& \mid \kappa \to \kappa & \textrm{type-level functions} \\ + &&& \mid \{\kappa\} & \textrm{type-level records} \\ + &&& \mid (\kappa \times \cdots \times \kappa) & \textrm{type-level tuples} \\ + &&& \mid (\kappa) & \textrm{explicit precedence} \\ +\end{array}$$ + +Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions. +$$\begin{array}{rrcll} + \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\ + &&& \mid \; ::: & \textrm{implicit} +\end{array}$$ + +\emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds. +$$\begin{array}{rrcll} + \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\ + &&& \mid \alpha & \textrm{constructor variable} \\ + \\ + &&& \mid \tau \to \tau & \textrm{function type} \\ + &&& \mid \alpha \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\ + &&& \mid \$ c & \textrm{record type} \\ + \\ + &&& \mid c \; c & \textrm{type-level function application} \\ + &&& \mid \lambda \alpha \; ? \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\ + \\ + &&& \mid () & \textrm{type-level unit} \\ + &&& \mid \#f & \textrm{field name} \\ + \\ + &&& \mid [c = c, \cdots, c = c] & \textrm{known-length type-level record} \\ + &&& \mid c \rc c & \textrm{type-level record concatenation} \\ + &&& \mid \mt{fold} & \textrm{type-level record fold} \\ + \\ + &&& \mid (c, \cdots, c) & \textrm{type-level tuple} \\ + &&& \mid c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\ + \\ + &&& \mid \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\ + \\ + &&& \mid (c) & \textrm{explicit precedence} \\ +\end{array}$$ + +\end{document} \ No newline at end of file -- cgit v1.2.3 From a69a769216ef5fa9e96168ca21d110f79c22f547 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 9 Dec 2008 14:44:52 -0500 Subject: Prepare to release --- CHANGELOG | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 7ba7088e..447761d5 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,9 +1,11 @@ ======== +20081209 ======== - Optimization: Fusing page writes with calls to recursive functions - Optimization of bottleneck compiler phases -- Start of manual +- Reference manual +- SQL arithmetic operators ======== 20081120 -- cgit v1.2.3 From 61177089183c5ff88122b55c64ee4258a421d4ec Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 12 Mar 2009 12:30:21 -0400 Subject: Update CHANGELOG --- CHANGELOG | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 447761d5..644b077d 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,17 @@ +======== +20090312 +======== + +- Replace type-level "fold" with "map" +- Replace expression-level "fold" with folders, defined in Top and + supported by some special compiler inference +- Replace guarded constructors with guarded types, introduced only by + guarded expression abstraction, and with a new explicit application form +- Kind polymorphism +- Generalize type classes to constructor classes +- Initial compilation of client-side code to JavaScript +- Initial support for mixed client- and server-side programming (i.e., "AJAX") + ======== 20081209 ======== @@ -14,7 +28,8 @@ - Fix bug that sometimes led to omission of initial "" in pages - Take advantage of nested functions in some demos - "profile" option that may appear in .urp files, to enable gprof profiling -- "-guided-demo" option that works like "-demo" but uses less screen space for prose +- "-guided-demo" option that works like "-demo" but uses less screen space for + prose ======== 20081118 @@ -24,7 +39,8 @@ - Primitive "time" type - Nullable SQL columns (via "option") - Cookies -- Compiler: Specialization of functions to known arguments (especially of function type) +- Compiler: Specialization of functions to known arguments (especially of + function type) ======== 20081028 -- cgit v1.2.3 From 0355e5c5e8471d4ecafbcc56fe6634ac4ed337b3 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 12 Mar 2009 12:37:02 -0400 Subject: Mention src/coq in CHANGELOG --- CHANGELOG | 1 + 1 file changed, 1 insertion(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 644b077d..0a85dce4 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -11,6 +11,7 @@ - Generalize type classes to constructor classes - Initial compilation of client-side code to JavaScript - Initial support for mixed client- and server-side programming (i.e., "AJAX") +- src/coq: Coq formalization of a core Ur-like calculus ======== 20081209 -- cgit v1.2.3 From 2fe043a303f84c2b96ec4ac116b5a6a509994459 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 5 Apr 2009 12:41:41 -0400 Subject: CHANGELOG before release --- CHANGELOG | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 0a85dce4..ca0f5704 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,13 @@ +======== +20090405 +======== + +- Asynchronous message-passing and the associated server-side client + bookkeeping +- Reimplement parts of the client-side runtime system to avoid space leaks +- spawn and sleep +- Expand the constructor class instance rule format + ======== 20090312 ======== -- cgit v1.2.3 From f48c39b31e2d82b1ef7da1aae7d0c555d26d3101 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 9 Apr 2009 15:58:36 -0400 Subject: Update CHANGELOG --- CHANGELOG | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index ca0f5704..51d5b05b 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,10 @@ +======== +Next +======== + +- Reimplement constructor class resolution to be more general and Prolog-like +- SQL table constraints + ======== 20090405 ======== -- cgit v1.2.3 From 17cb59d373d1a94731d3730b938776b524d9f81c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 9 Apr 2009 16:36:50 -0400 Subject: URLs --- CHANGELOG | 1 + include/urweb.h | 2 ++ lib/ur/basis.urs | 6 +++++- src/c/urweb.c | 4 ++++ src/mono_opt.sig | 2 ++ src/mono_opt.sml | 9 +++++++++ src/monoize.sml | 13 +++++++++++-- src/urweb.grm | 14 +++++++++++++- tests/img.ur | 3 +++ tests/img.urp | 3 +++ tests/url.ur | 13 +++++++++++++ tests/url.urp | 3 +++ tests/url.urs | 1 + 13 files changed, 70 insertions(+), 4 deletions(-) create mode 100644 tests/img.ur create mode 100644 tests/img.urp create mode 100644 tests/url.ur create mode 100644 tests/url.urp create mode 100644 tests/url.urs (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 51d5b05b..ee860622 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -4,6 +4,7 @@ Next - Reimplement constructor class resolution to be more general and Prolog-like - SQL table constraints +- URLs, with configurable gatekeeper function Basis.bless ======== 20090405 diff --git a/include/urweb.h b/include/urweb.h index 759fc5ac..2154a8ed 100644 --- a/include/urweb.h +++ b/include/urweb.h @@ -149,3 +149,5 @@ uw_Basis_channel uw_Basis_new_channel(uw_context, uw_unit); uw_unit uw_Basis_send(uw_context, uw_Basis_channel, uw_Basis_string); uw_Basis_client uw_Basis_self(uw_context, uw_unit); + +uw_Basis_string uw_Basis_bless(uw_context, uw_Basis_string); diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index f652165d..f2f378ee 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -486,7 +486,11 @@ val ul : bodyTag [] val hr : bodyTag [] -val a : bodyTag [Link = transaction page, Onclick = transaction unit] +type url +val bless : string -> url +val a : bodyTag [Link = transaction page, Href = url, Onclick = transaction unit] + +val img : bodyTag [Src = url] val form : ctx ::: {Unit} -> bind ::: {Type} -> [[Body] ~ ctx] => diff --git a/src/c/urweb.c b/src/c/urweb.c index 67985d35..89358a06 100644 --- a/src/c/urweb.c +++ b/src/c/urweb.c @@ -1973,3 +1973,7 @@ failure_kind uw_initialize(uw_context ctx) { return r; } + +uw_Basis_string uw_Basis_bless(uw_context ctx, uw_Basis_string s) { + return s; +} diff --git a/src/mono_opt.sig b/src/mono_opt.sig index d0268087..b1652c71 100644 --- a/src/mono_opt.sig +++ b/src/mono_opt.sig @@ -30,4 +30,6 @@ signature MONO_OPT = sig val optimize : Mono.file -> Mono.file val optExp : Mono.exp -> Mono.exp + val bless : (string -> bool) ref + end diff --git a/src/mono_opt.sml b/src/mono_opt.sml index dfa0420c..205ae3fb 100644 --- a/src/mono_opt.sml +++ b/src/mono_opt.sml @@ -30,6 +30,8 @@ structure MonoOpt :> MONO_OPT = struct open Mono structure U = MonoUtil +val bless = ref (fn _ : string => true) + fun typ t = t fun decl d = d @@ -371,6 +373,13 @@ fun exp e = | EJavaScript (_, _, SOME (e, _)) => e + | EFfiApp ("Basis", "bless", [(se as EPrim (Prim.String s), loc)]) => + (if !bless s then + () + else + ErrorMsg.errorAt loc "Invalid URL passed to 'bless'"; + se) + | EFfiApp ("Basis", "checkString", [(EPrim (Prim.String s), loc)]) => let fun uwify (cs, acc) = diff --git a/src/monoize.sml b/src/monoize.sml index 950de1e1..bf26fda2 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -126,6 +126,7 @@ fun monoType env = | L.CApp ((L.CFfi ("Basis", "read"), _), t) => readType (mt env dtmap t, loc) + | L.CFfi ("Basis", "url") => (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "xml"), _), _), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "xhtml"), _), _), _), _) => @@ -2075,6 +2076,14 @@ fun monoExp (env, st, fm) (all as (e, loc)) = L'.ERecord xes => xes | _ => raise Fail "Non-record attributes!" + val attrs = + if List.exists (fn ("Link", _, _) => true + | _ => false) attrs then + List.filter (fn ("Href", _, _) => false + | _ => true) attrs + else + attrs + fun findOnload (attrs, acc) = case attrs of [] => (NONE, acc) @@ -2137,8 +2146,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) = let val fooify = case x of - "Href" => urlifyExp - | "Link" => urlifyExp + "Link" => urlifyExp + | "Action" => urlifyExp | _ => attrifyExp val xp = " " ^ lowercaseFirst x ^ "=\"" diff --git a/src/urweb.grm b/src/urweb.grm index 7e1f6757..7288359a 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -1280,7 +1280,19 @@ tagHead: BEGIN_TAG (let attrs : ([]) | attr attrs (attr :: attrs) -attr : SYMBOL EQ attrv ((CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright)), attrv) +attr : SYMBOL EQ attrv ((CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright)), + if (SYMBOL = "href" orelse SYMBOL = "src") + andalso (case #1 attrv of + EPrim _ => true + | _ => false) then + let + val loc = s (attrvleft, attrvright) + in + (EApp ((EVar (["Basis"], "bless", Infer), loc), + attrv), loc) + end + else + attrv) attrv : INT (EPrim (Prim.Int INT), s (INTleft, INTright)) | FLOAT (EPrim (Prim.Float FLOAT), s (FLOATleft, FLOATright)) diff --git a/tests/img.ur b/tests/img.ur new file mode 100644 index 00000000..70896647 --- /dev/null +++ b/tests/img.ur @@ -0,0 +1,3 @@ +fun main () : transaction page = return +

+ diff --git a/tests/img.urp b/tests/img.urp new file mode 100644 index 00000000..ff71adee --- /dev/null +++ b/tests/img.urp @@ -0,0 +1,3 @@ +debug + +img diff --git a/tests/url.ur b/tests/url.ur new file mode 100644 index 00000000..c45681e0 --- /dev/null +++ b/tests/url.ur @@ -0,0 +1,13 @@ +val url = "http://www.yahoo.com/" + +fun readersChoice r = return + Your pick, boss + + +fun main () : transaction page = return + Google! + Yahoo!
+
+ + diff --git a/tests/url.urp b/tests/url.urp new file mode 100644 index 00000000..3d4961ef --- /dev/null +++ b/tests/url.urp @@ -0,0 +1,3 @@ +debug + +url diff --git a/tests/url.urs b/tests/url.urs new file mode 100644 index 00000000..6ac44e0b --- /dev/null +++ b/tests/url.urs @@ -0,0 +1 @@ +val main : unit -> transaction page -- cgit v1.2.3 From df4a000b4c97378ccadbd1f94d9f930f87228b28 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 23 Apr 2009 16:13:02 -0400 Subject: Cookie signatures for RPCs --- CHANGELOG | 3 +++ include/urweb.h | 1 + lib/js/urweb.js | 21 +++++++++++++++------ src/c/urweb.c | 35 ++++++++++++++++++++++++++--------- src/cjr_print.sml | 7 +++++++ src/jscomp.sml | 12 ++++++++---- src/mono.sml | 8 ++++---- src/mono_print.sml | 10 +++++----- src/mono_reduce.sml | 2 +- src/mono_util.sml | 4 ++-- src/monoize.sml | 6 +++++- tests/cookieJsec.ur | 27 +++++++++++++++++++++++++++ tests/cookieJsec.urp | 5 +++++ tests/cookieJsec.urs | 1 + 14 files changed, 110 insertions(+), 32 deletions(-) create mode 100644 tests/cookieJsec.ur create mode 100644 tests/cookieJsec.urp create mode 100644 tests/cookieJsec.urs (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index ee860622..d57c52fc 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -5,6 +5,9 @@ Next - Reimplement constructor class resolution to be more general and Prolog-like - SQL table constraints - URLs, with configurable gatekeeper function Basis.bless +- Client-side error handling callbacks +- CSS +- Signing cookie values cryptographically to thwart cross site request forgery ======== 20090405 diff --git a/include/urweb.h b/include/urweb.h index e20533a0..99ae3e69 100644 --- a/include/urweb.h +++ b/include/urweb.h @@ -55,6 +55,7 @@ const char *uw_Basis_get_script(uw_context, uw_unit); uw_Basis_string uw_Basis_maybe_onload(uw_context, uw_Basis_string); void uw_set_needs_push(uw_context, int); +void uw_set_needs_sig(uw_context, int); char *uw_Basis_htmlifyInt(uw_context, uw_Basis_int); char *uw_Basis_htmlifyFloat(uw_context, uw_Basis_float); diff --git a/lib/js/urweb.js b/lib/js/urweb.js index 877ed77f..a29914b9 100644 --- a/lib/js/urweb.js +++ b/lib/js/urweb.js @@ -353,7 +353,9 @@ function getXHR(uri) } } -function requestUri(xhr, uri) { +var sig = null; + +function requestUri(xhr, uri, needsSig) { xhr.open("GET", uri, true); if (client_id != null) { @@ -361,10 +363,17 @@ function requestUri(xhr, uri) { xhr.setRequestHeader("UrWeb-Pass", client_pass.toString()); } + if (needsSig) { + if (sig == null) + whine("Missing cookie signature!"); + + xhr.setRequestHeader("UrWeb-Sig", sig); + } + xhr.send(null); } -function rc(uri, parse, k) { +function rc(uri, parse, k, needsSig) { uri = flattenLocal(uri); var xhr = getXHR(); @@ -389,7 +398,7 @@ function rc(uri, parse, k) { } }; - requestUri(xhr, uri); + requestUri(xhr, uri, needsSig); } function path_join(s1, s2) { @@ -438,7 +447,7 @@ function listener() { var connect = function () { xhr.onreadystatechange = orsc; tid = window.setTimeout(onTimeout, timeout * 500); - requestUri(xhr, uri); + requestUri(xhr, uri, false); } orsc = function() { @@ -490,8 +499,8 @@ function listener() { } else { try { - servError("Error querying remote server for messages: " + xhr.status); - } catch (e) { servError("Error querying remote server for messages"); } + servErr("Error querying remote server for messages: " + xhr.status); + } catch (e) { servErr("Error querying remote server for messages"); } } } }; diff --git a/src/c/urweb.c b/src/c/urweb.c index bd42352f..6266e12d 100644 --- a/src/c/urweb.c +++ b/src/c/urweb.c @@ -300,7 +300,7 @@ struct uw_context { const char *script_header, *url_prefix; - int needs_push; + int needs_push, needs_sig; size_t n_deltas, used_deltas; delta *deltas; @@ -336,6 +336,7 @@ uw_context uw_init() { ctx->script_header = ""; ctx->url_prefix = "/"; ctx->needs_push = 0; + ctx->needs_sig = 0; ctx->error_message[0] = 0; @@ -589,6 +590,10 @@ void uw_set_needs_push(uw_context ctx, int n) { ctx->needs_push = n; } +void uw_set_needs_sig(uw_context ctx, int n) { + ctx->needs_sig = n; +} + static void buf_check_ctx(uw_context ctx, buf *b, size_t extra, const char *desc) { if (b->back - b->front < extra) { @@ -717,16 +722,30 @@ uw_Basis_string uw_Basis_maybe_onload(uw_context ctx, uw_Basis_string s) { } } +extern uw_Basis_string uw_cookie_sig(uw_context); + const char *uw_Basis_get_settings(uw_context ctx, uw_unit u) { - if (ctx->client == NULL) - return ""; - else { - char *r = uw_malloc(ctx, 59 + 3 * INTS_MAX + strlen(ctx->url_prefix)); - sprintf(r, "client_id=%u;client_pass=%d;url_prefix=\"%s\";timeout=%d;listener();", + if (ctx->client == NULL) { + if (ctx->needs_sig) { + char *sig = uw_cookie_sig(ctx); + char *r = uw_malloc(ctx, strlen(sig) + 8); + sprintf(r, "sig=\"%s\";", sig); + return r; + } + else + return ""; + } else { + char *sig = ctx->needs_sig ? uw_cookie_sig(ctx) : ""; + char *r = uw_malloc(ctx, 59 + 3 * INTS_MAX + strlen(ctx->url_prefix) + + (ctx->needs_sig ? strlen(sig) + 7 : 0)); + sprintf(r, "client_id=%u;client_pass=%d;url_prefix=\"%s\";timeout=%d;%s%s%slistener();", ctx->client->id, ctx->client->pass, ctx->url_prefix, - ctx->timeout); + ctx->timeout, + ctx->needs_sig ? "sig=\"" : "", + sig, + ctx->needs_sig ? "\";" : ""); return r; } } @@ -1998,8 +2017,6 @@ uw_Basis_string uw_Basis_makeSigString(uw_context ctx, uw_Basis_string sig) { return r; } -extern uw_Basis_string uw_cookie_sig(uw_context); - uw_Basis_string uw_Basis_sigString(uw_context ctx, uw_unit u) { return uw_cookie_sig(ctx); } diff --git a/src/cjr_print.sml b/src/cjr_print.sml index a47bb587..69332b49 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -2497,6 +2497,13 @@ fun p_file env (ds, ps) = string (!Monoize.urlPrefix), string "\");", newline]), + string "uw_set_needs_sig(ctx, ", + string (if couldWrite ek then + "1" + else + "0"), + string ");", + newline, string "uw_login(ctx);", newline, box [string "{", diff --git a/src/jscomp.sml b/src/jscomp.sml index f839a67d..e6da3d4b 100644 --- a/src/jscomp.sml +++ b/src/jscomp.sml @@ -113,7 +113,7 @@ fun varDepth (e, _) = | ESignalReturn e => varDepth e | ESignalBind (e1, e2) => Int.max (varDepth e1, varDepth e2) | ESignalSource e => varDepth e - | EServerCall (e, ek, _) => Int.max (varDepth e, varDepth ek) + | EServerCall (e, ek, _, _) => Int.max (varDepth e, varDepth ek) | ERecv (e, ek, _) => Int.max (varDepth e, varDepth ek) | ESleep (e, ek) => Int.max (varDepth e, varDepth ek) @@ -156,7 +156,7 @@ fun closedUpto d = | ESignalReturn e => cu inner e | ESignalBind (e1, e2) => cu inner e1 andalso cu inner e2 | ESignalSource e => cu inner e - | EServerCall (e, ek, _) => cu inner e andalso cu inner ek + | EServerCall (e, ek, _, _) => cu inner e andalso cu inner ek | ERecv (e, ek, _) => cu inner e andalso cu inner ek | ESleep (e, ek) => cu inner e andalso cu inner ek in @@ -956,7 +956,7 @@ fun process file = st) end - | EServerCall (e, ek, t) => + | EServerCall (e, ek, t, eff) => let val (e, st) = jsE inner (e, st) val (ek, st) = jsE inner (ek, st) @@ -967,7 +967,11 @@ fun process file = str ("), function(s){var t=s.split(\"/\");var i=0;return " ^ unurl ^ "},"), ek, - str ")"], + str ("," + ^ (case eff of + ReadCookieWrite => "true" + | _ => "false") + ^ ")")], st) end diff --git a/src/mono.sml b/src/mono.sml index dedb41ea..94314774 100644 --- a/src/mono.sml +++ b/src/mono.sml @@ -62,6 +62,9 @@ datatype javascript_mode = | Script | Source of typ +datatype effect = datatype Export.effect +datatype export_kind = datatype Export.export_kind + datatype exp' = EPrim of Prim.t | ERel of int @@ -109,15 +112,12 @@ datatype exp' = | ESignalBind of exp * exp | ESignalSource of exp - | EServerCall of exp * exp * typ + | EServerCall of exp * exp * typ * effect | ERecv of exp * exp * typ | ESleep of exp * exp withtype exp = exp' located -datatype effect = datatype Export.effect -datatype export_kind = datatype Export.export_kind - datatype decl' = DDatatype of string * int * (string * int * typ option) list | DVal of string * int * typ * exp * string diff --git a/src/mono_print.sml b/src/mono_print.sml index 9e819e5f..b01442e8 100644 --- a/src/mono_print.sml +++ b/src/mono_print.sml @@ -308,11 +308,11 @@ fun p_exp' par env (e, _) = p_exp env e, string ")"] - | EServerCall (n, e, _) => box [string "Server(", - p_exp env n, - string ")[", - p_exp env e, - string "]"] + | EServerCall (n, e, _, _) => box [string "Server(", + p_exp env n, + string ")[", + p_exp env e, + string "]"] | ERecv (n, e, _) => box [string "Recv(", p_exp env n, string ")[", diff --git a/src/mono_reduce.sml b/src/mono_reduce.sml index 4c337e14..c124a7b4 100644 --- a/src/mono_reduce.sml +++ b/src/mono_reduce.sml @@ -371,7 +371,7 @@ fun reduce file = | ESignalBind (e1, e2) => summarize d e1 @ summarize d e2 | ESignalSource e => summarize d e - | EServerCall (e, ek, _) => summarize d e @ summarize d ek @ [Unsure] + | EServerCall (e, ek, _, _) => summarize d e @ summarize d ek @ [Unsure] | ERecv (e, ek, _) => summarize d e @ summarize d ek @ [Unsure] | ESleep (e, ek) => summarize d e @ summarize d ek @ [Unsure] in diff --git a/src/mono_util.sml b/src/mono_util.sml index c7309df4..017b86ca 100644 --- a/src/mono_util.sml +++ b/src/mono_util.sml @@ -354,14 +354,14 @@ fun mapfoldB {typ = fc, exp = fe, bind} = fn e' => (ESignalSource e', loc)) - | EServerCall (s, ek, t) => + | EServerCall (s, ek, t, eff) => S.bind2 (mfe ctx s, fn s' => S.bind2 (mfe ctx ek, fn ek' => S.map2 (mft t, fn t' => - (EServerCall (s', ek', t'), loc)))) + (EServerCall (s', ek', t', eff), loc)))) | ERecv (s, ek, t) => S.bind2 (mfe ctx s, fn s' => diff --git a/src/monoize.sml b/src/monoize.sml index 5a164831..62a46277 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -2668,7 +2668,11 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L'.ERel 0, loc)), loc), (L'.ERecord [], loc)), loc)), loc)), loc) val ek = (L'.EApp (ekf, ek), loc) - val e = (L'.EServerCall (call, ek, t), loc) + val eff = if IS.member (!readCookie, n) then + L'.ReadCookieWrite + else + L'.ReadOnly + val e = (L'.EServerCall (call, ek, t, eff), loc) val e = liftExpInExp 0 e val unit = (L'.TRecord [], loc) val e = (L'.EAbs ("_", unit, unit, e), loc) diff --git a/tests/cookieJsec.ur b/tests/cookieJsec.ur new file mode 100644 index 00000000..46668cf8 --- /dev/null +++ b/tests/cookieJsec.ur @@ -0,0 +1,27 @@ +table t : {Id : int} + +cookie c : int + +fun setter r = + setCookie c (readError r.Id); + return Done + +fun writer () = + ido <- getCookie c; + case ido of + None => error No cookie + | Some id => dml (INSERT INTO t (Id) VALUES ({[id]})) + +fun preWriter () = return +

Id:
{[m.Nam]}:	{m.Widget s}
{[m.Nam]}:	{m.Widget s}


- - - else - !) - else - return }/> -	+ + + else + !) + else + return }/> +
Aggregates	{meta.Display acc}	{meta.Display acc}
Filters	{(meta.Handlers state).DisplayFilter filter}	{(meta.Handlers state).DisplayFilter filter}