Mercurial > urweb
changeset 1584:c37d8341940a
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 |
| files | src/elab_err.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml tests/unif1.ur |
| diffstat | 5 files changed, 101 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_err.sml Fri Oct 28 08:54:44 2011 -0400 +++ b/src/elab_err.sml Sat Oct 29 17:30:34 2011 -0400 @@ -262,7 +262,55 @@ fun lspan [] = ErrorMsg.dummySpan | lspan ((_, loc) :: _) = loc -val p_decl = P.p_decl +val baseLen = 2000 + +fun p_decl env d = + let + val fname = OS.FileSys.tmpName () + val out' = TextIO.openOut fname + val out = Print.openOut {dst = out', wid = 80} + + fun readFromFile () = + let + val inf = TextIO.openIn fname + + fun loop acc = + case TextIO.inputLine inf of + NONE => String.concat (rev acc) + | SOME line => loop (line :: acc) + in + loop [] + before TextIO.closeIn inf + end + in + Print.fprint out (P.p_decl env d); + TextIO.closeOut out'; + let + val content = readFromFile () + in + OS.FileSys.remove fname; + Print.PD.string (if size content <= baseLen then + content + else + let + val (befor, after) = Substring.position "<UNIF:" (Substring.full content) + in + if Substring.isEmpty after then + raise Fail "No unification variables in rendering" + else + Substring.concat [Substring.full "\n.....\n", + if Substring.size befor <= baseLen then + befor + else + Substring.slice (befor, Substring.size befor - baseLen, SOME baseLen), + if Substring.size after <= baseLen then + after + else + Substring.slice (after, 0, SOME baseLen), + Substring.full "\n.....\n"] + end) + end + end fun declError env err = case err of
--- a/src/elab_util.sig Fri Oct 28 08:54:44 2011 -0400 +++ b/src/elab_util.sig Sat Oct 29 17:30:34 2011 -0400 @@ -226,6 +226,8 @@ structure File : sig val maxName : Elab.file -> int + + val findDecl : (Elab.decl -> bool) -> Elab.file -> Elab.decl option end end
--- a/src/elab_util.sml Fri Oct 28 08:54:44 2011 -0400 +++ b/src/elab_util.sml Sat Oct 29 17:30:34 2011 -0400 @@ -1235,6 +1235,32 @@ | SgiConstraint _ => 0 | SgiClassAbs (_, n, _) => n | SgiClass (_, n, _, _) => n + +fun findDecl pred file = + let + fun decl d = + let + val r = case #1 d of + DStr (_, _, _, s) => str s + | _ => NONE + in + case r of + NONE => if pred d then SOME d else NONE + | _ => r + end + + and str s = + case #1 s of + StrConst ds => ListUtil.search decl ds + | StrFun (_, _, _, _, s) => str s + | StrApp (s1, s2) => + (case str s1 of + NONE => str s2 + | r => r) + | _ => NONE + in + ListUtil.search decl file + end end
--- a/src/elaborate.sml Fri Oct 28 08:54:44 2011 -0400 +++ b/src/elaborate.sml Sat Oct 29 17:30:34 2011 -0400 @@ -500,9 +500,9 @@ case c of L'.CUnif (_, loc, k, _, r as ref NONE) => (case #1 (hnormKind k) of - L'.KUnit => (r := SOME (L'.CUnit, loc); NONE) - | _ => SOME loc) - | _ => NONE + L'.KUnit => (r := SOME (L'.CUnit, loc); false) + | _ => true) + | _ => false val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, con = fn _ => false, @@ -512,13 +512,13 @@ str = fn _ => false, decl = fn _ => false} - val cunifsInDecl = U.Decl.search {kind = fn _ => NONE, + val cunifsInDecl = U.Decl.exists {kind = fn _ => false, con = cunifsRemain, - exp = fn _ => NONE, - sgn_item = fn _ => NONE, - sgn = fn _ => NONE, - str = fn _ => NONE, - decl = fn _ => NONE} + exp = fn _ => false, + sgn_item = fn _ => false, + sgn = fn _ => false, + str = fn _ => false, + decl = fn _ => false} fun occursCon r = U.Con.exists {kind = fn _ => false, @@ -4473,19 +4473,22 @@ if ErrorMsg.anyErrors () then () else - ignore (List.exists (fn d => if kunifsInDecl d then - (declError env'' (KunifsRemain [d]); - true) - else - false) file); + if List.exists kunifsInDecl file then + case U.File.findDecl kunifsInDecl file of + NONE => () + | SOME d => declError env'' (KunifsRemain [d]) + else + (); if ErrorMsg.anyErrors () then () else - ignore (List.exists (fn d => case cunifsInDecl d of - NONE => false - | SOME _ => (declError env'' (CunifsRemain [d]); - true)) file); + if List.exists cunifsInDecl file then + case U.File.findDecl cunifsInDecl file of + NONE => () + | SOME d => declError env'' (CunifsRemain [d]) + else + (); if ErrorMsg.anyErrors () then ()