Further simplification of the term replacing code.

We factorize the code for replace and subst, since it seems there is no
reason to keep them separate, not even performance. Some static invariants are
made explicit in the API.

3 files changed, 39 insertions, 70 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 2cfb33cef8..d60aa69ccb 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -979,35 +979,21 @@ let collapse_appl sigma c = match EConstr.kind sigma c with
 
 (* First utilities for avoiding telescope computation for subst_term *)
 
-let prefix_application sigma eq_fun (k,c) t =
+let prefix_application sigma eq_fun k l1 t =
   let open EConstr in
   let t' = collapse_appl sigma t in
-  match EConstr.kind sigma c, EConstr.kind sigma t' with
-    | App (f1,cl1), App (f2,cl2) ->
-        let l1 = Array.length cl1
-        and l2 = Array.length cl2 in
+  if 0 < l1 then match EConstr.kind sigma t' with
+    | App (f2,cl2) ->
+        let l2 = Array.length cl2 in
         if l1 <= l2
-           && eq_fun sigma (k, c) (mkApp (f2, Array.sub cl2 0 l1)) then
-          Some (mkApp (mkRel (k + 1), Array.sub cl2 l1 (l2 - l1)))
+           && eq_fun sigma k (mkApp (f2, Array.sub cl2 0 l1)) then
+          Some (Array.sub cl2 l1 (l2 - l1))
         else
           None
     | _ -> None
+  else None
 
-let my_prefix_application sigma eq_fun (k,c) by_c t =
-  let open EConstr in
-  let t' = collapse_appl sigma t in
-  match EConstr.kind sigma c, EConstr.kind sigma t' with
-    | App (f1,cl1), App (f2,cl2) ->
-        let l1 = Array.length cl1
-        and l2 = Array.length cl2 in
-        if l1 <= l2
-           && eq_fun sigma (k, c) (mkApp (f2, Array.sub cl2 0 l1)) then
-          Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
-        else
-          None
-    | _ -> None
-
-let eq_upto_lift cache sigma (k, c) t =
+let eq_upto_lift cache c sigma k t =
   let c =
     try Int.Map.find k !cache
     with Not_found ->
@@ -1017,47 +1003,28 @@ let eq_upto_lift cache sigma (k, c) t =
   in
   EConstr.eq_constr sigma c t
 
-(* 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];
-   works if [c] has rels *)
-
-let subst_term_gen sigma eq_fun c t =
-  let open EConstr in
-  let c = collapse_appl sigma c in
-  let rec substrec k t =
-    match prefix_application sigma eq_fun (k, c) t with
-      | Some x -> x
-      | None ->
-    if eq_fun sigma (k, c) t then mkRel (k + 1)
-    else
-      EConstr.map_with_binders sigma succ substrec k t
-  in
-  substrec 0 t
-
-let subst_term sigma c t =
-  let cache = ref Int.Map.empty in
-  let eq sigma kc t = eq_upto_lift cache sigma kc t in
-  subst_term_gen sigma eq c t
-
 (* 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]; works if [c1] and [c2] have rels *)
 
-let replace_term_gen sigma eq_fun c by_c in_t =
-  let c = collapse_appl sigma c in
+let replace_term_gen sigma eq_fun ar by_c in_t =
   let rec substrec k t =
-    match my_prefix_application sigma eq_fun (k, c) by_c t with
-      | Some x -> x
+    match prefix_application sigma eq_fun k ar t with
+      | Some args -> EConstr.mkApp (EConstr.Vars.lift k by_c, args)
       | None ->
-    (if eq_fun sigma (k, c) t then (EConstr.Vars.lift k by_c) else
+    (if eq_fun sigma k t then (EConstr.Vars.lift k by_c) else
       EConstr.map_with_binders sigma succ substrec k t)
   in
   substrec 0 in_t
 
 let replace_term sigma c byc t =
   let cache = ref Int.Map.empty in
-  let eq sigma kc t = eq_upto_lift cache sigma kc t in
-  replace_term_gen sigma eq c byc t
+  let c = collapse_appl sigma c in
+  let ar = Array.length (snd (decompose_app_vect sigma c)) in
+  let eq sigma k t = eq_upto_lift cache c sigma k t in
+  replace_term_gen sigma eq ar byc t
+
+let subst_term sigma c t = replace_term sigma c (EConstr.mkRel 1) t
 
 let vars_of_env env =
   let s = Environ.ids_of_named_context_val (Environ.named_context_val env) in
diff --git a/engine/termops.mli b/engine/termops.mli
index bfdb3fbc40..bdde2c450d 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -122,16 +122,12 @@ val pop : constr -> constr
 (** Substitution of an arbitrary large term. Uses equality modulo
    reduction of let *)
 
-(** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq]
-   as equality *)
-val subst_term_gen : Evd.evar_map ->
-  (Evd.evar_map -> int * constr -> constr -> bool) -> constr -> constr -> constr
-
-(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
-   as equality *)
+(** [replace_term_gen eq arity e c] replaces matching subterms according to
+    [eq] by [e] in [c]. If [arity] is non-zero applications of larger length
+    are handled atomically. *)
 val replace_term_gen :
-  Evd.evar_map -> (Evd.evar_map -> int * constr -> constr -> bool) ->
-    constr -> constr -> constr -> constr
+  Evd.evar_map -> (Evd.evar_map -> int -> constr -> bool) ->
+    int -> constr -> constr -> constr
 
 (** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
 val subst_term : Evd.evar_map -> constr -> constr -> constr
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3c7f8c55d7..67bf8d0d29 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2796,18 +2796,24 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let open Context.Rel.Declaration in
   let decls,cl = decompose_prod_n_assum sigma i cl in
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
-  let cache = ref Int.Map.empty in
-  let eq sigma (k, c) t =
-    let c =
-      try Int.Map.find k !cache
-      with Not_found ->
-        let c = EConstr.Vars.lift k c in
-        let () = cache := Int.Map.add k c !cache in
-        c
+  let newdecls,_ =
+    let c = Termops.collapse_appl sigma c in
+    let arity = Array.length (snd (Termops.decompose_app_vect sigma c)) in
+    let cache = ref Int.Map.empty in
+    let eq sigma k t =
+      let c =
+        try Int.Map.find k !cache
+        with Not_found ->
+          let c = EConstr.Vars.lift k c in
+          let () = cache := Int.Map.add k c !cache in
+          c
+      in
+      (* We use a nounivs equality because generalize morally takes a pattern as
+         argument, so we have to ignore freshly generated sorts. *)
+      EConstr.eq_constr_nounivs sigma c t
     in
-    EConstr.eq_constr_nounivs sigma c t
+    decompose_prod_n_assum sigma i (replace_term_gen sigma eq arity (mkRel 1) dummy_prod)
   in
-  let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma eq c dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name env sigma c t ids cl' na in
   let r = Retyping.relevance_of_type env sigma t in