From f78c57eee6a26977b329a7e2d452d17a9e91ac41 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Mon, 4 Nov 2013 15:14:23 -0500
Subject: Interpret 'table' signature items more flexibly, automatically adding
 (Ur) constraints to support a kind of subtyping over (SQL) constraint sets

---
 src/elaborate.sml | 36 +++++++++++++++++++-----------------
 1 file changed, 19 insertions(+), 17 deletions(-)

(limited to 'src/elaborate.sml')

diff --git a/src/elaborate.sml b/src/elaborate.sml
index ff5a3b95..9906cf92 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2595,17 +2595,12 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
              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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
              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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
              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 @@ and wildifyStr env (str, sgn) =
                              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 @@ and wildifyStr env (str, sgn) =
                                      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
-- 
cgit v1.2.3