summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 10:43:48 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 10:43:48 -0500
commitea5a24773259c147e806960843d3305a3c72067b (patch)
tree2e714f5fc0b6c669bad6c201f3a4b11fec490513 /src/elab_env.sml
parent12bb99a0ba702af12e89bfe544f2a572e5d4818d (diff)
Cookies through explify
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml27
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