# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1383596063 18000
# Node ID b7cd3c7c7edda7ff315b773f9b14df7a86e05a77
# Parent  8297968cf7ef62783d7198999f31926d346b020a
Interpret 'table' signature items more flexibly, automatically adding (Ur) constraints to support a kind of subtyping over (SQL) constraint sets

diff -r 8297968cf7ef -r b7cd3c7c7edd src/elaborate.sml
--- a/src/elaborate.sml	Mon Nov 04 08:38:20 2013 -0500
+++ b/src/elaborate.sml	Mon Nov 04 15:14:23 2013 -0500
@@ -2595,17 +2595,12 @@
              val (c', ck, gs') = elabCon (env, denv) c
              val pkey = cunif env (loc, cstK)
              val visible = cunif env (loc, cstK)
-             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 x' = x ^ "_hidden_constraints"
+             val (env', hidden_n) = E.pushCNamed env x' cstK NONE
+             val hidden = (L'.CNamed hidden_n, loc)
+
+             val uniques = (L'.CConcat (visible, hidden), loc)
 
              val ct = tableOf ()
              val ct = (L'.CApp (ct, c'), loc)
@@ -2619,8 +2614,6 @@
              val pst = (L'.CApp (pst, c'), loc)
              val pst = (L'.CApp (pst, pkey), loc)
 
-             val (env', n) = E.pushENamed env' x ct
-
              val (ce', cet, gs''') = elabExp (env', denv) ce
              val gs''' = List.mapPartial (fn Disjoint x => SOME x
                                            | _ => NONE) gs'''
@@ -2628,12 +2621,16 @@
              val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
              val cst = (L'.CApp (cst, c'), loc)
              val cst = (L'.CApp (cst, visible), loc)
+
+             val (env', n) = E.pushENamed env' x ct
          in
              checkKind env c' ck (L'.KRecord (L'.KType, loc), loc);
              checkCon env' pe' pet pst;
              checkCon env' ce' cet cst;
 
-             (ds @ [(L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
+             ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
+               (L'.SgiConstraint (visible, hidden), loc),
+               (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
          end
 
        | L.SgiStr (x, sgn) =>
@@ -3582,7 +3579,7 @@
                              SOME (L.CVar (s :: ms, x), loc)
                          end
                        | L'.CName s => SOME (L.CName s, loc)
-                       | L'.CRecord (_, xcs) =>
+                       | L'.CRecord (k, xcs) =>
                          let
                              fun fields xcs =
                                  case xcs of
@@ -3591,9 +3588,14 @@
                                      case (decompileCon env x, decompileCon env t, fields xcs) of
                                          (SOME x, SOME t, SOME xcs) => SOME ((x, t) :: xcs)
                                        | _ => NONE
+
+                             val c' = Option.map (fn xcs => (L.CRecord xcs, loc))
+                                                 (fields xcs)
                          in
-                             Option.map (fn xcs => (L.CRecord xcs, loc))
-                             (fields xcs)
+                             Option.map (fn c' =>
+                                            case decompileKind k of
+                                                NONE => c'
+                                              | SOME k' => (L.CAnnot (c', (L.KRecord k', loc)), loc)) c'
                          end
                        | L'.CConcat (c1, c2) =>
                          (case (decompileCon env c1, decompileCon env c2) of