Generalizing subst_term_occ so that it supports an arbitrary matching

function but also restricting it to closed matching and consequently
renaming it to subst_closed_term_occ.

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

4 files changed, 88 insertions, 57 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 715fc2360..b6c67555d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -854,7 +854,7 @@ let abstract_scheme env sigma (locc,a) c =
   if occur_meta a then
     mkLambda (na,ta,c)
   else
-    mkLambda (na,ta,subst_term_occ locc a c)
+    mkLambda (na,ta,subst_closed_term_occ locc a c)
 
 let pattern_occs loccs_trm env sigma c =
   let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index b10d8e935..9e8d22a87 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -622,10 +622,8 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
 	  None
     | _ -> None
 
-(* Recognizing occurrences of a given (closed) subterm in a term for Pattern :
-   [subst_term c t] substitutes [(Rel 1)] for all occurrences of (closed)
-   term [c] in a term [t] *)
-(*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*)
+(* Recognizing occurrences of a given subterm in a term: [subst_term c t]
+   substitutes [(Rel 1)] for all occurrences of term [c] in a term [t] *)
 
 let subst_term_gen eq_fun c t =
   let rec substrec (k,c as kc) t =
@@ -638,8 +636,8 @@ let subst_term_gen eq_fun c t =
   in
   substrec (1,c) t
 
