Mercurial > urweb

comparison src/elaborate.sml @ 1723:5ecf67553da8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
-unifyMore
author Adam Chlipala <adam@chlipala.net>
date Sun, 22 Apr 2012 09:08:45 -0400
parents 0bafdfae2ac7
children 4a03aa3251cb
comparison
equal deleted inserted replaced
1722:f7d9dc5d57eb 1723:5ecf67553da8
37 open Print 37 open Print
38 open ElabPrint 38 open ElabPrint
39 open ElabErr 39 open ElabErr
40 40
41 val dumpTypes = ref false 41 val dumpTypes = ref false
42 val unifyMore = ref false
42 43
43 structure IS = IntBinarySet 44 structure IS = IntBinarySet
44 structure IM = IntBinaryMap 45 structure IM = IntBinaryMap
45 46
46 structure SK = struct 47 structure SK = struct
4517 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)) 4518 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2))
4518 delayed 4519 delayed
4519 end 4520 end
4520 4521
4521 val checkConstraintErrors = ref (fn () => ()) 4522 val checkConstraintErrors = ref (fn () => ())
4523 fun stopHere () = not (!unifyMore) andalso ErrorMsg.anyErrors ()
4522 in 4524 in
4523 oneSummaryRound (); 4525 oneSummaryRound ();
4524 4526
4525 if ErrorMsg.anyErrors () then 4527 if stopHere () then
4526 () 4528 ()
4527 else 4529 else
4528 let 4530 let
4529 fun solver gs = 4531 fun solver gs =
4530 let 4532 let
4623 solver gs 4625 solver gs
4624 end; 4626 end;
4625 4627
4626 mayDelay := false; 4628 mayDelay := false;
4627 4629
4628 if ErrorMsg.anyErrors () then 4630 if stopHere () then
4629 () 4631 ()
4630 else 4632 else
4631 (app (fn (loc, env, k, s1, s2) => 4633 (app (fn (loc, env, k, s1, s2) =>
4632 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) 4634 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
4633 handle CUnify' (env', err) => (ErrorMsg.errorAt loc "Error in final record unification"; 4635 handle CUnify' (env', err) => (ErrorMsg.errorAt loc "Error in final record unification";
4639 eprefaces' [("Have", s1), 4641 eprefaces' [("Have", s1),
4640 ("Need", s2)]))) 4642 ("Need", s2)])))
4641 (!delayedUnifs); 4643 (!delayedUnifs);
4642 delayedUnifs := []); 4644 delayedUnifs := []);
4643 4645
4644 if ErrorMsg.anyErrors () then 4646 if stopHere () then
4645 () 4647 ()
4646 else 4648 else
4647 if List.exists kunifsInDecl file then 4649 if List.exists kunifsInDecl file then
4648 case U.File.findDecl kunifsInDecl file of 4650 case U.File.findDecl kunifsInDecl file of
4649 NONE => () 4651 NONE => ()
4650 | SOME d => declError env'' (KunifsRemain [d]) 4652 | SOME d => declError env'' (KunifsRemain [d])
4651 else 4653 else
4652 (); 4654 ();
4653 4655
4654 if ErrorMsg.anyErrors () then 4656 if stopHere () then
4655 () 4657 ()
4656 else 4658 else
4657 if List.exists cunifsInDecl file then 4659 if List.exists cunifsInDecl file then
4658 case U.File.findDecl cunifsInDecl file of 4660 case U.File.findDecl cunifsInDecl file of
4659 NONE => () 4661 NONE => ()
4660 | SOME d => declError env'' (CunifsRemain [d]) 4662 | SOME d => declError env'' (CunifsRemain [d])
4661 else 4663 else
4662 (); 4664 ();
4663 4665
4664 if ErrorMsg.anyErrors () then 4666 if stopHere () then
4665 () 4667 ()
4666 else 4668 else
4667 app (fn all as (env, _, _, loc) => 4669 app (fn all as (env, _, _, loc) =>
4668 case exhaustive all of 4670 case exhaustive all of
4669 NONE => () 4671 NONE => ()
4670 | SOME p => expError env (Inexhaustive (loc, p))) 4672 | SOME p => expError env (Inexhaustive (loc, p)))
4671 (!delayedExhaustives); 4673 (!delayedExhaustives);
4672 4674
4673 if ErrorMsg.anyErrors () then 4675 if stopHere () then
4674 () 4676 ()
4675 else 4677 else
4676 !checkConstraintErrors (); 4678 !checkConstraintErrors ();
4677 4679
4678 (*preface ("file", p_file env' file);*) 4680 (*preface ("file", p_file env' file);*)