Mercurial > urweb
changeset 1348:8a169fc0838b
Change tasks to support parametric code; add clientLeaves
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 18 Dec 2010 14:17:45 -0500 |
| parents | b106ca8200b1 |
| children | 87156c44824f |
| files | doc/manual.tex lib/ur/basis.urs src/cjr.sml src/cjr_print.sml src/cjrize.sml src/elaborate.sml src/prepare.sml tests/init.ur tests/initSimple.ur tests/initSimple.urp tests/initSimple.urs tests/roundTrip.ur |
| diffstat | 12 files changed, 102 insertions(+), 36 deletions(-) [+] |
line wrap: on
line diff
--- a/doc/manual.tex Sat Dec 18 10:56:31 2010 -0500 +++ b/doc/manual.tex Sat Dec 18 14:17:45 2010 -0500 @@ -962,8 +962,8 @@ \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$ $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{ - \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind} - & \Gamma \vdash e_2 :: \mt{Basis}.\mt{transaction} \; \{\} + \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind} \; \tau + & \Gamma \vdash e_2 :: \tau \to \mt{Basis}.\mt{transaction} \; \{\} }$$ $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{ @@ -2093,6 +2093,24 @@ Ur/Web includes a kind of automatic protection against cross site request forgery attacks. Whenever any page execution can have side effects and can also read at least one cookie value, all cookie values must be signed cryptographically, to ensure that the user has come to the current page by submitting a form on a real page generated by the proper server. Signing and signature checking are inserted automatically by the compiler. This prevents attacks like phishing schemes where users are directed to counterfeit pages with forms that submit to your application, where a user's cookies might be submitted without his knowledge, causing some undesired side effect. +\subsection{Tasks} + +In many web applications, it's useful to run code at points other than requests from browsers. Ur/Web's \emph{task} mechanism facilitates this. A type family of \emph{task kinds} is in the standard library: + +$$\begin{array}{l} +\mt{con} \; \mt{task\_kind} :: \mt{Type} \to \mt{Type} \\ +\mt{val} \; \mt{initialize} : \mt{task\_kind} \; \mt{unit} \\ +\mt{val} \; \mt{clientLeaves} : \mt{task\_kind} \; \mt{client} +\end{array}$$ + +A task kind names a particular extension point of generated applications, where the type parameter of a task kind describes which extra input data is available at that extension point. Add task code with the special declaration form $\mt{task} \; e_1 = e_2$, where $e_1$ is a task kind with data $\tau$, and $e_2$ is a function from $\tau$ to $\mt{transaction} \; \mt{unit}$. + +The currently supported task kinds are: +\begin{itemize} +\item $\mt{initialize}$: Code that is run in each freshly-allocated request context. +\item $\mt{clientLeaves}$: Code that is run for each client that the runtime system decides has surfed away. When a request that generates a new client handle is aborted, that handle will still eventually be passed to $\mt{clientLeaves}$ task code, even though the corresponding browser was never informed of the client handle's existence. In other words, in general, $\mt{clientLeaves}$ handlers will be called more times than there are actual clients. +\end{itemize} + \section{The Foreign Function Interface}
--- a/lib/ur/basis.urs Sat Dec 18 10:56:31 2010 -0500 +++ b/lib/ur/basis.urs Sat Dec 18 14:17:45 2010 -0500 @@ -810,8 +810,9 @@ (** Tasks *) -type task_kind -val initialize : task_kind +con task_kind :: Type -> Type +val initialize : task_kind unit +val clientLeaves : task_kind client (** Information flow security *)
--- a/src/cjr.sml Sat Dec 18 10:56:31 2010 -0500 +++ b/src/cjr.sml Sat Dec 18 14:17:45 2010 -0500 @@ -103,7 +103,7 @@ withtype exp = exp' located -datatype task = Initialize +datatype task = Initialize | ClientLeaves datatype decl' = DStruct of int * (string * typ) list @@ -123,7 +123,7 @@ | DCookie of string | DStyle of string - | DTask of task * exp + | DTask of task * string (* first arg name *) * string * exp | DOnError of int withtype decl = decl' located
--- a/src/cjr_print.sml Sat Dec 18 10:56:31 2010 -0500 +++ b/src/cjr_print.sml Sat Dec 18 14:17:45 2010 -0500 @@ -2794,7 +2794,8 @@ string "}", newline] - val initializers = List.mapPartial (fn (DTask (Initialize, e), _) => SOME e | _ => NONE) ds + val initializers = List.mapPartial (fn (DTask (Initialize, x1, x2, e), _) => SOME (x1, x2, e) | _ => NONE) ds + val expungers = List.mapPartial (fn (DTask (ClientLeaves, x1, x2, e), _) => SOME (x1, x2, e) | _ => NONE) ds val onError = ListUtil.search (fn (DOnError n, _) => SOME n | _ => NONE) ds @@ -2968,31 +2969,58 @@ newline, newline, - if hasDb then - box [string "static void uw_expunger(uw_context ctx, uw_Basis_client cli) {", - newline, + box [string "static void uw_expunger(uw_context ctx, uw_Basis_client cli) {", + newline, + + p_list_sep (box []) (fn (x1, x2, e) => box [string "({", + newline, + string "uw_Basis_client __uwr_", + string x1, + string "_0 = cli;", + newline, + string "uw_unit __uwr_", + string x2, + string "_1 = uw_unit_v;", + newline, + p_exp (E.pushERel (E.pushERel env x1 (TFfi ("Basis", "client"), ErrorMsg.dummySpan)) + x2 dummyt) e, + string ";", + newline, + string "});", + newline]) expungers, + + if hasDb then box [p_enamed env (!expunge), string "(ctx, cli);", - newline], - string "}", - newline, - newline, + newline] + else + box [], + string "}"], - string "static void uw_initializer(uw_context ctx) {", - newline, - box [p_list_sep (box []) (fn e => box [p_exp env e, - string ";", - newline]) initializers, - p_enamed env (!initialize), + newline, + string "static void uw_initializer(uw_context ctx) {", + newline, + box [p_list_sep (box []) (fn (x1, x2, e) => box [string "({", + newline, + string "uw_unit __uwr_", + string x1, + string "_0 = uw_unit_v, __uwr_", + string x2, + string "_1 = uw_unit_v;", + newline, + p_exp (E.pushERel (E.pushERel env x1 dummyt) x2 dummyt) e, + string ";", + newline, + string "});", + newline]) initializers, + if hasDb then + box [p_enamed env (!initialize), string "(ctx, uw_unit_v);", - newline], - string "}", - newline] - else - box [string "static void uw_expunger(uw_context ctx, uw_Basis_client cli) { };", - newline, - string "static void uw_initializer(uw_context ctx) { };", - newline], + newline] + else + box []], + string "}", + newline, case onError of NONE => box []
--- a/src/cjrize.sml Sat Dec 18 10:56:31 2010 -0500 +++ b/src/cjrize.sml Sat Dec 18 14:17:45 2010 -0500 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -662,15 +662,16 @@ | L.DStyle args => (SOME (L'.DStyle args, loc), NONE, sm) | L.DTask (e1, e2) => (case #1 e2 of - L.EAbs (_, _, _, e) => + L.EAbs (x1, _, _, (L.EAbs (x2, _, _, e), _)) => let val tk = case #1 e1 of L.EFfi ("Basis", "initialize") => L'.Initialize + | L.EFfi ("Basis", "clientLeaves") => L'.ClientLeaves | _ => (ErrorMsg.errorAt loc "Task kind not fully determined"; L'.Initialize) val (e, sm) = cifyExp (e, sm) in - (SOME (L'.DTask (tk, e), loc), NONE, sm) + (SOME (L'.DTask (tk, x1, x2, e), loc), NONE, sm) end | _ => (ErrorMsg.errorAt loc "Initializer has not been fully determined"; (NONE, NONE, sm)))
--- a/src/elaborate.sml Sat Dec 18 10:56:31 2010 -0500 +++ b/src/elaborate.sml Sat Dec 18 14:17:45 2010 -0500 @@ -3962,9 +3962,14 @@ val (e1', t1, gs1) = elabExp (env, denv) e1 val (e2', t2, gs2) = elabExp (env, denv) e2 + val targ = cunif (loc, (L'.KType, loc)) + val t1' = (L'.CModProj (!basis_r, [], "task_kind"), loc) + val t1' = (L'.CApp (t1', targ), loc) + val t2' = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc), (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)), loc) + val t2' = (L'.TFun (targ, t2'), loc) in checkCon env e1' t1 t1'; checkCon env e2' t2 t2';
--- a/src/prepare.sml Sat Dec 18 10:56:31 2010 -0500 +++ b/src/prepare.sml Sat Dec 18 14:17:45 2010 -0500 @@ -325,11 +325,11 @@ | DJavaScript _ => (d, st) | DCookie _ => (d, st) | DStyle _ => (d, st) - | DTask (tk, e) => + | DTask (tk, x1, x2, e) => let val (e, st) = prepExp (e, st) in - ((DTask (tk, e), loc), st) + ((DTask (tk, x1, x2, e), loc), st) end | DOnError _ => (d, st)
--- a/tests/init.ur Sat Dec 18 10:56:31 2010 -0500 +++ b/tests/init.ur Sat Dec 18 14:17:45 2010 -0500 @@ -1,6 +1,6 @@ sequence seq table fred : {A : int, B : int} -task initialize = +task initialize = fn () => setval seq 1; dml (INSERT INTO fred (A, B) VALUES (0, 1))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/initSimple.ur Sat Dec 18 14:17:45 2010 -0500 @@ -0,0 +1,3 @@ +task initialize = fn () => debug "I ran!" + +fun main () = return <xml>Hi!</xml>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/initSimple.urp Sat Dec 18 14:17:45 2010 -0500 @@ -0,0 +1,1 @@ +initSimple
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/initSimple.urs Sat Dec 18 14:17:45 2010 -0500 @@ -0,0 +1,1 @@ +val main : {} -> transaction page
--- a/tests/roundTrip.ur Sat Dec 18 10:56:31 2010 -0500 +++ b/tests/roundTrip.ur Sat Dec 18 14:17:45 2010 -0500 @@ -1,12 +1,18 @@ table channels : { Client : client, Channel : channel (string * int * float) } PRIMARY KEY Client +table dearlyDeparted : { Client : option client, When : time } + +task clientLeaves = fn cli : client => + dml (INSERT INTO dearlyDeparted (Client, When) VALUES ({[Some cli]}, CURRENT_TIMESTAMP)); + debug "Our favorite client has LEFT!" + fun writeBack v = me <- self; r <- oneRow (SELECT channels.Channel FROM channels WHERE channels.Client = {[me]}); send r.Channels.Channel v -fun main () = +fun main' () = me <- self; ch <- channel; dml (INSERT INTO channels (Client, Channel) VALUES ({[me]}, {[ch]})); @@ -27,7 +33,7 @@ fun sender s n f = sleep 2000; - writeBack (s, n, f); + rpc (writeBack (s, n, f)); sender (s ^ "!") (n + 1) (f + 1.23) in return <xml><body onload={onDisconnect (alert "Server booted me"); @@ -37,3 +43,5 @@ <dyn signal={Buffer.render buf}/> </body></xml> end + +fun main () = return <xml><body><form><submit action={main'}/></form></body></xml>