Mercurial > urweb
changeset 1576:f6c74b4bc4e6
Change error message display order: only show disjointness/type class failures if all record unifications succeeded
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 15 Oct 2011 10:31:30 -0400 |
| parents | 287604b4a08d |
| children | 911ebbd23919 |
| files | src/elaborate.sml tests/nopoly.ur |
| diffstat | 2 files changed, 39 insertions(+), 36 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Sat Oct 15 10:19:50 2011 -0400 +++ b/src/elaborate.sml Sat Oct 15 10:31:30 2011 -0400 @@ -4335,6 +4335,8 @@ unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)) delayed end + + val checkConstraintErrors = ref (fn () => ()) in oneSummaryRound (); @@ -4404,42 +4406,36 @@ ([], _) => () | (_, true) => (oneSummaryRound (); solver gs) | _ => - app (fn Disjoint (loc, env, denv, c1, c2) => - let - val c1' = ElabOps.hnormCon env c1 - val c2' = ElabOps.hnormCon env c2 - - fun isUnif (c, _) = - case c of - L'.CUnif _ => true - | _ => false - - fun maybeAttr (c, _) = - case c of - L'.CRecord ((L'.KType, _), xts) => true - | _ => false - in - ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; - eprefaces' [("Con 1", p_con env c1), - ("Con 2", p_con env c2), - ("Hnormed 1", p_con env c1'), - ("Hnormed 2", p_con env c2')]; - - (*app (fn (loc, env, k, s1, s2) => - eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)), - ("s2", p_summary env (normalizeRecordSummary env s2))]) - (!delayedUnifs);*) - - if (isUnif c1' andalso maybeAttr c2') - orelse (isUnif c2' andalso maybeAttr c1') then - TextIO.output (TextIO.stdErr, - "You may be using a disallowed attribute with an HTML tag.\n") - else - () - end - | TypeClass (env, c, r, loc) => - expError env (Unresolvable (loc, c))) - gs + checkConstraintErrors := + (fn () => app (fn Disjoint (loc, env, denv, c1, c2) => + let + val c1' = ElabOps.hnormCon env c1 + val c2' = ElabOps.hnormCon env c2 + + fun isUnif (c, _) = + case c of + L'.CUnif _ => true + | _ => false + + fun maybeAttr (c, _) = + case c of + L'.CRecord ((L'.KType, _), xts) => true + | _ => false + in + ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; + eprefaces' [("Con 1", p_con env c1), + ("Con 2", p_con env c2), + ("Hnormed 1", p_con env c1'), + ("Hnormed 2", p_con env c2')] + + (*app (fn (loc, env, k, s1, s2) => + eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)), + ("s2", p_summary env (normalizeRecordSummary env s2))]) + (!delayedUnifs);*) + end + | TypeClass (env, c, r, loc) => + expError env (Unresolvable (loc, c))) + gs) end in solver gs @@ -4483,6 +4479,11 @@ | SOME p => expError env (Inexhaustive (loc, p))) (!delayedExhaustives); + if ErrorMsg.anyErrors () then + () + else + !checkConstraintErrors (); + (*preface ("file", p_file env' file);*) if !dumpTypes then