Fix constrMatching as well as change/e_contextually to allow

matching partial applications of primitive projections. Fixes bug #3637.

7 files changed, 54 insertions, 63 deletions

diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index 95fb7ac68..d4cbad054 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -154,7 +154,7 @@ let merge_binding allow_bound_rels stk n cT subst =
       else raise PatternMatchingFailure
   in
   constrain n c subst
-
+      
 let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
   let convref ref c = 
     match ref, kind_of_term c with
@@ -221,65 +221,28 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
           else (* Might be a projection on the right *)
 	    match kind_of_term c2 with
 	    | Proj (pr, c) ->
-	      if diff == -1 then (* Do as if it was p c args2 *)
-		let subst = sorec stk env subst (PApp (PMeta meta, [|args1.(0)|])) c2 in
-		  Array.fold_left2 (sorec stk env) subst (Array.tl args1) args2
-	      else (* diff < 0, Expand the projection completely: p params c args2 *)
-      		let ty = Retyping.get_type_of env sigma c in
-		let (i,u), ind_args = Inductive.find_rectype env ty in
-		let term = mkApp (mkConstU (pr,u), 
-				  Array.of_list (ind_args @ (c :: Array.to_list args2)))
-		in
-		  sorec stk env subst p term
+	      let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
+		sorec stk env subst p term
 	    | _ -> raise PatternMatchingFailure)
 	   
       | PApp (c1,arg1), App (c2,arg2) ->
-	let diff = Array.length arg2 - Array.length arg1 in
 	(match c1, kind_of_term c2 with
+	| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r pr) ->
+	  raise PatternMatchingFailure
 	  (* eta-expanded version of projection against projection *)
-	| PRef (ConstRef r), Proj (p,c) when eq_constant r p ->
-      	  let pb = Environ.lookup_projection p env in
-	  let npars = pb.Declarations.proj_npars in
-	  let narg1 = Array.length arg1 in
-	    if narg1 >= npars + 1 then
-	      let pars, args = Array.chop (npars + 1) arg1 in
-	      let subst = sorec stk env subst (PApp (c1, pars)) c2 in
-		try Array.fold_left2 (sorec stk env) subst args arg2
-		with Invalid_argument _ -> raise PatternMatchingFailure
-	    else raise PatternMatchingFailure
-         (* meta against projection *)
-	| PMeta meta, Proj (p,c) when diff != 0 -> 
-          if diff == -1 then (* One more arg for the meta *)
-	    Array.fold_left2 (sorec stk env) (sorec stk env subst (PApp (c1, [|arg1.(0)|])) c2)
-	      (Array.tl arg1) arg2
-	  else raise PatternMatchingFailure
-	| _ ->
+	| _, Proj (pr,c) ->
+	  let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
+	    sorec stk env subst p term
+	| _, _ ->
           try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
           with Invalid_argument _ -> raise PatternMatchingFailure)
-
-      | PApp (PMeta (Some n), args), Proj (pr, c2) ->
-      	let ty = Retyping.get_type_of env sigma c2 in
-	let (i,u), ind_args = Inductive.find_rectype env ty in
-	  if Array.length args == 1 then 
-	    let term = mkApp (mkConstU (pr,u), Array.of_list ind_args) in
-	    let subst = merge_binding allow_bound_rels stk n term subst in
-      	      sorec stk env subst args.(0) c2
-	  else 
-	    let term = 
-	      mkApp (mkConstU (pr,u), Array.of_list (ind_args @ [c2]))
-	    in 
-	      sorec stk env subst p term
-		
-      | PApp (PRef (ConstRef c1),arg1), Proj (p2,c2) when eq_constant c1 p2 ->
-	let pb = Environ.lookup_projection p2 env in
-	let npars = pb.Declarations.proj_npars in
-	  if Array.length arg1 == npars + 1 then
-      	    let ty = Retyping.get_type_of env sigma c2 in
-	    let _, pars' = Inductive.find_rectype env ty in
-	    let subst = List.fold_left2 (sorec stk env) subst 
-	      (Array.to_list (Array.sub arg1 0 npars)) pars' in
-	      sorec stk env subst arg1.(npars) c2
-	  else raise PatternMatchingFailure
+	  
+      | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 pr) -> 
+	raise PatternMatchingFailure
+	
+      | PApp (c, args), Proj (pr, c2) ->
+	let term = Retyping.expand_projection env sigma pr c2 [] in
+	  sorec stk env subst p term
 
       | PProj (p1,c1), Proj (p2,c2) when eq_constant p1 p2 ->
           sorec stk env subst c1 c2
@@ -464,7 +427,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
     authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Proj (p,c') ->
     let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
-    let next () = try_aux [env] [c'] next_mk_ctx next in
+    let next () = 
+      if partial_app then
+	let term = Retyping.expand_projection env sigma p c' [] in
+	  aux env term mk_ctx next
+      else
+	try_aux [env] [c'] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
       authorized_occ env sigma partial_app closed pat c mk_ctx next
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f8e959075..15b16a36b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -835,8 +835,8 @@ let choose_less_dependent_instance evk evd term args =
   | [] -> None
   | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
 
-let apply_on_subterm evdref f c t =
-  let rec applyrec (k,c as kc) t =
+let apply_on_subterm env evdref f c t =
+  let rec applyrec (env,(k,c) as acc) t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
@@ -845,13 +845,14 @@ let apply_on_subterm evdref f c t =
       match kind_of_term t with
       | Evar (evk,args) when Evd.is_undefined !evdref evk ->
           let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
-          let g (_,b,_) a = if Option.is_empty b then applyrec kc a else a in
+          let g (_,b,_) a = if Option.is_empty b then applyrec acc a else a in
           mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
       | _ ->
-        map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c))
-	  applyrec kc 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
   in
-  applyrec (0,c) t
+  applyrec (env,(0,c)) t
 
 let filter_possible_projections c ty ctxt args =
   let fv1 = free_rels c in
@@ -932,7 +933,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         evdref := evd;
         evsref := (fst (destEvar ev),evty)::!evsref;
         ev in
-      set_holes evdref (apply_on_subterm evdref set_var c rhs) subst
+      set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst
   | [] -> rhs in
 
   let subst = make_subst (ctxt,Array.to_list args,argoccs) in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ba877d35c..e47fad81b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -101,6 +101,14 @@ 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 0d0f3c0e5..86c9908c8 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -69,3 +69,9 @@ 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/retyping.ml b/pretyping/retyping.ml
index 8f1a16dce..3374da327 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -241,3 +241,9 @@ let sorts_of_context env evc ctxt =
       let s = get_sort_of env evc t in
       (push_rel d env,s::sorts) in
   snd (aux ctxt)
+
+let expand_projection env sigma pr c args =
+  let ty = get_type_of env sigma c in
+  let (i,u), ind_args = Inductive.find_rectype env ty in
+    mkApp (mkConstU (pr,u), 
+	   Array.of_list (ind_args @ (c :: args)))
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index a694faf4e..3cbbc8a5d 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -45,3 +45,5 @@ val type_of_global_reference_knowing_conclusion :
   env -> evar_map -> constr -> types -> evar_map * types
 
 val sorts_of_context : env -> evar_map -> rel_context -> sorts list
+
+val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index acae69b68..8875d1d93 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -973,9 +973,9 @@ let e_contextually byhead (occs,c) f env sigma t =
       else
 	t
     with ConstrMatching.PatternMatchingFailure ->
-      map_constr_with_binders_left_to_right
+      Evarsolve.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;