Mercurial > urweb

annotate src/elab_err.sig @ 1843:0da75c01a993

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make CGI programs use Status header to set HTTP status code
author Adam Chlipala <adam@chlipala.net>
date Tue, 05 Mar 2013 09:29:50 -0500
parents 0bafdfae2ac7
children 799be3911ce3
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
adamc@329 84
adamc@329 85 val expError : ElabEnv.env -> exp_error -> unit
adamc@329 86
adamc@329 87 datatype decl_error =
adamc@329 88 KunifsRemain of Elab.decl list
adamc@329 89 | CunifsRemain of Elab.decl list
adamc@329 90 | Nonpositive of Elab.decl
adamc@329 91
adamc@329 92 val declError : ElabEnv.env -> decl_error -> unit
adamc@329 93
adamc@329 94 datatype sgn_error =
adamc@329 95 UnboundSgn of ErrorMsg.span * string
adamc@1000 96 | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
adam@1719 97 | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * ElabEnv.env * kunify_error
adam@1719 98 | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * ElabEnv.env * cunify_error
adamc@1000 99 | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
adam@1719 100 * (Elab.con * Elab.con * ElabEnv.env * cunify_error) option
adamc@1000 101 | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
adamc@329 102 | UnWhereable of Elab.sgn * string
adam@1719 103 | WhereWrongKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
adamc@329 104 | NotIncludable of Elab.sgn
adamc@329 105 | DuplicateCon of ErrorMsg.span * string
adamc@329 106 | DuplicateVal of ErrorMsg.span * string
adamc@329 107 | DuplicateSgn of ErrorMsg.span * string
adamc@329 108 | DuplicateStr of ErrorMsg.span * string
adamc@329 109 | NotConstraintsable of Elab.sgn
adamc@329 110
adamc@329 111 val sgnError : ElabEnv.env -> sgn_error -> unit
adamc@329 112
adamc@329 113 datatype str_error =
adamc@329 114 UnboundStr of ErrorMsg.span * string
adamc@329 115 | NotFunctor of Elab.sgn
adamc@329 116 | FunctorRebind of ErrorMsg.span
adamc@329 117 | UnOpenable of Elab.sgn
adam@1719 118 | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * ElabEnv.env * kunify_error)
adamc@329 119 | DuplicateConstructor of string * ErrorMsg.span
adamc@329 120 | NotDatatype of ErrorMsg.span
adamc@329 121
adamc@329 122 val strError : ElabEnv.env -> str_error -> unit
adamc@329 123
adamc@329 124 end