aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-11 14:11:17 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-11 14:11:17 -0400
commitd5eb08193a3a5e5d8117d4b2a2eb644288f4c9d0 (patch)
treee1461576f206a882ad17cfea31c29860344dfe1c /src/elaborate.sml
parent750ee01b9760664192e6ff63d221033b141c3d70 (diff)
Tweaks to table signatures and MonoOpt summarizing
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml18
1 files changed, 12 insertions, 6 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 07818a57..8902409d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2237,14 +2237,21 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
| L.SgiTable (x, c, pe, ce) =>
let
val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
- val x' = x ^ "_hidden_constraints"
- val (env', hidden_n) = E.pushCNamed env x' cstK NONE
- val hidden = (L'.CNamed hidden_n, loc)
val (c', ck, gs') = elabCon (env, denv) c
val pkey = cunif (loc, cstK)
val visible = cunif (loc, cstK)
- val uniques = (L'.CConcat (visible, hidden), loc)
+ val (env', ds, uniques) =
+ case (#1 pe, #1 ce) of
+ (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) =>
+ let
+ val x' = x ^ "_hidden_constraints"
+ val (env', hidden_n) = E.pushCNamed env x' cstK NONE
+ val hidden = (L'.CNamed hidden_n, loc)
+ in
+ (env', [(L'.SgiConAbs (x', hidden_n, cstK), loc)], (L'.CConcat (visible, hidden), loc))
+ end
+ | _ => (env, [], visible)
val ct = tableOf ()
val ct = (L'.CApp (ct, c'), loc)
@@ -2272,8 +2279,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
checkCon env' pe' pet pst;
checkCon env' ce' cet cst;
- ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
- (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
+ (ds @ [(L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
end
| L.SgiStr (x, sgn) =>