Mercurial > urweb
diff src/elaborate.sml @ 1886:b7cd3c7c7edd
Interpret 'table' signature items more flexibly, automatically adding (Ur) constraints to support a kind of subtyping over (SQL) constraint sets
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 04 Nov 2013 15:14:23 -0500 |
parents | 5125b1df6045 |
children | 006633a0039a |
line wrap: on
line diff
--- 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