Mercurial > urweb
diff src/elaborate.sml @ 90:94ef20a31550
Fancier head normalization pushed inside of Disjoint
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 03 Jul 2008 11:04:25 -0400 |
| parents | 7bab29834cd6 |
| children | 4327abd52997 |
line wrap: on
line diff
--- a/src/elaborate.sml Tue Jul 01 16:06:58 2008 -0400 +++ b/src/elaborate.sml Thu Jul 03 11:04:25 2008 -0400 @@ -251,13 +251,13 @@ val ku1 = kunif loc val ku2 = kunif loc - val denv' = D.assert env denv (c1', c2') - val (c', k, gs3) = elabCon (env, denv') c + val (denv', gs3) = D.assert env denv (c1', c2') + val (c', k, gs4) = elabCon (env, denv') c in checkKind env c1' k1 (L'.KRecord ku1, loc); checkKind env c2' k2 (L'.KRecord ku2, loc); - ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3) + ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) end | L.TRecord c => let @@ -330,13 +330,13 @@ val ku1 = kunif loc val ku2 = kunif loc - val denv' = D.assert env denv (c1', c2') - val (c', k, gs3) = elabCon (env, denv') c + val (denv', gs3) = D.assert env denv (c1', c2') + val (c', k, gs4) = elabCon (env, denv') c in checkKind env c1' k1 (L'.KRecord ku1, loc); checkKind env c2' k2 (L'.KRecord ku2, loc); - ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3) + ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) end | L.CName s => @@ -369,8 +369,7 @@ let val r2 = (L'.CRecord (k, [xc']), loc) in - map (fn cs => (loc, env, denv, cs)) (D.prove env denv (r1, r2, loc)) - @ ds + D.prove env denv (r1, r2, loc) @ ds end) ds rest in @@ -389,7 +388,7 @@ checkKind env c1' k1 k; checkKind env c2' k2 k; ((L'.CConcat (c1', c2'), loc), k, - map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1', c2', loc)) @ gs1 @ gs2) + D.prove env denv (c1', c2', loc) @ gs1 @ gs2) end | L.CFold => let @@ -545,23 +544,7 @@ | L'.CError => kerror | L'.CUnif (_, k, _, _) => k -fun hnormCon (env, denv) c = - let - val cAll as (c, loc) = ElabOps.hnormCon env c - - fun doDisj (c1, c2, c) = - let - val (c, gs) = hnormCon (env, denv) c - in - (c, - map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1, c2, loc)) @ gs) - end - in - case c of - L'.CDisjoint cs => doDisj cs - | L'.TDisjoint cs => doDisj cs - | _ => (cAll, []) - end +val hnormCon = D.hnormCon fun unifyRecordCons (env, denv) (c1, c2) = let @@ -703,9 +686,9 @@ let val (c1, gs1) = hnormCon (env, denv) c1 val (c2, gs2) = hnormCon (env, denv) c2 + val gs3 = unifyCons'' (env, denv) c1 c2 in - unifyCons'' (env, denv) c1 c2; - gs1 @ gs2 + gs1 @ gs2 @ gs3 end and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) = @@ -1040,13 +1023,13 @@ val ku1 = kunif loc val ku2 = kunif loc - val denv' = D.assert env denv (c1', c2') - val (e', t, gs3) = elabExp (env, denv') e + val (denv', gs3) = D.assert env denv (c1', c2') + val (e', t, gs4) = elabExp (env, denv') e in checkKind env c1' k1 (L'.KRecord ku1, loc); checkKind env c2' k2 (L'.KRecord ku2, loc); - (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3) + (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4) end | L.ERecord xes => @@ -1075,8 +1058,7 @@ val xc' = (x', t') val r2 = (L'.CRecord (k, [xc']), loc) in - map (fn cs => (loc, env, denv, cs)) (D.prove env denv (r1, r2, loc)) - @ gs + D.prove env denv (r1, r2, loc) @ gs end) gs rest in @@ -1100,9 +1082,7 @@ val gs3 = checkCon (env, denv) e' et (L'.TRecord (L'.CConcat (first, rest), loc), loc) - val gs4 = - map (fn cs => (loc, env, denv, cs)) - (D.prove env denv (first, rest, loc)) + val gs4 = D.prove env denv (first, rest, loc) in ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4) end @@ -1287,12 +1267,12 @@ val (c1', k1, gs1) = elabCon (env, denv) c1 val (c2', k2, gs2) = elabCon (env, denv) c2 - val denv = D.assert env denv (c1', c2') + val (denv, gs3) = D.assert env denv (c1', c2') in checkKind env c1' k1 (L'.KRecord (kunif loc), loc); checkKind env c2' k2 (L'.KRecord (kunif loc), loc); - ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) + ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) end and elabSgn (env, denv) (sgn, loc) = @@ -1484,7 +1464,16 @@ val denv = case cso of NONE => (strError env (UnboundStr (loc, str)); denv) - | SOME cs => foldl (fn ((c1, c2), denv) => D.assert env denv (c1, c2)) denv cs + | SOME cs => foldl (fn ((c1, c2), denv) => + let + val (denv, gs) = D.assert env denv (c1, c2) + in + case gs of + [] => () + | _ => raise Fail "dopenConstraints: Sub-constraints remain"; + + denv + end) denv cs in denv end @@ -1500,7 +1489,10 @@ fun sgiBindsD (env, denv) (sgi, _) = case sgi of - L'.SgiConstraint (c1, c2) => D.assert env denv (c1, c2) + L'.SgiConstraint (c1, c2) => + (case D.assert env denv (c1, c2) of + (denv, []) => denv + | _ => raise Fail "sgiBindsD: Sub-constraints remain") | _ => denv fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = @@ -1634,7 +1626,15 @@ case sgi1 of L'.SgiConstraint (c1, d1) => if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then - SOME (env, D.assert env denv (c2, d2)) + let + val (denv, gs) = D.assert env denv (c2, d2) + in + case gs of + [] => () + | _ => raise Fail "subSgn: Sub-constraints remain"; + + SOME (env, denv) + end else NONE | _ => NONE) @@ -1793,14 +1793,14 @@ let val (c1', k1, gs1) = elabCon (env, denv) c1 val (c2', k2, gs2) = elabCon (env, denv) c2 - val gs3 = map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1', c2', loc)) + val gs3 = D.prove env denv (c1', c2', loc) - val denv' = D.assert env denv (c1', c2') + val (denv', gs4) = D.assert env denv (c1', c2') in checkKind env c1' k1 (L'.KRecord (kunif loc), loc); checkKind env c2' k2 (L'.KRecord (kunif loc), loc); - ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3)) + ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4)) end | L.DOpenConstraints (m, ms) => @@ -1982,13 +1982,15 @@ if ErrorMsg.anyErrors () then () else - app (fn (loc, env, denv, (c1, c2)) => + app (fn (loc, env, denv, c1, c2) => case D.prove env denv (c1, c2, loc) of [] => () | _ => (ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; eprefaces' [("Con 1", p_con env c1), - ("Con 2", p_con env c2)])) gs; + ("Con 2", p_con env c2), + ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), + ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) gs; (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file end