Cookies through explify

13 files changed, 41 insertions, 277 deletions

diff --git a/src/elab.sml b/src/elab.sml
index afb8f7aa..d00d1f1a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -135,11 +135,8 @@ datatype sgn_item' =
        | SgiStr of string * int * sgn
        | SgiSgn of string * int * sgn
        | SgiConstraint of con * con
-       | SgiTable of int * string * int * con
-       | 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
diff --git a/src/elab_env.sml b/src/elab_env.sml
index a782771a..b14cd06c 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -588,11 +588,8 @@ fun sgiSeek (sgi, (sgns, strs, cons)) =
       | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
       | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
       | SgiConstraint _ => (sgns, strs, cons)
-      | SgiTable _ => (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
@@ -931,30 +928,9 @@ fun sgiBinds env (sgi, loc) =
       | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
       | SgiConstraint _ => env
 
-      | SgiTable (tn, x, n, c) =>
-        let
-            val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
-        in
-            pushENamedAs env x n t
-        end
-      | SgiSequence (tn, x, n) =>
-        let
-            val t = (CModProj (tn, [], "sql_sequence"), loc)
-        in
-            pushENamedAs env x n t
-        end
-
       | 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 =
     ElabUtil.Con.map {kind = id,
                       con = sgnS_con x}
@@ -1099,11 +1075,8 @@ fun sgnSeekConstraints (str, sgis) =
                   | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
                   | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
                   | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
-                  | SgiTable _ => seek (sgis, sgns, strs, cons, acc)
-                  | 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
diff --git a/src/elab_print.sml b/src/elab_print.sml
index a686abe5..2afedef1 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -516,16 +516,6 @@ fun p_sgn_item env (sgi, _) =
                                        string "~",
                                        space,
                                        p_con env c2]
-      | SgiTable (_, x, n, c) => box [string "table",
-                                      space,
-                                      p_named x n,
-                                      space,
-                                      string ":",
-                                      space,
-                                      p_con env c]
-      | SgiSequence (_, x, n) => box [string "sequence",
-                                      space,
-                                      p_named x n]
       | SgiClassAbs (x, n) => box [string "class",
                                    space,
                                    p_named x n]
@@ -536,13 +526,6 @@ 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
diff --git a/src/elab_util.sml b/src/elab_util.sml
index fe75ee0d..9c25ae86 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -538,20 +538,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                             S.map2 (con ctx c2,
                                     fn c2' =>
                                        (SgiConstraint (c1', c2'), loc)))
-              | SgiTable (tn, x, n, c) =>
-                S.map2 (con ctx c,
-                        fn c' =>
-                           (SgiTable (tn, x, n, c'), loc))
-              | SgiSequence _ => S.return2 siAll
               | SgiClassAbs _ => S.return2 siAll
               | SgiClass (x, n, c) =>
                 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)
@@ -575,13 +566,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  | SgiSgn (x, _, sgn) =>
                                                    bind (ctx, Sgn (x, sgn))
                                                  | SgiConstraint _ => ctx
-                                                 | SgiTable _ => ctx
-                                                 | SgiSequence _ => ctx
                                                  | 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)))
-                                                 | SgiCookie _ => ctx,
+                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))),
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
@@ -1005,11 +993,8 @@ and maxNameSgi (sgi, _) =
       | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | SgiConstraint _ => 0
-      | 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 3a966eaf..3b70c623 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1932,22 +1932,6 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
         end
 
