From 0d7365e6ddcbd14933fcedae777649d31fb311cc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 Mar 2019 17:33:58 +0100
Subject: EConstr iterators respect the binding structure of cases.

Fixes #3166.
---
 engine/eConstr.ml                 | 18 +++++++--
 engine/eConstr.mli                |  4 ++
 engine/termops.ml                 | 36 +++++++++++------
 test-suite/bugs/closed/bug_3166.v | 84 +++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/bug_3166.v | 84 ---------------------------------------
 5 files changed, 126 insertions(+), 100 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_3166.v
 delete mode 100644 test-suite/bugs/opened/bug_3166.v

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index ec255aad03..7748df1a9b 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -373,6 +373,18 @@ let expand_case env _sigma (ci, u, pms, p, iv, c, bl) =
   let bl = of_constr_array bl in
   (ci, p, iv, c, bl)
 
+let annotate_case env sigma (ci, u, pms, p, iv, c, bl as case) =
+  let (_, p, _, _, bl) = expand_case env sigma case in
+  let p =
+    (* Too bad we need to fetch this data in the environment, should be in the
+      case_info instead. *)
+    let (_, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
+    decompose_lam_n_decls sigma (mip.Declarations.mind_nrealdecls + 1) p
+  in
+  let mk_br c n = decompose_lam_n_decls sigma n c in
+  let bl = Array.map2 mk_br bl ci.ci_cstr_ndecls in
+  (ci, u, pms, p, iv, c, bl)
+
 let expand_branch env _sigma u pms (ind, i) (nas, _br) =
   let open Declarations in
   let u = EInstance.unsafe_to_instance u in
@@ -413,9 +425,9 @@ let iter_with_full_binders env sigma g f n c =
   | App (c,l) -> f n c; Array.Fun1.iter f n l
   | Evar (_,l) -> List.iter (fun c -> f n c) l
   | Case (ci,u,pms,p,iv,c,bl) ->
-    (* FIXME: skip the type annotations *)
-    let (ci, p, iv, c, bl) = expand_case env sigma (ci, u, pms, p, iv, c, bl) in
-    f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
+    let (ci, _, pms, p, iv, c, bl) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let f_ctx (ctx, c) = f (List.fold_right g ctx n) c in
+    Array.Fun1.iter f n pms; f_ctx p; iter_invert (f n) iv; f n c; Array.iter f_ctx bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2add7b0b5e..e914d4f884 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -343,6 +343,10 @@ val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
 val expand_case : Environ.env -> Evd.evar_map ->
   case -> (case_info * t * case_invert * t * t array)
 
+val annotate_case : Environ.env -> Evd.evar_map -> case ->
+  case_info * EInstance.t * t array * (rel_context * t) * case_invert * t * (rel_context * t) array
+(** Same as above, but doesn't turn contexts into binders *)
+
 val expand_branch : Environ.env -> Evd.evar_map ->
   EInstance.t -> t array -> constructor -> case_branch -> rel_context
 (** Given a universe instance and parameters for the inductive type,
diff --git a/engine/termops.ml b/engine/termops.ml
index d331ecc458..4dc584cfa8 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -651,15 +651,19 @@ let map_constr_with_binders_left_to_right env sigma g f l c =
       if List.for_all2 (==) al' al then c
       else mkEvar (e, al')
   | Case (ci,u,pms,p,iv,b,bl) ->
-      (* FIXME: skip annotations? *)
-      let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, b, bl) in
+      let (ci, _, pms, p0, _, b, bl0) = annotate_case env sigma (ci, u, pms, p, iv, b, bl) in
+      let f_ctx (nas, _ as r) (ctx, c) =
+        let c' = f (List.fold_right g ctx l) c in
+        if c' == c then r else (nas, c')
+      in
       (* In v8 concrete syntax, predicate is after the term to match! *)
       let b' = f l b in
+      let pms' = Array.map_left (f l) pms in
+      let p' = f_ctx p p0 in
       let iv' = map_invert (f l) iv in
-      let p' = f l p in
-      let bl' = Array.map_left (f l) bl in
-      if b' == b && p' == p && iv' == iv && bl' == bl then c
-      else mkCase (EConstr.contract_case env sigma (ci, p', iv', b', bl'))
+      let bl' = Array.map_left (fun (c, c0) -> f_ctx c c0) (Array.map2 (fun x y -> (x, y)) bl bl0) in
+        if b' == b && pms' == pms && p' == p && iv' == iv && bl' == bl then c
+        else mkCase (ci, u, pms', p', iv', b', bl')
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
@@ -713,13 +717,18 @@ let map_constr_with_full_binders env sigma g f l cstr =
       let al' = List.map (f l) al in
       if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
   | Case (ci, u, pms, p, iv, c, bl) ->
-      let (ci, p, iv, c, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in
-      let p' = f l p in
+      let (ci, _, pms, p0, _, c, bl0) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+      let f_ctx (nas, _ as r) (ctx, c) =
+        let c' = f (List.fold_right g ctx l) c in
+        if c' == c then r else (nas, c')
+      in
+      let pms' = Array.Smart.map (f l) pms in
+      let p' = f_ctx p p0 in
       let iv' = map_invert (f l) iv in
       let c' = f l c in
-      let bl' = Array.map (f l) bl in
-      if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
-        mkCase (EConstr.contract_case env sigma (ci, p', iv', c', bl'))
+      let bl' = Array.map2 f_ctx bl bl0 in
+      if pms==pms' && p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
+        mkCase (ci, u, pms', p', iv', c', bl')
   | Fix (ln,(lna,tl,bl as fx)) ->
       let tl' = Array.map (f l) tl in
       let l' = fold_rec_types g fx l in
@@ -760,8 +769,9 @@ let fold_constr_with_full_binders env sigma g f n acc c =
   | Proj (_,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
   | Case (ci, u, pms, p, iv, c, bl) ->
-    let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in
-    Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+    let (ci, _, pms, p, _, c, bl) = EConstr.annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let f_ctx acc (ctx, c) = f (List.fold_right g ctx n) acc c in
+    Array.fold_left f_ctx (f n (fold_invert (f n) (f_ctx (Array.fold_left (f n) acc pms) p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
diff --git a/test-suite/bugs/closed/bug_3166.v b/test-suite/bugs/closed/bug_3166.v
new file mode 100644
index 0000000000..3b3375fdd8
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3166.v
@@ -0,0 +1,84 @@
+Set Asymmetric Patterns.
+
+Section eq.
+  Let A := { X : Type & X }.
+  Let B := (fun x : A => projT1 x).
+  Let T := (fun (a' : A) (b' : B a') => projT2 a' = b').
+  Let T' := T.
+  Let t1T := (fun _ : A => unit).
+  Let f1 := (fun x (_ : t1T x) => projT2 x).
+  Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)).
+  Let t1T' := t1T.
+  Let f1' := f1.
+  Let t1' := t1.
+
+  Theorem eq_matches_commute
+          a' b' (t' : T a' b')
+          (rta : forall b'', T' a' b'' -> A)
+          (rtb : forall b'' t'', B (rta b'' t''))
+          (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y)))
+          (R : forall (b : B (rta b' t')), T _ b -> Type)
+          (r1 : forall y, R (f1 _ y) (@t1 _ y))
+  : match
+      match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with
+        | eq_refl => rt1 tt
+      end
+      as t0 in (@eq _ _ b0)
+      return R b0 t0
+    with
+      | eq_refl => r1 tt
+    end
+    =
+    match t'
+          as t0' in (@eq _ _ b0')
+          return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type)
+                         (r1 : forall y, R (f1 _ y) (@t1 _ y)),
+                    R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with
+                           | eq_refl => rt1 tt
+                         end))
+    with
+      | eq_refl => fun _ r1 =>
+                      match rt1 tt with
+                        | eq_refl => r1 tt
+                      end
+    end R r1.
+  Proof.
+    destruct t'; reflexivity.
+  Defined.
+
+  Theorem eq_match_beta2
+          a b (t : T a b)
+          X
+          (R : forall b' (t' : T a b'), X b' -> Type)
+          (r1 : forall y x, R _ (@t1 _ y) x)
+          x
+  : match t as t' in (@eq _ _ b') return forall x, R b' t' x with
+      | eq_refl => r1 tt
+    end (x b)
+    =
+    match t as t' in (@eq _ _ b') return R b' t' (x b') with
+      | eq_refl => r1 tt (x _)
+    end.
+  Proof.
+    destruct t; reflexivity.
+  Defined.
+End eq.
+
+Definition typeof {T} (_ : T) := T.
+
+Eval compute in (eq_sym (eq_sym _)).
+Goal forall T (x y : T) (p : x = y), True.
+  intros.
+  pose proof
+       (@eq_matches_commute
+          (existT (fun T => T) T x) y p
+          (fun b'' _ => existT (fun T => T) T b'')
+          (fun _ _ => x)
+          (fun _ => eq_refl)
+          (fun x' _ => x' = y)
+          (fun _ => eq_refl)
+        ) as H0.
+  compute in H0.
+  change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
+  pose proof (fun k => @eq_trans _ _ _ k H0).
+Abort.
diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v
deleted file mode 100644
index baf87631f0..0000000000
--- a/test-suite/bugs/opened/bug_3166.v
+++ /dev/null
@@ -1,84 +0,0 @@
-Set Asymmetric Patterns.
-
-Section eq.
-  Let A := { X : Type & X }.
-  Let B := (fun x : A => projT1 x).
-  Let T := (fun (a' : A) (b' : B a') => projT2 a' = b').
-  Let T' := T.
-  Let t1T := (fun _ : A => unit).
-  Let f1 := (fun x (_ : t1T x) => projT2 x).
-  Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)).
-  Let t1T' := t1T.
-  Let f1' := f1.
-  Let t1' := t1.
-
-  Theorem eq_matches_commute
-          a' b' (t' : T a' b')
-          (rta : forall b'', T' a' b'' -> A)
-          (rtb : forall b'' t'', B (rta b'' t''))
-          (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y)))
-          (R : forall (b : B (rta b' t')), T _ b -> Type)
-          (r1 : forall y, R (f1 _ y) (@t1 _ y))
-  : match
-      match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with
-        | eq_refl => rt1 tt
-      end
-      as t0 in (@eq _ _ b0)
-      return R b0 t0
-    with
-      | eq_refl => r1 tt
-    end
-    =
-    match t'
-          as t0' in (@eq _ _ b0')
-          return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type)
-                         (r1 : forall y, R (f1 _ y) (@t1 _ y)),
-                    R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with
-                           | eq_refl => rt1 tt
-                         end))
-    with
-      | eq_refl => fun _ r1 =>
-                      match rt1 tt with
-                        | eq_refl => r1 tt
-                      end
-    end R r1.
-  Proof.
-    destruct t'; reflexivity.
-  Defined.
-
-  Theorem eq_match_beta2
-          a b (t : T a b)
-          X
-          (R : forall b' (t' : T a b'), X b' -> Type)
-          (r1 : forall y x, R _ (@t1 _ y) x)
-          x
-  : match t as t' in (@eq _ _ b') return forall x, R b' t' x with
-      | eq_refl => r1 tt
-    end (x b)
-    =
-    match t as t' in (@eq _ _ b') return R b' t' (x b') with
-      | eq_refl => r1 tt (x _)
-    end.
-  Proof.
-    destruct t; reflexivity.
-  Defined.
-End eq.
-
-Definition typeof {T} (_ : T) := T.
-
-Eval compute in (eq_sym (eq_sym _)).
-Goal forall T (x y : T) (p : x = y), True.
-  intros.
-  pose proof
-       (@eq_matches_commute
-          (existT (fun T => T) T x) y p
-          (fun b'' _ => existT (fun T => T) T b'')
-          (fun _ _ => x)
-          (fun _ => eq_refl)
-          (fun x' _ => x' = y)
-          (fun _ => eq_refl)
-        ) as H0.
-  compute in H0.
-  change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
-  Fail pose proof (fun k => @eq_trans _ _ _ k H0).
-Abort.
-- 
cgit v1.2.3