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 10533 2008-02-08 16:54:47Z msozeau $ *)
21
| NotEnoughAbstractionInFixBody
22
| RecursionNotOnInductiveType of constr
23
| RecursionOnIllegalTerm of int * constr * int list * int list
24
| NotEnoughArgumentsForFixCall of int
26
| CodomainNotInductiveType of constr
27
| NestedRecursiveOccurrences
28
| UnguardedRecursiveCall of constr
29
| RecCallInTypeOfAbstraction of constr
30
| RecCallInNonRecArgOfConstructor of constr
31
| RecCallInTypeOfDef of constr
32
| RecCallInCaseFun of constr
33
| RecCallInCaseArg of constr
34
| RecCallInCasePred of constr
35
| NotGuardedForm of constr
38
| NonInformativeToInformative
39
| StrongEliminationOnNonSmallType
44
| UnboundVar of variable
45
| NotAType of unsafe_judgment
46
| BadAssumption of unsafe_judgment
47
| ReferenceVariables of constr
48
| ElimArity of inductive * sorts_family list * constr * unsafe_judgment
49
* (sorts_family * sorts_family * arity_error) option
50
| CaseNotInductive of unsafe_judgment
51
| WrongCaseInfo of inductive * case_info
52
| NumberBranches of unsafe_judgment * int
53
| IllFormedBranch of constr * int * constr * constr
54
| Generalization of (name * types) * unsafe_judgment
55
| ActualType of unsafe_judgment * types
57
(int * constr * constr) * unsafe_judgment * unsafe_judgment array
58
| CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
59
| IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array
61
int * name array * unsafe_judgment array * types array
63
exception TypeError of env * type_error
65
let nfj {uj_val=c;uj_type=ct} =
66
{uj_val=c;uj_type=nf_betaiota ct}
68
let error_unbound_rel env n =
69
raise (TypeError (env, UnboundRel n))
71
let error_unbound_var env v =
72
raise (TypeError (env, UnboundVar v))
74
let error_not_type env j =
75
raise (TypeError (env, NotAType j))
77
let error_assumption env j =
78
raise (TypeError (env, BadAssumption j))
80
let error_reference_variables env id =
81
raise (TypeError (env, ReferenceVariables id))
83
let error_elim_arity env ind aritylst c pj okinds =
84
raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds)))
86
let error_case_not_inductive env j =
87
raise (TypeError (env, CaseNotInductive j))
89
let error_number_branches env cj expn =
90
raise (TypeError (env, NumberBranches (nfj cj,expn)))
92
let error_ill_formed_branch env c i actty expty =
93
raise (TypeError (env,
94
IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty)))
96
let error_generalization env nvar c =
97
raise (TypeError (env, Generalization (nvar,c)))
99
let error_actual_type env j expty =
100
raise (TypeError (env, ActualType (j,expty)))
102
let error_cant_apply_not_functional env rator randl =
103
raise (TypeError (env, CantApplyNonFunctional (rator,randl)))
105
let error_cant_apply_bad_type env t rator randl =
106
raise (TypeError (env, CantApplyBadType (t,rator,randl)))
108
let error_ill_formed_rec_body env why lna i fixenv vdefj =
109
raise (TypeError (env, IllFormedRecBody (why,lna,i,fixenv,vdefj)))
111
let error_ill_typed_rec_body env i lna vdefj vargs =
112
raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))