adam@1303: (* Copyright (c) 2008-2010, 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: signature ELAB_ERR = sig adamc@329: adamc@623: datatype kind_error = adamc@623: UnboundKind of ErrorMsg.span * string adamc@623: adamc@623: val kindError : ElabEnv.env -> kind_error -> unit adamc@623: adamc@329: datatype kunify_error = adamc@329: KOccursCheckFailed of Elab.kind * Elab.kind adamc@329: | KIncompatible of Elab.kind * Elab.kind adam@1639: | KScope of Elab.kind * Elab.kind adamc@329: adamc@623: val kunifyError : ElabEnv.env -> kunify_error -> unit 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 Elab.con * Elab.kind * Elab.kind * ElabEnv.env * kunify_error adamc@329: | DuplicateField of ErrorMsg.span * string adamc@329: | ProjBounds of Elab.con * int adamc@329: | ProjMismatch of Elab.con * Elab.kind adamc@329: adamc@329: val conError : ElabEnv.env -> con_error -> unit adamc@329: adamc@329: datatype cunify_error = adam@1719: CKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error adamc@329: | COccursCheckFailed of Elab.con * Elab.con adamc@329: | CIncompatible of Elab.con * Elab.con adamc@329: | CExplicitness of Elab.con * Elab.con adamc@413: | CKindof of Elab.kind * Elab.con * string adam@1719: | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * (ElabEnv.env * cunify_error) option) option adam@1303: | TooLifty of ErrorMsg.span * ErrorMsg.span adam@1303: | TooUnify of Elab.con * Elab.con adam@1306: | TooDeep adam@1639: | CScope of Elab.con * Elab.con adamc@329: adamc@329: val cunifyError : ElabEnv.env -> cunify_error -> unit 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 Elab.exp * Elab.con * Elab.con * ElabEnv.env * cunify_error adamc@339: | Unif of string * ErrorMsg.span * Elab.con adamc@329: | WrongForm of string * Elab.exp * Elab.con adamc@329: | IncompatibleCons of Elab.con * Elab.con adamc@329: | DuplicatePatternVariable of ErrorMsg.span * string adam@1719: | PatUnify of Elab.pat * Elab.con * Elab.con * ElabEnv.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 * Elab.pat adamc@329: | DuplicatePatField of ErrorMsg.span * string adamc@329: | Unresolvable of ErrorMsg.span * Elab.con adamc@329: | OutOfContext of ErrorMsg.span * (Elab.exp * Elab.con) option adamc@329: | IllegalRec of string * Elab.exp adam@2009: | IllegalFlex of Source.exp adamc@329: adamc@329: val expError : ElabEnv.env -> exp_error -> unit adamc@329: adamc@329: datatype decl_error = adamc@329: KunifsRemain of Elab.decl list adamc@329: | CunifsRemain of Elab.decl list adamc@329: | Nonpositive of Elab.decl adamc@329: adamc@329: val declError : ElabEnv.env -> decl_error -> unit adamc@329: adamc@329: datatype sgn_error = adamc@329: UnboundSgn of ErrorMsg.span * string adamc@1000: | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item adam@1719: | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * ElabEnv.env * kunify_error adam@1719: | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * ElabEnv.env * cunify_error adamc@1000: | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item adam@1719: * (Elab.con * Elab.con * ElabEnv.env * cunify_error) option adamc@1000: | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn adamc@329: | UnWhereable of Elab.sgn * string adam@1719: | WhereWrongKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error adamc@329: | NotIncludable of Elab.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 Elab.sgn adamc@329: adamc@329: val sgnError : ElabEnv.env -> sgn_error -> unit adamc@329: adamc@329: datatype str_error = adamc@329: UnboundStr of ErrorMsg.span * string adamc@329: | NotFunctor of Elab.sgn adamc@329: | FunctorRebind of ErrorMsg.span adamc@329: | UnOpenable of Elab.sgn adam@1719: | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * ElabEnv.env * kunify_error) adamc@329: | DuplicateConstructor of string * ErrorMsg.span adamc@329: | NotDatatype of ErrorMsg.span adamc@329: adamc@329: val strError : ElabEnv.env -> str_error -> unit adamc@329: adamc@329: end