Mercurial > urweb

annotate src/elab_err.sig @ 2291:50ad02829abd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make cache flushes happen immediately instead of at end of transaction.
author Ziv Scully <ziv@mit.edu>
date Tue, 17 Nov 2015 02:44:37 -0500
parents 799be3911ce3
children
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
adam@1639 38 | KScope of Elab.kind * Elab.kind
adamc@329 39
adamc@623 40 val kunifyError : ElabEnv.env -> kunify_error -> unit
adamc@329 41
adamc@329 42 datatype con_error =
adamc@329 43 UnboundCon of ErrorMsg.span * string
adamc@329 44 | UnboundDatatype of ErrorMsg.span * string
adamc@329 45 | UnboundStrInCon of ErrorMsg.span * string
adam@1719 46 | WrongKind of Elab.con * Elab.kind * Elab.kind * ElabEnv.env * kunify_error
adamc@329 47 | DuplicateField of ErrorMsg.span * string
adamc@329 48 | ProjBounds of Elab.con * int
adamc@329 49 | ProjMismatch of Elab.con * Elab.kind
adamc@329 50
adamc@329 51 val conError : ElabEnv.env -> con_error -> unit
adamc@329 52
adamc@329 53 datatype cunify_error =
adam@1719 54 CKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
adamc@329 55 | COccursCheckFailed of Elab.con * Elab.con
adamc@329 56 | CIncompatible of Elab.con * Elab.con
adamc@329 57 | CExplicitness of Elab.con * Elab.con
adamc@413 58 | CKindof of Elab.kind * Elab.con * string
adam@1719 59 | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * (ElabEnv.env * cunify_error) option) option
adam@1303 60 | TooLifty of ErrorMsg.span * ErrorMsg.span
adam@1303 61 | TooUnify of Elab.con * Elab.con
adam@1306 62 | TooDeep
adam@1639 63 | CScope of Elab.con * Elab.con
adamc@329 64
adamc@329 65 val cunifyError : ElabEnv.env -> cunify_error -> unit
adamc@329 66
adamc@329 67 datatype exp_error =
adamc@329 68 UnboundExp of ErrorMsg.span * string
adamc@329 69 | UnboundStrInExp of ErrorMsg.span * string
adam@1719 70 | Unify of Elab.exp * Elab.con * Elab.con * ElabEnv.env * cunify_error
adamc@339 71 | Unif of string * ErrorMsg.span * Elab.con
adamc@329 72 | WrongForm of string * Elab.exp * Elab.con
adamc@329 73 | IncompatibleCons of Elab.con * Elab.con
adamc@329 74 | DuplicatePatternVariable of ErrorMsg.span * string
adam@1719 75 | PatUnify of Elab.pat * Elab.con * Elab.con * ElabEnv.env * cunify_error
adamc@329 76 | UnboundConstructor of ErrorMsg.span * string list * string
adamc@329 77 | PatHasArg of ErrorMsg.span
adamc@329 78 | PatHasNoArg of ErrorMsg.span
adamc@819 79 | Inexhaustive of ErrorMsg.span * Elab.pat
adamc@329 80 | DuplicatePatField of ErrorMsg.span * string
adamc@329 81 | Unresolvable of ErrorMsg.span * Elab.con
adamc@329 82 | OutOfContext of ErrorMsg.span * (Elab.exp * Elab.con) option
adamc@329 83 | IllegalRec of string * Elab.exp
adam@2009 84 | IllegalFlex of Source.exp
adamc@329 85
adamc@329 86 val expError : ElabEnv.env -> exp_error -> unit
adamc@329 87
adamc@329 88 datatype decl_error =
adamc@329 89 KunifsRemain of Elab.decl list
adamc@329 90 | CunifsRemain of Elab.decl list
adamc@329 91 | Nonpositive of Elab.decl
adamc@329 92
adamc@329 93 val declError : ElabEnv.env -> decl_error -> unit
adamc@329 94
adamc@329 95 datatype sgn_error =
adamc@329 96 UnboundSgn of ErrorMsg.span * string
adamc@1000 97 | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
adam@1719 98 | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * ElabEnv.env * kunify_error
adam@1719 99 | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * ElabEnv.env * cunify_error
adamc@1000 100 | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
adam@1719 101 * (Elab.con * Elab.con * ElabEnv.env * cunify_error) option
adamc@1000 102 | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
adamc@329 103 | UnWhereable of Elab.sgn * string
adam@1719 104 | WhereWrongKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
adamc@329 105 | NotIncludable of Elab.sgn
adamc@329 106 | DuplicateCon of ErrorMsg.span * string
adamc@329 107 | DuplicateVal of ErrorMsg.span * string
adamc@329 108 | DuplicateSgn of ErrorMsg.span * string
adamc@329 109 | DuplicateStr of ErrorMsg.span * string
adamc@329 110 | NotConstraintsable of Elab.sgn
adamc@329 111
adamc@329 112 val sgnError : ElabEnv.env -> sgn_error -> unit
adamc@329 113
adamc@329 114 datatype str_error =
adamc@329 115 UnboundStr of ErrorMsg.span * string
adamc@329 116 | NotFunctor of Elab.sgn
adamc@329 117 | FunctorRebind of ErrorMsg.span
adamc@329 118 | UnOpenable of Elab.sgn
adam@1719 119 | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * ElabEnv.env * kunify_error)
adamc@329 120 | DuplicateConstructor of string * ErrorMsg.span
adamc@329 121 | NotDatatype of ErrorMsg.span
adamc@329 122
adamc@329 123 val strError : ElabEnv.env -> str_error -> unit
adamc@329 124
adamc@329 125 end