Cookies through elaborate

15 files changed, 160 insertions, 12 deletions

diff --git a/lib/basis.urs b/lib/basis.urs
index 806a9623..84fb4e4c 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -84,6 +84,10 @@ val bind : t1 ::: Type -> t2 ::: Type
 
 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 *)
 
diff --git a/src/elab.sml b/src/elab.sml
index b5350c2a..afb8f7aa 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -139,6 +139,7 @@ datatype sgn_item' =
        | 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 @@ datatype decl' =
        | 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
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 6b762abd..a782771a 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -592,6 +592,7 @@ fun sgiSeek (sgi, (sgns, strs, cons)) =
       | 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 @@ fun sgiBinds env (sgi, loc) =
 
       | 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 @@ fun sgnSeekConstraints (str, sgis) =
                   | 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 @@ fun declBinds env (d, loc) =
             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
diff --git a/src/elab_print.sml b/src/elab_print.sml
index b236954e..a686abe5 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -536,6 +536,13 @@ fun p_sgn_item env (sgi, _) =
                                    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 @@ fun p_decl env (dAll as (d, _) : decl) =
       | 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
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 57a94486..fe75ee0d 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -548,6 +548,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  | 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                    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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
 
               | 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 @@ and maxNameDecl (d, _) =
       | 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 @@ and maxNameSgi (sgi, _) =
       | 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
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index b0f2d331..3a966eaf 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1760,6 +1760,7 @@ val hnormSgn = E.hnormSgn
 
 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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             ([(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 @@ and elabSgn (env, denv) (sgn, loc) =
                                        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 @@ fun dopen (env, denv) {str, strs, sgn} =
                                               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 @@ fun sgiOfDecl (d, loc) =
       | 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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                  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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                          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 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
 
               | 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 @@ and elabStr (env, denv) (str, loc) =
                                           (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
diff --git a/src/elisp/urweb-defs.el b/src/elisp/urweb-defs.el
index fe4da2e4..5551b7a2 100644
--- a/src/elisp/urweb-defs.el
+++ b/src/elisp/urweb-defs.el
@@ -108,7 +108,7 @@ notion of \"the end of an outline\".")
                  "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 @@ notion of \"the end of an outline\".")
      (,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 @@ for all symbols and in all lines starting with the given symbol."
   (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
diff --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el
index 1a578cf9..223006fc 100644
--- a/src/elisp/urweb-mode.el
+++ b/src/elisp/urweb-mode.el
@@ -136,7 +136,7 @@ See doc for the variable `urweb-mode-info'."
 	       "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 @@ See doc for the variable `urweb-mode-info'."
     ("\\<\\(\\(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+\\)"
diff --git a/src/source.sml b/src/source.sml
index 7e204390..a0591afb 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -85,6 +85,7 @@ datatype sgn_item' =
        | 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 @@ datatype decl' =
        | DSequence of string
        | DClass of string * con
        | DDatabase of string
+       | DCookie of string * con
 
      and str' =
          StrConst of decl list
diff --git a/src/source_print.sml b/src/source_print.sml
index 9e6608df..d33fb38d 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -428,6 +428,13 @@ fun p_sgn_item (sgi, _) =
                                 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 @@ fun p_decl ((d, _) : decl) =
                             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",
diff --git a/src/unnest.sml b/src/unnest.sml
index b56daf8a..6a37d484 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -348,6 +348,7 @@ fun unnest file =
                   | DSequence _ => default ()
                   | DClass _ => default ()
                   | DDatabase _ => default ()
+                  | DCookie _ => default ()
             end
 
         and doStr (all as (str, loc), st) =
diff --git a/src/urweb.grm b/src/urweb.grm
index 1555dc37..879afb9c 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -201,6 +201,7 @@ fun tagIn bt =
  | 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 @@ decl   : CON SYMBOL cargl2 kopt EQ cexp (let
                                          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 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
                                          in
                                              (SgiClass (SYMBOL1, c), s (CLASSleft, cexpright))
                                          end)
+       | COOKIE SYMBOL COLON cexp       (SgiCookie (SYMBOL, cexp), s (COOKIEleft, cexpright))
 
 sgis   :                                ([])
        | sgi sgis                       (sgi :: sgis)
diff --git a/src/urweb.lex b/src/urweb.lex
index d5393e7d..f5ea558a 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -313,6 +313,7 @@ notags = [^<{\n]+;
 <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));
diff --git a/tests/cookie.ur b/tests/cookie.ur
new file mode 100644
index 00000000..b2bca580
--- /dev/null
+++ b/tests/cookie.ur
@@ -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>
+
diff --git a/tests/cookie.urp b/tests/cookie.urp
new file mode 100644
index 00000000..61a1a1e0
--- /dev/null
+++ b/tests/cookie.urp
@@ -0,0 +1,3 @@
+debug
+
+cookie