summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 10:29:55 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 10:29:55 -0500
commitcf761fbfd28af10fb6e11bdf583f2821abecfe44 (patch)
tree5857f5dc14c0b71b191d1a267c9a8fdfcee03810 /src/elaborate.sml
parent52bcb1e926570966efe93672e968999f4f2e14f8 (diff)
Cookies through elaborate
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml66
1 files changed, 65 insertions, 1 deletions
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