summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-10-15 14:27:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-10-15 14:27:38 -0400
commite177d0dd0db2639bd056e81296f2f0f5c930ad5f (patch)
tree57e7694ac353640b75428a5601da1a33ed7b3cca /src
parent39310f94944779f726fdf389373dafb1c1e32a20 (diff)
Better subSgn error locations
Diffstat (limited to 'src')
-rw-r--r--src/elab_err.sig11
-rw-r--r--src/elab_err.sml29
-rw-r--r--src/elaborate.sml45
3 files changed, 46 insertions, 39 deletions
diff --git a/src/elab_err.sig b/src/elab_err.sig
index 10cda7d3..18596d04 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -88,11 +88,12 @@ signature ELAB_ERR = sig
datatype sgn_error =
UnboundSgn of ErrorMsg.span * string
- | UnmatchedSgi of Elab.sgn_item
- | SgiWrongKind of Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
- | SgiWrongCon of Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
- | SgiMismatchedDatatypes of Elab.sgn_item * Elab.sgn_item * (Elab.con * Elab.con * cunify_error) option
- | SgnWrongForm of Elab.sgn * Elab.sgn
+ | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
+ | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
+ | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
+ | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
+ * (Elab.con * Elab.con * cunify_error) option
+ | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
| UnWhereable of Elab.sgn * string
| WhereWrongKind of Elab.kind * Elab.kind * kunify_error
| NotIncludable of Elab.sgn
diff --git a/src/elab_err.sml b/src/elab_err.sml
index dc34560b..6d9bd2e6 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -259,11 +259,12 @@ fun declError env err =
datatype sgn_error =
UnboundSgn of ErrorMsg.span * string
- | UnmatchedSgi of sgn_item
- | SgiWrongKind of sgn_item * kind * sgn_item * kind * kunify_error
- | SgiWrongCon of sgn_item * con * sgn_item * con * cunify_error
- | SgiMismatchedDatatypes of sgn_item * sgn_item * (con * con * cunify_error) option
- | SgnWrongForm of sgn * sgn
+ | UnmatchedSgi of ErrorMsg.span * sgn_item
+ | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * kunify_error
+ | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * cunify_error
+ | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
+ * (con * con * cunify_error) option
+ | SgnWrongForm of ErrorMsg.span * sgn * sgn
| UnWhereable of sgn * string
| WhereWrongKind of kind * kind * kunify_error
| NotIncludable of sgn
@@ -280,25 +281,25 @@ fun sgnError env err =
case err of
UnboundSgn (loc, s) =>
ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
- | UnmatchedSgi (sgi as (_, loc)) =>
+ | UnmatchedSgi (loc, sgi) =>
(ErrorMsg.errorAt loc "Unmatched signature item";
eprefaces' [("Item", p_sgn_item env sgi)])
- | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
- (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
+ | SgiWrongKind (loc, sgi1, k1, sgi2, k2, kerr) =>
+ (ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
eprefaces' [("Have", p_sgn_item env sgi1),
("Need", p_sgn_item env sgi2),
("Kind 1", p_kind env k1),
("Kind 2", p_kind env k2)];
kunifyError env kerr)
- | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
- (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
+ | SgiWrongCon (loc, sgi1, c1, sgi2, c2, cerr) =>
+ (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
eprefaces' [("Have", p_sgn_item env sgi1),
("Need", p_sgn_item env sgi2),
("Con 1", p_con env c1),
("Con 2", p_con env c2)];
cunifyError env cerr)
- | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
- (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
+ | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
+ (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
eprefaces' [("Have", p_sgn_item env sgi1),
("Need", p_sgn_item env sgi2)];
Option.app (fn (c1, c2, ue) =>
@@ -306,8 +307,8 @@ fun sgnError env err =
[("Con 1", p_con env c1),
("Con 2", p_con env c2)];
cunifyError env ue)) cerro)
- | SgnWrongForm (sgn1, sgn2) =>
- (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
+ | SgnWrongForm (loc, sgn1, sgn2) =>
+ (ErrorMsg.errorAt loc "Incompatible signatures:";
eprefaces' [("Sig 1", p_sgn env sgn1),
("Sig 2", p_sgn env sgn2)])
| UnWhereable (sgn, x) =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9aeac8f3..b46c262e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2516,7 +2516,7 @@ and sgiOfDecl (d, loc) =
| L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
| L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
-and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
+and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
("sgn2", p_sgn env sgn2)];*)
case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
@@ -2575,7 +2575,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
seek env sgis1
end
- val seek = seek' (fn env => (sgnError env (UnmatchedSgi sgi2All);
+ val seek = seek' (fn env => (sgnError env (UnmatchedSgi (strLoc, sgi2All));
env))
in
case sgi of
@@ -2587,7 +2587,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
let
val () = unifyKinds env k1 k2
handle KUnify (k1, k2, err) =>
- sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+ sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
+ sgi2All, k2, err))
val env = E.pushCNamedAs env x n1 k1 co1
in
SOME (if n1 = n2 then
@@ -2655,7 +2656,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
(unifyCons env loc c1 c2;
good ())
handle CUnify (c1, c2, err) =>
- (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+ (sgnError env (SgiWrongCon (strLoc, sgi1All, c1,
+ sgi2All, c2, err));
good ())
end
else
@@ -2675,7 +2677,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
else
let
fun mismatched ue =
- (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
+ (sgnError env (SgiMismatchedDatatypes (strLoc, sgi1All, sgi2All, ue));
SOME env)
val k = (L'.KType, loc)
@@ -2780,7 +2782,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
(unifyCons env loc t1 t2;
good ())
handle CUnify (c1, c2, err) =>
- (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+ (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err));
good ())
end
else
@@ -2801,7 +2803,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
unifyCons env loc c1 (sub2 c2);
SOME env)
handle CUnify (c1, c2, err) =>
- (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+ (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err));
SOME env)
else
NONE
@@ -2813,7 +2815,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
L'.SgiStr (x', n1, sgn1) =>
if x = x' then
let
- val () = subSgn' counterparts env sgn1 sgn2
+ val () = subSgn' counterparts env strLoc sgn1 sgn2
val env = E.pushStrNamedAs env x n1 sgn1
val env = if n1 = n2 then
env
@@ -2834,8 +2836,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
L'.SgiSgn (x', n1, sgn1) =>
if x = x' then
let
- val () = subSgn' counterparts env sgn1 sgn2
- val () = subSgn' counterparts env sgn2 sgn1
+ val () = subSgn' counterparts env strLoc sgn1 sgn2
+ val () = subSgn' counterparts env strLoc sgn2 sgn1
val env = E.pushSgnNamedAs env x n2 sgn2
val env = if n1 = n2 then
@@ -2869,7 +2871,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
let
val () = unifyKinds env k1 k2
handle KUnify (k1, k2, err) =>
- sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+ sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
+ sgi2All, k2, err))
val env = E.pushCNamedAs env x n1 k1 co
in
@@ -2895,7 +2898,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
let
val () = unifyKinds env k1 k2
handle KUnify (k1, k2, err) =>
- sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+ sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
+ sgi2All, k2, err))
val c2 = sub2 c2
@@ -2914,7 +2918,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
(unifyCons env loc c1 c2;
good ())
handle CUnify (c1, c2, err) =>
- (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+ (sgnError env (SgiWrongCon (strLoc, sgi1All, c1,
+ sgi2All, c2, err));
good ())
end
else
@@ -2937,11 +2942,11 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
else
subStrInSgn (n2, n1) ran2
in
- subSgn' counterparts env dom2 dom1;
- subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2
+ subSgn' counterparts env strLoc dom2 dom1;
+ subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) strLoc ran1 ran2
end
- | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
+ | _ => sgnError env (SgnWrongForm (strLoc, sgn1, sgn2)))
and subSgn env = subSgn' (ref IM.empty) env
@@ -3405,7 +3410,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
val str = wildifyStr env (str, formal)
val (str', actual, gs2) = elabStr (env, denv) str
in
- subSgn env (selfifyAt env {str = str', sgn = actual}) formal;
+ subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal;
(str', formal, enD gs1 @ gs2)
end
@@ -3786,7 +3791,7 @@ and elabStr (env, denv) (str, loc) =
let
val (ran', gs) = elabSgn (env', denv') ran
in
- subSgn env' actual ran';
+ subSgn env' loc actual ran';
(ran', gs)
end
in
@@ -3807,7 +3812,7 @@ and elabStr (env, denv) (str, loc) =
case #1 (hnormSgn env sgn1) of
L'.SgnError => (strerror, sgnerror, [])
| L'.SgnFun (m, n, dom, ran) =>
- (subSgn env sgn2 dom;
+ (subSgn env loc sgn2 dom;
case #1 (hnormSgn env ran) of
L'.SgnError => (strerror, sgnerror, [])
| L'.SgnConst sgis =>
@@ -3878,7 +3883,7 @@ fun elabFile basis topStr topSgn env file =
| NONE => expError env (Unresolvable (loc, c))
end) gs
- val () = subSgn env' topSgn' topSgn
+ val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn
val (env', top_n) = E.pushStrNamed env' "Top" topSgn
val () = top_r := top_n