Mercurial > urweb
diff src/elaborate.sml @ 705:e6706a1df013
Track uniqueness sets in table types
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 07 Apr 2009 14:11:32 -0400 |
| parents | 70cbdcf5989b |
| children | 1fb318c17546 |
line wrap: on
line diff
--- a/src/elaborate.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/elaborate.sml Tue Apr 07 14:11:32 2009 -0400 @@ -880,88 +880,6 @@ (L'.CError, _) => () | (_, L'.CError) => () - | (L'.CRecord _, _) => isRecord () - | (_, L'.CRecord _) => isRecord () - | (L'.CConcat _, _) => isRecord () - | (_, L'.CConcat _) => isRecord () - - | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => - if r1 = r2 then - () - else - (unifyKinds env k1 k2; - r1 := SOME c2All) - - | (L'.CUnif (_, _, _, r), _) => - if occursCon r c2All then - err COccursCheckFailed - else - r := SOME c2All - | (_, L'.CUnif (_, _, _, r)) => - if occursCon r c1All then - err COccursCheckFailed - else - r := SOME c1All - - | (L'.CUnit, L'.CUnit) => () - - | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => - (unifyCons' env d1 d2; - unifyCons' env r1 r2) - | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => - if expl1 <> expl2 then - err CExplicitness - else - (unifyKinds env d1 d2; - let - (*val befor = Time.now ()*) - val env' = E.pushCRel env x1 d1 - in - (*TextIO.print ("E.pushCRel: " - ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) - ^ "\n");*) - unifyCons' env' r1 r2 - end) - | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 - | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => - (unifyCons' env c1 c2; - unifyCons' env d1 d2; - unifyCons' env e1 e2) - - | (L'.CRel n1, L'.CRel n2) => - if n1 = n2 then - () - else - err CIncompatible - | (L'.CNamed n1, L'.CNamed n2) => - if n1 = n2 then - () - else - err CIncompatible - - | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => - (unifyCons' env d1 d2; - unifyCons' env r1 r2) - | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => - (unifyKinds env k1 k2; - unifyCons' (E.pushCRel env x1 k1) c1 c2) - - | (L'.CName n1, L'.CName n2) => - if n1 = n2 then - () - else - err CIncompatible - - | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => - if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then - () - else - err CIncompatible - - | (L'.CTuple cs1, L'.CTuple cs2) => - ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) - handle ListPair.UnequalLengths => err CIncompatible) - | (L'.CProj (c1, n1), _) => let fun trySnd () = @@ -1020,6 +938,88 @@ | _ => err CIncompatible) | _ => err CIncompatible) + | (L'.CRecord _, _) => isRecord () + | (_, L'.CRecord _) => isRecord () + | (L'.CConcat _, _) => isRecord () + | (_, L'.CConcat _) => isRecord () + + | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => + if r1 = r2 then + () + else + (unifyKinds env k1 k2; + r1 := SOME c2All) + + | (L'.CUnif (_, _, _, r), _) => + if occursCon r c2All then + err COccursCheckFailed + else + r := SOME c2All + | (_, L'.CUnif (_, _, _, r)) => + if occursCon r c1All then + err COccursCheckFailed + else + r := SOME c1All + + | (L'.CUnit, L'.CUnit) => () + + | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => + (unifyCons' env d1 d2; + unifyCons' env r1 r2) + | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => + if expl1 <> expl2 then + err CExplicitness + else + (unifyKinds env d1 d2; + let + (*val befor = Time.now ()*) + val env' = E.pushCRel env x1 d1 + in + (*TextIO.print ("E.pushCRel: " + ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) + ^ "\n");*) + unifyCons' env' r1 r2 + end) + | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 + | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => + (unifyCons' env c1 c2; + unifyCons' env d1 d2; + unifyCons' env e1 e2) + + | (L'.CRel n1, L'.CRel n2) => + if n1 = n2 then + () + else + err CIncompatible + | (L'.CNamed n1, L'.CNamed n2) => + if n1 = n2 then + () + else + err CIncompatible + + | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => + (unifyCons' env d1 d2; + unifyCons' env r1 r2) + | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => + (unifyKinds env k1 k2; + unifyCons' (E.pushCRel env x1 k1) c1 c2) + + | (L'.CName n1, L'.CName n2) => + if n1 = n2 then + () + else + err CIncompatible + + | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => + if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then + () + else + err CIncompatible + + | (L'.CTuple cs1, L'.CTuple cs2) => + ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) + handle ListPair.UnequalLengths => err CIncompatible) + | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => (unifyKinds env dom1 dom2; unifyKinds env ran1 ran2) @@ -2319,7 +2319,8 @@ | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] | L'.DExport _ => [] - | L'.DTable (tn, x, n, c, _) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)] + | L'.DTable (tn, x, n, c, _, cc) => + [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), cc), loc)), loc)] | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] | L'.DDatabase _ => [] @@ -3268,17 +3269,22 @@ | L.DTable (x, c, e) => let val (c', k, gs') = elabCon (env, denv) c - val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) + val uniques = cunif (loc, (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)) + + val ct = tableOf () + val ct = (L'.CApp (ct, c'), loc) + val ct = (L'.CApp (ct, uniques), loc) + + val (env, n) = E.pushENamed env x ct val (e', et, gs'') = elabExp (env, denv) e - val names = cunif (loc, (L'.KRecord (L'.KUnit, loc), loc)) val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) - val cst = (L'.CApp (cst, names), loc) val cst = (L'.CApp (cst, c'), loc) + val cst = (L'.CApp (cst, uniques), loc) in checkKind env c' k (L'.KRecord (L'.KType, loc), loc); checkCon env e' et cst; - ([(L'.DTable (!basis_r, x, n, c', e'), loc)], (env, denv, gs'' @ enD gs' @ gs)) + ([(L'.DTable (!basis_r, x, n, c', e', uniques), loc)], (env, denv, gs'' @ enD gs' @ gs)) end | L.DSequence x => let