-      | L.SgiTable (x, c) =>
-        let
-            val (c', k, gs) = elabCon (env, denv) c
-            val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
-        in
-            checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
-            ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs))
-        end
-
-      | L.SgiSequence x =>
-        let
-            val (env, n) = E.pushENamed env x (sequenceOf ())
-        in
-            ([(L'.SgiSequence (!basis_r, x, n), loc)], (env, denv, gs))
-        end
-
       | L.SgiClassAbs x =>
         let
             val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
@@ -1968,15 +1952,6 @@ 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 =>
@@ -2038,18 +2013,6 @@ and elabSgn (env, denv) (sgn, loc) =
                                        ();
                                    (cons, vals, sgns, SS.add (strs, x)))
                                 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
-                                | L'.SgiTable (_, x, _, _) =>
-                                  (if SS.member (vals, x) then
-                                       sgnError env (DuplicateVal (loc, x))
-                                   else
-                                       ();
-                                   (cons, SS.add (vals, x), sgns, strs))
-                                | L'.SgiSequence (_, x, _) =>
-                                  (if SS.member (vals, x) then
-                                       sgnError env (DuplicateVal (loc, x))
-                                   else
-                                       ();
-                                   (cons, SS.add (vals, x), sgns, strs))
                                 | L'.SgiClassAbs (x, _) =>
                                   (if SS.member (cons, x) then
                                        sgnError env (DuplicateCon (loc, x))
@@ -2061,13 +2024,7 @@ and elabSgn (env, denv) (sgn, loc) =
                                        sgnError env (DuplicateCon (loc, x))
                                    else
                                        ();
-                                   (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.add (cons, x), vals, sgns, strs)))
                     (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
         in
             ((L'.SgnConst sgis', loc), gs)
@@ -2199,12 +2156,6 @@ fun dopen (env, denv) {str, strs, sgn} =
                                               (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
                                             | L'.SgiConstraint (c1, c2) =>
                                               (L'.DConstraint (c1, c2), loc)
-                                            | L'.SgiTable (_, x, n, c) =>
-                                              (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc),
-                                                        (L'.EModProj (str, strs, x), loc)), loc)
-                                            | L'.SgiSequence (_, x, n) =>
-                                              (L'.DVal (x, n, sequenceOf (),
-                                                        (L'.EModProj (str, strs, x), loc)), loc)
                                             | L'.SgiClassAbs (x, n) =>
                                               let
                                                   val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
@@ -2219,9 +2170,6 @@ 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)
@@ -2274,11 +2222,11 @@ fun sgiOfDecl (d, loc) =
       | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
       | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
       | L'.DExport _ => []
-      | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)]
-      | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)]
+      | L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)]
+      | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), 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)]
+      | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
 
 fun sgiBindsD (env, denv) (sgi, _) =
     case sgi of
@@ -2508,36 +2456,6 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                  SOME (env, denv))
                                      else
                                          NONE
-                                   | L'.SgiTable (_, x', n1, c1) =>
-                                     if x = x' then
-                                         (case unifyCons (env, denv) (L'.CApp (tableOf (), 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
-                                   | L'.SgiSequence (_, x', n1) =>
-                                     if x = x' then
-                                         (case unifyCons (env, denv) (sequenceOf ()) c2 of
-                                              [] => SOME (env, denv)
-                                            | _ => NONE)
-                                         handle CUnify (c1, c2, err) =>
-                                                (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
-                                                 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) =>
@@ -2600,31 +2518,6 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                          NONE
                                    | _ => NONE)
 
-                      | L'.SgiTable (_, x, n2, c2) =>
-                        seek (fn sgi1All as (sgi1, _) =>
-                                 case sgi1 of
-                                     L'.SgiTable (_, 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)
-
-                      | L'.SgiSequence (_, x, n2) =>
-                        seek (fn sgi1All as (sgi1, _) =>
-                                 case sgi1 of
-                                     L'.SgiSequence (_, x', n1) =>
-                                     if x = x' then
-                                         SOME (env, denv)
-                                     else
-                                         NONE
-                                   | _ => NONE)
-
                       | L'.SgiClassAbs (x, n2) =>
                         seek (fn sgi1All as (sgi1, _) =>
                                  let
@@ -2681,21 +2574,6 @@ 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)
@@ -3347,26 +3225,6 @@ and elabStr (env, denv) (str, loc) =
                                   ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
                               end
                             | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
