Mercurial > urweb

comparison src/elaborate.sml @ 1584:c37d8341940a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Shorter, more focused error messages about undetermined unification variables
author Adam Chlipala <adam@chlipala.net>
date Sat, 29 Oct 2011 17:30:34 -0400
parents 7fcdf836b761
children d5fb78321cca
comparison
equal deleted inserted replaced
1583:7fcdf836b761 1584:c37d8341940a
498 | _ => false 498 | _ => false
499 fun cunifsRemain c = 499 fun cunifsRemain c =
500 case c of 500 case c of
501 L'.CUnif (_, loc, k, _, r as ref NONE) => 501 L'.CUnif (_, loc, k, _, r as ref NONE) =>
502 (case #1 (hnormKind k) of 502 (case #1 (hnormKind k) of
503 L'.KUnit => (r := SOME (L'.CUnit, loc); NONE) 503 L'.KUnit => (r := SOME (L'.CUnit, loc); false)
504 | _ => SOME loc) 504 | _ => true)
505 | _ => NONE 505 | _ => false
506 506
507 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, 507 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
508 con = fn _ => false, 508 con = fn _ => false,
509 exp = fn _ => false, 509 exp = fn _ => false,
510 sgn_item = fn _ => false, 510 sgn_item = fn _ => false,
511 sgn = fn _ => false, 511 sgn = fn _ => false,
512 str = fn _ => false, 512 str = fn _ => false,
513 decl = fn _ => false} 513 decl = fn _ => false}
514 514
515 val cunifsInDecl = U.Decl.search {kind = fn _ => NONE, 515 val cunifsInDecl = U.Decl.exists {kind = fn _ => false,
516 con = cunifsRemain, 516 con = cunifsRemain,
517 exp = fn _ => NONE, 517 exp = fn _ => false,
518 sgn_item = fn _ => NONE, 518 sgn_item = fn _ => false,
519 sgn = fn _ => NONE, 519 sgn = fn _ => false,
520 str = fn _ => NONE, 520 str = fn _ => false,
521 decl = fn _ => NONE} 521 decl = fn _ => false}
522 522
523 fun occursCon r = 523 fun occursCon r =
524 U.Con.exists {kind = fn _ => false, 524 U.Con.exists {kind = fn _ => false,
525 con = fn L'.CUnif (_, _, _, _, r') => r = r' 525 con = fn L'.CUnif (_, _, _, _, r') => r = r'
526 | _ => false} 526 | _ => false}
4471 delayedUnifs := []); 4471 delayedUnifs := []);
4472 4472
4473 if ErrorMsg.anyErrors () then 4473 if ErrorMsg.anyErrors () then
4474 () 4474 ()
4475 else 4475 else
4476 ignore (List.exists (fn d => if kunifsInDecl d then 4476 if List.exists kunifsInDecl file then
4477 (declError env'' (KunifsRemain [d]); 4477 case U.File.findDecl kunifsInDecl file of
4478 true) 4478 NONE => ()
4479 else 4479 | SOME d => declError env'' (KunifsRemain [d])
4480 false) file); 4480 else
4481 ();
4481 4482
4482 if ErrorMsg.anyErrors () then 4483 if ErrorMsg.anyErrors () then
4483 () 4484 ()
4484 else 4485 else
4485 ignore (List.exists (fn d => case cunifsInDecl d of 4486 if List.exists cunifsInDecl file then
4486 NONE => false 4487 case U.File.findDecl cunifsInDecl file of
4487 | SOME _ => (declError env'' (CunifsRemain [d]); 4488 NONE => ()
4488 true)) file); 4489 | SOME d => declError env'' (CunifsRemain [d])
4490 else
4491 ();
4489 4492
4490 if ErrorMsg.anyErrors () then 4493 if ErrorMsg.anyErrors () then
4491 () 4494 ()
4492 else 4495 else
4493 app (fn all as (env, _, _, loc) => 4496 app (fn all as (env, _, _, loc) =>