Mercurial > urweb
changeset 460:d34834af4512
Cookies through explify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 06 Nov 2008 10:43:48 -0500 |
| parents | f542bc3133dc |
| children | 5c9606deacb6 |
| files | src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_env.sml src/expl_print.sml src/expl_util.sml src/explify.sml src/source.sml src/source_print.sml src/urweb.grm |
| diffstat | 13 files changed, 41 insertions(+), 277 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/elab.sml Thu Nov 06 10:43:48 2008 -0500 @@ -135,11 +135,8 @@ | 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
--- a/src/elab_env.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/elab_env.sml Thu Nov 06 10:43:48 2008 -0500 @@ -588,11 +588,8 @@ | 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 @@ | 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 @@ | 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
--- a/src/elab_print.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/elab_print.sml Thu Nov 06 10:43:48 2008 -0500 @@ -516,16 +516,6 @@ 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 @@ 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
--- a/src/elab_util.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/elab_util.sml Thu Nov 06 10:43:48 2008 -0500 @@ -538,20 +538,11 @@ 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 @@ | 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 @@ | 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
--- a/src/elaborate.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/elaborate.sml Thu Nov 06 10:43:48 2008 -0500 @@ -1932,22 +1932,6 @@ ([(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 @@ ([(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 @@ (); (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 @@ 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 @@ (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 @@ 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 @@ | 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 @@ 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 @@ 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 @@ 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 @@ ((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 @@ (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/expl.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/expl.sml Thu Nov 06 10:43:48 2008 -0500 @@ -110,8 +110,6 @@ | 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 @@ | 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
--- a/src/expl_env.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/expl_env.sml Thu Nov 06 10:43:48 2008 -0500 @@ -295,6 +295,12 @@ 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 @@ | 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
--- a/src/expl_print.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/expl_print.sml Thu Nov 06 10:43:48 2008 -0500 @@ -471,16 +471,6 @@ 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 @@ | 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/expl_util.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/expl_util.sml Thu Nov 06 10:43:48 2008 -0500 @@ -432,11 +432,6 @@ 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 @@ | 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))
--- a/src/explify.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/explify.sml Thu Nov 06 10:43:48 2008 -0500 @@ -137,8 +137,6 @@ | 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 @@ | 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
--- a/src/source.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/source.sml Thu Nov 06 10:43:48 2008 -0500 @@ -81,11 +81,8 @@ | 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
--- a/src/source_print.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/source_print.sml Thu Nov 06 10:43:48 2008 -0500 @@ -408,16 +408,6 @@ 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 @@ 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
--- a/src/urweb.grm Thu Nov 06 10:29:55 2008 -0500 +++ b/src/urweb.grm Thu Nov 06 10:43:48 2008 -0500 @@ -497,8 +497,19 @@ 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 @@ 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)