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
|
adamc@1071
|
58 | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con) option
|
adam@1303
|
59 | TooLifty of ErrorMsg.span * ErrorMsg.span
|
adam@1303
|
60 | TooUnify of Elab.con * Elab.con
|
adamc@329
|
61
|
adamc@329
|
62 val cunifyError : ElabEnv.env -> cunify_error -> unit
|
adamc@329
|
63
|
adamc@329
|
64 datatype exp_error =
|
adamc@329
|
65 UnboundExp of ErrorMsg.span * string
|
adamc@329
|
66 | UnboundStrInExp of ErrorMsg.span * string
|
adamc@329
|
67 | Unify of Elab.exp * Elab.con * Elab.con * cunify_error
|
adamc@339
|
68 | Unif of string * ErrorMsg.span * Elab.con
|
adamc@329
|
69 | WrongForm of string * Elab.exp * Elab.con
|
adamc@329
|
70 | IncompatibleCons of Elab.con * Elab.con
|
adamc@329
|
71 | DuplicatePatternVariable of ErrorMsg.span * string
|
adamc@329
|
72 | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error
|
adamc@329
|
73 | UnboundConstructor of ErrorMsg.span * string list * string
|
adamc@329
|
74 | PatHasArg of ErrorMsg.span
|
adamc@329
|
75 | PatHasNoArg of ErrorMsg.span
|
adamc@819
|
76 | Inexhaustive of ErrorMsg.span * Elab.pat
|
adamc@329
|
77 | DuplicatePatField of ErrorMsg.span * string
|
adamc@329
|
78 | Unresolvable of ErrorMsg.span * Elab.con
|
adamc@329
|
79 | OutOfContext of ErrorMsg.span * (Elab.exp * Elab.con) option
|
adamc@329
|
80 | IllegalRec of string * Elab.exp
|
adamc@329
|
81
|
adamc@329
|
82 val expError : ElabEnv.env -> exp_error -> unit
|
adamc@329
|
83
|
adamc@329
|
84 datatype decl_error =
|
adamc@329
|
85 KunifsRemain of Elab.decl list
|
adamc@329
|
86 | CunifsRemain of Elab.decl list
|
adamc@329
|
87 | Nonpositive of Elab.decl
|
adamc@329
|
88
|
adamc@329
|
89 val declError : ElabEnv.env -> decl_error -> unit
|
adamc@329
|
90
|
adamc@329
|
91 datatype sgn_error =
|
adamc@329
|
92 UnboundSgn of ErrorMsg.span * string
|
adamc@1000
|
93 | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
|
adamc@1000
|
94 | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
|
adamc@1000
|
95 | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
|
adamc@1000
|
96 | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
|
adamc@1000
|
97 * (Elab.con * Elab.con * cunify_error) option
|
adamc@1000
|
98 | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
|
adamc@329
|
99 | UnWhereable of Elab.sgn * string
|
adamc@329
|
100 | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
|
adamc@329
|
101 | NotIncludable of Elab.sgn
|
adamc@329
|
102 | DuplicateCon of ErrorMsg.span * string
|
adamc@329
|
103 | DuplicateVal of ErrorMsg.span * string
|
adamc@329
|
104 | DuplicateSgn of ErrorMsg.span * string
|
adamc@329
|
105 | DuplicateStr of ErrorMsg.span * string
|
adamc@329
|
106 | NotConstraintsable of Elab.sgn
|
adamc@329
|
107
|
adamc@329
|
108 val sgnError : ElabEnv.env -> sgn_error -> unit
|
adamc@329
|
109
|
adamc@329
|
110 datatype str_error =
|
adamc@329
|
111 UnboundStr of ErrorMsg.span * string
|
adamc@329
|
112 | NotFunctor of Elab.sgn
|
adamc@329
|
113 | FunctorRebind of ErrorMsg.span
|
adamc@329
|
114 | UnOpenable of Elab.sgn
|
adamc@706
|
115 | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * kunify_error)
|
adamc@329
|
116 | DuplicateConstructor of string * ErrorMsg.span
|
adamc@329
|
117 | NotDatatype of ErrorMsg.span
|
adamc@329
|
118
|
adamc@329
|
119 val strError : ElabEnv.env -> str_error -> unit
|
adamc@329
|
120
|
adamc@329
|
121 end
|