Refined second_order_matching so that a constraint on which

occurrences to abstract can be given. This allows to force "destruct"
to necessarily abstract over all occurrences of its main argument
(only the sub-arguments that occur in the inductive type of the main
argument have their occurrences constrained by typing). This
incidentally avoids "rewrite" succeeding in rewriting only a part of
the occurrences it has to rewrite. This repairs the failure of
RecursiveDefinition which failed after pattern unification fix from
r14642).

Full support for selecting occurrence of main argument still to be
done though.

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

3 files changed, 27 insertions, 12 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 53c659062e..ec581eaf16 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -618,7 +618,7 @@ let set_solve_evars f = solve_evars := f
  * proposition from Dan Grayson]
  *)
 
-let second_order_matching ts env_rhs evd (evk,args) rhs =
+let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   try
   let args = Array.to_list args in
   let evi = Evd.find_undefined evd evk in
@@ -629,18 +629,26 @@ let second_order_matching ts env_rhs evd (evk,args) rhs =
   let instance = List.map mkVar (List.map pi1 ctxt) in
 
   let rec make_subst = function
-  | (id,_,t)::ctxt, c::l when isVarId id c -> make_subst (ctxt,l)
-  | (id,_,t)::ctxt, c::l ->
+  | (id,_,t)::ctxt, c::l, occs::occsl when isVarId id c ->
+      if occs<>None then
+        error "Cannot force abstraction on identity instance."
+      else
+        make_subst (ctxt,l,occsl)
+  | (id,_,t)::ctxt, c::l, occs::occsl ->
       let evs = ref [] in
       let filter = List.map2 (&&) filter (filter_possible_projections c args) in
       let ty = Retyping.get_type_of env_rhs evd c in
-      (id,t,c,ty,evs,filter) :: make_subst (ctxt,l)
-  | [], [] -> []
-  | _ -> anomaly "Signature and instance do not match" in
+      (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt,l,occsl)
+  | [], [], [] -> []
+  | _ -> anomaly "Signature, instance and occurrences list do not match" in
 
   let rec set_holes evdref rhs = function
-  | (id,_,c,cty,evsref,filter)::subst ->
+  | (id,_,c,cty,evsref,filter,occs)::subst ->
       let set_var k =
+        match occs with
+        | Some (false,[]) -> mkVar id
+        | Some _ -> error "Selection of specific occurrences not supported"
+        | None ->
         let evty = set_holes evdref cty subst in
         let instance = snd (list_filter2 (fun b c -> b) (filter,instance)) in
         let evd,ev = new_evar_instance sign !evdref evty ~filter instance in
@@ -650,7 +658,7 @@ let second_order_matching ts env_rhs evd (evk,args) rhs =
       set_holes evdref (apply_on_subterm set_var c rhs) subst
   | [] -> rhs in
 
-  let subst = make_subst (ctxt,args) in
+  let subst = make_subst (ctxt,args,argoccs) in
 
   let evdref = ref evd in
   let rhs = set_holes evdref rhs subst in
@@ -664,7 +672,7 @@ let second_order_matching ts env_rhs evd (evk,args) rhs =
       raise Exit in
 
   let rec abstract_free_holes evd = function
-  | (id,idty,c,_,evsref,_)::l ->
+  | (id,idty,c,_,evsref,_,_)::l ->
       let rec force_instantiation evd = function
       | (evk,evty)::evs ->
           let evd =
@@ -695,7 +703,8 @@ let second_order_matching ts env_rhs evd (evk,args) rhs =
 let second_order_matching_with_args ts env evd ev l t =
 (*
   let evd,ev = evar_absorb_arguments env evd ev l in
-  second_order_matching ts env evd ev t
+  let argoccs = array_map_to_list (fun _ -> None) (snd ev) in
+  second_order_matching ts env evd ev argoccs t
 *)
   (evd,false)
 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 27a71be241..3e2ca7aedf 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -10,6 +10,7 @@ open Names
 open Term
 open Sign
 open Environ
+open Termops
 open Reductionops
 open Evd
 
@@ -43,4 +44,4 @@ val check_conv_record : constr * types list -> constr * types list ->
 val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
 
 val second_order_matching : transparent_state -> env -> evar_map -> 
-  existential -> constr -> evar_map * bool
+  existential -> occurrences option list -> constr -> evar_map * bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 693ea43957..a660745859 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -64,11 +64,16 @@ let abstract_list_all env evd typ c l =
   with UserError _ | Type_errors.TypeError _ ->
     error_cannot_find_well_typed_abstraction env evd p l
 
+let set_occurrences_of_last_arg args =
+  Some all_occurrences :: List.tl (array_map_to_list (fun _ -> None) args)
+
 let abstract_list_all_with_dependencies env evd typ c l =
   let evd,ev = new_evar evd env typ in
   let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in
+  let argoccs = set_occurrences_of_last_arg (snd ev') in
   let evd,b =
-    Evarconv.second_order_matching empty_transparent_state env evd ev' c in
+    Evarconv.second_order_matching empty_transparent_state
+      env evd ev' argoccs c in
   if b then nf_evar evd (existential_value evd (destEvar ev))
   else error "Cannot find a well-typed abstraction."