1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: type_errors.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
15
type unsafe_judgment = constr * constr
23
| NotEnoughAbstractionInFixBody
24
| RecursionNotOnInductiveType of constr
25
| RecursionOnIllegalTerm of int * constr * int list * int list
26
| NotEnoughArgumentsForFixCall of int
28
| CodomainNotInductiveType of constr
29
| NestedRecursiveOccurrences
30
| UnguardedRecursiveCall of constr
31
| RecCallInTypeOfAbstraction of constr
32
| RecCallInNonRecArgOfConstructor of constr
33
| RecCallInTypeOfDef of constr
34
| RecCallInCaseFun of constr
35
| RecCallInCaseArg of constr
36
| RecCallInCasePred of constr
37
| NotGuardedForm of constr
40
| NonInformativeToInformative
41
| StrongEliminationOnNonSmallType
46
| UnboundVar of variable
47
| NotAType of unsafe_judgment
48
| BadAssumption of unsafe_judgment
49
| ReferenceVariables of constr
50
| ElimArity of inductive * sorts_family list * constr * unsafe_judgment
51
* (sorts_family * sorts_family * arity_error) option
52
| CaseNotInductive of unsafe_judgment
53
| WrongCaseInfo of inductive * case_info
54
| NumberBranches of unsafe_judgment * int
55
| IllFormedBranch of constr * int * constr * constr
56
| Generalization of (name * constr) * unsafe_judgment
57
| ActualType of unsafe_judgment * constr
59
(int * constr * constr) * unsafe_judgment * unsafe_judgment array
60
| CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
61
| IllFormedRecBody of guard_error * name array * int
63
int * name array * unsafe_judgment array * constr array
65
exception TypeError of env * type_error
67
let nfj (c,ct) = (c, nf_betaiota ct)
69
let error_unbound_rel env n =
70
raise (TypeError (env, UnboundRel n))
72
let error_unbound_var env v =
73
raise (TypeError (env, UnboundVar v))
75
let error_not_type env j =
76
raise (TypeError (env, NotAType j))
78
let error_assumption env j =
79
raise (TypeError (env, BadAssumption j))
81
let error_reference_variables env id =
82
raise (TypeError (env, ReferenceVariables id))
84
let error_elim_arity env ind aritylst c pj okinds =
85
raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds)))
87
let error_case_not_inductive env j =
88
raise (TypeError (env, CaseNotInductive j))
90
let error_number_branches env cj expn =
91
raise (TypeError (env, NumberBranches (nfj cj,expn)))
93
let error_ill_formed_branch env c i actty expty =
94
raise (TypeError (env,
95
IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty)))
97
let error_generalization env nvar c =
98
raise (TypeError (env, Generalization (nvar,c)))
100
let error_actual_type env j expty =
101
raise (TypeError (env, ActualType (j,expty)))
103
let error_cant_apply_not_functional env rator randl =
104
raise (TypeError (env, CantApplyNonFunctional (rator,randl)))
106
let error_cant_apply_bad_type env t rator randl =
107
raise (TypeError (env, CantApplyBadType (t,rator,randl)))
109
let error_ill_formed_rec_body env why lna i =
110
raise (TypeError (env, IllFormedRecBody (why,lna,i)))
112
let error_ill_typed_rec_body env i lna vdefj vargs =
113
raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))