aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/environ.ml14
-rw-r--r--kernel/environ.mli19
-rw-r--r--kernel/type_errors.ml58
-rw-r--r--kernel/type_errors.mli58
4 files changed, 82 insertions, 67 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a543f1957..5688813ad6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -469,9 +469,11 @@ let lookup_modtype mp env =
(*s Judgments. *)
-type unsafe_judgment = {
- uj_val : constr;
- uj_type : types }
+type ('constr, 'types) punsafe_judgment = {
+ uj_val : 'constr;
+ uj_type : 'types }
+
+type unsafe_judgment = (constr, types) punsafe_judgment
let make_judge v tj =
{ uj_val = v;
@@ -480,10 +482,12 @@ let make_judge v tj =
let j_val j = j.uj_val
let j_type j = j.uj_type
-type unsafe_type_judgment = {
- utj_val : constr;
+type 'types punsafe_type_judgment = {
+ utj_val : 'types;
utj_type : sorts }
+type unsafe_type_judgment = types punsafe_type_judgment
+
(*s Compilation of global declaration *)
let compile_constant_body = Cbytegen.compile_constant_body false
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ea570cb4a8..b7431dbe5f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -238,18 +238,21 @@ val keep_hyps : env -> Id.Set.t -> Context.Named.t
actually only a datatype to store a term with its type and the type of its
type. *)
-type unsafe_judgment = {
- uj_val : constr;
- uj_type : types }
+type ('constr, 'types) punsafe_judgment = {
+ uj_val : 'constr;
+ uj_type : 'types }
-val make_judge : constr -> types -> unsafe_judgment
-val j_val : unsafe_judgment -> constr
-val j_type : unsafe_judgment -> types
+type unsafe_judgment = (constr, types) punsafe_judgment
-type unsafe_type_judgment = {
- utj_val : constr;
+val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment
+val j_val : ('constr, 'types) punsafe_judgment -> 'constr
+val j_type : ('constr, 'types) punsafe_judgment -> 'types
+
+type 'types punsafe_type_judgment = {
+ utj_val : 'types;
utj_type : sorts }
+type unsafe_type_judgment = types punsafe_type_judgment
(** {6 Compilation of global declaration } *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 5071f0ad5d..5e17638152 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -13,52 +13,56 @@ open Reduction
(* Type errors. *)
-type guard_error =
+type 'constr pguard_error =
(* Fixpoints *)
| NotEnoughAbstractionInFixBody
- | RecursionNotOnInductiveType of constr
- | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
+ | RecursionNotOnInductiveType of 'constr
+ | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(* CoFixpoints *)
- | CodomainNotInductiveType of constr
+ | 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
+ | 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 guard_error = constr pguard_error
type arity_error =
| NonInformativeToInformative
| StrongEliminationOnNonSmallType
| WrongArity
-type type_error =
+type ('constr, 'types) ptype_error =
| UnboundRel of int
| UnboundVar of variable
- | NotAType of unsafe_judgment
- | BadAssumption of unsafe_judgment
- | ReferenceVariables of identifier * constr
- | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
+ | NotAType of ('constr, 'types) punsafe_judgment
+ | BadAssumption of ('constr, 'types) punsafe_judgment
+ | ReferenceVariables of identifier * 'constr
+ | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
* (sorts_family * sorts_family * arity_error) option
- | CaseNotInductive of unsafe_judgment
+ | CaseNotInductive of ('constr, 'types) punsafe_judgment
| WrongCaseInfo of pinductive * case_info
- | NumberBranches of unsafe_judgment * int
- | IllFormedBranch of constr * pconstructor * constr * constr
- | Generalization of (Name.t * types) * unsafe_judgment
- | ActualType of unsafe_judgment * types
+ | 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
| CantApplyBadType of
- (int * constr * constr) * unsafe_judgment * unsafe_judgment array
- | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
- | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array
+ (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 array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
- int * Name.t array * unsafe_judgment array * types array
+ int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
| UnsatisfiedConstraints of Univ.constraints
+type type_error = (constr, types) ptype_error
+
exception TypeError of env * type_error
let nfj env {uj_val=c;uj_type=ct} =
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 0c3a952b8d..bd6032716f 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -14,52 +14,56 @@ open Environ
(*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
notation i*)
-type guard_error =
+type 'constr pguard_error =
(** Fixpoints *)
| NotEnoughAbstractionInFixBody
- | RecursionNotOnInductiveType of constr
- | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
+ | RecursionNotOnInductiveType of 'constr
+ | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(** CoFixpoints *)
- | CodomainNotInductiveType of constr
+ | 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
+ | 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 guard_error = constr pguard_error
type arity_error =
| NonInformativeToInformative
| StrongEliminationOnNonSmallType
| WrongArity
-type type_error =
+type ('constr, 'types) ptype_error =
| UnboundRel of int
| UnboundVar of variable
- | NotAType of unsafe_judgment
- | BadAssumption of unsafe_judgment
- | ReferenceVariables of identifier * constr
- | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
+ | NotAType of ('constr, 'types) punsafe_judgment
+ | BadAssumption of ('constr, 'types) punsafe_judgment
+ | ReferenceVariables of identifier * 'constr
+ | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
* (sorts_family * sorts_family * arity_error) option
- | CaseNotInductive of unsafe_judgment
+ | CaseNotInductive of ('constr, 'types) punsafe_judgment
| WrongCaseInfo of pinductive * case_info
- | NumberBranches of unsafe_judgment * int
- | IllFormedBranch of constr * pconstructor * constr * constr
- | Generalization of (Name.t * types) * unsafe_judgment
- | ActualType of unsafe_judgment * types
+ | 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
| CantApplyBadType of
- (int * constr * constr) * unsafe_judgment * unsafe_judgment array
- | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
- | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array
+ (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 array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
- int * Name.t array * unsafe_judgment array * types array
+ int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
| UnsatisfiedConstraints of Univ.constraints
+type type_error = (constr, types) ptype_error
+
exception TypeError of env * type_error
val error_unbound_rel : env -> int -> 'a
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:59:23 +0000