Mercurial > urweb
changeset 1000:5d7e05b4a5c0
Better subSgn error locations
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 15 Oct 2009 14:27:38 -0400 |
| parents | 8d821baac99e |
| children | 1d456a06ea4e |
| files | src/elab_err.sig src/elab_err.sml src/elaborate.sml tests/functor.urp |
| diffstat | 4 files changed, 49 insertions(+), 39 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_err.sig Mon Oct 12 18:17:57 2009 -0400 +++ b/src/elab_err.sig Thu Oct 15 14:27:38 2009 -0400 @@ -88,11 +88,12 @@ 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
--- a/src/elab_err.sml Mon Oct 12 18:17:57 2009 -0400 +++ b/src/elab_err.sml Thu Oct 15 14:27:38 2009 -0400 @@ -259,11 +259,12 @@ 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 @@ 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 @@ [("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) =>
--- a/src/elaborate.sml Mon Oct 12 18:17:57 2009 -0400 +++ b/src/elaborate.sml Thu Oct 15 14:27:38 2009 -0400 @@ -2516,7 +2516,7 @@ | 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 @@ 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 @@ 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 @@ (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 @@ 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 @@ (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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ (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 @@ 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 @@ 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 @@ 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 @@ 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 @@ | 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