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
|