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