aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/inductive.ml8
-rw-r--r--kernel/type_errors.ml5
-rw-r--r--kernel/type_errors.mli1
-rw-r--r--pretyping/cases.ml6
-rw-r--r--pretyping/pretyping.ml29
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/typing.ml11
-rw-r--r--pretyping/typing.mli6
-rw-r--r--test-suite/success/change.v8
10 files changed, 52 insertions, 26 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index aeeefbfa42..21f86233ab 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -233,12 +233,6 @@ let type_of_constructors ind (mib,mip) =
(************************************************************************)
-let error_elim_expln kp ki =
- match kp,ki with
- | (InType | InSet), InProp -> NonInformativeToInformative
- | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
- | _ -> WrongArity
-
(* Type of case predicates *)
let local_rels ctxt =
@@ -290,7 +284,7 @@ exception LocalArity of (sorts_family * sorts_family * arity_error) option
let check_allowed_sort ksort specif =
if not (List.exists ((=) ksort) (elim_sorts specif)) then
let s = inductive_sort_family (snd specif) in
- raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
+ raise (LocalArity (Some(ksort,s,error_elim_explain ksort s)))
let is_correct_arity env c pj ind specif params =
let arsign,_ = get_instantiated_arity specif params in
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 0f849e11ab..8f129999b4 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -109,4 +109,9 @@ let error_ill_formed_rec_body env why lna i fixenv vdefj =
let error_ill_typed_rec_body env i lna vdefj vargs =
raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))
+let error_elim_explain kp ki =
+ match kp,ki with
+ | (InType | InSet), InProp -> NonInformativeToInformative
+ | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
+ | _ -> WrongArity
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 2bf96f3227..7c61e10571 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -97,3 +97,4 @@ val error_ill_formed_rec_body :
val error_ill_typed_rec_body :
env -> int -> name array -> unsafe_judgment array -> types array -> 'a
+val error_elim_explain : sorts_family -> sorts_family -> arity_error
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 121d7dcc1b..b104db0267 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -947,7 +947,7 @@ let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs)
let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
- let pred= abstract_predicate env !evdref indf current dep tms p in
+ let pred = abstract_predicate env !evdref indf current dep tms p in
(pred, whd_betaiota !evdref
(applist (pred, realargs@[current])))
@@ -1169,7 +1169,9 @@ and match_current pb tomatch =
find_predicate pb.caseloc pb.env pb.evdref
pb.pred current indt (names,dep) pb.tomatch in
let ci = make_case_info pb.env mind pb.casestyle in
- let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
+ let pred = nf_betaiota !(pb.evdref) pred in
+ let case = mkCase (ci,pred,current,brvals) in
+ Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
let inst = List.map mkRel deps in
{ uj_val = applist (case, inst);
uj_type = substl inst typ }
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 69ee8d0290..7762d18f65 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -559,10 +559,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let fj = pretype (mk_tycon fty) env_f evdref lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let v =
- let mis,_ = dest_ind_family indf in
- let ci = make_case_info env mis LetStyle in
- mkCase (ci, p, cj.uj_val,[|f|]) in
- { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+ let ind,_ = dest_ind_family indf in
+ let ci = make_case_info env ind LetStyle in
+ Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+ mkCase (ci, p, cj.uj_val,[|f|]) in
+ { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
| None ->
let tycon = lift_tycon cs.cs_nargs tycon in
@@ -578,9 +579,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let ccl = refresh_universes ccl in
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
- let mis,_ = dest_ind_family indf in
- let ci = make_case_info env mis LetStyle in
- mkCase (ci, p, cj.uj_val,[|f|])
+ let ind,_ = dest_ind_family indf in
+ let ci = make_case_info env ind LetStyle in
+ Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+ mkCase (ci, p, cj.uj_val,[|f|])
in { uj_val = v; uj_type = ccl })
| GIf (loc,c,(na,po),b1,b2) ->
@@ -611,10 +613,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let ccl = nf_evar !evdref pj.utj_val in
let pred = it_mkLambda_or_LetIn ccl psign in
let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
- let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
- uj_type = typ} tycon
- in
- jtyp.uj_val, jtyp.uj_type
+ pred, typ
| None ->
let p = match tycon with
| Some (None, ty) -> ty
@@ -644,9 +643,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let b1 = f cstrs.(0) b1 in
let b2 = f cstrs.(1) b2 in
let v =
- let mis,_ = dest_ind_family indf in
- let ci = make_case_info env mis IfStyle in
- mkCase (ci, pred, cj.uj_val, [|b1;b2|])
+ let ind,_ = dest_ind_family indf in
+ let ci = make_case_info env ind IfStyle in
+ let pred = nf_evar !evdref pred in
+ Typing.check_allowed_sort env !evdref ind cj.uj_val pred;
+ mkCase (ci, pred, cj.uj_val, [|b1;b2|])
in
{ uj_val = v; uj_type = p }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 834c27969e..e8acd67caf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -770,7 +770,7 @@ let splay_arity env sigma c =
| Sort s -> l,s
| _ -> invalid_arg "splay_arity"
-let sort_of_arity env c = snd (splay_arity env Evd.empty c)
+let sort_of_arity env sigma c = snd (splay_arity env sigma c)
let splay_prod_n env sigma n =
let rec decrec env m ln c = if m = 0 then (ln,c) else
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1a90b23f21..3ffc587ef8 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -152,7 +152,7 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr
val splay_prod : env -> evar_map -> constr -> (name * constr) list * constr
val splay_lam : env -> evar_map -> constr -> (name * constr) list * constr
val splay_arity : env -> evar_map -> constr -> (name * constr) list * sorts
-val sort_of_arity : env -> constr -> sorts
+val sort_of_arity : env -> evar_map -> constr -> sorts
val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr
val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr
val splay_prod_assum :
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b40605f228..85abe2569b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -68,6 +68,16 @@ let e_judge_of_case env evdref ci pj cj lfj =
{ uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
uj_type = rslty }
+let check_allowed_sort env sigma ind c p =
+ let pj = Retyping.get_judgment_of env sigma p in
+ let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
+ let specif = Global.lookup_inductive ind in
+ let sorts = elim_sorts specif in
+ if not (List.exists ((=) ksort) sorts) then
+ let s = inductive_sort_family (snd specif) in
+ error_elim_arity env ind sorts c pj
+ (Some(ksort,s,error_elim_explain ksort s))
+
let e_judge_of_cast env evdref cj k tj =
let expected_type = tj.utj_val in
if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
@@ -218,4 +228,3 @@ let solve_evars env evd c =
let c = (execute env evdref c).uj_val in
(* side-effect on evdref *)
nf_evar !evdref c
-
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1e75d375d9..e2fd6a9d84 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Names
open Term
open Environ
open Evd
@@ -27,3 +28,8 @@ val meta_type : evar_map -> metavariable -> types
(** Solve existential variables using typing *)
val solve_evars : env -> evar_map -> constr -> constr
+
+(** Raise an error message if incorrect elimination for this inductive *)
+(** (first constr is term to match, second is return predicate) *)
+val check_allowed_sort : env -> evar_map -> inductive -> constr -> constr ->
+ unit
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 5ac6ce82b5..c65cf3036c 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -30,3 +30,11 @@ change 3 at 1 with (1+2) in H |- *.
change 3 at 1 with (1+2) in H, H|-.
change 3 in |- * at 1.
*)
+
+(* Test that pretyping checks allowed elimination sorts *)
+
+Goal True.
+Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x).
+Fail change True with
+ match ex_intro _ True (eq_refl True) with ex_intro x _ => x end.
+Abort.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 10:28:26 +0000