aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/cases.ml25
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1834.v174
2 files changed, 188 insertions, 11 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 932138f304..a89d5a942c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -871,20 +871,23 @@ let generalize_predicate (names,(nadep,_)) ny d tms ccl =
(* where pred is computed by abstract_predicate and PI tms.ccl by *)
(* extract_predicate *)
(*****************************************************************************)
-let rec extract_predicate l ccl = function
+let rec extract_predicate ccl = function
| Alias (deppat,nondeppat,_,_)::tms ->
(* substitution already done in build_branch *)
- extract_predicate l ccl tms
- | Abstract d'::tms ->
- let d' = map_rel_declaration (lift (List.length l)) d' in
- substl l (mkProd_or_LetIn d' (extract_predicate [] ccl tms))
+ extract_predicate ccl tms
+ | Abstract d::tms ->
+ mkProd_or_LetIn d (extract_predicate ccl tms)
| Pushed ((cur,NotInd _),_,(dep,_))::tms ->
- extract_predicate (if dep<>Anonymous then cur::l else l) ccl tms
+ let tms = if dep<>Anonymous then lift_tomatch_stack 1 tms else tms in
+ let pred = extract_predicate ccl tms in
+ if dep<>Anonymous then subst1 cur pred else pred
| Pushed ((cur,IsInd (_,IndType(_,realargs),_)),_,(dep,_))::tms ->
- let l = List.rev realargs@l in
- extract_predicate (if dep<>Anonymous then cur::l else l) ccl tms
+ let k = if dep<>Anonymous then 1 else 0 in
+ let tms = lift_tomatch_stack (List.length realargs + k) tms in
+ let pred = extract_predicate ccl tms in
+ substl (if dep<>Anonymous then cur::realargs else realargs) pred
| [] ->
- substl l ccl
+ ccl
let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl =
let sign = make_arity_signature env true indf in
@@ -897,7 +900,7 @@ let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl =
| _ -> (* Initial case *) tms in
let sign = List.map2 (fun na (_,c,t) -> (na,c,t)) (nadep::names) sign in
let ccl = if nadep <> Anonymous then ccl else lift_predicate 1 ccl tms in
- let pred = extract_predicate [] ccl tms in
+ let pred = extract_predicate ccl tms in
it_mkLambda_or_LetIn_name env pred sign
let known_dependent (_,dep) = (dep = KnownDep)
@@ -1703,7 +1706,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred =
let sigma = Option.cata (fun tycon ->
let na = (Name (id_of_string "x"),KnownNotDep) in
let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in
- let predinst = extract_predicate [] predcclj.uj_val tms in
+ let predinst = extract_predicate predcclj.uj_val tms in
Coercion.inh_conv_coerces_to loc env !evdref predinst tycon)
!evdref tycon in
let predccl = (j_nf_evar sigma predcclj).uj_val in
diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v
new file mode 100644
index 0000000000..947d15f0d2
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1834.v
@@ -0,0 +1,174 @@
+(* This tests rather deep nesting of abstracted terms *)
+
+(* This used to fail before Nov 2011 because of a de Bruijn indice bug
+ in extract_predicate.
+
+ Note: use of eq_ok allows shorten notations but was not in the
+ original example
+*)
+
+Scheme eq_rec_dep := Induction for eq Sort Type.
+
+Section Teq.
+
+Variable P0: Type.
+Variable P1: forall (y0:P0), Type.
+Variable P2: forall y0 (y1:P1 y0), Type.
+Variable P3: forall y0 y1 (y2:P2 y0 y1), Type.
+Variable P4: forall y0 y1 y2 (y3:P3 y0 y1 y2), Type.
+Variable P5: forall y0 y1 y2 y3 (y4:P4 y0 y1 y2 y3), Type.
+
+Variable x0:P0.
+
+Inductive eq0 : P0 -> Prop :=
+ refl0: eq0 x0.
+
+Definition eq_0 y0 := x0 = y0.
+
+Variable x1:P1 x0.
+
+Inductive eq1 : forall y0, P1 y0 -> Prop :=
+ refl1: eq1 x0 x1.
+
+Definition S0_0 y0 (e0:eq_0 y0) :=
+ eq_rec_dep P0 x0 (fun y0 e0 => P1 y0) x1 y0 e0.
+
+Definition eq_ok0 y0 y1 (E: eq_0 y0) := S0_0 y0 E = y1.
+
+Definition eq_1 y0 y1 :=
+ {E0:eq_0 y0 | eq_ok0 y0 y1 E0}.
+
+Variable x2:P2 x0 x1.
+
+Inductive eq2 :
+forall y0 y1, P2 y0 y1 -> Prop :=
+refl2: eq2 x0 x1 x2.
+
+Definition S1_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P2 y0 (S0_0 y0 e0)) x2 y0 e0.
+
+Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+ eq_rec_dep (P1 y0) (S0_0 y0 e0) (fun y1 e1 => P2 y0 y1)
+ (S1_0 y0 e0)
+ y1 e1.
+
+Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) :=
+ match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end.
+
+Definition eq_2 y0 y1 y2 :=
+ {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}.
+
+Variable x3:P3 x0 x1 x2.
+
+Inductive eq3 :
+forall y0 y1 y2, P3 y0 y1 y2 -> Prop :=
+refl3: eq3 x0 x1 x2 x3.
+
+Definition S2_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P3 y0 (S0_0 y0 e0) (S1_0 y0 e0)) x3 y0 e0.
+
+Definition S2_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+ eq_rec_dep (P1 y0) (S0_0 y0 e0)
+ (fun y1 e1 => P3 y0 y1 (S1_1 y0 y1 e0 e1))
+ (S2_0 y0 e0)
+ y1 e1.
+
+Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) :=
+ eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+ (fun y2 e2 => P3 y0 y1 y2)
+ (S2_1 y0 y1 e0 e1)
+ y2 e2.
+
+Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop :=
+ match E with exist (exist e0 e1) e2 =>
+ S2_2 y0 y1 y2 e0 e1 e2 = y3 end.
+
+Definition eq_3 y0 y1 y2 y3 :=
+ {E2: eq_2 y0 y1 y2 | eq_ok2 y0 y1 y2 y3 E2}.
+
+Variable x4:P4 x0 x1 x2 x3.
+
+Inductive eq4 :
+forall y0 y1 y2 y3, P4 y0 y1 y2 y3 -> Prop :=
+refl4: eq4 x0 x1 x2 x3 x4.
+
+Definition S3_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P4 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0))
+ x4 y0 e0.
+
+Definition S3_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+ eq_rec_dep (P1 y0) (S0_0 y0 e0)
+ (fun y1 e1 => P4 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1))
+ (S3_0 y0 e0)
+ y1 e1.
+
+Definition S3_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) :=
+ eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+ (fun y2 e2 => P4 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2))
+ (S3_1 y0 y1 e0 e1)
+ y2 e2.
+
+Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):=
+ eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2)
+ (fun y3 e3 => P4 y0 y1 y2 y3)
+ (S3_2 y0 y1 y2 e0 e1 e2)
+ y3 e3.
+
+Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop :=
+ match E with exist (exist (exist e0 e1) e2) e3 =>
+ S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end.
+
+Definition eq_4 y0 y1 y2 y3 y4 :=
+ {E3: eq_3 y0 y1 y2 y3 | eq_ok3 y0 y1 y2 y3 y4 E3}.
+
+Variable x5:P5 x0 x1 x2 x3 x4.
+
+Inductive eq5 :
+forall y0 y1 y2 y3 y4, P5 y0 y1 y2 y3 y4 -> Prop :=
+refl5: eq5 x0 x1 x2 x3 x4 x5.
+
+Definition S4_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0
+(fun y0 e0 => P5 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0) (S3_0 y0 e0))
+ x5 y0 e0.
+
+Definition S4_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+ eq_rec_dep (P1 y0) (S0_0 y0 e0)
+ (fun y1 e1 => P5 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1) (S3_1 y0 y1 e0
+e1))
+ (S4_0 y0 e0)
+ y1 e1.
+
+Definition S4_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) :=
+ eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+ (fun y2 e2 => P5 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2) (S3_2 y0 y1 y2 e0 e1 e2))
+ (S4_1 y0 y1 e0 e1)
+ y2 e2.
+
+Definition S4_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):=
+ eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2)
+ (fun y3 e3 => P5 y0 y1 y2 y3 (S3_3 y0 y1 y2 y3 e0 e1 e2 e3))
+ (S4_2 y0 y1 y2 e0 e1 e2)
+ y3 e3.
+
+Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+ (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3)
+ (e4:S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4) :=
+ eq_rec_dep (P4 y0 y1 y2 y3) (S3_3 y0 y1 y2 y3 e0 e1 e2 e3)
+ (fun y4 e4 => P5 y0 y1 y2 y3 y4)
+ (S4_3 y0 y1 y2 y3 e0 e1 e2 e3)
+ y4 e4.
+
+Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop :=
+ match E with exist (exist (exist (exist e0 e1) e2) e3) e4 =>
+ S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end.
+
+Definition eq_5 y0 y1 y2 y3 y4 y5 :=
+ {E4: eq_4 y0 y1 y2 y3 y4 | eq_ok4 y0 y1 y2 y3 y4 y5 E4 }.
+
+End Teq.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 16:48:47 +0000