Mercurial > urweb
changeset 459:f542bc3133dc
Cookies through elaborate
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 06 Nov 2008 10:29:55 -0500 |
| parents | 8f65b0fa3b29 |
| children | d34834af4512 |
| files | lib/basis.urs src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/elisp/urweb-defs.el src/elisp/urweb-mode.el src/source.sml src/source_print.sml src/unnest.sml src/urweb.grm src/urweb.lex tests/cookie.ur tests/cookie.urp |
| diffstat | 15 files changed, 160 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/basis.urs Thu Nov 06 10:04:03 2008 -0500 +++ b/lib/basis.urs Thu Nov 06 10:29:55 2008 -0500 @@ -84,6 +84,10 @@ 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 + (** SQL *)
--- a/src/elab.sml Thu Nov 06 10:04:03 2008 -0500 +++ b/src/elab.sml Thu Nov 06 10:29:55 2008 -0500 @@ -139,6 +139,7 @@ | SgiSequence of int * string * int | SgiClassAbs of string * int | SgiClass of string * int * con + | SgiCookie of int * string * int * con and sgn' = SgnConst of sgn_item list @@ -166,6 +167,7 @@ | DSequence of int * string * int | DClass of string * int * con | DDatabase of string + | DCookie of int * string * int * con and str' = StrConst of decl list
--- a/src/elab_env.sml Thu Nov 06 10:04:03 2008 -0500 +++ b/src/elab_env.sml Thu Nov 06 10:29:55 2008 -0500 @@ -592,6 +592,7 @@ | SgiSequence _ => (sgns, strs, cons) | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x)) | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) + | SgiCookie _ => (sgns, strs, cons) fun sgnSeek f sgis = let @@ -945,6 +946,13 @@ | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c) + + | SgiCookie (tn, x, n, c) => + let + val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc) + in + pushENamedAs env x n t + end fun sgnSubCon x = @@ -1095,6 +1103,7 @@ | SgiSequence _ => seek (sgis, sgns, strs, cons, acc) | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) + | SgiCookie _ => seek (sgis, sgns, strs, cons, acc) in seek (sgis, IM.empty, IM.empty, IM.empty, []) end @@ -1189,6 +1198,12 @@ pushClass env n end | DDatabase _ => env + | DCookie (tn, x, n, c) => + let + val t = (CApp ((CModProj (tn, [], "cookie"), loc), c), loc) + in + pushENamedAs env x n t + end fun patBinds env (p, loc) = case p of
--- a/src/elab_print.sml Thu Nov 06 10:04:03 2008 -0500 +++ b/src/elab_print.sml Thu Nov 06 10:29:55 2008 -0500 @@ -536,6 +536,13 @@ string "=", space, p_con env c] + | SgiCookie (_, x, n, c) => box [string "cookie", + space, + p_named x n, + space, + string ":", + space, + p_con env c] and p_sgn env (sgn, _) = case sgn of @@ -707,6 +714,13 @@ | DDatabase s => box [string "database", space, string s] + | DCookie (_, x, n, c) => box [string "cookie", + space, + p_named x n, + space, + string ":", + space, + p_con env c] and p_str env (str, _) = case str of
--- a/src/elab_util.sml Thu Nov 06 10:04:03 2008 -0500 +++ b/src/elab_util.sml Thu Nov 06 10:29:55 2008 -0500 @@ -548,6 +548,10 @@ S.map2 (con ctx c, fn c' => (SgiClass (x, n, c'), loc)) + | SgiCookie (tn, x, n, c) => + S.map2 (con ctx c, + fn c' => + (SgiCookie (tn, x, n, c'), loc)) and sg ctx s acc = S.bindP (sg' ctx s acc, sgn ctx) @@ -576,7 +580,8 @@ | SgiClassAbs (x, n) => bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) | SgiClass (x, n, _) => - bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))), + bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) + | SgiCookie _ => ctx, sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -720,7 +725,10 @@ bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc))) | DClass (x, n, _) => bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) - | DDatabase _ => ctx, + | DDatabase _ => ctx + | DCookie (tn, x, n, c) => + bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc), + c), loc))), mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -821,6 +829,11 @@ | DDatabase _ => S.return2 dAll + | DCookie (tn, x, n, c) => + S.map2 (mfc ctx c, + fn c' => + (DCookie (tn, x, n, c'), loc)) + and mfvi ctx (x, n, c, e) = S.bind2 (mfc ctx c, fn c' => @@ -955,9 +968,10 @@ | DConstraint _ => 0 | DClass (_, n, _) => n | DExport _ => 0 - | DTable (n, _, _, _) => n - | DSequence (n, _, _) => n + | DTable (n1, _, n2, _) => Int.max (n1, n2) + | DSequence (n1, _, n2) => Int.max (n1, n2) | DDatabase _ => 0 + | DCookie (n1, _, n2, _) => Int.max (n1, n2) and maxNameStr (str, _) = case str of @@ -991,10 +1005,11 @@ | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) | SgiConstraint _ => 0 - | SgiTable (n, _, _, _) => n - | SgiSequence (n, _, _) => n + | SgiTable (n1, _, n2, _) => Int.max (n1, n2) + | SgiSequence (n1, _, n2) => Int.max (n1, n2) | SgiClassAbs (_, n) => n | SgiClass (_, n, _) => n + | SgiCookie (n1, _, n2, _) => Int.max (n1, n2) end
--- a/src/elaborate.sml Thu Nov 06 10:04:03 2008 -0500 +++ b/src/elaborate.sml Thu Nov 06 10:29:55 2008 -0500 @@ -1760,6 +1760,7 @@ fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan) +fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan) fun elabSgn_item ((sgi, loc), (env, denv, gs)) = case sgi of @@ -1967,6 +1968,15 @@ ([(L'.SgiClass (x, n, c'), loc)], (env, denv, [])) end + | L.SgiCookie (x, c) => + let + val (c', k, gs) = elabCon (env, denv) c + val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc) + in + checkKind env c' k (L'.KType, loc); + ([(L'.SgiCookie (!basis_r, x, n, c'), loc)], (env, denv, gs)) + end + and elabSgn (env, denv) (sgn, loc) = case sgn of L.SgnConst sgis => @@ -2051,7 +2061,13 @@ sgnError env (DuplicateCon (loc, x)) else (); - (SS.add (cons, x), vals, sgns, strs))) + (SS.add (cons, x), vals, sgns, strs)) + | L'.SgiCookie (_, x, _, _) => + (if SS.member (vals, x) then + sgnError env (DuplicateVal (loc, x)) + else + (); + (cons, SS.add (vals, x), sgns, strs))) (SS.empty, SS.empty, SS.empty, SS.empty) sgis' in ((L'.SgnConst sgis', loc), gs) @@ -2203,6 +2219,9 @@ in (L'.DCon (x, n, k, c), loc) end + | L'.SgiCookie (_, x, n, c) => + (L'.DVal (x, n, (L'.CApp (cookieOf (), c), loc), + (L'.EModProj (str, strs, x), loc)), loc) in (d, (E.declBinds env' d, denv')) end) @@ -2259,6 +2278,7 @@ | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)] | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] | L'.DDatabase _ => [] + | L'.DCookie (tn, x, n, c) => [(L'.SgiCookie (tn, x, n, c), loc)] fun sgiBindsD (env, denv) (sgi, _) = case sgi of @@ -2508,6 +2528,16 @@ SOME (env, denv)) else NONE + | L'.SgiCookie (_, x', n1, c1) => + if x = x' then + (case unifyCons (env, denv) (L'.CApp (cookieOf (), c1), loc) c2 of + [] => SOME (env, denv) + | _ => NONE) + handle CUnify (c1, c2, err) => + (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); + SOME (env, denv)) + else + NONE | _ => NONE) | L'.SgiStr (x, n2, sgn2) => @@ -2651,6 +2681,21 @@ L'.SgiClass (x', n1, c1) => found (x', n1, c1) | _ => NONE end) + + | L'.SgiCookie (_, x, n2, c2) => + seek (fn sgi1All as (sgi1, _) => + case sgi1 of + L'.SgiCookie (_, x', n1, c1) => + if x = x' then + (case unifyCons (env, denv) c1 c2 of + [] => SOME (env, denv) + | _ => NONE) + handle CUnify (c1, c2, err) => + (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); + SOME (env, denv)) + else + NONE + | _ => NONE) end in ignore (foldl folder (env, denv) sgis2) @@ -3194,6 +3239,15 @@ | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs)) + | L.DCookie (x, c) => + let + val (c', k, gs') = elabCon (env, denv) c + val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc) + in + checkKind env c' k (L'.KType, loc); + ([(L'.DCookie (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) + end + (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) in (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll), @@ -3336,6 +3390,16 @@ (SS.add (cons, x), x) in ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs) + end + | L'.SgiCookie (tn, x, n, c) => + let + val (vals, x) = + if SS.member (vals, x) then + (vals, "?" ^ x) + else + (SS.add (vals, x), x) + in + ((L'.SgiCookie (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs) end) ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
--- a/src/elisp/urweb-defs.el Thu Nov 06 10:04:03 2008 -0500 +++ b/src/elisp/urweb-defs.el Thu Nov 06 10:29:55 2008 -0500 @@ -108,7 +108,7 @@ "datatype" "type" "open" "include" urweb-module-head-syms "con" "fold" "where" "extern" "constraint" "constraints" - "table" "sequence" "class") + "table" "sequence" "class" "cookie") "Symbols starting an sexp.") ;; (defconst urweb-not-arg-start-re @@ -134,7 +134,7 @@ (,urweb-=-starter-syms nil) (("case" "datatype" "if" "then" "else" "let" "open" "sig" "struct" "type" "val" - "con" "constraint" "table" "sequence" "class"))))) + "con" "constraint" "table" "sequence" "class" "cookie"))))) (defconst urweb-starters-indent-after (urweb-syms-re "let" "in" "struct" "sig") @@ -188,7 +188,7 @@ (append urweb-module-head-syms '("datatype" "fun" "open" "type" "val" "and" - "con" "constraint" "table" "sequence" "class")) + "con" "constraint" "table" "sequence" "class" "cookie")) "The starters of new expressions.") (defconst urweb-exptrail-syms
--- a/src/elisp/urweb-mode.el Thu Nov 06 10:04:03 2008 -0500 +++ b/src/elisp/urweb-mode.el Thu Nov 06 10:29:55 2008 -0500 @@ -136,7 +136,7 @@ "datatype" "else" "end" "extern" "fn" "fold" "fun" "functor" "if" "include" "of" "open" "let" "in" - "rec" "sequence" "sig" "signature" + "rec" "sequence" "sig" "signature" "cookie" "struct" "structure" "table" "then" "type" "val" "where" "with" @@ -223,7 +223,7 @@ ("\\<\\(\\(data\\)?type\\|con\\|class\\)\\s-+\\(\\sw+\\)" (1 font-lock-keyword-face) (3 (amAttribute font-lock-type-def-face))) - ("\\<\\(val\\|table\\|sequence\\)\\s-+\\(\\sw+\\>\\s-*\\)?\\(\\sw+\\)\\s-*[=:]" + ("\\<\\(val\\|table\\|sequence\\|cookie\\)\\s-+\\(\\sw+\\>\\s-*\\)?\\(\\sw+\\)\\s-*[=:]" (1 font-lock-keyword-face) (3 (amAttribute font-lock-variable-name-face))) ("\\<\\(structure\\|functor\\)\\s-+\\(\\sw+\\)"
--- a/src/source.sml Thu Nov 06 10:04:03 2008 -0500 +++ b/src/source.sml Thu Nov 06 10:29:55 2008 -0500 @@ -85,6 +85,7 @@ | SgiSequence of string | SgiClassAbs of string | SgiClass of string * con + | SgiCookie of string * con and sgn' = SgnConst of sgn_item list @@ -157,6 +158,7 @@ | DSequence of string | DClass of string * con | DDatabase of string + | DCookie of string * con and str' = StrConst of decl list
--- a/src/source_print.sml Thu Nov 06 10:04:03 2008 -0500 +++ b/src/source_print.sml Thu Nov 06 10:29:55 2008 -0500 @@ -428,6 +428,13 @@ string "=", space, p_con c] + | SgiCookie (x, c) => box [string "cookie", + space, + string x, + space, + string ":", + space, + p_con c] and p_sgn (sgn, _) = case sgn of @@ -579,6 +586,14 @@ space, string s] + | DCookie (x, c) => box [string "cookie", + space, + string x, + space, + string ":", + space, + p_con c] + and p_str (str, _) = case str of StrConst ds => box [string "struct",
--- a/src/unnest.sml Thu Nov 06 10:04:03 2008 -0500 +++ b/src/unnest.sml Thu Nov 06 10:29:55 2008 -0500 @@ -348,6 +348,7 @@ | DSequence _ => default () | DClass _ => default () | DDatabase _ => default () + | DCookie _ => default () end and doStr (all as (str, loc), st) =
--- a/src/urweb.grm Thu Nov 06 10:04:03 2008 -0500 +++ b/src/urweb.grm Thu Nov 06 10:29:55 2008 -0500 @@ -201,6 +201,7 @@ | LET | IN | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE + | COOKIE | CASE | IF | THEN | ELSE | XML_BEGIN of string | XML_END | XML_BEGIN_END of string @@ -426,6 +427,7 @@ in [(DClass (SYMBOL1, c), s (CLASSleft, cexpright))] end) + | COOKIE SYMBOL COLON cexp ([(DCookie (SYMBOL, cexp), s (COOKIEleft, cexpright))]) kopt : (NONE) | DCOLON kind (SOME kind) @@ -506,6 +508,7 @@ in (SgiClass (SYMBOL1, c), s (CLASSleft, cexpright)) end) + | COOKIE SYMBOL COLON cexp (SgiCookie (SYMBOL, cexp), s (COOKIEleft, cexpright)) sgis : ([]) | sgi sgis (sgi :: sgis)
--- a/src/urweb.lex Thu Nov 06 10:04:03 2008 -0500 +++ b/src/urweb.lex Thu Nov 06 10:29:55 2008 -0500 @@ -313,6 +313,7 @@ <INITIAL> "table" => (Tokens.TABLE (pos yypos, pos yypos + size yytext)); <INITIAL> "sequence" => (Tokens.SEQUENCE (pos yypos, pos yypos + size yytext)); <INITIAL> "class" => (Tokens.CLASS (pos yypos, pos yypos + size yytext)); +<INITIAL> "cookie" => (Tokens.COOKIE (pos yypos, pos yypos + size yytext)); <INITIAL> "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); <INITIAL> "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/cookie.ur Thu Nov 06 10:29:55 2008 -0500 @@ -0,0 +1,9 @@ +cookie c : string + +fun main () : transaction page = + setCookie c "Hi"; + so <- getCookie c; + case so of + None => return <xml>No cookie</xml> + | Some s => return <xml>Cookie: {[s]}</xml> +