From 93ea9206cbf29617feb23646f95e794b11e87793 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 6 Mar 2021 22:54:16 +0100 Subject: Algorithmically faster algorithm for term replacing. Instead of recomputing the n-th lifts of terms for every subterm under a context, we introduce a table storing the value of this lift across contexts. While not the most efficient algorithmically, it is still much more efficient in practice and does not exhibit the exponential behaviour of replacing under different subcontexts. In an ideal world we would have an equality function on terms that allows to compute equality up to lifts, which would prevent having to even compute the lift at all, but the current fix has the advantage to be self-contained and not require dangerous tweaking of an equality function which is already complex enough as it is. Fixes #13896: cbn very slow. --- engine/termops.ml | 58 ++++++++++++++++++++++++++++++++++-------------------- engine/termops.mli | 4 ++-- 2 files changed, 39 insertions(+), 23 deletions(-) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index 4dc584cfa8..2cfb33cef8 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -981,67 +981,83 @@ let collapse_appl sigma c = match EConstr.kind sigma c with let prefix_application sigma eq_fun (k,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 + 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 c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma (k, c) (mkApp (f2, Array.sub cl2 0 l1)) then + Some (mkApp (mkRel (k + 1), Array.sub cl2 l1 (l2 - l1))) else None | _ -> 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 + 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 c' (mkApp (f2, Array.sub cl2 0 l1)) then + && 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 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 + 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 open Vars in - let rec substrec (k,c as kc) t = - match prefix_application sigma eq_fun kc t with + 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 c t then mkRel k + if eq_fun sigma (k, c) t then mkRel (k + 1) else - EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t + EConstr.map_with_binders sigma succ substrec k t in - substrec (1,c) t + substrec 0 t -let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c 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 rec substrec (k,c as kc) t = - match my_prefix_application sigma eq_fun kc by_c t with + let c = collapse_appl sigma c in + let rec substrec k t = + match my_prefix_application sigma eq_fun (k, c) by_c t with | Some x -> x | 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, c) 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 = replace_term_gen sigma EConstr.eq_constr c byc 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 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..bfdb3fbc40 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -125,12 +125,12 @@ val pop : constr -> constr (** [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 + (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 *) val replace_term_gen : - Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) -> + Evd.evar_map -> (Evd.evar_map -> int * constr -> constr -> bool) -> constr -> constr -> constr -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) -- cgit v1.2.3 From 285419e99996354ad2056bc38725c7a592124e7c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 6 Mar 2021 23:32:45 +0100 Subject: 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. --- engine/termops.ml | 69 ++++++++++++++---------------------------------------- engine/termops.mli | 14 ++++------- 2 files changed, 23 insertions(+), 60 deletions(-) (limited to 'engine') 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 -- cgit v1.2.3