-                            | L'.SgiTable (tn, x, n, c) =>
-                              let
-                                  val (vals, x) =
-                                      if SS.member (vals, x) then
-                                          (vals, "?" ^ x)
-                                      else
-                                          (SS.add (vals, x), x)
-                              in
-                                  ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
-                              end
-                            | L'.SgiSequence (tn, x, n) =>
-                              let
-                                  val (vals, x) =
-                                      if SS.member (vals, x) then
-                                          (vals, "?" ^ x)
-                                      else
-                                          (SS.add (vals, x), x)
-                              in
-                                  ((L'.SgiSequence (tn, x, n), loc) :: sgis, cons, vals, sgns, strs)
-                              end
                             | L'.SgiClassAbs (x, n) =>
                               let
                                   val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
@@ -3390,16 +3248,6 @@ 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/expl.sml b/src/expl.sml
index 8f531516..57396684 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -110,8 +110,6 @@ datatype sgn_item' =
        | SgiVal of string * int * con
        | SgiSgn of string * int * sgn
        | SgiStr of string * int * sgn
-       | SgiTable of int * string * int * con
-       | SgiSequence of int * string * int
 
 and sgn' =
     SgnConst of sgn_item list
@@ -136,6 +134,7 @@ datatype decl' =
        | DTable of int * string * int * con
        | DSequence of int * string * int
        | DDatabase of string
+       | DCookie of int * string * int * con
 
      and str' =
          StrConst of decl list
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 43456c41..0fefec2d 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -295,6 +295,12 @@ fun declBinds env (d, loc) =
             pushENamed env x n t
         end
       | DDatabase _ => env
+      | DCookie (tn, x, n, c) =>
+        let
+            val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc)
+        in
+            pushENamed env x n t
+        end
 
 fun sgiBinds env (sgi, loc) =
     case sgi of
@@ -341,17 +347,4 @@ fun sgiBinds env (sgi, loc) =
       | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
       | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
 
-      | SgiTable (tn, x, n, c) =>
-        let
-            val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
-        in
-            pushENamed env x n t
-        end
-      | SgiSequence (tn, x, n) =>
-        let
-            val t = (CModProj (tn, [], "sql_sequence"), loc)
-        in
-            pushENamed env x n t
-        end
-
 end
diff --git a/src/expl_print.sml b/src/expl_print.sml
index aecc3a84..2d41ab34 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -471,16 +471,6 @@ fun p_sgn_item env (sgi, _) =
                                    string "=",
                                    space,
                                    p_sgn env sgn]
-      | SgiTable (_, x, n, c) => box [string "table",
-                                      space,
-                                      p_named x n,
-                                      space,
-                                      string ":",
-                                      space,
-                                      p_con env c]
-      | SgiSequence (_, x, n) => box [string "sequence",
-                                      space,
-                                      p_named x n]
 
 and p_sgn env (sgn, loc) =
     case sgn of
