Mercurial > urweb
changeset 1719:0bafdfae2ac7
Saving proper environments, to use in displaying nested error messages
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 21 Apr 2012 14:57:00 -0400 |
| parents | dd12d6d9e9a7 |
| children | 30c0ca20bf59 |
| files | src/elab_err.sig src/elab_err.sml src/elaborate.sml tests/saveEnv.ur |
| diffstat | 4 files changed, 91 insertions(+), 90 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_err.sig Sat Apr 21 14:06:03 2012 -0400 +++ b/src/elab_err.sig Sat Apr 21 14:57:00 2012 -0400 @@ -43,7 +43,7 @@ UnboundCon of ErrorMsg.span * string | UnboundDatatype of ErrorMsg.span * string | UnboundStrInCon of ErrorMsg.span * string - | WrongKind of Elab.con * Elab.kind * Elab.kind * kunify_error + | WrongKind of Elab.con * Elab.kind * Elab.kind * ElabEnv.env * kunify_error | DuplicateField of ErrorMsg.span * string | ProjBounds of Elab.con * int | ProjMismatch of Elab.con * Elab.kind @@ -51,12 +51,12 @@ val conError : ElabEnv.env -> con_error -> unit datatype cunify_error = - CKind of Elab.kind * Elab.kind * kunify_error + CKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error | COccursCheckFailed of Elab.con * Elab.con | CIncompatible of Elab.con * Elab.con | CExplicitness of Elab.con * Elab.con | CKindof of Elab.kind * Elab.con * string - | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * cunify_error option) option + | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * (ElabEnv.env * cunify_error) option) option | TooLifty of ErrorMsg.span * ErrorMsg.span | TooUnify of Elab.con * Elab.con | TooDeep @@ -67,12 +67,12 @@ datatype exp_error = UnboundExp of ErrorMsg.span * string | UnboundStrInExp of ErrorMsg.span * string - | Unify of Elab.exp * Elab.con * Elab.con * cunify_error + | Unify of Elab.exp * Elab.con * Elab.con * ElabEnv.env * cunify_error | Unif of string * ErrorMsg.span * Elab.con | WrongForm of string * Elab.exp * Elab.con | IncompatibleCons of Elab.con * Elab.con | DuplicatePatternVariable of ErrorMsg.span * string - | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error + | PatUnify of Elab.pat * Elab.con * Elab.con * ElabEnv.env * cunify_error | UnboundConstructor of ErrorMsg.span * string list * string | PatHasArg of ErrorMsg.span | PatHasNoArg of ErrorMsg.span @@ -94,13 +94,13 @@ datatype sgn_error = UnboundSgn of ErrorMsg.span * string | 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 + | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * ElabEnv.env * kunify_error + | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * ElabEnv.env * cunify_error | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item - * (Elab.con * Elab.con * cunify_error) option + * (Elab.con * Elab.con * ElabEnv.env * cunify_error) option | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn | UnWhereable of Elab.sgn * string - | WhereWrongKind of Elab.kind * Elab.kind * kunify_error + | WhereWrongKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error | NotIncludable of Elab.sgn | DuplicateCon of ErrorMsg.span * string | DuplicateVal of ErrorMsg.span * string @@ -115,7 +115,7 @@ | NotFunctor of Elab.sgn | FunctorRebind of ErrorMsg.span | UnOpenable of Elab.sgn - | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * kunify_error) + | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * ElabEnv.env * kunify_error) | DuplicateConstructor of string * ErrorMsg.span | NotDatatype of ErrorMsg.span
--- a/src/elab_err.sml Sat Apr 21 14:06:03 2012 -0400 +++ b/src/elab_err.sml Sat Apr 21 14:57:00 2012 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2010, Adam Chlipala +(* Copyright (c) 2008-2010, 2012, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -72,7 +72,7 @@ UnboundCon of ErrorMsg.span * string | UnboundDatatype of ErrorMsg.span * string | UnboundStrInCon of ErrorMsg.span * string - | WrongKind of con * kind * kind * kunify_error + | WrongKind of con * kind * kind * E.env * kunify_error | DuplicateField of ErrorMsg.span * string | ProjBounds of con * int | ProjMismatch of con * kind @@ -85,12 +85,12 @@ ErrorMsg.errorAt loc ("Unbound datatype " ^ s) | UnboundStrInCon (loc, s) => ErrorMsg.errorAt loc ("Unbound structure " ^ s) - | WrongKind (c, k1, k2, kerr) => + | WrongKind (c, k1, k2, env', kerr) => (ErrorMsg.errorAt (#2 c) "Wrong kind"; eprefaces' [("Constructor", p_con env c), ("Have kind", p_kind env k1), ("Need kind", p_kind env k2)]; - kunifyError env kerr) + kunifyError env' kerr) | DuplicateField (loc, s) => ErrorMsg.errorAt loc ("Duplicate record field " ^ s) | ProjBounds (c, n) => @@ -103,24 +103,24 @@ ("Kind", p_kind env k)]) datatype cunify_error = - CKind of kind * kind * kunify_error + CKind of kind * kind * E.env * kunify_error | COccursCheckFailed of con * con | CIncompatible of con * con | CExplicitness of con * con | CKindof of kind * con * string - | CRecordFailure of con * con * (con * con * con * cunify_error option) option + | CRecordFailure of con * con * (con * con * con * (E.env * cunify_error) option) option | TooLifty of ErrorMsg.span * ErrorMsg.span | TooUnify of con * con | TooDeep | CScope of con * con -fun cunifyError env err = +fun cunifyError env err : unit = case err of - CKind (k1, k2, kerr) => + CKind (k1, k2, env', kerr) => (eprefaces "Kind unification failure" [("Have", p_kind env k1), ("Need", p_kind env k2)]; - kunifyError env kerr) + kunifyError env' kerr) | COccursCheckFailed (c1, c2) => eprefaces "Constructor occurs check failed" [("Have", p_con env c1), @@ -148,7 +148,7 @@ ("Value 1", p_con env t1), ("Value 2", p_con env t2)])); case fo of - SOME (_, _, _, SOME err') => cunifyError env err' + SOME (_, _, _, SOME (env', err')) => cunifyError env' err' | _ => ()) | TooLifty (loc1, loc2) => (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings"; @@ -166,12 +166,12 @@ datatype exp_error = UnboundExp of ErrorMsg.span * string | UnboundStrInExp of ErrorMsg.span * string - | Unify of exp * con * con * cunify_error + | Unify of exp * con * con * E.env * cunify_error | Unif of string * ErrorMsg.span * con | WrongForm of string * exp * con | IncompatibleCons of con * con | DuplicatePatternVariable of ErrorMsg.span * string - | PatUnify of pat * con * con * cunify_error + | PatUnify of pat * con * con * E.env * cunify_error | UnboundConstructor of ErrorMsg.span * string list * string | PatHasArg of ErrorMsg.span | PatHasNoArg of ErrorMsg.span @@ -197,12 +197,12 @@ ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) | UnboundStrInExp (loc, s) => ErrorMsg.errorAt loc ("Unbound structure " ^ s) - | Unify (e, c1, c2, uerr) => + | Unify (e, c1, c2, env', uerr) => (ErrorMsg.errorAt (#2 e) "Unification failure"; eprefaces' [("Expression", p_exp env e), ("Have con", p_con env c1), ("Need con", p_con env c2)]; - cunifyError env uerr) + cunifyError env' uerr) | Unif (action, loc, c) => (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action); eprefaces' [("Con", p_con env c)]) @@ -216,12 +216,12 @@ ("Need", p_con env c2)]) | DuplicatePatternVariable (loc, s) => ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s) - | PatUnify (p, c1, c2, uerr) => + | PatUnify (p, c1, c2, env', uerr) => (ErrorMsg.errorAt (#2 p) "Unification failure for pattern"; eprefaces' [("Pattern", p_pat env p), ("Have con", p_con env c1), ("Need con", p_con env c2)]; - cunifyError env uerr) + cunifyError env' uerr) | UnboundConstructor (loc, ms, s) => ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern") | PatHasArg loc => @@ -329,13 +329,13 @@ datatype sgn_error = UnboundSgn of ErrorMsg.span * string | 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 + | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * E.env * kunify_error + | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * E.env * cunify_error | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item - * (con * con * cunify_error) option + * (con * con * E.env * cunify_error) option | SgnWrongForm of ErrorMsg.span * sgn * sgn | UnWhereable of sgn * string - | WhereWrongKind of kind * kind * kunify_error + | WhereWrongKind of kind * kind * E.env * kunify_error | NotIncludable of sgn | DuplicateCon of ErrorMsg.span * string | DuplicateVal of ErrorMsg.span * string @@ -353,29 +353,29 @@ | UnmatchedSgi (loc, sgi) => (ErrorMsg.errorAt loc "Unmatched signature item"; eprefaces' [("Item", p_sgn_item env sgi)]) - | SgiWrongKind (loc, sgi1, k1, sgi2, k2, kerr) => + | SgiWrongKind (loc, sgi1, k1, sgi2, k2, env', 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 (loc, sgi1, c1, sgi2, c2, cerr) => + kunifyError env' kerr) + | SgiWrongCon (loc, sgi1, c1, sgi2, c2, env', 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) + cunifyError env' cerr) | 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) => + Option.app (fn (c1, c2, env', ue) => (eprefaces "Unification error" - [("Con 1", p_con env c1), - ("Con 2", p_con env c2)]; - cunifyError env ue)) cerro) + [("Con 1", p_con env' c1), + ("Con 2", p_con env' c2)]; + cunifyError env' ue)) cerro) | SgnWrongForm (loc, sgn1, sgn2) => (ErrorMsg.errorAt loc "Incompatible signatures:"; eprefaces' [("Sig 1", p_sgn env sgn1), @@ -384,11 +384,11 @@ (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; eprefaces' [("Signature", p_sgn env sgn), ("Field", PD.string x)]) - | WhereWrongKind (k1, k2, kerr) => + | WhereWrongKind (k1, k2, env', kerr) => (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'"; eprefaces' [("Have", p_kind env k1), ("Need", p_kind env k2)]; - kunifyError env kerr) + kunifyError env' kerr) | NotIncludable sgn => (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; eprefaces' [("Signature", p_sgn env sgn)]) @@ -409,7 +409,7 @@ | NotFunctor of sgn | FunctorRebind of ErrorMsg.span | UnOpenable of sgn - | NotType of ErrorMsg.span * kind * (kind * kind * kunify_error) + | NotType of ErrorMsg.span * kind * (kind * kind * E.env * kunify_error) | DuplicateConstructor of string * ErrorMsg.span | NotDatatype of ErrorMsg.span @@ -425,12 +425,12 @@ | UnOpenable sgn => (ErrorMsg.errorAt (#2 sgn) "Un-openable structure"; eprefaces' [("Signature", p_sgn env sgn)]) - | NotType (loc, k, (k1, k2, ue)) => + | NotType (loc, k, (k1, k2, env', ue)) => (ErrorMsg.errorAt loc "'val' type kind is not 'Type'"; eprefaces' [("Kind", p_kind env k), ("Subkind 1", p_kind env k1), ("Subkind 2", p_kind env k2)]; - kunifyError env ue) + kunifyError env' ue) | DuplicateConstructor (x, loc) => ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x) | NotDatatype loc =>
--- a/src/elaborate.sml Sat Apr 21 14:06:03 2012 -0400 +++ b/src/elaborate.sml Sat Apr 21 14:57:00 2012 -0400 @@ -86,11 +86,11 @@ and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan) - exception KUnify' of kunify_error + exception KUnify' of E.env * kunify_error fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) = let - fun err f = raise KUnify' (f (k1All, k2All)) + fun err f = raise KUnify' (env, f (k1All, k2All)) in case (k1, k2) of (L'.KType, L'.KType) => () @@ -179,16 +179,16 @@ | _ => err KIncompatible end - exception KUnify of L'.kind * L'.kind * kunify_error + exception KUnify of L'.kind * L'.kind * E.env * kunify_error fun unifyKinds env k1 k2 = unifyKinds' env k1 k2 - handle KUnify' err => raise KUnify (k1, k2, err) + handle KUnify' (env', err) => raise KUnify (k1, k2, env', err) fun checkKind env c k1 k2 = unifyKinds env k1 k2 - handle KUnify (k1, k2, err) => - conError env (WrongKind (c, k1, k2, err)) + handle KUnify (k1, k2, env', err) => + conError env (WrongKind (c, k1, k2, env', err)) val dummy = ErrorMsg.dummySpan @@ -563,7 +563,7 @@ con = fn L'.CUnif (_, _, _, _, r') => r = r' | _ => false} - exception CUnify' of cunify_error + exception CUnify' of E.env * cunify_error type record_summary = { fields : (L'.con * L'.con) list, @@ -589,7 +589,7 @@ fun p_summary env s = p_con env (summaryToCon s) - exception CUnify of L'.con * L'.con * cunify_error + exception CUnify of L'.con * L'.con * E.env * cunify_error fun kindof env (c, loc) = case c of @@ -618,7 +618,7 @@ (case hnormKind (kindof env c) of (L'.KArrow (_, k), _) => k | (L'.KError, _) => kerror - | k => raise CUnify' (CKindof (k, c, "arrow"))) + | k => raise CUnify' (env, CKindof (k, c, "arrow"))) | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) @@ -653,7 +653,7 @@ r := L'.KKnown k; k end) - | k => raise CUnify' (CKindof (k, c, "tuple"))) + | k => raise CUnify' (env, CKindof (k, c, "tuple"))) | L'.CError => kerror | L'.CUnif (_, _, k, _, _) => k @@ -662,7 +662,7 @@ | L'.CKApp (c, k) => (case hnormKind (kindof env c) of (L'.KFun (_, k'), _) => subKindInKind (0, k) k' - | k => raise CUnify' (CKindof (k, c, "kapp"))) + | k => raise CUnify' (env, CKindof (k, c, "kapp"))) | L'.TKFun _ => ktype exception GuessFailure @@ -758,7 +758,7 @@ r := L'.KKnown (L'.KRecord k, #2 c); k end - | k => raise CUnify' (CKindof (k, c, "record")) + | k => raise CUnify' (env, CKindof (k, c, "record")) val k1 = rkindof c1 val k2 = rkindof c2 @@ -987,10 +987,10 @@ findPointwise fs1 else SOME (nm1, c1, c2, (unifyCons env loc c1 c2; NONE) - handle CUnify (_, _, err) => (reducedSummaries := NONE; - SOME err)) + handle CUnify (_, _, env', err) => (reducedSummaries := NONE; + SOME (env', err))) in - raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1))) + raise CUnify' (env, CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1))) end fun default () = if !mayDelay then @@ -1009,7 +1009,7 @@ in if occursCon r c then (reducedSummaries := NONE; - raise CUnify' (COccursCheckFailed (cr, c))) + raise CUnify' (env, COccursCheckFailed (cr, c))) else let val sq = squish nl c @@ -1027,7 +1027,7 @@ in if occursCon r c then (reducedSummaries := NONE; - raise CUnify' (COccursCheckFailed (cr, c))) + raise CUnify' (env, COccursCheckFailed (cr, c))) else let val sq = squish nl c @@ -1119,7 +1119,7 @@ and unifyCons'' env loc (c1All as (c1, _)) (c2All as (c2, _)) = let - fun err f = raise CUnify' (f (c1All, c2All)) + fun err f = raise CUnify' (env, f (c1All, c2All)) fun projSpecial1 (c1, n1, onFail) = let @@ -1344,18 +1344,18 @@ and unifyCons env loc c1 c2 = unifyCons' env loc c1 c2 - handle CUnify' err => raise CUnify (c1, c2, err) - | KUnify args => raise CUnify (c1, c2, CKind args) + handle CUnify' (env', err) => raise CUnify (c1, c2, env', err) + | KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg) fun checkCon env e c1 c2 = unifyCons env (#2 e) c1 c2 - handle CUnify (c1, c2, err) => - expError env (Unify (e, c1, c2, err)) + handle CUnify (c1, c2, env', err) => + expError env (Unify (e, c1, c2, env', err)) fun checkPatCon env p c1 c2 = unifyCons env (#2 p) c1 c2 - handle CUnify (c1, c2, err) => - expError env (PatUnify (p, c1, c2, err)) + handle CUnify (c1, c2, env', err) => + expError env (PatUnify (p, c1, c2, env', err)) fun primType env p = case p of @@ -2579,7 +2579,7 @@ val (env', n) = E.pushENamed env x c' in (unifyKinds env ck ktype - handle KUnify ue => strError env (NotType (loc, ck, ue))); + handle KUnify arg => strError env (NotType (loc, ck, arg))); ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) end @@ -3056,9 +3056,9 @@ if x = x' then let val () = unifyKinds env k1 k2 - handle KUnify (k1, k2, err) => + handle KUnify (k1, k2, env', err) => sgnError env (SgiWrongKind (loc, sgi1All, k1, - sgi2All, k2, err)) + sgi2All, k2, env', err)) val env = E.pushCNamedAs env x n1 k1 co1 in SOME (if n1 = n2 then @@ -3125,9 +3125,9 @@ in (unifyCons env loc c1 c2; good ()) - handle CUnify (c1, c2, err) => + handle CUnify (c1, c2, env', err) => (sgnError env (SgiWrongCon (loc, sgi1All, c1, - sgi2All, c2, err)); + sgi2All, c2, env', err)); good ()) end else @@ -3251,8 +3251,8 @@ in (unifyCons env loc t1 t2; good ()) - handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err)); + handle CUnify (c1, c2, env', err) => + (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, env', err)); good ()) end else @@ -3272,8 +3272,8 @@ ("c2'", p_con env (sub2 c2))];*) unifyCons env loc c1 (sub2 c2); SOME env) - handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err)); + handle CUnify (c1, c2, env', err) => + (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, env', err)); SOME env) else NONE @@ -3340,9 +3340,9 @@ if x = x' then let val () = unifyKinds env k1 k2 - handle KUnify (k1, k2, err) => + handle KUnify (k1, k2, env', err) => sgnError env (SgiWrongKind (loc, sgi1All, k1, - sgi2All, k2, err)) + sgi2All, k2, env', err)) val env = E.pushCNamedAs env x n1 k1 co in @@ -3367,9 +3367,9 @@ if x = x' then let val () = unifyKinds env k1 k2 - handle KUnify (k1, k2, err) => + handle KUnify (k1, k2, env', err) => sgnError env (SgiWrongKind (loc, sgi1All, k1, - sgi2All, k2, err)) + sgi2All, k2, env', err)) val c2 = sub2 c2 @@ -3387,9 +3387,9 @@ in (unifyCons env loc c1 c2; good ()) - handle CUnify (c1, c2, err) => + handle CUnify (c1, c2, env', err) => (sgnError env (SgiWrongCon (loc, sgi1All, c1, - sgi2All, c2, err)); + sgi2All, c2, env', err)); good ()) end else @@ -4630,14 +4630,14 @@ else (app (fn (loc, env, k, s1, s2) => unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) - handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification"; - cunifyError env err; - case !reducedSummaries of - NONE => () - | SOME (s1, s2) => - (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:"; - eprefaces' [("Have", s1), - ("Need", s2)]))) + handle CUnify' (env', err) => (ErrorMsg.errorAt loc "Error in final record unification"; + cunifyError env' err; + case !reducedSummaries of + NONE => () + | SOME (s1, s2) => + (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:"; + eprefaces' [("Have", s1), + ("Need", s2)]))) (!delayedUnifs); delayedUnifs := []);