Move the specific map_constr_with_binders_left_to_right

for e_contextually where it is used. Bug #3648 is fixed.

6 files changed, 109 insertions, 19 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 15b16a36bc..3b3c9f9eed 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -850,7 +850,7 @@ let apply_on_subterm env evdref f c t =
       | _ ->
         map_constr_with_binders_left_to_right
 	  (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
-	  applyrec acc !evdref t
+	  applyrec acc t
   in
   applyrec (env,(0,c)) t
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index e47fad81bb..ba877d35c8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -101,14 +101,6 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
   in
     if !modified then !evdref, t' else !evdref, t
 
-let map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = 
-  match kind_of_term c with
-  | Proj (p, r) -> (* Treat specially for partial applications *)
-    let t = Retyping.expand_projection env sigma p r [] in
-      map_constr_with_binders_left_to_right g f	acc t
-  | _ -> map_constr_with_binders_left_to_right g f acc c
-      
-
 (************************)
 (* Unification results  *)
 (************************)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 86c9908c84..0d0f3c0e51 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -69,9 +69,3 @@ val check_evar_instance :
 
 val remove_instance_local_defs :
   evar_map -> existential_key -> constr array -> constr list
-
-(* This is up to partial applications and primitive projection expansion *)
-val map_constr_with_binders_left_to_right : 
-  (Context.rel_declaration -> (env * 'a) -> (env * 'a)) ->
-  ((env * 'a) -> constr -> constr) ->
-  (env * 'a) -> evar_map -> constr -> constr
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 44ff2b5b8c..01317ba253 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -150,8 +150,7 @@ let pattern_of_constr sigma t =
     | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
-    | Proj (p, c) ->  
-        PProj (constant_of_kn(canonical_con p), pattern_of_constr c)
+    | Proj (p, c) -> PProj (constant_of_kn(canonical_con p), pattern_of_constr c)
     | Evar (evk,ctxt as ev) ->
         (match snd (Evd.evar_source evk sigma) with
           | Evar_kinds.MatchingVar (b,id) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f0d0d45267..6f6de95fcd 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -945,6 +945,26 @@ let matches_head env sigma c t =
 
 let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false
 
+(** FIXME: Specific function to handle projections: it ignores what happens on the
+    parameters. This is a temporary fix while rewrite etc... are not up to equivalence
+    of the projection and it's eta expanded form.
+*)
+let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = 
+  match kind_of_term c with
+  | Proj (p, r) -> (* Treat specially for partial applications *)
+    let t = Retyping.expand_projection env sigma p r [] in
+    let hdf, al = destApp t in
+    let a = al.(Array.length al - 1) in
+    let app = (mkApp (t, Array.sub al 0 (Array.length al - 1))) in
+    let app' = f acc app in
+    let a' = f acc a in
+    let hdf', al' = destApp app' in
+      if hdf' == hdf then
+        (* Still the same projection, we ignore the change in parameters *)
+	mkProj (p, a')
+      else mkApp (app', [| a' |])
+  | _ -> map_constr_with_binders_left_to_right g f acc c
+
 let e_contextually byhead (occs,c) f env sigma t =
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
@@ -977,9 +997,9 @@ let e_contextually byhead (occs,c) f env sigma t =
       else
 	t
     with ConstrMatching.PatternMatchingFailure ->
-      map_constr_with_binders_left_to_right 
+      change_map_constr_with_binders_left_to_right 
 	(fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
-        traverse envc t
+        traverse envc sigma t
   in
   let t' = traverse (env,c) t in
   if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
diff --git a/test-suite/bugs/closed/3648.v b/test-suite/bugs/closed/3648.v
new file mode 100644
index 0000000000..1256d125f5
--- /dev/null
+++ b/test-suite/bugs/closed/3648.v
@@ -0,0 +1,85 @@
+(* File reduced by coq-bug-finder from original input, then from 8808 lines to 424 lines, then from 432 lines to 196 lines, then from\
+ 145 lines to 82 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+
+Reserved Infix "o" (at level 40, left associativity).
+Global Set Primitive Projections.
+
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+
+Record PreCategory :=
+  { object :> Type;
+    morphism : object -> object -> Type;
+
+    identity : forall x, morphism x x;
+    compose : forall s d d',
+                morphism d d'
+                -> morphism s d
+                -> morphism s d'
+    where "f 'o' g" := (compose f g)
+  }.
+Arguments identity {!C%category} / x%object : rename.
+
+Infix "o" := (@compose _ _ _ _) : morphism_scope.
+
+Local Open Scope morphism_scope.
+Definition prodC (C D : PreCategory) : PreCategory.
+  refine (@Build_PreCategory
+            (C * D)%type
+            (fun s d => (morphism C (fst s) (fst d)
+                         * morphism D (snd s) (snd d))%type)
+            (fun x => (identity (fst x), identity (snd x)))
+            (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1))).
+Defined.
+
+Local Infix "*" := prodC : category_scope.
+
+Delimit Scope functor_scope with functor.
+
+Record Functor (C D : PreCategory) :=
+  {
+    object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d
+                              -> morphism D (object_of s) (object_of d);
+    identity_of : forall x, morphism_of _ _ (identity x)
+                            = identity (object_of x)
+  }.
+Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
+
+Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
+Definition functor_category (C D : PreCategory) : PreCategory.
+  exact (@Build_PreCategory (Functor C D)
+                            (@NaturalTransformation C D)
+                            $(admit)$
+                            $(admit)$).
+Defined.
+
+Local Notation "C -> D" := (functor_category C D) : category_scope.
+Variable C1 : PreCategory.
+Variable C2 : PreCategory.
+Variable D : PreCategory.
+
+Definition functor_object_of
+: (C1 -> (C2 -> D))%category -> (C1 * C2 -> D)%category.
+Proof.
+  intro F; hnf in F |- *.
+  refine (Build_Functor
+            (prodC C1 C2) D
+            (fun c1c2 => F (fst c1c2) (snd c1c2))
+            (fun s d m => F (fst d) _1 (snd m) o (@morphism_of _ _ F _ _ (fst m)) (snd s))
+            _).
+  intros.
+  rewrite identity_of.
+  cbn.
+  rewrite (identity_of _ _ F (fst x)).
+  Undo.
+(* Toplevel input, characters 20-55:
+Error:
+Found no subterm matching "F _1 (identity (fst x))" in the current goal. *)
+  rewrite identity_of. (* Toplevel input, characters 15-34:
+Error:
+Found no subterm matching "morphism_of ?202 (identity ?203)" in the current goal. *)
\ No newline at end of file