summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_env.sml15
-rw-r--r--src/elab_print.sml14
-rw-r--r--src/elab_util.sml27
-rw-r--r--src/elaborate.sml66
-rw-r--r--src/elisp/urweb-defs.el6
-rw-r--r--src/elisp/urweb-mode.el4
-rw-r--r--src/source.sml2
-rw-r--r--src/source_print.sml15
-rw-r--r--src/unnest.sml1
-rw-r--r--src/urweb.grm3
-rw-r--r--src/urweb.lex1
12 files changed, 144 insertions, 12 deletions
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));
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 15:34:28 +0000