Mercurial > urweb
diff src/elab_env.sml @ 203:dd82457fda82
Parsing and elaborating 'table'
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 14 Aug 2008 13:20:29 -0400 |
parents | aa54250f58ac |
children | cb8f69556975 |
line wrap: on
line diff
--- a/src/elab_env.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/elab_env.sml Thu Aug 14 13:20:29 2008 -0400 @@ -404,6 +404,16 @@ | 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 @@ | 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 @@ | 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 @@ | 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