Mercurial > urweb

comparison src/elaborate.sml @ 1576:f6c74b4bc4e6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 c7d0328ba777
children ec466c1e082a
comparison
equal deleted inserted replaced
1575:287604b4a08d 1576:f6c74b4bc4e6
4333 delayedUnifs := []; 4333 delayedUnifs := [];
4334 app (fn (loc, env, k, s1, s2) => 4334 app (fn (loc, env, k, s1, s2) =>
4335 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)) 4335 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2))
4336 delayed 4336 delayed
4337 end 4337 end
4338
4339 val checkConstraintErrors = ref (fn () => ())
4338 in 4340 in
4339 oneSummaryRound (); 4341 oneSummaryRound ();
4340 4342
4341 if ErrorMsg.anyErrors () then 4343 if ErrorMsg.anyErrors () then
4342 () 4344 ()
4402 in 4404 in
4403 case (gs, solved) of 4405 case (gs, solved) of
4404 ([], _) => () 4406 ([], _) => ()
4405 | (_, true) => (oneSummaryRound (); solver gs) 4407 | (_, true) => (oneSummaryRound (); solver gs)
4406 | _ => 4408 | _ =>
4407 app (fn Disjoint (loc, env, denv, c1, c2) => 4409 checkConstraintErrors :=
4408 let 4410 (fn () => app (fn Disjoint (loc, env, denv, c1, c2) =>
4409 val c1' = ElabOps.hnormCon env c1 4411 let
4410 val c2' = ElabOps.hnormCon env c2 4412 val c1' = ElabOps.hnormCon env c1
4411 4413 val c2' = ElabOps.hnormCon env c2
4412 fun isUnif (c, _) = 4414
4413 case c of 4415 fun isUnif (c, _) =
4414 L'.CUnif _ => true 4416 case c of
4415 | _ => false 4417 L'.CUnif _ => true
4416 4418 | _ => false
4417 fun maybeAttr (c, _) = 4419
4418 case c of 4420 fun maybeAttr (c, _) =
4419 L'.CRecord ((L'.KType, _), xts) => true 4421 case c of
4420 | _ => false 4422 L'.CRecord ((L'.KType, _), xts) => true
4421 in 4423 | _ => false
4422 ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; 4424 in
4423 eprefaces' [("Con 1", p_con env c1), 4425 ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
4424 ("Con 2", p_con env c2), 4426 eprefaces' [("Con 1", p_con env c1),
4425 ("Hnormed 1", p_con env c1'), 4427 ("Con 2", p_con env c2),
4426 ("Hnormed 2", p_con env c2')]; 4428 ("Hnormed 1", p_con env c1'),
4427 4429 ("Hnormed 2", p_con env c2')]
4428 (*app (fn (loc, env, k, s1, s2) => 4430
4429 eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)), 4431 (*app (fn (loc, env, k, s1, s2) =>
4430 ("s2", p_summary env (normalizeRecordSummary env s2))]) 4432 eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)),
4431 (!delayedUnifs);*) 4433 ("s2", p_summary env (normalizeRecordSummary env s2))])
4432 4434 (!delayedUnifs);*)
4433 if (isUnif c1' andalso maybeAttr c2') 4435 end
4434 orelse (isUnif c2' andalso maybeAttr c1') then 4436 | TypeClass (env, c, r, loc) =>
4435 TextIO.output (TextIO.stdErr, 4437 expError env (Unresolvable (loc, c)))
4436 "You may be using a disallowed attribute with an HTML tag.\n") 4438 gs)
4437 else
4438 ()
4439 end
4440 | TypeClass (env, c, r, loc) =>
4441 expError env (Unresolvable (loc, c)))
4442 gs
4443 end 4439 end
4444 in 4440 in
4445 solver gs 4441 solver gs
4446 end; 4442 end;
4447 4443
4480 app (fn all as (env, _, _, loc) => 4476 app (fn all as (env, _, _, loc) =>
4481 case exhaustive all of 4477 case exhaustive all of
4482 NONE => () 4478 NONE => ()
4483 | SOME p => expError env (Inexhaustive (loc, p))) 4479 | SOME p => expError env (Inexhaustive (loc, p)))
4484 (!delayedExhaustives); 4480 (!delayedExhaustives);
4481
4482 if ErrorMsg.anyErrors () then
4483 ()
4484 else
4485 !checkConstraintErrors ();
4485 4486
4486 (*preface ("file", p_file env' file);*) 4487 (*preface ("file", p_file env' file);*)
4487 4488
4488 if !dumpTypes then 4489 if !dumpTypes then
4489 let 4490 let