diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-06 10:43:48 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-06 10:43:48 -0500 |
| commit | ea5a24773259c147e806960843d3305a3c72067b (patch) | |
| tree | 2e714f5fc0b6c669bad6c201f3a4b11fec490513 /src/elab_env.sml | |
| parent | 12bb99a0ba702af12e89bfe544f2a572e5d4818d (diff) | |
Cookies through explify
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 27 |
1 files changed, 0 insertions, 27 deletions
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 |