Mercurial > urweb

comparison src/elaborate.sml @ 153:cfe6f9db74aa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
radio and radioOption
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 11:10:23 -0400
parents 67ab26888839
children 34ccd7d2bea8
comparison
equal deleted inserted replaced
152:67ab26888839 153:cfe6f9db74aa
443 CKind of L'.kind * L'.kind * kunify_error 443 CKind of L'.kind * L'.kind * kunify_error
444 | COccursCheckFailed of L'.con * L'.con 444 | COccursCheckFailed of L'.con * L'.con
445 | CIncompatible of L'.con * L'.con 445 | CIncompatible of L'.con * L'.con
446 | CExplicitness of L'.con * L'.con 446 | CExplicitness of L'.con * L'.con
447 | CKindof of L'.kind * L'.con 447 | CKindof of L'.kind * L'.con
448 | CRecordFailure 448 | CRecordFailure of PD.pp_desc * PD.pp_desc
449 449
450 exception CUnify' of cunify_error 450 exception CUnify' of cunify_error
451 451
452 fun cunifyError env err = 452 fun cunifyError env err =
453 case err of 453 case err of
470 ("Con 2", p_con env c2)] 470 ("Con 2", p_con env c2)]
471 | CKindof (k, c) => 471 | CKindof (k, c) =>
472 eprefaces "Unexpected kind for kindof calculation" 472 eprefaces "Unexpected kind for kindof calculation"
473 [("Kind", p_kind k), 473 [("Kind", p_kind k),
474 ("Con", p_con env c)] 474 ("Con", p_con env c)]
475 | CRecordFailure => 475 | CRecordFailure (s1, s2) =>
476 eprefaces "Can't unify record constructors" [] 476 eprefaces "Can't unify record constructors"
477 [("Summary 1", s1),
478 ("Summary 2", s2)]
477 479
478 exception SynUnif = E.SynUnif 480 exception SynUnif = E.SynUnif
479 481
480 open ElabOps 482 open ElabOps
481 483
675 case (unifs1, unifs2) of 677 case (unifs1, unifs2) of
676 ([], _) => 678 ([], _) =>
677 if clear then 679 if clear then
678 List.app (fn (_, r) => r := SOME empty) unifs2 680 List.app (fn (_, r) => r := SOME empty) unifs2
679 else 681 else
680 raise CUnify' CRecordFailure 682 raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2))
681 | (_, []) => 683 | (_, []) =>
682 if clear then 684 if clear then
683 List.app (fn (_, r) => r := SOME empty) unifs1 685 List.app (fn (_, r) => r := SOME empty) unifs1
684 else 686 else
685 raise CUnify' CRecordFailure 687 raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2))
686 | ((c1, _) :: rest1, (_, r2) :: rest2) => 688 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
687 (r2 := SOME c1; 689 (r2 := SOME c1;
688 pairOffUnifs (rest1, rest2)) 690 pairOffUnifs (rest1, rest2))
689 in 691 in
690 pairOffUnifs (unifs1, unifs2) 692 pairOffUnifs (unifs1, unifs2)