diff options
Diffstat (limited to 'kernel/type_errors.ml')
| -rw-r--r-- | kernel/type_errors.ml | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 481ffc290c..c45fe1cf00 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -33,6 +33,7 @@ type 'constr pguard_error = | RecCallInCasePred of 'constr | NotGuardedForm of 'constr | ReturnPredicateNotCoInductive of 'constr + | FixpointOnIrrelevantInductive type guard_error = constr pguard_error @@ -47,8 +48,8 @@ type ('constr, 'types) ptype_error = | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr - | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment - * (Sorts.family * Sorts.family * arity_error) option + | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment + * (Sorts.family list * 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 @@ -59,11 +60,13 @@ type ('constr, 'types) ptype_error = | 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 array * int * env * ('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 array * ('constr, 'types) punsafe_judgment array * 'types array + int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.Constraint.t | UndeclaredUniverse of Univ.Level.t + | DisallowedSProp + | BadRelevance type type_error = (constr, types) ptype_error @@ -102,8 +105,8 @@ let error_assumption env j = let error_reference_variables env id c = raise (TypeError (env, ReferenceVariables (id,c))) -let error_elim_arity env ind aritylst c pj okinds = - raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds))) +let error_elim_arity env ind c pj okinds = + raise (TypeError (env, ElimArity (ind,c,pj,okinds))) let error_case_not_inductive env j = raise (TypeError (env, CaseNotInductive j)) @@ -149,6 +152,12 @@ let error_unsatisfied_constraints env c = let error_undeclared_universe env l = raise (TypeError (env, UndeclaredUniverse l)) +let error_disallowed_sprop env = + raise (TypeError (env, DisallowedSProp)) + +let error_bad_relevance env = + raise (TypeError (env, BadRelevance)) + let map_pguard_error f = function | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) @@ -165,6 +174,7 @@ let map_pguard_error f = function | RecCallInCasePred c -> RecCallInCasePred (f c) | NotGuardedForm c -> NotGuardedForm (f c) | ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c) +| FixpointOnIrrelevantInductive -> FixpointOnIrrelevantInductive let map_ptype_error f = function | UnboundRel n -> UnboundRel n @@ -172,7 +182,7 @@ let map_ptype_error f = function | 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) +| ElimArity (pi, c, j, ar) -> ElimArity (pi, 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) @@ -189,3 +199,5 @@ let map_ptype_error f = function IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t) | UnsatisfiedConstraints g -> UnsatisfiedConstraints g | UndeclaredUniverse l -> UndeclaredUniverse l +| DisallowedSProp -> DisallowedSProp +| BadRelevance -> BadRelevance |