Mercurial > urweb

annotate src/elab_err.sig @ 1591:20f898c29525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweaks to choices of source positions to use in error messages, including for subSgn
author Adam Chlipala <adam@chlipala.net>
date Sat, 05 Nov 2011 13:12:07 -0400
parents e525ad571e15
children 6c00d8af6239
rev   line source
adam@1303 1 (* Copyright (c) 2008-2010, 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@623 30 datatype kind_error =
adamc@623 31 UnboundKind of ErrorMsg.span * string
adamc@623 32
adamc@623 33 val kindError : ElabEnv.env -> kind_error -> unit
adamc@623 34
adamc@329 35 datatype kunify_error =
adamc@329 36 KOccursCheckFailed of Elab.kind * Elab.kind
adamc@329 37 | KIncompatible of Elab.kind * Elab.kind
adamc@329 38
adamc@623 39 val kunifyError : ElabEnv.env -> kunify_error -> unit
adamc@329 40
adamc@329 41 datatype con_error =
adamc@329 42 UnboundCon of ErrorMsg.span * string
adamc@329 43 | UnboundDatatype of ErrorMsg.span * string
adamc@329 44 | UnboundStrInCon of ErrorMsg.span * string
adamc@329 45 | WrongKind of Elab.con * Elab.kind * Elab.kind * kunify_error
adamc@329 46 | DuplicateField of ErrorMsg.span * string
adamc@329 47 | ProjBounds of Elab.con * int
adamc@329 48 | ProjMismatch of Elab.con * Elab.kind
adamc@329 49
adamc@329 50 val conError : ElabEnv.env -> con_error -> unit
adamc@329 51
adamc@329 52 datatype cunify_error =
adamc@329 53 CKind of Elab.kind * Elab.kind * kunify_error
adamc@329 54 | COccursCheckFailed of Elab.con * Elab.con
adamc@329 55 | CIncompatible of Elab.con * Elab.con
adamc@329 56 | CExplicitness of Elab.con * Elab.con
adamc@413 57 | CKindof of Elab.kind * Elab.con * string
adam@1359 58 | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * cunify_error option) option
adam@1303 59 | TooLifty of ErrorMsg.span * ErrorMsg.span
adam@1303 60 | TooUnify of Elab.con * Elab.con
adam@1306 61 | TooDeep
adamc@329 62
adamc@329 63 val cunifyError : ElabEnv.env -> cunify_error -> unit
adamc@329 64
adamc@329 65 datatype exp_error =
adamc@329 66 UnboundExp of ErrorMsg.span * string
adamc@329 67 | UnboundStrInExp of ErrorMsg.span * string
adamc@329 68 | Unify of Elab.exp * Elab.con * Elab.con * cunify_error
adamc@339 69 | Unif of string * ErrorMsg.span * Elab.con
adamc@329 70 | WrongForm of string * Elab.exp * Elab.con
adamc@329 71 | IncompatibleCons of Elab.con * Elab.con
adamc@329 72 | DuplicatePatternVariable of ErrorMsg.span * string
adamc@329 73 | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error
adamc@329 74 | UnboundConstructor of ErrorMsg.span * string list * string
adamc@329 75 | PatHasArg of ErrorMsg.span
adamc@329 76 | PatHasNoArg of ErrorMsg.span
adamc@819 77 | Inexhaustive of ErrorMsg.span * Elab.pat
adamc@329 78 | DuplicatePatField of ErrorMsg.span * string
adamc@329 79 | Unresolvable of ErrorMsg.span * Elab.con
adamc@329 80 | OutOfContext of ErrorMsg.span * (Elab.exp * Elab.con) option
adamc@329 81 | IllegalRec of string * Elab.exp
adamc@329 82
adamc@329 83 val expError : ElabEnv.env -> exp_error -> unit
adamc@329 84
adamc@329 85 datatype decl_error =
adamc@329 86 KunifsRemain of Elab.decl list
adamc@329 87 | CunifsRemain of Elab.decl list
adamc@329 88 | Nonpositive of Elab.decl
adamc@329 89
adamc@329 90 val declError : ElabEnv.env -> decl_error -> unit
adamc@329 91
adamc@329 92 datatype sgn_error =
adamc@329 93 UnboundSgn of ErrorMsg.span * string
adamc@1000 94 | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
adamc@1000 95 | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
adamc@1000 96 | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
adamc@1000 97 | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
adamc@1000 98 * (Elab.con * Elab.con * cunify_error) option
adamc@1000 99 | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
adamc@329 100 | UnWhereable of Elab.sgn * string
adamc@329 101 | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
adamc@329 102 | NotIncludable of Elab.sgn
adamc@329 103 | DuplicateCon of ErrorMsg.span * string
adamc@329 104 | DuplicateVal of ErrorMsg.span * string
adamc@329 105 | DuplicateSgn of ErrorMsg.span * string
adamc@329 106 | DuplicateStr of ErrorMsg.span * string
adamc@329 107 | NotConstraintsable of Elab.sgn
adamc@329 108
adamc@329 109 val sgnError : ElabEnv.env -> sgn_error -> unit
adamc@329 110
adamc@329 111 datatype str_error =
adamc@329 112 UnboundStr of ErrorMsg.span * string
adamc@329 113 | NotFunctor of Elab.sgn
adamc@329 114 | FunctorRebind of ErrorMsg.span
adamc@329 115 | UnOpenable of Elab.sgn
adamc@706 116 | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * kunify_error)
adamc@329 117 | DuplicateConstructor of string * ErrorMsg.span
adamc@329 118 | NotDatatype of ErrorMsg.span
adamc@329 119
adamc@329 120 val strError : ElabEnv.env -> str_error -> unit
adamc@329 121
adamc@329 122 end