1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Constr
open Environ
open Univ
open UVars
(** Type errors. {% \label{typeerrors} %} *)
(*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
notation i*)
type 'constr pfix_guard_error =
(* Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of 'constr
| RecursionOnIllegalTerm of int * (env * 'constr) * (int list * int list) Lazy.t
| NotEnoughArgumentsForFixCall of int
| FixpointOnIrrelevantInductive
type 'constr pcofix_guard_error =
(* CoFixpoints *)
| CodomainNotInductiveType of 'constr
| NestedRecursiveOccurrences
| UnguardedRecursiveCall of 'constr
| RecCallInTypeOfAbstraction of 'constr
| RecCallInNonRecArgOfConstructor of 'constr
| RecCallInTypeOfDef of 'constr
| RecCallInCaseFun of 'constr
| RecCallInCaseArg of 'constr
| RecCallInCasePred of 'constr
| NotGuardedForm of 'constr
| ReturnPredicateNotCoInductive of 'constr
type 'constr pguard_error =
| FixGuardError of 'constr pfix_guard_error
| CoFixGuardError of 'constr pcofix_guard_error
type fix_guard_error = constr pfix_guard_error
type cofix_guard_error = constr pcofix_guard_error
type guard_error = constr pguard_error
type ('constr, 'types) pcant_apply_bad_type =
(int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
type ('constr, 'types, 'r) ptype_error =
| UnboundRel of int
| UnboundVar of variable
| NotAType of ('constr, 'types) punsafe_judgment
| BadAssumption of ('constr, 'types) punsafe_judgment
| ReferenceVariables of Id.t * GlobRef.t
| ElimArity of pinductive * 'constr * Sorts.t option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
| CaseOnPrivateInd of inductive
| WrongCaseInfo of pinductive * case_info
| NumberBranches of ('constr, 'types) punsafe_judgment * int
| IllFormedCaseParams
| IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
| Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
| ActualType of ('constr, 'types) punsafe_judgment * 'types
| IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types
| CantApplyBadType of ('constr, 'types) pcant_apply_bad_type
| CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
| IllFormedRecBody of 'constr pguard_error * (Name.t,'r) Context.pbinder_annot array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * (Name.t,'r) Context.pbinder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
| UnsatisfiedQConstraints of Sorts.QConstraints.t
| UnsatisfiedConstraints of Constraints.t
| UndeclaredQualities of Sorts.QVar.Set.t
| UndeclaredUniverse of Level.t
| DisallowedSProp
| BadBinderRelevance of 'r * ('constr, 'types, 'r) Context.Rel.Declaration.pt
| BadCaseRelevance of 'r * 'constr
| BadInvert
| BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
| UndeclaredUsedVariables of { declared_vars : Id.Set.t; inferred_vars : Id.Set.t }
type type_error = (constr, types, Sorts.relevance) ptype_error
exception TypeError of env * type_error
(** The different kinds of errors that may result of a malformed inductive
definition. *)
type inductive_error =
| NonPos of env * constr * constr
| NotEnoughArgs of env * constr * constr
| NotConstructor of env * Id.t * constr * constr * int * int
| NonPar of env * constr * int * constr * constr
| SameNamesTypes of Id.t
| SameNamesConstructors of Id.t
| SameNamesOverlap of Id.t list
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
| MissingConstraints of (Sorts.t list * Sorts.t)
(* each universe in the set should have been <= the other one *)
exception InductiveError of inductive_error
(** Raising functions *)
val error_unbound_rel : env -> int -> 'a
val error_unbound_var : env -> variable -> 'a
val error_not_type : env -> unsafe_judgment -> 'a
val error_assumption : env -> unsafe_judgment -> 'a
val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a
val error_elim_arity :
env -> pinductive -> constr -> Sorts.t option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> 'a
val error_case_on_private_ind : env -> inductive -> 'a
val error_number_branches : env -> unsafe_judgment -> int -> 'a
val error_ill_formed_branch : env -> constr -> pconstructor -> constr -> constr -> 'a
val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a
val error_actual_type : env -> unsafe_judgment -> types -> 'a
val error_incorrect_primitive : env -> (CPrimitives.op_or_type,types) punsafe_judgment -> types -> 'a
val error_cant_apply_not_functional :
env -> unsafe_judgment -> unsafe_judgment array -> 'a
val error_cant_apply_bad_type :
env -> int * constr * constr ->
unsafe_judgment -> unsafe_judgment array -> 'a
val error_ill_formed_rec_body :
env -> guard_error -> Name.t binder_annot array -> int -> env -> unsafe_judgment array -> 'a
val error_ill_typed_rec_body :
env -> int -> Name.t binder_annot array -> unsafe_judgment array -> types array -> 'a
val error_unsatisfied_qconstraints : env -> Sorts.QConstraints.t -> 'a
val error_unsatisfied_constraints : env -> Constraints.t -> 'a
val error_undeclared_qualities : env -> Sorts.QVar.Set.t -> 'a
val error_undeclared_universe : env -> Level.t -> 'a
val error_disallowed_sprop : env -> 'a
val error_bad_binder_relevance : env -> Sorts.relevance -> rel_declaration -> 'a
val error_bad_case_relevance : env -> Sorts.relevance -> Constr.case -> 'a
val error_bad_invert : env -> 'a
val error_bad_variance : env -> lev:Level.t -> expected:Variance.t -> actual:Variance.t -> 'a
val error_undeclared_used_variables : env -> declared_vars:Id.Set.t -> inferred_vars:Id.Set.t -> 'a
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('r1 -> 'r2) -> ('c -> 'd) -> ('c, 'c, 'r1) ptype_error -> ('d, 'd, 'r2) ptype_error
|
