From d1898695cba6c924456d7de4d1b700072310f752 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 21 Apr 2012 14:57:00 -0400 Subject: Saving proper environments, to use in displaying nested error messages --- src/elab_err.sml | 66 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 33 insertions(+), 33 deletions(-) (limited to 'src/elab_err.sml') diff --git a/src/elab_err.sml b/src/elab_err.sml index 1951d971..f21ddce0 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -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 @@ datatype con_error = 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 @@ fun conError env err = 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 @@ fun conError env err = ("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 @@ fun cunifyError env err = ("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 @@ fun cunifyError env err = 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 @@ fun expError env err = 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 @@ fun expError env err = ("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 @@ fun declError env err = 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 @@ fun sgnError env err = | 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 @@ fun sgnError env err = (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 @@ datatype str_error = | 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 @@ fun strError env err = | 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 => -- cgit v1.2.3