diff src/elab_util.sml @ 205:cb8f69556975

Elaborating 'SELECT *' queries
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 15:24:59 -0400
parents dd82457fda82
children cc68da3801bc
line wrap: on
line diff
--- a/src/elab_util.sml	Thu Aug 14 13:59:11 2008 -0400
+++ b/src/elab_util.sml	Thu Aug 14 15:24:59 2008 -0400
@@ -436,10 +436,10 @@
                             S.map2 (con ctx c2,
                                     fn c2' =>
                                        (SgiConstraint (c1', c2'), loc)))
-              | SgiTable (x, n, c) =>
+              | SgiTable (tn, x, n, c) =>
                 S.map2 (con ctx c,
                         fn c' =>
-                           (SgiTable (x, n, c'), loc))
+                           (SgiTable (tn, x, n, c'), loc))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -600,7 +600,9 @@
                                                    bind (ctx, Str (x, sgn))
                                                  | DConstraint _ => ctx
                                                  | DExport _ => ctx
-                                                 | DTable _ => ctx,
+                                                 | DTable (tn, x, n, c) =>
+                                                   bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc),
+                                                                                c), loc))),
                                                mfd ctx d)) ctx ds,
                      fn ds' => (StrConst ds', loc))
               | StrVar _ => S.return2 strAll
@@ -688,10 +690,10 @@
                                     fn str' =>
                                        (DExport (en, sgn', str'), loc)))
 
-              | DTable (x, n, c) =>
+              | DTable (tn, x, n, c) =>
                 S.map2 (mfc ctx c,
                         fn c' =>
-                           (DTable (x, n, c'), loc))
+                           (DTable (tn, x, n, c'), loc))
 
         and mfvi ctx (x, n, c, e) =
             S.bind2 (mfc ctx c,