aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/ground.ml12
-rw-r--r--plugins/funind/functional_principles_proofs.ml5
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/ltac/rewrite.ml10
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacentries.mli2
-rw-r--r--plugins/ssr/ssrbwd.ml3
-rw-r--r--plugins/ssr/ssrcommon.ml77
-rw-r--r--plugins/ssr/ssrcommon.mli9
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--plugins/ssr/ssrequality.ml13
-rw-r--r--plugins/ssrmatching/ssrmatching.ml91
-rw-r--r--plugins/ssrmatching/ssrmatching.mli8
13 files changed, 21 insertions, 215 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 516b04ea21..6a80525200 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,16 +18,16 @@ open Tacticals.New
open Globnames
let update_flags ()=
- let f acc coe =
- match coe.Classops.coe_value with
- | ConstRef c -> Names.Cpred.add c acc
- | _ -> acc
+ let open TransparentState in
+ let f accu coe = match coe.Classops.coe_value with
+ | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
+ | _ -> accu
in
- let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in
+ let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
red_flags:=
CClosure.RedFlags.red_add_transparent
CClosure.betaiotazeta
- (Names.Id.Pred.full,Names.Cpred.complement pred)
+ flags
let ground_tac solver startseq =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 651895aa08..ef1d1af199 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -131,8 +131,7 @@ let finish_proof dynamic_infos g =
g
-let refine c =
- Tacmach.refine c
+let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)
let thin l = Proofview.V82.of_tactic (Tactics.clear l)
@@ -1487,7 +1486,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
Eauto.eauto_with_bases
(true,5)
[(fun _ sigma -> (sigma, Lazy.force refl_equal))]
- [Hints.Hint_db.empty empty_transparent_state false]
+ [Hints.Hint_db.empty TransparentState.empty false]
)
)
)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 63a3e0582d..6e5e3f9353 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1359,7 +1359,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
Eauto.eauto_with_bases
(true,5)
[(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
- [Hints.Hint_db.empty empty_transparent_state false]
+ [Hints.Hint_db.empty TransparentState.empty false]
]
)
)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 16cb75ea2f..fee469032c 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -528,7 +528,7 @@ let decompose_applied_relation env sigma (c,l) =
let rewrite_db = "rewrite"
-let conv_transparent_state = (Id.Pred.empty, Cpred.full)
+let conv_transparent_state = TransparentState.cst_full
let rewrite_transparent_state () =
Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)
@@ -537,8 +537,8 @@ let rewrite_core_unif_flags = {
Unification.modulo_conv_on_closed_terms = None;
Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
- Unification.modulo_delta = empty_transparent_state;
- Unification.modulo_delta_types = full_transparent_state;
+ Unification.modulo_delta = TransparentState.empty;
+ Unification.modulo_delta_types = TransparentState.full;
Unification.check_applied_meta_types = true;
Unification.use_pattern_unification = true;
Unification.use_meta_bound_pattern_unification = true;
@@ -585,12 +585,12 @@ let general_rewrite_unif_flags () =
Unification.modulo_conv_on_closed_terms = Some ts;
Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
Unification.modulo_delta = ts;
- Unification.modulo_delta_types = full_transparent_state;
+ Unification.modulo_delta_types = TransparentState.full;
Unification.modulo_betaiota = true }
in {
Unification.core_unify_flags = core_flags;
Unification.merge_unify_flags = core_flags;
- Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = empty_transparent_state };
+ Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TransparentState.empty };
Unification.allow_K_in_toplevel_higher_order_unification = true;
Unification.resolve_evars = true
}
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 188d5de7de..ac2d88dec2 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -697,7 +697,7 @@ type ('b, 'c) argument_interp =
| ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp
| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
| ArgInterpLegacy :
- (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+ (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
type ('a, 'b, 'c) tactic_argument = {
arg_parsing : 'a Vernacextend.argument_rule;
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 79f9e093fb..309db539d0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -125,7 +125,7 @@ type ('b, 'c) argument_interp =
| ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp
| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
| ArgInterpLegacy :
- (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+ (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
type ('a, 'b, 'c) tactic_argument = {
arg_parsing : 'a Vernacextend.argument_rule;
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 1c4508abf4..3e0fbc9a8c 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -104,8 +104,6 @@ let mkRAppView ist gl rv gv =
let nb_view_imps = interp_view_nbimps ist gl rv in
mkRApp rv (mkRHoles (abs nb_view_imps))
-let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";;
-
let refine_interp_apply_view dbl ist gl gv =
let pair i = List.map (fun x -> i, x) in
let rv = pf_intern_term ist gl gv in
@@ -113,7 +111,6 @@ let refine_interp_apply_view dbl ist gl gv =
let interp_with (dbl, hint) =
let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in
interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
- let interp_with x = prof_apply_interp_with.profile interp_with x in
let rec loop = function
| [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
| h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 80d421b9fc..0a781ea8a9 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1000,7 +1000,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
| _ -> assert false
in loop sigma t [] n in
pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
- Tacmach.refine_no_check t gl
+ Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl
let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in
@@ -1017,81 +1017,6 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
with e when CErrors.noncritical e -> raise dependent_apply_error
-(** Profiling *)(* {{{ *************************************************************)
-type profiler = {
- profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
- reset : unit -> unit;
- print : unit -> unit }
-let profile_now = ref false
-let something_profiled = ref false
-let profilers = ref []
-let add_profiler f = profilers := f :: !profilers;;
-let _ =
- Goptions.declare_bool_option
- { Goptions.optname = "ssreflect profiling";
- Goptions.optkey = ["SsrProfiling"];
- Goptions.optread = (fun _ -> !profile_now);
- Goptions.optdepr = false;
- Goptions.optwrite = (fun b ->
- Ssrmatching.profile b;
- profile_now := b;
- if b then List.iter (fun f -> f.reset ()) !profilers;
- if not b then List.iter (fun f -> f.print ()) !profilers) }
-let () =
- let prof_total =
- let init = ref 0.0 in {
- profile = (fun f x -> assert false);
- reset = (fun () -> init := Unix.gettimeofday ());
- print = (fun () -> if !something_profiled then
- prerr_endline
- (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
- "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in
- let prof_legenda = {
- profile = (fun f x -> assert false);
- reset = (fun () -> ());
- print = (fun () -> if !something_profiled then begin
- prerr_endline
- (Printf.sprintf "!! %39s ---------- --------- --------- ---------"
- (String.make 39 '-'));
- prerr_endline
- (Printf.sprintf "!! %-39s %10s %9s %9s %9s"
- "function" "#calls" "total" "max" "average") end) } in
- add_profiler prof_legenda;
- add_profiler prof_total
-;;
-
-let mk_profiler s =
- let total, calls, max = ref 0.0, ref 0, ref 0.0 in
- let reset () = total := 0.0; calls := 0; max := 0.0 in
- let profile f x =
- if not !profile_now then f x else
- let before = Unix.gettimeofday () in
- try
- incr calls;
- let res = f x in
- let after = Unix.gettimeofday () in
- let delta = after -. before in
- total := !total +. delta;
- if delta > !max then max := delta;
- res
- with exc ->
- let after = Unix.gettimeofday () in
- let delta = after -. before in
- total := !total +. delta;
- if delta > !max then max := delta;
- raise exc in
- let print () =
- if !calls <> 0 then begin
- something_profiled := true;
- prerr_endline
- (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
- s !calls !total !max (!total /. (float_of_int !calls))) end in
- let prof = { profile = profile; reset = reset; print = print } in
- add_profiler prof;
- prof
-;;
-(* }}} *)
-
(* We wipe out all the keywords generated by the grammar rules we defined. *)
(* The user is supposed to Require Import ssreflect or Require ssreflect *)
(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index cf4e4b354e..e25c93bf0a 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -164,7 +164,7 @@ val mk_lterm : constr_expr -> ssrterm
val mk_ast_closure_term :
[ `None | `Parens | `DoubleParens | `At ] ->
Constrexpr.constr_expr -> ast_closure_term
-val interp_ast_closure_term : Geninterp.interp_sign -> Proof_type.goal
+val interp_ast_closure_term : Geninterp.interp_sign -> Goal.goal
Evd.sigma -> ast_closure_term -> Evd.evar_map * ast_closure_term
val subst_ast_closure_term : Mod_subst.substitution -> ast_closure_term -> ast_closure_term
val glob_ast_closure_term : Genintern.glob_sign -> ast_closure_term -> ast_closure_term
@@ -378,13 +378,6 @@ val pf_interp_gen_aux :
val is_name_in_ipats :
Id.t -> ssripats -> bool
-type profiler = {
- profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
- reset : unit -> unit;
- print : unit -> unit }
-
-val mk_profiler : string -> profiler
-
(** Basic tactics *)
val introid : ?orig:Name.t ref -> Id.t -> v82tac
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index d09b81593e..1bd88ae3dd 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -398,7 +398,7 @@ let revtoptac n0 gl =
let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in
let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
- refine (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])) gl
+ Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl
let equality_inj l b id c gl =
let msg = ref "" in
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 2a69e3f23a..22475fef34 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -425,11 +425,6 @@ let rwcltac cl rdx dir sr gl =
in
tclTHEN cvtac' rwtac gl
-let prof_rwcltac = mk_profiler "rwrxtac.rwcltac";;
-let rwcltac cl rdx dir sr gl =
- prof_rwcltac.profile (rwcltac cl rdx dir sr) gl
-;;
-
[@@@ocaml.warning "-3"]
let lz_coq_prod =
@@ -455,8 +450,6 @@ let ssr_is_setoid env =
Rewrite.is_applied_rewrite_relation env
sigma [] (EConstr.mkApp (r, args)) <> None
-let prof_rwxrtac_find_rule = mk_profiler "rwrxtac.find_rule";;
-
let closed0_check cl p gl =
if closed0 cl then
errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env (pf_env gl) (project gl) p)
@@ -556,7 +549,6 @@ let rwrxtac occ rdx_pat dir rule gl =
d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r)
with _ -> rwtac rs in
rwtac rules in
- let find_rule rdx = prof_rwxrtac_find_rule.profile find_rule rdx in
let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
let find_R, conclude = match rdx_pat with
| Some (_, (In_T _ | In_X_In_T _)) | None ->
@@ -582,11 +574,6 @@ let rwrxtac occ rdx_pat dir rule gl =
rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
;;
-let prof_rwxrtac = mk_profiler "rwrxtac";;
-let rwrxtac occ rdx_pat dir rule gl =
- prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl
-;;
-
let ssrinstancesofrule ist dir arg gl =
let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
let rule = interp_term ist gl arg in
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 142d1ac790..8cb0a8b463 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -174,82 +174,6 @@ let nf_evar sigma c =
(* }}} *)
-(** Profiling *)(* {{{ *************************************************************)
-type profiler = {
- profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
- reset : unit -> unit;
- print : unit -> unit }
-let profile_now = ref false
-let something_profiled = ref false
-let profilers = ref []
-let add_profiler f = profilers := f :: !profilers;;
-let profile b =
- profile_now := b;
- if b then List.iter (fun f -> f.reset ()) !profilers;
- if not b then List.iter (fun f -> f.print ()) !profilers
-;;
-let _ =
- Goptions.declare_bool_option
- { Goptions.optname = "ssrmatching profiling";
- Goptions.optkey = ["SsrMatchingProfiling"];
- Goptions.optread = (fun _ -> !profile_now);
- Goptions.optdepr = false;
- Goptions.optwrite = profile }
-let () =
- let prof_total =
- let init = ref 0.0 in {
- profile = (fun f x -> assert false);
- reset = (fun () -> init := Unix.gettimeofday ());
- print = (fun () -> if !something_profiled then
- prerr_endline
- (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
- "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in
- let prof_legenda = {
- profile = (fun f x -> assert false);
- reset = (fun () -> ());
- print = (fun () -> if !something_profiled then begin
- prerr_endline
- (Printf.sprintf "!! %39s ---------- --------- --------- ---------"
- (String.make 39 '-'));
- prerr_endline
- (Printf.sprintf "!! %-39s %10s %9s %9s %9s"
- "function" "#calls" "total" "max" "average") end) } in
- add_profiler prof_legenda;
- add_profiler prof_total
-;;
-
-let mk_profiler s =
- let total, calls, max = ref 0.0, ref 0, ref 0.0 in
- let reset () = total := 0.0; calls := 0; max := 0.0 in
- let profile f x =
- if not !profile_now then f x else
- let before = Unix.gettimeofday () in
- try
- incr calls;
- let res = f x in
- let after = Unix.gettimeofday () in
- let delta = after -. before in
- total := !total +. delta;
- if delta > !max then max := delta;
- res
- with exc ->
- let after = Unix.gettimeofday () in
- let delta = after -. before in
- total := !total +. delta;
- if delta > !max then max := delta;
- raise exc in
- let print () =
- if !calls <> 0 then begin
- something_profiled := true;
- prerr_endline
- (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
- s !calls !total !max (!total /. (float_of_int !calls))) end in
- let prof = { profile = profile; reset = reset; print = print } in
- add_profiler prof;
- prof
-;;
-(* }}} *)
-
exception NoProgress
(** Unification procedures. *)
@@ -286,11 +210,6 @@ let unif_EQ_args env sigma pa a =
let rec loop i = (i = n) || unif_EQ env sigma pa.(i) a.(i) && loop (i + 1) in
loop 0
-let prof_unif_eq_args = mk_profiler "unif_EQ_args";;
-let unif_EQ_args env sigma pa a =
- prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a
-;;
-
let unif_HO env ise p c =
try Evarconv.the_conv_x env p c ise
with Evarconv.UnableToUnify(ise, err) ->
@@ -650,11 +569,6 @@ let match_upats_FO upats env sigma0 ise orig_c =
iter_constr_LR loop f; Array.iter loop a in
try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO.")
-let prof_FO = mk_profiler "match_upats_FO";;
-let match_upats_FO upats env sigma0 ise c =
- prof_FO.profile (match_upats_FO upats env sigma0) ise c
-;;
-
let match_upats_HO ~on_instance upats env sigma0 ise c =
let dont_impact_evars = dont_impact_evars_in c in
@@ -706,11 +620,6 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
if !it_did_match then raise NoProgress;
!failed_because_of_TC
-let prof_HO = mk_profiler "match_upats_HO";;
-let match_upats_HO ~on_instance upats env sigma0 ise c =
- prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c
-;;
-
let fixed_upat evd = function
| {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index b3ddb52e85..93a8c48435 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -221,10 +221,6 @@ val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
(* One can also "Set SsrMatchingDebug" from a .v *)
val debug : bool -> unit
-(* One should delimit a snippet with "Set SsrMatchingProfiling" and
- * "Unset SsrMatchingProfiling" to get timings *)
-val profile : bool -> unit
-
val ssrinstancesof : cpattern -> Tacmach.tactic
(** Functions used for grammar extensions. Do not use. *)
@@ -234,7 +230,7 @@ sig
val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type
val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern
val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern
- val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern
+ val interp_rpattern : Geninterp.interp_sign -> Goal.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern
val pr_rpattern : rpattern -> Pp.t
val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern
val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
@@ -242,7 +238,7 @@ sig
val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern
val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern
- val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern
+ val interp_ssrterm : Geninterp.interp_sign -> Goal.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern
val pr_ssrterm : cpattern -> Pp.t
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:10:32 +0000