Merge PR #13907: Algorithmically faster algorithm for term replacing.

Reviewed-by: SkySkimmer

4 files changed, 78 insertions, 58 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 4dc584cfa8..d60aa69ccb 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -979,69 +979,52 @@ 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 c' = collapse_appl sigma c and 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
+  let t' = collapse_appl sigma t 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 c' (mkApp (f2, Array.sub cl2 0 l1)) then
-          Some (mkApp (mkRel k, 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 c' = collapse_appl sigma c and 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 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
-
-(* 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 open Vars in
-  let rec substrec (k,c as kc) t =
-    match prefix_application sigma eq_fun kc t with
-      | Some x -> x
-      | None ->
-    if eq_fun sigma c t then mkRel k
-    else
-      EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
+let eq_upto_lift cache c 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
-  substrec (1,c) t
-
-let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t
+  EConstr.eq_constr sigma 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 rec substrec (k,c as kc) t =
-    match my_prefix_application sigma eq_fun kc by_c t with
-      | Some x -> x
+let replace_term_gen sigma eq_fun ar by_c in_t =
+  let rec substrec k t =
+    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 c t then (EConstr.Vars.lift k by_c) else
-      EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c))
-        substrec kc t)
+    (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,c) in_t
+  substrec 0 in_t
+
+let replace_term sigma c byc t =
+  let cache = ref Int.Map.empty in
+  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 replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c 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 12df61e4c8..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 -> 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 -> 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 cbf12ac22f..67bf8d0d29 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2796,7 +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 newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in
+  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
+    decompose_prod_n_assum sigma i (replace_term_gen sigma eq arity (mkRel 1) 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
diff --git a/test-suite/bugs/closed/bug_13896.v b/test-suite/bugs/closed/bug_13896.v
new file mode 100644
index 0000000000..10f24d8564
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13896.v
@@ -0,0 +1,24 @@
+Inductive type : Set :=
+    Tptr : type -> type
+  | Tref : type -> type
+  | Trv_ref : type -> type
+  | Tint : type -> type -> type
+  | Tvoid : type
+  | Tarray : type -> type -> type
+  | Tnamed : type -> type
+  | Tfunction : type -> type -> type -> type
+  | Tbool : type
+  | Tmember_pointer : type -> type -> type
+  | Tfloat : type -> type
+  | Tqualified : type -> type -> type
+  | Tnullptr : type
+  | Tarch : type -> type -> type
+.
+Definition type_eq_dec : forall (ty1 ty2 : type), { ty1 = ty2 } + { ty1 <> ty2 }.
+Proof. fix IHty1 1.  decide equality. Defined.
+
+Goal (if type_eq_dec (Tptr Tvoid) (Tptr Tvoid) then True else False).
+Proof.
+timeout 1 cbn.
+constructor.
+Qed.