diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/elab_err.sml | 50 | ||||
| -rw-r--r-- | src/elab_util.sig | 2 | ||||
| -rw-r--r-- | src/elab_util.sml | 26 | ||||
| -rw-r--r-- | src/elaborate.sml | 39 |
4 files changed, 98 insertions, 19 deletions
diff --git a/src/elab_err.sml b/src/elab_err.sml index 00f1e4fc..84c8c61f 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -262,7 +262,55 @@ datatype decl_error = 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 diff --git a/src/elab_util.sig b/src/elab_util.sig index 88bdc892..2998e7db 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -226,6 +226,8 @@ end structure File : sig val maxName : Elab.file -> int + + val findDecl : (Elab.decl -> bool) -> Elab.file -> Elab.decl option end end diff --git a/src/elab_util.sml b/src/elab_util.sml index fd8163c2..bf0185b1 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -1235,6 +1235,32 @@ and maxNameSgi (sgi, _) = | 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 diff --git a/src/elaborate.sml b/src/elaborate.sml index 5b54db9a..9051299a 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -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 @@ fun elabFile basis topStr topSgn env file = 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 () |