diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 40 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 3 |
4 files changed, 51 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 886d6b1feb..ab046f02f7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -682,6 +682,10 @@ type ('constr, 'types) punsafe_judgment = { uj_val : 'constr; uj_type : 'types } +let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type } +let on_judgment_value f j = { j with uj_val = f j.uj_val } +let on_judgment_type f j = { j with uj_type = f j.uj_type } + type unsafe_judgment = (constr, types) punsafe_judgment let make_judge v tj = diff --git a/kernel/environ.mli b/kernel/environ.mli index a9e0717559..0df9b91c4a 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -317,6 +317,10 @@ type ('constr, 'types) punsafe_judgment = { uj_val : 'constr; uj_type : 'types } +val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment +val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment +val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment + type unsafe_judgment = (constr, types) punsafe_judgment val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index fd050085d7..964d32c6b3 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -144,3 +144,43 @@ let error_unsatisfied_constraints env c = let error_undeclared_universe env l = raise (TypeError (env, UndeclaredUniverse l)) + +let map_pguard_error f = function +| NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody +| RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) +| RecursionOnIllegalTerm (n, (env, c), l1, l2) -> RecursionOnIllegalTerm (n, (env, f c), l1, l2) +| NotEnoughArgumentsForFixCall n -> NotEnoughArgumentsForFixCall n +| CodomainNotInductiveType c -> CodomainNotInductiveType (f c) +| NestedRecursiveOccurrences -> NestedRecursiveOccurrences +| UnguardedRecursiveCall c -> UnguardedRecursiveCall (f c) +| RecCallInTypeOfAbstraction c -> RecCallInTypeOfAbstraction (f c) +| RecCallInNonRecArgOfConstructor c -> RecCallInNonRecArgOfConstructor (f c) +| RecCallInTypeOfDef c -> RecCallInTypeOfDef (f c) +| RecCallInCaseFun c -> RecCallInCaseFun (f c) +| RecCallInCaseArg c -> RecCallInCaseArg (f c) +| RecCallInCasePred c -> RecCallInCasePred (f c) +| NotGuardedForm c -> NotGuardedForm (f c) +| ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c) + +let map_ptype_error f = function +| UnboundRel n -> UnboundRel n +| UnboundVar id -> UnboundVar id +| NotAType j -> NotAType (on_judgment f j) +| BadAssumption j -> BadAssumption (on_judgment f j) +| ReferenceVariables (id, c) -> ReferenceVariables (id, f c) +| ElimArity (pi, dl, c, j, ar) -> ElimArity (pi, dl, f c, on_judgment f j, ar) +| CaseNotInductive j -> CaseNotInductive (on_judgment f j) +| WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci) +| NumberBranches (j, n) -> NumberBranches (on_judgment f j, n) +| IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2) +| Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j) +| ActualType (j, t) -> ActualType (on_judgment f j, f t) +| CantApplyBadType ((n, c1, c2), j, vj) -> + CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj) +| CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv) +| IllFormedRecBody (ge, na, n, env, jv) -> + IllFormedRecBody (map_pguard_error f ge, na, n, env, Array.map (on_judgment f) jv) +| IllTypedRecBody (n, na, jv, t) -> + IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t) +| UnsatisfiedConstraints g -> UnsatisfiedConstraints g +| UndeclaredUniverse l -> UndeclaredUniverse l diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 3e954d6a8e..4b832930e1 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -130,3 +130,6 @@ val error_elim_explain : Sorts.family -> Sorts.family -> arity_error val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a val error_undeclared_universe : env -> Univ.Level.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 |