diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-14 13:20:29 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-14 13:20:29 -0400 |
| commit | 25658a4755c86ffbda946fb8b97f882f3ce7a724 (patch) | |
| tree | 4ef4c28ab7483566127b841e2396bcc05d98e23d /src/elab_env.sml | |
| parent | 4a22e79410139a25a9615275c3b9adcd165a5988 (diff) | |
Parsing and elaborating 'table'
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index eac0c662..2d6afa4a 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -404,6 +404,16 @@ fun sgiBinds env (sgi, loc) = | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | SgiConstraint _ => env + | SgiTable (x, n, c) => + (case lookupStr env "Basis" of + NONE => raise Fail "ElabEnv.sgiBinds: Can't find Basis" + | SOME (n, _) => + let + val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) + in + pushENamedAs env x n t + end) + fun sgnSeek f sgis = let fun seek (sgis, sgns, strs, cons) = @@ -431,6 +441,7 @@ fun sgnSeek f sgis = | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) | SgiConstraint _ => seek (sgis, sgns, strs, cons) + | SgiTable _ => seek (sgis, sgns, strs, cons) in seek (sgis, IM.empty, IM.empty, IM.empty) end @@ -666,6 +677,7 @@ 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) in seek (sgis, IM.empty, IM.empty, IM.empty, []) end @@ -725,5 +737,14 @@ fun declBinds env (d, loc) = | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn | DConstraint _ => env | DExport _ => env + | DTable (x, n, c) => + (case lookupStr env "Basis" of + NONE => raise Fail "ElabEnv.declBinds: Can't find Basis" + | SOME (n, _) => + let + val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) + in + pushENamedAs env x n t + end) end |