Adding subst_term up to conv

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

3 files changed, 60 insertions, 11 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index dfc1e2f89..b10d8e935 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -673,27 +673,50 @@ let error_invalid_occurrence l =
     (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
      prlist_with_sep spc int l ++ str ".")
 
-let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
+let error_cannot_unify_occurrences pos (nowhere_except_in,locs) =
+(*
+  let l = List.filter ((>) !pos) locs in
+  let l =
+    if nowhere_except_in then list_subtract (interval 1 (!pos-1)) l else l in
+  errorlabstrm "" (str "Cannot unify occurrence at position " ++ int pos ++
+    plural n " with occurrence" ++ plural n " at position" ++
+    spc() ++ pr_enum l ++ str".")
+*)
+  errorlabstrm "" (str "Cannot unify occurrence at position " ++ int pos ++
+    strbrk " in a way compatible with the other unifications found for the given term.")
+
+let is_selected pos (nowhere_except_in,locs) =
+  nowhere_except_in && List.mem pos locs ||
+  not nowhere_except_in && not (List.mem pos locs)
+
+let subst_term_occ_gen_modulo (nowhere_except_in,locs as plocs) 
+    unify_fun merge_fun substs occ c t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
+  let substs = ref substs in
+  let add_subst subst =
+    try substs := merge_fun subst !substs
+    with _ -> error_cannot_unify_occurrences !pos plocs in
   assert (List.for_all (fun x -> x >= 0) locs);
   let rec substrec (k,c as kc) t =
-    if nowhere_except_in & !pos > maxocc then t
-    else
-    if eq_constr c t then
-      let r =
-	if nowhere_except_in then
-	  if List.mem !pos locs then (mkRel k) else t
-	else
-	  if List.mem !pos locs then t else (mkRel k)
+    if nowhere_except_in & !pos > maxocc then t else
+    try
+      let subst = unify_fun c t in
+      let r = if is_selected !pos plocs then (add_subst subst; mkRel k) else t
       in incr pos; r
-    else
+    with _ ->
       map_constr_with_binders_left_to_right
 	(fun d (k,c) -> (k+1,lift 1 c))
         substrec kc t
   in
   let t' = substrec (1,c) t in
-  (!pos, t')
+  (!substs,!pos, t')
+
+let subst_term_occ_gen plocs pos c t =
+  let (_,pos,t) = subst_term_occ_gen_modulo plocs 
+    (fun c1 c2 -> if eq_constr c1 c2 then () else raise Exit)
+    (fun () () -> ()) () pos c t in
+  (pos,t)
 
 let subst_term_occ (nowhere_except_in,locs as plocs) c t =
   if locs = [] then if nowhere_except_in then t else subst_term c t
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index c6ca30407..c74551735 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -153,6 +153,13 @@ val no_occurrences_in_set : occurrences
 val subst_term_occ_gen :
   occurrences -> int -> constr -> types -> int * types
 
+(** [subst_term_occ_gen_modulo] looks for subterm modulo a comparison
+    function returning a substitution of type ['a]; a function for
+    merging substitution and an initial substitution are required too *)
+val subst_term_occ_gen_modulo :
+  occurrences -> (constr -> constr -> 'a) -> ('a -> 'a -> 'a) -> 'a ->
+  int -> constr -> types -> 'a * int * types
+
 (** [subst_term_occ occl c d] replaces occurrences of [c] at
    positions [occl] by [Rel 1] in [d] (see also Note OCC) *)
 val subst_term_occ : occurrences -> constr -> constr -> constr
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ac91af5d2..1cc5c585d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1660,6 +1660,25 @@ let letin_tac with_eq name c occs gl =
 (* Implementation without generalisation: abbrev will be lost in hyps in *)
 (* in the extracted proof *)
 
+let default_matching_flags = {
+  modulo_conv_on_closed_terms = Some empty_transparent_state;
+  use_metas_eagerly_in_conv_on_closed_terms = false;
+  modulo_delta = empty_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  resolve_evars = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = false;
+  frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = false;
+  modulo_eta = false;
+  allow_K_in_toplevel_higher_order_unification = false
+}
+
+let matching_fun sigma c1 c2 =
+  w_unify false env CONV flags:default_matching_flags
+
+
 let letin_abstract id c (occs,check_occs) gl =
   let env = pf_env gl in
   let compute_dependency _ (hyp,_,_ as d) depdecls =