aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/termops.ml79
-rw-r--r--engine/termops.mli14
-rw-r--r--engine/uState.ml3
-rw-r--r--engine/univGen.ml10
-rw-r--r--engine/univGen.mli6
-rw-r--r--engine/univMinim.ml3
-rw-r--r--engine/univProblem.ml24
-rw-r--r--engine/univProblem.mli2
-rw-r--r--engine/univSubst.ml6
9 files changed, 41 insertions, 106 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/engine/uState.ml b/engine/uState.ml
index 20ea24dd87..81559778f2 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -296,9 +296,6 @@ let add_constraints uctx cstrs =
universes = UGraph.merge_constraints cstrs' uctx.universes;
weak_constraints = weak; }
-(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
-
let add_universe_constraints uctx cstrs =
let univs, local = uctx.local in
let vars, weak, local' = process_universe_constraints uctx cstrs in
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 278ca6bf34..b917d91512 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,14 +13,14 @@ open Names
open Constr
open Univ
-type univ_unique_id = int
(* Generator of levels *)
-let new_univ_id, set_remote_new_univ_id =
- RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
- ~build:(fun n -> n)
+let new_univ_id =
+ let cnt = ref 0 in
+ fun () -> incr cnt; !cnt
let new_univ_global () =
- Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
+ let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in
+ Univ.Level.UGlobal.make (Global.current_dirpath ()) s (new_univ_id ())
let fresh_level () =
Univ.Level.make (new_univ_global ())
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 05737411f5..743d819747 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -13,12 +13,6 @@ open Constr
open Environ
open Univ
-
-(** The global universe counter *)
-type univ_unique_id
-val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
-val new_univ_id : unit -> univ_unique_id (** for the stm *)
-
(** Side-effecting functions creating new universe levels. *)
val new_univ_global : unit -> Level.UGlobal.t
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 4ed6e97526..86bf2c9298 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -406,6 +406,3 @@ let normalize_context_set ~lbound g ctx us algs weak =
in
let us = normalize_opt_subst us in
(us, algs), (ctx', Constraint.union noneqs eqs)
-
-(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 8d6689933c..10ee601f3f 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Univ
-open UnivSubst
type t =
| ULe of Universe.t * Universe.t
@@ -22,24 +21,6 @@ let is_trivial = function
| ULe (u, v) | UEq (u, v) -> Universe.equal u v
| ULub (u, v) | UWeak (u, v) -> Level.equal u v
-let subst_univs fn = function
- | ULe (u, v) ->
- let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
- if Universe.equal u' v' then None
- else Some (ULe (u',v'))
- | UEq (u, v) ->
- let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
- if Universe.equal u' v' then None
- else Some (ULe (u',v'))
- | ULub (u, v) ->
- let u' = level_subst_of fn u and v' = level_subst_of fn v in
- if Level.equal u' v' then None
- else Some (ULub (u',v'))
- | UWeak (u, v) ->
- let u' = level_subst_of fn u and v' = level_subst_of fn v in
- if Level.equal u' v' then None
- else Some (UWeak (u',v'))
-
module Set = struct
module S = Set.Make(
struct
@@ -88,11 +69,6 @@ module Set = struct
let equal x y =
x == y || equal x y
-
- let subst_univs subst csts =
- fold
- (fun c -> Option.fold_right add (subst_univs subst c))
- csts empty
end
type 'a accumulator = Set.t -> 'a -> 'a option
diff --git a/engine/univProblem.mli b/engine/univProblem.mli
index 575f5ac847..6c7a11f529 100644
--- a/engine/univProblem.mli
+++ b/engine/univProblem.mli
@@ -32,8 +32,6 @@ module Set : sig
include Set.S with type elt = t
val pr : t -> Pp.t
-
- val subst_univs : universe_subst_fn -> t -> t
end
type 'a accumulator = Set.t -> 'a -> 'a option
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 330ed5d0ad..c76a4cd751 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -83,12 +83,6 @@ let subst_univs_constr subst c =
let f = Univ.make_subst subst in
subst_univs_fn_constr f c
-let subst_univs_constr =
- if Flags.profile then
- let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
- CProfile.profile2 subst_univs_constr_key subst_univs_constr
- else subst_univs_constr
-
let normalize_univ_variable ~find =
let rec aux cur =
let b = find cur in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 13:43:41 +0000