summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/manual.tex22
-rw-r--r--lib/ur/basis.urs5
-rw-r--r--src/cjr.sml4
-rw-r--r--src/cjr_print.sml72
-rw-r--r--src/cjrize.sml7
-rw-r--r--src/elaborate.sml5
-rw-r--r--src/prepare.sml4
-rw-r--r--tests/init.ur2
-rw-r--r--tests/initSimple.ur3
-rw-r--r--tests/initSimple.urp1
-rw-r--r--tests/initSimple.urs1
-rw-r--r--tests/roundTrip.ur12
12 files changed, 102 insertions, 36 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index a8d799d8..5a7110cb 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -962,8 +962,8 @@ $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\
\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 @@ The HTTP standard suggests that GET requests only be used in ways that generate
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}
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 6fa92a7c..2a61b701 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -810,8 +810,9 @@ val show_xml : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> show (xml
(** 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 *)
diff --git a/src/cjr.sml b/src/cjr.sml
index 5013033f..c57128cf 100644
--- a/src/cjr.sml
+++ b/src/cjr.sml
@@ -103,7 +103,7 @@ datatype exp' =
withtype exp = exp' located
-datatype task = Initialize
+datatype task = Initialize | ClientLeaves
datatype decl' =
DStruct of int * (string * typ) list
@@ -123,7 +123,7 @@ datatype decl' =
| 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
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index fbbbc548..2bb5775e 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -2794,7 +2794,8 @@ fun p_file env (ds, ps) =
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 @@ fun p_file env (ds, ps) =
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 []
diff --git a/src/cjrize.sml b/src/cjrize.sml
index 2915b0ca..0505af62 100644
--- a/src/cjrize.sml
+++ b/src/cjrize.sml
@@ -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 @@ fun cifyDecl ((d, loc), sm) =
| 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)))
diff --git a/src/elaborate.sml b/src/elaborate.sml
index b1515b6e..76e22139 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3962,9 +3962,14 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
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';
diff --git a/src/prepare.sml b/src/prepare.sml
index 4d81940f..1b7454dc 100644
--- a/src/prepare.sml
+++ b/src/prepare.sml
@@ -325,11 +325,11 @@ fun prepDecl (d as (_, loc), st) =
| 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)
diff --git a/tests/init.ur b/tests/init.ur
index aafbb55f..8040612d 100644
--- a/tests/init.ur
+++ b/tests/init.ur
@@ -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))
diff --git a/tests/initSimple.ur b/tests/initSimple.ur
new file mode 100644
index 00000000..e1c94280
--- /dev/null
+++ b/tests/initSimple.ur
@@ -0,0 +1,3 @@
+task initialize = fn () => debug "I ran!"
+
+fun main () = return <xml>Hi!</xml>
diff --git a/tests/initSimple.urp b/tests/initSimple.urp
new file mode 100644
index 00000000..c2374400
--- /dev/null
+++ b/tests/initSimple.urp
@@ -0,0 +1 @@
+initSimple
diff --git a/tests/initSimple.urs b/tests/initSimple.urs
new file mode 100644
index 00000000..901d6bf2
--- /dev/null
+++ b/tests/initSimple.urs
@@ -0,0 +1 @@
+val main : {} -> transaction page
diff --git a/tests/roundTrip.ur b/tests/roundTrip.ur
index d22b2d41..0ee3f8f7 100644
--- a/tests/roundTrip.ur
+++ b/tests/roundTrip.ur
@@ -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 main () =
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 @@ fun main () =
<dyn signal={Buffer.render buf}/>
</body></xml>
end
+
+fun main () = return <xml><body><form><submit action={main'}/></form></body></xml>
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-17 17:52:39 +0000