Mercurial > urweb

comparison src/elaborate.sml @ 1886:b7cd3c7c7edd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
1885:8297968cf7ef 1886:b7cd3c7c7edd
2593 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) 2593 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
2594 2594
2595 val (c', ck, gs') = elabCon (env, denv) c 2595 val (c', ck, gs') = elabCon (env, denv) c
2596 val pkey = cunif env (loc, cstK) 2596 val pkey = cunif env (loc, cstK)
2597 val visible = cunif env (loc, cstK) 2597 val visible = cunif env (loc, cstK)
2598 val (env', ds, uniques) = 2598
2599 case (#1 pe, #1 ce) of 2599 val x' = x ^ "_hidden_constraints"
2600 (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) => 2600 val (env', hidden_n) = E.pushCNamed env x' cstK NONE
2601 let 2601 val hidden = (L'.CNamed hidden_n, loc)
2602 val x' = x ^ "_hidden_constraints" 2602
2603 val (env', hidden_n) = E.pushCNamed env x' cstK NONE 2603 val uniques = (L'.CConcat (visible, hidden), loc)
2604 val hidden = (L'.CNamed hidden_n, loc)
2605 in
2606 (env', [(L'.SgiConAbs (x', hidden_n, cstK), loc)], (L'.CConcat (visible, hidden), loc))
2607 end
2608 | _ => (env, [], visible)
2609 2604
2610 val ct = tableOf () 2605 val ct = tableOf ()
2611 val ct = (L'.CApp (ct, c'), loc) 2606 val ct = (L'.CApp (ct, c'), loc)
2612 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) 2607 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc)
2613 2608
2617 2612
2618 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) 2613 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc)
2619 val pst = (L'.CApp (pst, c'), loc) 2614 val pst = (L'.CApp (pst, c'), loc)
2620 val pst = (L'.CApp (pst, pkey), loc) 2615 val pst = (L'.CApp (pst, pkey), loc)
2621 2616
2622 val (env', n) = E.pushENamed env' x ct
2623
2624 val (ce', cet, gs''') = elabExp (env', denv) ce 2617 val (ce', cet, gs''') = elabExp (env', denv) ce
2625 val gs''' = List.mapPartial (fn Disjoint x => SOME x 2618 val gs''' = List.mapPartial (fn Disjoint x => SOME x
2626 | _ => NONE) gs''' 2619 | _ => NONE) gs'''
2627 2620
2628 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) 2621 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
2629 val cst = (L'.CApp (cst, c'), loc) 2622 val cst = (L'.CApp (cst, c'), loc)
2630 val cst = (L'.CApp (cst, visible), loc) 2623 val cst = (L'.CApp (cst, visible), loc)
2624
2625 val (env', n) = E.pushENamed env' x ct
2631 in 2626 in
2632 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); 2627 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc);
2633 checkCon env' pe' pet pst; 2628 checkCon env' pe' pet pst;
2634 checkCon env' ce' cet cst; 2629 checkCon env' ce' cet cst;
2635 2630
2636 (ds @ [(L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) 2631 ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
2632 (L'.SgiConstraint (visible, hidden), loc),
2633 (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
2637 end 2634 end
2638 2635
2639 | L.SgiStr (x, sgn) => 2636 | L.SgiStr (x, sgn) =>
2640 let 2637 let
2641 val (sgn', gs') = elabSgn (env, denv) sgn 2638 val (sgn', gs') = elabSgn (env, denv) sgn
3580 val (s, _) = E.lookupStrNamed env m1 3577 val (s, _) = E.lookupStrNamed env m1
3581 in 3578 in
3582 SOME (L.CVar (s :: ms, x), loc) 3579 SOME (L.CVar (s :: ms, x), loc)
3583 end 3580 end
3584 | L'.CName s => SOME (L.CName s, loc) 3581 | L'.CName s => SOME (L.CName s, loc)
3585 | L'.CRecord (_, xcs) => 3582 | L'.CRecord (k, xcs) =>
3586 let 3583 let
3587 fun fields xcs = 3584 fun fields xcs =
3588 case xcs of 3585 case xcs of
3589 [] => SOME [] 3586 [] => SOME []
3590 | (x, t) :: xcs => 3587 | (x, t) :: xcs =>
3591 case (decompileCon env x, decompileCon env t, fields xcs) of 3588 case (decompileCon env x, decompileCon env t, fields xcs) of
3592 (SOME x, SOME t, SOME xcs) => SOME ((x, t) :: xcs) 3589 (SOME x, SOME t, SOME xcs) => SOME ((x, t) :: xcs)
3593 | _ => NONE 3590 | _ => NONE
3591
3592 val c' = Option.map (fn xcs => (L.CRecord xcs, loc))
3593 (fields xcs)
3594 in 3594 in
3595 Option.map (fn xcs => (L.CRecord xcs, loc)) 3595 Option.map (fn c' =>
3596 (fields xcs) 3596 case decompileKind k of
3597 NONE => c'
3598 | SOME k' => (L.CAnnot (c', (L.KRecord k', loc)), loc)) c'
3597 end 3599 end
3598 | L'.CConcat (c1, c2) => 3600 | L'.CConcat (c1, c2) =>
3599 (case (decompileCon env c1, decompileCon env c2) of 3601 (case (decompileCon env c1, decompileCon env c2) of
3600 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc) 3602 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
3601 | _ => NONE) 3603 | _ => NONE)