adam@1719: (* Copyright (c) 2008-2010, 2012, Adam Chlipala adamc@329: * All rights reserved. adamc@329: * adamc@329: * Redistribution and use in source and binary forms, with or without adamc@329: * modification, are permitted provided that the following conditions are met: adamc@329: * adamc@329: * - Redistributions of source code must retain the above copyright notice, adamc@329: * this list of conditions and the following disclaimer. adamc@329: * - Redistributions in binary form must reproduce the above copyright notice, adamc@329: * this list of conditions and the following disclaimer in the documentation adamc@329: * and/or other materials provided with the distribution. adamc@329: * - The names of contributors may not be used to endorse or promote products adamc@329: * derived from this software without specific prior written permission. adamc@329: * adamc@329: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@329: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@329: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@329: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@329: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@329: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@329: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@329: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@329: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@329: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@329: * POSSIBILITY OF SUCH DAMAGE. adamc@329: *) adamc@329: adamc@329: structure ElabErr :> ELAB_ERR = struct adamc@329: adamc@329: structure L = Source adamc@329: open Elab adamc@329: adamc@329: structure E = ElabEnv adamc@329: structure U = ElabUtil adamc@329: adamc@329: open Print adamc@329: structure P = ElabPrint adamc@329: adamc@329: val p_kind = P.p_kind adamc@623: adamc@623: datatype kind_error = adamc@623: UnboundKind of ErrorMsg.span * string adamc@623: adamc@623: fun kindError env err = adamc@623: case err of adamc@623: UnboundKind (loc, s) => adamc@623: ErrorMsg.errorAt loc ("Unbound kind variable " ^ s) adamc@329: adamc@329: datatype kunify_error = adamc@329: KOccursCheckFailed of kind * kind adamc@329: | KIncompatible of kind * kind adam@1639: | KScope of kind * kind adamc@329: adamc@623: fun kunifyError env err = adamc@329: case err of adamc@329: KOccursCheckFailed (k1, k2) => adamc@329: eprefaces "Kind occurs check failed" adamc@623: [("Kind 1", p_kind env k1), adamc@623: ("Kind 2", p_kind env k2)] adamc@329: | KIncompatible (k1, k2) => adamc@329: eprefaces "Incompatible kinds" adamc@623: [("Kind 1", p_kind env k1), adamc@623: ("Kind 2", p_kind env k2)] adam@1639: | KScope (k1, k2) => adam@1639: eprefaces "Scoping prevents kind unification" adam@1639: [("Kind 1", p_kind env k1), adam@1639: ("Kind 2", p_kind env k2)] adamc@329: adam@1714: fun p_con env c = P.p_con env (ElabOps.reduceCon env c) adamc@329: adamc@329: datatype con_error = adamc@329: UnboundCon of ErrorMsg.span * string adamc@329: | UnboundDatatype of ErrorMsg.span * string adamc@329: | UnboundStrInCon of ErrorMsg.span * string adam@1719: | WrongKind of con * kind * kind * E.env * kunify_error adamc@329: | DuplicateField of ErrorMsg.span * string adamc@329: | ProjBounds of con * int adamc@329: | ProjMismatch of con * kind adamc@329: adamc@329: fun conError env err = adamc@329: case err of adamc@329: UnboundCon (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) adamc@329: | UnboundDatatype (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Unbound datatype " ^ s) adamc@329: | UnboundStrInCon (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Unbound structure " ^ s) adam@1719: | WrongKind (c, k1, k2, env', kerr) => adamc@329: (ErrorMsg.errorAt (#2 c) "Wrong kind"; adamc@329: eprefaces' [("Constructor", p_con env c), adamc@623: ("Have kind", p_kind env k1), adamc@623: ("Need kind", p_kind env k2)]; adam@1719: kunifyError env' kerr) adamc@329: | DuplicateField (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Duplicate record field " ^ s) adamc@329: | ProjBounds (c, n) => adamc@329: (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection"; adamc@329: eprefaces' [("Constructor", p_con env c), adamc@329: ("Index", Print.PD.string (Int.toString n))]) adamc@329: | ProjMismatch (c, k) => adamc@329: (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; adamc@329: eprefaces' [("Constructor", p_con env c), adamc@623: ("Kind", p_kind env k)]) adamc@329: adamc@329: datatype cunify_error = adam@1719: CKind of kind * kind * E.env * kunify_error adamc@329: | COccursCheckFailed of con * con adamc@329: | CIncompatible of con * con adamc@329: | CExplicitness of con * con adamc@413: | CKindof of kind * con * string adam@1719: | CRecordFailure of con * con * (con * con * con * (E.env * cunify_error) option) option adam@1303: | TooLifty of ErrorMsg.span * ErrorMsg.span adam@1303: | TooUnify of con * con adam@1306: | TooDeep adam@1639: | CScope of con * con adamc@329: adam@1719: fun cunifyError env err : unit = adamc@329: case err of adam@1719: CKind (k1, k2, env', kerr) => adamc@329: (eprefaces "Kind unification failure" adam@1582: [("Have", p_kind env k1), adam@1582: ("Need", p_kind env k2)]; adam@1719: kunifyError env' kerr) adamc@329: | COccursCheckFailed (c1, c2) => adamc@329: eprefaces "Constructor occurs check failed" adam@1582: [("Have", p_con env c1), adam@1582: ("Need", p_con env c2)] adamc@329: | CIncompatible (c1, c2) => adamc@329: eprefaces "Incompatible constructors" adam@1582: [("Have", p_con env c1), adam@1582: ("Need", p_con env c2)] adamc@329: | CExplicitness (c1, c2) => adamc@329: eprefaces "Differing constructor function explicitness" adam@1582: [("Have", p_con env c1), adam@1582: ("Need", p_con env c2)] adamc@413: | CKindof (k, c, expected) => adamc@413: eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")") adamc@623: [("Kind", p_kind env k), adamc@329: ("Con", p_con env c)] adamc@1071: | CRecordFailure (c1, c2, fo) => adam@1359: (eprefaces "Can't unify record constructors" adam@1582: (("Have", p_con env c1) adam@1582: :: ("Need", p_con env c2) adam@1359: :: (case fo of adam@1359: NONE => [] adam@1359: | SOME (nm, t1, t2, _) => adam@1359: [("Field", p_con env nm), adam@1359: ("Value 1", p_con env t1), adam@1359: ("Value 2", p_con env t2)])); adam@1359: case fo of adam@1719: SOME (_, _, _, SOME (env', err')) => cunifyError env' err' adam@1359: | _ => ()) adam@1303: | TooLifty (loc1, loc2) => adam@1303: (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings"; adam@1303: eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))]) adam@1303: | TooUnify (c1, c2) => adam@1303: (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable"; adam@1303: eprefaces' [("Replacement", p_con env c1), adam@1303: ("Body", p_con env c2)]) adam@1306: | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting" adam@1639: | CScope (c1, c2) => adam@1639: eprefaces "Scoping prevents constructor unification" adam@1639: [("Have", p_con env c1), adam@1639: ("Need", p_con env c2)] adamc@329: adamc@329: datatype exp_error = adamc@329: UnboundExp of ErrorMsg.span * string adamc@329: | UnboundStrInExp of ErrorMsg.span * string adam@1719: | Unify of exp * con * con * E.env * cunify_error adamc@339: | Unif of string * ErrorMsg.span * con adamc@329: | WrongForm of string * exp * con adamc@329: | IncompatibleCons of con * con adamc@329: | DuplicatePatternVariable of ErrorMsg.span * string adam@1719: | PatUnify of pat * con * con * E.env * cunify_error adamc@329: | UnboundConstructor of ErrorMsg.span * string list * string adamc@329: | PatHasArg of ErrorMsg.span adamc@329: | PatHasNoArg of ErrorMsg.span adamc@819: | Inexhaustive of ErrorMsg.span * pat adamc@329: | DuplicatePatField of ErrorMsg.span * string adamc@329: | Unresolvable of ErrorMsg.span * con adamc@329: | OutOfContext of ErrorMsg.span * (exp * con) option adamc@329: | IllegalRec of string * exp adam@2009: | IllegalFlex of Source.exp adamc@329: adam@1714: val simplExp = U.Exp.mapB {kind = fn _ => fn k => k, adam@1714: con = fn env => fn c => #1 (ElabOps.reduceCon env (c, ErrorMsg.dummySpan)), adam@1714: exp = fn _ => fn e => e, adam@1714: bind = fn (env, U.Exp.RelC (x, k)) => E.pushCRel env x k adam@1714: | (env, U.Exp.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co adam@1714: | (env, _) => env} adam@1714: adam@1714: fun p_exp env e = P.p_exp env (simplExp env e) adamc@329: val p_pat = P.p_pat adamc@329: adamc@329: fun expError env err = adamc@329: case err of adamc@329: UnboundExp (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) adamc@329: | UnboundStrInExp (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Unbound structure " ^ s) adam@1719: | Unify (e, c1, c2, env', uerr) => adamc@329: (ErrorMsg.errorAt (#2 e) "Unification failure"; adamc@329: eprefaces' [("Expression", p_exp env e), adamc@329: ("Have con", p_con env c1), adamc@329: ("Need con", p_con env c2)]; adam@1719: cunifyError env' uerr) adamc@339: | Unif (action, loc, c) => adamc@339: (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action); adamc@329: eprefaces' [("Con", p_con env c)]) adamc@329: | WrongForm (variety, e, t) => adamc@329: (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety); adamc@329: eprefaces' [("Expression", p_exp env e), adamc@329: ("Type", p_con env t)]) adamc@329: | IncompatibleCons (c1, c2) => adamc@329: (ErrorMsg.errorAt (#2 c1) "Incompatible constructors"; adam@1582: eprefaces' [("Have", p_con env c1), adam@1582: ("Need", p_con env c2)]) adamc@329: | DuplicatePatternVariable (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s) adam@1719: | PatUnify (p, c1, c2, env', uerr) => adamc@329: (ErrorMsg.errorAt (#2 p) "Unification failure for pattern"; adamc@329: eprefaces' [("Pattern", p_pat env p), adamc@329: ("Have con", p_con env c1), adamc@329: ("Need con", p_con env c2)]; adam@1719: cunifyError env' uerr) adamc@329: | UnboundConstructor (loc, ms, s) => adamc@329: ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern") adamc@329: | PatHasArg loc => adamc@329: ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument" adamc@329: | PatHasNoArg loc => adamc@329: ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument" adamc@819: | Inexhaustive (loc, p) => adamc@819: (ErrorMsg.errorAt loc "Inexhaustive 'case'"; adamc@819: eprefaces' [("Missed case", p_pat env p)]) adamc@329: | DuplicatePatField (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern") adamc@329: | OutOfContext (loc, co) => adamc@329: (ErrorMsg.errorAt loc "Type class wildcard occurs out of context"; adamc@329: Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e), adamc@329: ("Type", p_con env c)]) co) adamc@329: | Unresolvable (loc, c) => adamc@329: (ErrorMsg.errorAt loc "Can't resolve type class instance"; adam@1742: eprefaces' ([("Class constraint", p_con env c)] adam@1742: @ (case E.resolveFailureCause () of adam@1742: NONE => [] adam@1778: | SOME c' => [("Reduced to unresolvable", p_con env c')]))(*; adam@1778: app (fn (c, rs) => (eprefaces' [("CLASS", p_con env c)]; adam@1778: app (fn (c, e) => eprefaces' [("RULE", p_con env c), adam@1778: ("IMPL", p_exp env e)]) rs)) adam@1778: (E.listClasses env)*)) adamc@329: | IllegalRec (x, e) => adamc@329: (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)"; adamc@329: eprefaces' [("Variable", PD.string x), adamc@329: ("Expression", p_exp env e)]) adam@2009: | IllegalFlex e => adam@2009: (ErrorMsg.errorAt (#2 e) "Flex record syntax (\"...\") only allowed in patterns"; adam@2009: eprefaces' [("Expression", SourcePrint.p_exp e)]) adamc@329: adamc@329: adamc@329: datatype decl_error = adamc@329: KunifsRemain of decl list adamc@329: | CunifsRemain of decl list adamc@329: | Nonpositive of decl adamc@329: adamc@329: fun lspan [] = ErrorMsg.dummySpan adamc@329: | lspan ((_, loc) :: _) = loc adamc@329: adam@1584: val baseLen = 2000 adam@1584: adam@1584: fun p_decl env d = adam@1584: let adam@1584: val fname = OS.FileSys.tmpName () adam@1584: val out' = TextIO.openOut fname adam@1584: val out = Print.openOut {dst = out', wid = 80} adam@1584: adam@1584: fun readFromFile () = adam@1584: let adam@1584: val inf = TextIO.openIn fname adam@1584: adam@1584: fun loop acc = adam@1584: case TextIO.inputLine inf of adam@1584: NONE => String.concat (rev acc) adam@1584: | SOME line => loop (line :: acc) adam@1584: in adam@1584: loop [] adam@1584: before TextIO.closeIn inf adam@1584: end adam@1584: in adam@1584: Print.fprint out (P.p_decl env d); adam@1584: TextIO.closeOut out'; adam@1584: let adam@1584: val content = readFromFile () adam@1584: in adam@1584: OS.FileSys.remove fname; adam@1584: Print.PD.string (if size content <= baseLen then adam@1584: content adam@1584: else adam@1584: let adam@1584: val (befor, after) = Substring.position " adam@1521: (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration\n(look for them as \"\")"; adamc@329: eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)]) adamc@329: | CunifsRemain ds => adam@1521: (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration\n(look for them as \"\")"; adamc@329: eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)]) adamc@329: | Nonpositive d => adamc@329: (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)"; adamc@329: eprefaces' [("Decl", p_decl env d)]) adamc@329: adamc@329: datatype sgn_error = adamc@329: UnboundSgn of ErrorMsg.span * string adamc@1000: | UnmatchedSgi of ErrorMsg.span * sgn_item adam@1719: | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * E.env * kunify_error adam@1719: | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * E.env * cunify_error adamc@1000: | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item adam@1719: * (con * con * E.env * cunify_error) option adamc@1000: | SgnWrongForm of ErrorMsg.span * sgn * sgn adamc@329: | UnWhereable of sgn * string adam@1719: | WhereWrongKind of kind * kind * E.env * kunify_error adamc@329: | NotIncludable of sgn adamc@329: | DuplicateCon of ErrorMsg.span * string adamc@329: | DuplicateVal of ErrorMsg.span * string adamc@329: | DuplicateSgn of ErrorMsg.span * string adamc@329: | DuplicateStr of ErrorMsg.span * string adamc@329: | NotConstraintsable of sgn adamc@329: adamc@329: val p_sgn_item = P.p_sgn_item adamc@329: val p_sgn = P.p_sgn adamc@329: adamc@329: fun sgnError env err = adamc@329: case err of adamc@329: UnboundSgn (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Unbound signature variable " ^ s) adamc@1000: | UnmatchedSgi (loc, sgi) => adamc@329: (ErrorMsg.errorAt loc "Unmatched signature item"; adamc@329: eprefaces' [("Item", p_sgn_item env sgi)]) adam@1719: | SgiWrongKind (loc, sgi1, k1, sgi2, k2, env', kerr) => adamc@1000: (ErrorMsg.errorAt loc "Kind unification failure in signature matching:"; adamc@329: eprefaces' [("Have", p_sgn_item env sgi1), adamc@329: ("Need", p_sgn_item env sgi2), adamc@623: ("Kind 1", p_kind env k1), adamc@623: ("Kind 2", p_kind env k2)]; adam@1719: kunifyError env' kerr) adam@1719: | SgiWrongCon (loc, sgi1, c1, sgi2, c2, env', cerr) => adamc@1000: (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:"; adamc@329: eprefaces' [("Have", p_sgn_item env sgi1), adamc@329: ("Need", p_sgn_item env sgi2), adamc@329: ("Con 1", p_con env c1), adamc@329: ("Con 2", p_con env c2)]; adam@1719: cunifyError env' cerr) adamc@1000: | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) => adamc@1000: (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:"; adamc@329: eprefaces' [("Have", p_sgn_item env sgi1), adamc@329: ("Need", p_sgn_item env sgi2)]; adam@1719: Option.app (fn (c1, c2, env', ue) => adamc@329: (eprefaces "Unification error" adam@1719: [("Con 1", p_con env' c1), adam@1719: ("Con 2", p_con env' c2)]; adam@1719: cunifyError env' ue)) cerro) adamc@1000: | SgnWrongForm (loc, sgn1, sgn2) => adamc@1000: (ErrorMsg.errorAt loc "Incompatible signatures:"; adamc@329: eprefaces' [("Sig 1", p_sgn env sgn1), adamc@329: ("Sig 2", p_sgn env sgn2)]) adamc@329: | UnWhereable (sgn, x) => adamc@329: (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; adamc@329: eprefaces' [("Signature", p_sgn env sgn), adamc@329: ("Field", PD.string x)]) adam@1719: | WhereWrongKind (k1, k2, env', kerr) => adamc@329: (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'"; adamc@623: eprefaces' [("Have", p_kind env k1), adamc@623: ("Need", p_kind env k2)]; adam@1719: kunifyError env' kerr) adamc@329: | NotIncludable sgn => adamc@329: (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; adamc@329: eprefaces' [("Signature", p_sgn env sgn)]) adamc@329: | DuplicateCon (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature") adamc@329: | DuplicateVal (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature") adamc@329: | DuplicateSgn (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature") adamc@329: | DuplicateStr (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature") adamc@329: | NotConstraintsable sgn => adamc@329: (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'"; adamc@329: eprefaces' [("Signature", p_sgn env sgn)]) adamc@329: adamc@329: datatype str_error = adamc@329: UnboundStr of ErrorMsg.span * string adamc@329: | NotFunctor of sgn adamc@329: | FunctorRebind of ErrorMsg.span adamc@329: | UnOpenable of sgn adam@1719: | NotType of ErrorMsg.span * kind * (kind * kind * E.env * kunify_error) adamc@329: | DuplicateConstructor of string * ErrorMsg.span adamc@329: | NotDatatype of ErrorMsg.span adamc@329: adamc@329: fun strError env err = adamc@329: case err of adamc@329: UnboundStr (loc, s) => adamc@329: ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) adamc@329: | NotFunctor sgn => adamc@329: (ErrorMsg.errorAt (#2 sgn) "Application of non-functor"; adamc@329: eprefaces' [("Signature", p_sgn env sgn)]) adamc@329: | FunctorRebind loc => adamc@329: ErrorMsg.errorAt loc "Attempt to rebind functor" adamc@329: | UnOpenable sgn => adamc@329: (ErrorMsg.errorAt (#2 sgn) "Un-openable structure"; adamc@329: eprefaces' [("Signature", p_sgn env sgn)]) adam@1719: | NotType (loc, k, (k1, k2, env', ue)) => adamc@706: (ErrorMsg.errorAt loc "'val' type kind is not 'Type'"; adamc@623: eprefaces' [("Kind", p_kind env k), adamc@623: ("Subkind 1", p_kind env k1), adamc@623: ("Subkind 2", p_kind env k2)]; adam@1719: kunifyError env' ue) adamc@329: | DuplicateConstructor (x, loc) => adamc@329: ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x) adamc@329: | NotDatatype loc => adamc@329: ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype" adamc@329: adamc@329: end