aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mlg3
-rw-r--r--plugins/ssrmatching/plugin_base.dune1
-rw-r--r--plugins/ssrmatching/ssrmatching.ml101
-rw-r--r--plugins/ssrmatching/ssrmatching.mli10
4 files changed, 10 insertions, 105 deletions
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 3f0794fdd4..4ddaeb49fd 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -11,7 +11,6 @@
{
open Ltac_plugin
-open Pcoq
open Pcoq.Constr
open Ssrmatching
open Ssrmatching.Internal
@@ -69,7 +68,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" -> '('
| Tok.KEYWORD "@" -> '@'
| _ -> ' '
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
}
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune
index 1450a94de1..06f67c3774 100644
--- a/plugins/ssrmatching/plugin_base.dune
+++ b/plugins/ssrmatching/plugin_base.dune
@@ -2,5 +2,4 @@
(name ssrmatching_plugin)
(public_name coq.plugins.ssrmatching)
(synopsis "Coq ssrmatching plugin")
- (flags :standard -open Gramlib)
(libraries coq.plugins.ltac))
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index bb6decd848..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) ->
@@ -354,14 +273,16 @@ let nf_open_term sigma0 ise c =
let c' = nf c in let _ = Evd.fold copy_def sigma0 () in
!s', Evd.evar_universe_context s, EConstr.of_constr c'
-let unif_end env sigma0 ise0 pt ok =
+let unif_end ?(solve_TC=true) env sigma0 ise0 pt ok =
let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
let tcs = Evd.get_typeclass_evars ise in
let s, uc, t = nf_open_term sigma0 ise pt in
let ise1 = create_evar_defs s in
let ise1 = Evd.set_typeclass_evars ise1 (Evar.Set.filter (fun ev -> Evd.is_undefined ise1 ev) tcs) in
let ise1 = Evd.set_universe_context ise1 uc in
- let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in
+ let ise2 =
+ if solve_TC then Typeclasses.resolve_typeclasses ~fail:true env ise1
+ else ise1 in
if not (ok ise) then raise NoProgress else
if ise2 == ise1 then (s, uc, t)
else
@@ -370,7 +291,7 @@ let unif_end env sigma0 ise0 pt ok =
let unify_HO env sigma0 t1 t2 =
let sigma = unif_HO env sigma0 t1 t2 in
- let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in
+ let sigma, uc, _ = unif_end ~solve_TC:false env sigma0 sigma t2 (fun _ -> true) in
Evd.set_universe_context sigma uc
let pf_unify_HO gl t1 t2 =
@@ -648,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
@@ -704,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
@@ -1386,7 +1297,7 @@ let () =
let () = Tacenv.register_ml_tactic name [|mltac|] in
let tac =
TacFun ([Name (Id.of_string "pattern")],
- TacML (Loc.tag ({ mltac_name = name; mltac_index = 0 }, []))) in
+ TacML (CAst.make ({ mltac_name = name; mltac_index = 0 }, []))) in
let obj () =
Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
Mltop.declare_cache_obj obj "ssrmatching_plugin"
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index f478d48ea3..93a8c48435 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -201,7 +201,7 @@ val assert_done : 'a option ref -> 'a
(** Very low level APIs.
these are calls to evarconv's [the_conv_x] followed by
- [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
+ [solve_unif_constraints_with_heuristics].
In case of failure they raise [NoMatch] *)
val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map
@@ -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-01 19:00:13 +0000