Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).

(technically, since the signature "tomatch" of terms to match and of
terms to generalize is typed in a context that does not consider terms
to match as binders while the return predicate do consider them as
binders, the adjusment of the context of the "tomatch" to the context
of the predicate needs lifting in each missing part of the "tomatch"
context, what was not done)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14664 85f007b7-540e-0410-9357-904b9bb8a0f7

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.