Mercurial > urweb
changeset 1591:20f898c29525
Tweaks to choices of source positions to use in error messages, including for subSgn
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 05 Nov 2011 13:12:07 -0400 |
| parents | 60d438cdb3a5 |
| children | 1c9f8f06c1d6 |
| files | src/elab_ops.sml src/elaborate.sml |
| diffstat | 2 files changed, 40 insertions(+), 28 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_ops.sml Sat Nov 05 12:32:20 2011 -0400 +++ b/src/elab_ops.sml Sat Nov 05 13:12:07 2011 -0400 @@ -156,7 +156,7 @@ fun hnormCon env (cAll as (c, loc)) = case c of - CUnif (nl, _, _, _, ref (SOME c)) => hnormCon env (E.mliftConInCon nl c) + CUnif (nl, _, _, _, ref (SOME c)) => (#1 (hnormCon env (E.mliftConInCon nl c)), loc) | CNamed xn => (case E.lookupCNamed env xn of
--- a/src/elaborate.sml Sat Nov 05 12:32:20 2011 -0400 +++ b/src/elaborate.sml Sat Nov 05 13:12:07 2011 -0400 @@ -1255,6 +1255,11 @@ Disjoint of D.goal | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span + fun relocConstraint loc c = + case c of + Disjoint (_, a, b, c, d) => Disjoint (loc, a, b, c, d) + | TypeClass (a, b, c, _) => TypeClass (a, b, c, loc) + val enD = map Disjoint fun isClassOrFolder env cl = @@ -1351,10 +1356,12 @@ else (e, t, []) | t => (e, t, []) + + val (e, t, gs) = case infer of + L.DontInfer => unravelKind (t, e) + | _ => unravel (t, e) in - case infer of - L.DontInfer => unravelKind (t, e) - | _ => unravel (t, e) + ((#1 e, loc), (#1 t, loc), map (relocConstraint loc) gs) end fun elabPat (pAll as (p, loc), (env, bound)) = @@ -1865,6 +1872,11 @@ Mods = #Mods r} end +fun chaseUnifs c = + case #1 c of + L'.CUnif (_, _, _, _, ref (SOME c)) => chaseUnifs c + | _ => c + fun elabExp (env, denv) (eAll as (e, loc)) = let (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) @@ -1933,7 +1945,7 @@ val ef = (L'.EApp (e1', e2'), loc) val (ef, et, gs3) = case findHead e1 e1' of - NONE => (ef, ran, []) + NONE => (ef, (#1 (chaseUnifs ran), loc), []) | SOME infer => elabHead (env, denv) infer ef ran in (ef, et, gs1 @ gs2 @ gs3) @@ -1983,7 +1995,7 @@ ("eb", p_con (E.pushCRel env x k) eb), ("c", p_con env c'), ("eb'", p_con env eb')];*) - (ef, eb', gs1 @ enD gs2 @ gs3) + (ef, (#1 eb', loc), gs1 @ enD gs2 @ gs3) end | _ => @@ -2040,7 +2052,7 @@ val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc) val gs2 = D.prove env denv (c1, c2, loc) in - (e', t', enD gs2 @ gs1) + (e', (#1 (chaseUnifs t'), loc), enD gs2 @ gs1) end | L.ERecord xes => @@ -2915,14 +2927,14 @@ in case sgi of L'.SgiConAbs (x, n2, k2) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => let fun found (x', n1, k1, co1) = if x = x' then let val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => - sgnError env (SgiWrongKind (strLoc, sgi1All, k1, + sgnError env (SgiWrongKind (loc, sgi1All, k1, sgi2All, k2, err)) val env = E.pushCNamedAs env x n1 k1 co1 in @@ -2969,7 +2981,7 @@ end) | L'.SgiCon (x, n2, k2, c2) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => let fun found (x', n1, k1, c1) = if x = x' then @@ -2991,7 +3003,7 @@ (unifyCons env loc c1 c2; good ()) handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, + (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err)); good ()) end @@ -3006,13 +3018,13 @@ | L'.SgiDatatype dts2 => let - fun found' (sgi1All, (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) = + fun found' (sgi1All as (_, loc), (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) = if x1 <> x2 then NONE else let fun mismatched ue = - (sgnError env (SgiMismatchedDatatypes (strLoc, sgi1All, sgi2All, ue)); + (sgnError env (SgiMismatchedDatatypes (loc, sgi1All, sgi2All, ue)); SOME env) val k = (L'.KType, loc) @@ -3095,7 +3107,7 @@ end | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => case sgi1 of L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) => if x = x' then @@ -3117,7 +3129,7 @@ (unifyCons env loc t1 t2; good ()) handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err)); + (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err)); good ()) end else @@ -3126,7 +3138,7 @@ | _ => NONE) | L'.SgiVal (x, n2, c2) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => case sgi1 of L'.SgiVal (x', n1, c1) => if x = x' then @@ -3138,19 +3150,19 @@ unifyCons env loc c1 (sub2 c2); SOME env) handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err)); + (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err)); SOME env) else NONE | _ => NONE) | L'.SgiStr (x, n2, sgn2) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => case sgi1 of L'.SgiStr (x', n1, sgn1) => if x = x' then let - val () = subSgn' counterparts env strLoc sgn1 sgn2 + val () = subSgn' counterparts env loc sgn1 sgn2 val env = E.pushStrNamedAs env x n1 sgn1 val env = if n1 = n2 then env @@ -3166,13 +3178,13 @@ | _ => NONE) | L'.SgiSgn (x, n2, sgn2) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => case sgi1 of L'.SgiSgn (x', n1, sgn1) => if x = x' then let - val () = subSgn' counterparts env strLoc sgn1 sgn2 - val () = subSgn' counterparts env strLoc sgn2 sgn1 + val () = subSgn' counterparts env loc sgn1 sgn2 + val () = subSgn' counterparts env loc sgn2 sgn1 val env = E.pushSgnNamedAs env x n2 sgn2 val env = if n1 = n2 then @@ -3188,7 +3200,7 @@ | _ => NONE) | L'.SgiConstraint (c2, d2) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => case sgi1 of L'.SgiConstraint (c1, d1) => if consEq env loc (c1, c2) @@ -3199,14 +3211,14 @@ | _ => NONE) | L'.SgiClassAbs (x, n2, k2) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => let fun found (x', n1, k1, co) = if x = x' then let val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => - sgnError env (SgiWrongKind (strLoc, sgi1All, k1, + sgnError env (SgiWrongKind (loc, sgi1All, k1, sgi2All, k2, err)) val env = E.pushCNamedAs env x n1 k1 co @@ -3226,14 +3238,14 @@ | _ => NONE end) | L'.SgiClass (x, n2, k2, c2) => - seek (fn (env, sgi1All as (sgi1, _)) => + seek (fn (env, sgi1All as (sgi1, loc)) => let fun found (x', n1, k1, c1) = if x = x' then let val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => - sgnError env (SgiWrongKind (strLoc, sgi1All, k1, + sgnError env (SgiWrongKind (loc, sgi1All, k1, sgi2All, k2, err)) val c2 = sub2 c2 @@ -3253,7 +3265,7 @@ (unifyCons env loc c1 c2; good ()) handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, + (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err)); good ()) end