Mercurial > urweb

annotate src/elab_err.sig @ 413:6a0e54400805

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sum prose
author Adam Chlipala <adamc@hcoop.net>
date Tue, 21 Oct 2008 19:56:20 -0400
parents 075b36dbb1a4
children 588b9d16b00a
rev   line source
adamc@329 1 (* Copyright (c) 2008, Adam Chlipala
adamc@329 2 * All rights reserved.
adamc@329 3 *
adamc@329 4 * Redistribution and use in source and binary forms, with or without
adamc@329 5 * modification, are permitted provided that the following conditions are met:
adamc@329 6 *
adamc@329 7 * - Redistributions of source code must retain the above copyright notice,
adamc@329 8 * this list of conditions and the following disclaimer.
adamc@329 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@329 10 * this list of conditions and the following disclaimer in the documentation
adamc@329 11 * and/or other materials provided with the distribution.
adamc@329 12 * - The names of contributors may not be used to endorse or promote products
adamc@329 13 * derived from this software without specific prior written permission.
adamc@329 14 *
adamc@329 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@329 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@329 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@329 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@329 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@329 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@329 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@329 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@329 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@329 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@329 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@329 26 *)
adamc@329 27
adamc@329 28 signature ELAB_ERR = sig
adamc@329 29
adamc@329 30 datatype kunify_error =
adamc@329 31 KOccursCheckFailed of Elab.kind * Elab.kind
adamc@329 32 | KIncompatible of Elab.kind * Elab.kind
adamc@329 33
adamc@329 34 val kunifyError : kunify_error -> unit
adamc@329 35
adamc@329 36 datatype con_error =
adamc@329 37 UnboundCon of ErrorMsg.span * string
adamc@329 38 | UnboundDatatype of ErrorMsg.span * string
adamc@329 39 | UnboundStrInCon of ErrorMsg.span * string
adamc@329 40 | WrongKind of Elab.con * Elab.kind * Elab.kind * kunify_error
adamc@329 41 | DuplicateField of ErrorMsg.span * string
adamc@329 42 | ProjBounds of Elab.con * int
adamc@329 43 | ProjMismatch of Elab.con * Elab.kind
adamc@329 44
adamc@329 45 val conError : ElabEnv.env -> con_error -> unit
adamc@329 46
adamc@329 47 datatype cunify_error =
adamc@329 48 CKind of Elab.kind * Elab.kind * kunify_error
adamc@329 49 | COccursCheckFailed of Elab.con * Elab.con
adamc@329 50 | CIncompatible of Elab.con * Elab.con
adamc@329 51 | CExplicitness of Elab.con * Elab.con
adamc@413 52 | CKindof of Elab.kind * Elab.con * string
adamc@329 53 | CRecordFailure of Elab.con * Elab.con
adamc@329 54
adamc@329 55 val cunifyError : ElabEnv.env -> cunify_error -> unit
adamc@329 56
adamc@329 57 datatype exp_error =
adamc@329 58 UnboundExp of ErrorMsg.span * string
adamc@329 59 | UnboundStrInExp of ErrorMsg.span * string
adamc@329 60 | Unify of Elab.exp * Elab.con * Elab.con * cunify_error
adamc@339 61 | Unif of string * ErrorMsg.span * Elab.con
adamc@329 62 | WrongForm of string * Elab.exp * Elab.con
adamc@329 63 | IncompatibleCons of Elab.con * Elab.con
adamc@329 64 | DuplicatePatternVariable of ErrorMsg.span * string
adamc@329 65 | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error
adamc@329 66 | UnboundConstructor of ErrorMsg.span * string list * string
adamc@329 67 | PatHasArg of ErrorMsg.span
adamc@329 68 | PatHasNoArg of ErrorMsg.span
adamc@329 69 | Inexhaustive of ErrorMsg.span
adamc@329 70 | DuplicatePatField of ErrorMsg.span * string
adamc@329 71 | Unresolvable of ErrorMsg.span * Elab.con
adamc@329 72 | OutOfContext of ErrorMsg.span * (Elab.exp * Elab.con) option
adamc@329 73 | IllegalRec of string * Elab.exp
adamc@329 74
adamc@329 75 val expError : ElabEnv.env -> exp_error -> unit
adamc@329 76
adamc@329 77 datatype decl_error =
adamc@329 78 KunifsRemain of Elab.decl list
adamc@329 79 | CunifsRemain of Elab.decl list
adamc@329 80 | Nonpositive of Elab.decl
adamc@329 81
adamc@329 82 val declError : ElabEnv.env -> decl_error -> unit
adamc@329 83
adamc@329 84 datatype sgn_error =
adamc@329 85 UnboundSgn of ErrorMsg.span * string
adamc@329 86 | UnmatchedSgi of Elab.sgn_item
adamc@329 87 | SgiWrongKind of Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
adamc@329 88 | SgiWrongCon of Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
adamc@329 89 | SgiMismatchedDatatypes of Elab.sgn_item * Elab.sgn_item * (Elab.con * Elab.con * cunify_error) option
adamc@329 90 | SgnWrongForm of Elab.sgn * Elab.sgn
adamc@329 91 | UnWhereable of Elab.sgn * string
adamc@329 92 | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
adamc@329 93 | NotIncludable of Elab.sgn
adamc@329 94 | DuplicateCon of ErrorMsg.span * string
adamc@329 95 | DuplicateVal of ErrorMsg.span * string
adamc@329 96 | DuplicateSgn of ErrorMsg.span * string
adamc@329 97 | DuplicateStr of ErrorMsg.span * string
adamc@329 98 | NotConstraintsable of Elab.sgn
adamc@329 99
adamc@329 100 val sgnError : ElabEnv.env -> sgn_error -> unit
adamc@329 101
adamc@329 102 datatype str_error =
adamc@329 103 UnboundStr of ErrorMsg.span * string
adamc@329 104 | NotFunctor of Elab.sgn
adamc@329 105 | FunctorRebind of ErrorMsg.span
adamc@329 106 | UnOpenable of Elab.sgn
adamc@329 107 | NotType of Elab.kind * (Elab.kind * Elab.kind * kunify_error)
adamc@329 108 | DuplicateConstructor of string * ErrorMsg.span
adamc@329 109 | NotDatatype of ErrorMsg.span
adamc@329 110
adamc@329 111 val strError : ElabEnv.env -> str_error -> unit
adamc@329 112
adamc@329 113 end