Mercurial > urweb

comparison src/elaborate.sml @ 1582:dfb38a333816

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Harmonize have/need terminology in error messages; display canceled record summaries on errors
author Adam Chlipala <adam@chlipala.net>
date Thu, 27 Oct 2011 08:36:31 -0400
parents ec466c1e082a
children 7fcdf836b761
comparison
equal deleted inserted replaced
1581:1ced338f691a 1582:dfb38a333816
696 | L'.CUnif _ => raise CantSquish 696 | L'.CUnif _ => raise CantSquish
697 | _ => c, 697 | _ => c,
698 bind = fn (bound, U.Con.RelC _) => bound + 1 698 bind = fn (bound, U.Con.RelC _) => bound + 1
699 | (bound, _) => bound} 0 699 | (bound, _) => bound} 0
700 700
701 val reducedSummaries = ref (NONE : (Print.PD.pp_desc * Print.PD.pp_desc) option)
702
701 fun unifyRecordCons env (loc, c1, c2) = 703 fun unifyRecordCons env (loc, c1, c2) =
702 let 704 let
703 fun rkindof c = 705 fun rkindof c =
704 case hnormKind (kindof env c) of 706 case hnormKind (kindof env c) of
705 (L'.KRecord k, _) => k 707 (L'.KRecord k, _) => k
888 if isGuessable (other2, fs1, unifs1) then 890 if isGuessable (other2, fs1, unifs1) then
889 ([], [], [], [], [], []) 891 ([], [], [], [], [], [])
890 else 892 else
891 (fs1, fs2, others1, others2, unifs1, unifs2) 893 (fs1, fs2, others1, others2, unifs1, unifs2)
892 | _ => (fs1, fs2, others1, others2, unifs1, unifs2) 894 | _ => (fs1, fs2, others1, others2, unifs1, unifs2)
895
896 val () = if !mayDelay then
897 ()
898 else
899 reducedSummaries := SOME (p_summary env {fields = fs1, unifs = unifs1, others = others1},
900 p_summary env {fields = fs2, unifs = unifs2, others = others2})
893 901
894 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 902 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
895 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 903 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
896 904
897 val empty = (L'.CRecord (k, []), loc) 905 val empty = (L'.CRecord (k, []), loc)
4448 () 4456 ()
4449 else 4457 else
4450 (app (fn (loc, env, k, s1, s2) => 4458 (app (fn (loc, env, k, s1, s2) =>
4451 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) 4459 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
4452 handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification"; 4460 handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification";
4453 cunifyError env err)) 4461 cunifyError env err;
4462 case !reducedSummaries of
4463 NONE => ()
4464 | SOME (s1, s2) =>
4465 (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:";
4466 eprefaces' [("Have", s1),
4467 ("Need", s2)])))
4454 (!delayedUnifs); 4468 (!delayedUnifs);
4455 delayedUnifs := []); 4469 delayedUnifs := []);
4456 4470
4457 if ErrorMsg.anyErrors () then 4471 if ErrorMsg.anyErrors () then
4458 () 4472 ()