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
|
(************************************************************************)
(* * 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
(** Type errors. {% \label{typeerrors} %} *)
(*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
notation i*)
type 'constr pguard_error =
(** Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of 'constr
| RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(** 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
| FixpointOnIrrelevantInductive
type guard_error = constr pguard_error
type arity_error =
| NonInformativeToInformative
| StrongEliminationOnNonSmallType
| WrongArity
type ('constr, 'types) 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 * ('constr, 'types) punsafe_judgment
* (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
| WrongCaseInfo of pinductive * case_info
| NumberBranches of ('constr, 'types) punsafe_judgment * int
| 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
(int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
| CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
| IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
| UnsatisfiedConstraints of Constraint.t
| UndeclaredUniverse of Level.t
| DisallowedSProp
| BadRelevance
| BadInvert
| BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
type type_error = (constr, types) 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 (Universe.Set.t * Universe.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 -> unsafe_judgment ->
(Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> '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 Context.binder_annot array -> int -> env -> unsafe_judgment array -> 'a
val error_ill_typed_rec_body :
env -> int -> Name.t Context.binder_annot array -> unsafe_judgment array -> types array -> 'a
val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
val error_unsatisfied_constraints : env -> Constraint.t -> 'a
val error_undeclared_universe : env -> Level.t -> 'a
val error_disallowed_sprop : env -> 'a
val error_bad_relevance : env -> 'a
val error_bad_invert : env -> 'a
val error_bad_variance : env -> lev:Level.t -> expected:Variance.t -> actual:Variance.t -> 'a
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
|