@@ -635,6 +625,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/expl_util.sml b/src/expl_util.sml
index 337ea8d6..2bd9eabd 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -432,11 +432,6 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                 S.map2 (sg ctx s,
                      fn s' =>
                         (SgiSgn (x, n, s'), loc))
-              | SgiTable (tn, x, n, c) =>
-                S.map2 (con ctx c,
-                        fn c' =>
-                           (SgiTable (tn, x, n, c'), loc))
-              | SgiSequence _ => S.return2 siAll
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -458,9 +453,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  | SgiStr (x, _, sgn) =>
                                                    bind (ctx, Str (x, sgn))
                                                  | SgiSgn (x, _, sgn) =>
-                                                   bind (ctx, Sgn (x, sgn))
-                                                 | SgiTable _ => ctx
-                                                 | SgiSequence _ => ctx,
+                                                   bind (ctx, Sgn (x, sgn)),
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
diff --git a/src/explify.sml b/src/explify.sml
index e19bb200..4115476b 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -137,8 +137,6 @@ fun explifySgi (sgi, loc) =
       | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
       | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
       | L.SgiConstraint _ => NONE
-      | L.SgiTable (nt, x, n, c) => SOME (L'.SgiTable (nt, x, n, explifyCon c), loc)
-      | L.SgiSequence (nt, x, n) => SOME (L'.SgiSequence (nt, x, n), loc)
       | L.SgiClassAbs (x, n) => SOME (L'.SgiConAbs (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)), loc)
       | L.SgiClass (x, n, c) => SOME (L'.SgiCon (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc),
                                                  explifyCon c), loc)
@@ -175,6 +173,7 @@ fun explifyDecl (d, loc : EM.span) =
       | L.DClass (x, n, c) => SOME (L'.DCon (x, n,
                                              (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), explifyCon c), loc)
       | L.DDatabase s => SOME (L'.DDatabase s, loc)
+      | L.DCookie (nt, x, n, c) => SOME (L'.DCookie (nt, x, n, explifyCon c), loc)
 
 and explifyStr (str, loc) =
     case str of
diff --git a/src/source.sml b/src/source.sml
index a0591afb..2a348338 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -81,11 +81,8 @@ datatype sgn_item' =
        | SgiSgn of string * sgn
        | SgiInclude of sgn
        | SgiConstraint of con * con
-       | SgiTable of string * con
-       | SgiSequence of string
        | SgiClassAbs of string
        | SgiClass of string * con
-       | SgiCookie of string * con
 
 and sgn' =
     SgnConst of sgn_item list
diff --git a/src/source_print.sml b/src/source_print.sml
index d33fb38d..3c26812f 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -408,16 +408,6 @@ fun p_sgn_item (sgi, _) =
                                        string "~",
                                        space,
                                        p_con c2]
-      | SgiTable (x, c) => box [string "table",
-                                space,
-                                string x,
-                                space,
-                                string ":",
-                                space,
-                                p_con c]
-      | SgiSequence x => box [string "sequence",
-                              space,
-                              string x]
       | SgiClassAbs x => box [string "class",
                               space,
                               string x]
@@ -428,13 +418,6 @@ 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
diff --git a/src/urweb.grm b/src/urweb.grm
index 879afb9c..b2f2d486 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -497,8 +497,19 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
                                          s (FUNCTORleft, sgn2right))
        | INCLUDE sgn                    (SgiInclude sgn, s (INCLUDEleft, sgnright))
        | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
-       | TABLE SYMBOL COLON cexp        (SgiTable (SYMBOL, entable cexp), s (TABLEleft, cexpright))
-       | SEQUENCE SYMBOL                (SgiSequence SYMBOL, s (SEQUENCEleft, SYMBOLright))
+       | TABLE SYMBOL COLON cexp        (let
+                                             val loc = s (TABLEleft, cexpright)
+                                             val t = (CApp ((CVar (["Basis"], "sql_table"), loc),
+                                                            entable cexp), loc)
+                                         in
+                                             (SgiVal (SYMBOL, t), loc)
+                                         end)
+       | SEQUENCE SYMBOL                (let
+                                             val loc = s (SEQUENCEleft, SYMBOLright)
+                                             val t = (CVar (["Basis"], "sql_sequence"), loc)
+                                         in
+                                             (SgiVal (SYMBOL, t), loc)
+                                         end)
        | CLASS SYMBOL                   (SgiClassAbs SYMBOL, s (CLASSleft, SYMBOLright))
        | CLASS SYMBOL EQ cexp           (SgiClass (SYMBOL, cexp), s (CLASSleft, cexpright))
        | CLASS SYMBOL SYMBOL EQ cexp    (let
@@ -508,7 +519,13 @@ 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))
+       | COOKIE SYMBOL COLON cexp       (let
+                                             val loc = s (COOKIEleft, cexpright)
+                                             val t = (CApp ((CVar (["Basis"], "http_cookie"), loc),
+                                                            entable cexp), loc)
+                                         in
+                                             (SgiVal (SYMBOL, t), loc)
+                                         end)
 
 sgis   :                                ([])
        | sgi sgis                       (sgi :: sgis)