summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elab_err.sml50
-rw-r--r--src/elab_util.sig2
-rw-r--r--src/elab_util.sml26
-rw-r--r--src/elaborate.sml39
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
()