summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-14 15:24:59 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-14 15:24:59 -0400
commit9a65eddb59384f5784ed3ef0a641ca65b52645ce (patch)
tree6c2cbea03ee39858bde49e54932e19e744ba84c6 /src/elab_util.sml
parent14fbe79a3735e547f03cd8e95ca925fbdbb1841a (diff)
Elaborating 'SELECT *' queries
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml12
1 files changed, 7 insertions, 5 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 8cd02549..3c1860c7 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -436,10 +436,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
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,