-(* Recognizing occurrences of a given (closed) subterm in a term :
-   [replace_term c1 c2 t] substitutes [c2] for all occurrences of (closed)
+(* Recognizing occurrences of a given subterm in a term :
+   [replace_term c1 c2 t] substitutes [c2] for all occurrences of
    term [c1] in a term [t] *)
 (*i Meme remarque : a priori [c] n'est pas forcement clos i*)
 
@@ -689,64 +687,88 @@ 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 =
+exception NotUnifiable
+
+let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) 
+    match_fun merge_fun substs occ 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 =
+    with NotUnifiable -> error_cannot_unify_occurrences !pos plocs in
+  let rec substrec k t =
     if nowhere_except_in & !pos > maxocc then t else
     try
-      let subst = unify_fun c t in
+      let subst = match_fun t in
       let r = if is_selected !pos plocs then (add_subst subst; mkRel k) else t
       in incr pos; r
     with _ ->
-      map_constr_with_binders_left_to_right
-	(fun d (k,c) -> (k+1,lift 1 c))
-        substrec kc t
+      map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
   in
-  let t' = substrec (1,c) t in
+  let t' = substrec 1 t in
   (!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
+let is_nowhere (nowhere_except_in,locs) = nowhere_except_in && locs = [] 
+
+let check_used_occurrences nbocc (nowhere_except_in,locs) =
+  let rest = List.filter (fun o -> o >= nbocc) locs in
+  if rest <> [] then error_invalid_occurrence rest
+
+let proceed_with_occurrences f plocs x =
+  if is_nowhere plocs then (* optimization *) x else
+  begin
+    assert (List.for_all (fun x -> x >= 0) (snd plocs));
+    let (nbocc,x) = f 1 x in
+    check_used_occurrences nbocc plocs;
+    x
+  end
+
+let subst_closed_term_occ_gen plocs pos c t =
+  let (_,pos,t) = subst_closed_term_occ_gen_modulo plocs 
+    (fun c' -> if eq_constr c c' then () else raise Exit)
+    (fun () () -> ()) () pos 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
-  else
-    let (nbocc,t') = subst_term_occ_gen plocs 1 c t in
-    let rest = List.filter (fun o -> o >= nbocc) locs in
-    if rest <> [] then error_invalid_occurrence rest;
-    t'
+let subst_closed_term_occ plocs c t =
+  proceed_with_occurrences (fun occ -> subst_closed_term_occ_gen plocs occ c)
+    plocs t
 
 type hyp_location_flag = (* To distinguish body and type of local defs *)
   | InHyp
   | InHypTypeOnly
   | InHypValueOnly
 
-let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,typ as d) =
-  match bodyopt,hloc with
-  | None, InHypValueOnly -> errorlabstrm "" (pr_id id ++ str " has no value")
-  | None, _ -> (id,None,subst_term_occ plocs c typ)
-  | Some body, InHypTypeOnly -> (id,Some body,subst_term_occ plocs c typ)
-  | Some body, InHypValueOnly -> (id,Some (subst_term_occ plocs c body),typ)
+let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
+  match bodyopt,hyploc with
+  | None, InHypValueOnly ->
+      errorlabstrm "" (pr_id id ++ str " has no value.")
+  | None, _ | Some _, InHypTypeOnly ->
+      let acc,typ = f acc typ in acc,(id,bodyopt,typ)
+  | Some body, InHypValueOnly ->
+      let acc,body = f acc body in acc,(id,Some body,typ)
   | Some body, InHyp ->
-	if locs = [] then
-	  if nowhere_except_in then d
-	  else (id,Some (subst_term c body),subst_term c typ)
-	else
-	  let (nbocc,body') = subst_term_occ_gen plocs 1 c body in
-	  let (nbocc',t') = subst_term_occ_gen plocs nbocc c typ in
-	  let rest = List.filter (fun o -> o >= nbocc') locs in
-	  if rest <> [] then error_invalid_occurrence rest;
-	  (id,Some body',t')
+      let acc,body = f acc body in
+      let acc,typ = f acc typ in
+      acc,(id,Some body,typ)
+
+let subst_closed_term_occ_decl (plocs,hyploc) c d =
+  proceed_with_occurrences
+    (map_named_declaration_with_hyploc
+       (fun occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d
+
+let subst_closed_term_occ_decl_modulo (plocs,hyploc)
+    match_fun merge_fun substs d =
+  let subst = ref substs in
+  proceed_with_occurrences
+    (map_named_declaration_with_hyploc
+        (fun occ t ->
+          let (substs,occ,t) =
+            subst_closed_term_occ_gen_modulo plocs
+              match_fun merge_fun !subst occ t
+          in subst := substs; (occ,t))
+        hyploc)
+    plocs d
 
 let vars_of_env env =
   let s =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index c74551735..2e202bf07 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -148,34 +148,43 @@ type occurrences = bool * int list
 val all_occurrences : occurrences
 val no_occurrences_in_set : occurrences
 
-(** [subst_term_occ_gen occl n c d] replaces occurrences of [c] at
+(** [subst_closed_term_occ_gen occl n c d] replaces occurrences of closed [c] at
    positions [occl], counting from [n], by [Rel 1] in [d] *)
-val subst_term_occ_gen :
+val subst_closed_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_closed_term_occ_gen_modulo] looks for subterm modulo a
+    testing function returning a substitution of type ['a] (or failing
+    with NotUnifiable); a function for merging substitution (possibly
+    failing with NotUnifiable) and an initial substitution are
+    required too *)
 
-(** [subst_term_occ occl c d] replaces occurrences of [c] at
+exception NotUnifiable
+
+val subst_closed_term_occ_gen_modulo :
+  occurrences -> (constr -> 'a) -> ('a -> 'a -> 'a) -> 'a ->
+  int -> constr -> 'a * int * types
+
+(** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at
    positions [occl] by [Rel 1] in [d] (see also Note OCC) *)
-val subst_term_occ : occurrences -> constr -> constr -> constr
+val subst_closed_term_occ : occurrences -> constr -> constr -> constr
 
-(** [subst_term_occ_decl occl c decl] replaces occurrences of [c] at
-   positions [occl] by [Rel 1] in [decl] *)
+(** [subst_closed_term_occ_decl occl c decl] replaces occurrences of closed [c]
+   at positions [occl] by [Rel 1] in [decl] *)
 
 type hyp_location_flag = (** To distinguish body and type of local defs *)
   | InHyp
   | InHypTypeOnly
   | InHypValueOnly
 
-val subst_term_occ_decl :
+val subst_closed_term_occ_decl :
   occurrences * hyp_location_flag -> constr -> named_declaration ->
       named_declaration
 
+val subst_closed_term_occ_decl_modulo :
+  occurrences * hyp_location_flag -> (constr -> 'a) -> ('a -> 'a -> 'a) -> 'a ->
+  named_declaration -> named_declaration
+
 val error_invalid_occurrence : int list -> 'a
 
 (** Alternative term equalities *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4610c06ce..4a873f1f9 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,7 +49,7 @@ let abstract_scheme env c l lname_typ =
    are unclear...
        if occur_meta ta then error "cannot find a type for the generalisation"
        else *) if occur_meta a then mkLambda_name env (na,ta,t)
-       else mkLambda_name env (na,ta,subst_term_occ locc a t))
+       else mkLambda_name env (na,ta,subst_closed_term_occ locc a t))
     c
     (List.rev l)
     lname_typ