aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrbool.v2
-rw-r--r--plugins/ssr/ssrbwd.ml3
-rw-r--r--plugins/ssr/ssrcommon.ml100
-rw-r--r--plugins/ssr/ssrcommon.mli17
-rw-r--r--plugins/ssr/ssrelim.ml5
-rw-r--r--plugins/ssr/ssrequality.ml17
-rw-r--r--plugins/ssr/ssrfun.v2
-rw-r--r--plugins/ssr/ssrparser.mlg10
8 files changed, 43 insertions, 113 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index a618fc781f..3a7cf41d43 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -371,7 +371,7 @@ Ltac prop_congr := apply: prop_congr.
Lemma is_true_true : true. Proof. by []. Qed.
Lemma not_false_is_true : ~ false. Proof. by []. Qed.
Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
-Hint Resolve is_true_true not_false_is_true is_true_locked_true.
+Hint Resolve is_true_true not_false_is_true is_true_locked_true : core.
(** Shorter names. **)
Definition isT := is_true_true.
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 ebe4aac213..efc4a2c743 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -242,7 +242,6 @@ let interp_refine ist gl rc =
let flags = {
Pretyping.use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = None;
fail_evar = false;
expand_evars = true }
in
@@ -499,6 +498,22 @@ let pf_e_type_of gl t =
let sigma, ty = Typing.type_of env sigma t in
re_sig it sigma, ty
+let pf_resolve_typeclasses ~where ~fail gl =
+ let sigma, env, it = project gl, pf_env gl, sig_it gl in
+ let filter =
+ let evset = Evarutil.undefined_evars_of_term sigma where in
+ fun k _ -> Evar.Set.mem k evset in
+ let sigma = Typeclasses.resolve_typeclasses ~filter ~fail env sigma in
+ re_sig it sigma
+
+let resolve_typeclasses ~where ~fail env sigma =
+ let filter =
+ let evset = Evarutil.undefined_evars_of_term sigma where in
+ fun k _ -> Evar.Set.mem k evset in
+ let sigma = Typeclasses.resolve_typeclasses ~filter ~fail env sigma in
+ sigma
+
+
let nf_evar sigma t =
EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
@@ -844,7 +859,7 @@ let ssr_n_tac seed n gl =
with Not_found ->
if n = -1 then fail "The ssreflect library was not loaded"
else fail ("The tactic "^name^" was not found") in
- let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
+ let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
Proofview.V82.of_tactic (Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr)) gl
let donetac n gl = ssr_n_tac "done" n gl
@@ -985,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
@@ -1002,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 *)
@@ -1152,8 +1092,8 @@ let tclDO n tac =
let _, info = CErrors.push e in
let e' = CErrors.UserError (l, prefix i ++ s) in
Util.iraise (e', info)
- | Ploc.Exc(loc, CErrors.UserError (l, s)) ->
- raise (Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+ | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) ->
+ raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
let rec loop i gl =
if i = n then tac_err_at i gl else
(tclTHEN (tac_err_at i) (loop (i + 1))) gl in
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 566a933522..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
@@ -335,6 +335,14 @@ val refine_with :
?beta:bool ->
?with_evars:bool ->
evar_map * EConstr.t -> v82tac
+
+val pf_resolve_typeclasses :
+ where:EConstr.t ->
+ fail:bool -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma
+val resolve_typeclasses :
+ where:EConstr.t ->
+ fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map
+
(*********************** Wrapped Coq tactics *****************************)
val rewritetac : ssrdir -> EConstr.t -> tactic
@@ -370,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 5067d8af31..2c9ec3a7cf 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -353,6 +353,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
ppdebug(lazy Pp.(str"elim_pred_ty=" ++ pp_term gl pty));
let gl = pf_unify_HO gl pred elim_pred in
let elim = fire_subst gl elim in
+ let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in
let gl, _ = pf_e_type_of gl elim in
(* check that the patterns do not contain non instantiated dependent metas *)
let () =
@@ -397,13 +398,13 @@ 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
try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
with
- | Ploc.Exc(_,CErrors.UserError (_,s))
+ | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
| CErrors.UserError (_,s)
when msg := Pp.string_of_ppcmds s;
!msg = "Not a projectable equality but a discriminable one." ||
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 036b20bfcd..22475fef34 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -377,6 +377,10 @@ let is_construct_ref sigma c r =
let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
let rwcltac cl rdx dir sr gl =
+ let sr =
+ let sigma, r = sr in
+ let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in
+ sigma, r in
let n, r_n,_, ucst = pf_abs_evars gl sr in
let r_n' = pf_abs_cterm gl n r_n in
let r' = EConstr.Vars.subst_var pattern_id r_n' in
@@ -421,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 =
@@ -451,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)
@@ -552,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 ->
@@ -578,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/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index e2c0ed7c8b..6535cad8b7 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -398,7 +398,7 @@ End ExtensionalEquality.
Typeclasses Opaque eqfun.
Typeclasses Opaque eqrel.
-Hint Resolve frefl rrefl.
+Hint Resolve frefl rrefl : core.
Notation "f1 =1 f2" := (eqfun f1 f2)
(at level 70, no associativity) : fun_scope.
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 52240f5896..7c91860228 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1545,9 +1545,9 @@ let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
let swaptacarg (loc, b) = (b, []), Some (TacId [])
let check_seqtacarg dir arg = match snd arg, dir with
- | ((true, []), Some (TacAtom (loc, _))), L2R ->
+ | ((true, []), Some (TacAtom { CAst.loc })), L2R ->
CErrors.user_err ?loc (str "expected \"last\"")
- | ((false, []), Some (TacAtom (loc, _))), R2L ->
+ | ((false, []), Some (TacAtom { CAst.loc })), R2L ->
CErrors.user_err ?loc (str "expected \"first\"")
| _, _ -> arg
@@ -1677,7 +1677,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (*
| ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in
let tacname = ssrtac_name name in () *)
-let ssrtac_atom ?loc name args = TacML (Loc.tag ?loc (ssrtac_entry name 0, args))
+let ssrtac_atom ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name 0, args))
let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args
let tclintros_expr ?loc tac ipats =
@@ -1704,7 +1704,7 @@ END
GRAMMAR EXTEND Gram
GLOBAL: tactic_expr;
- ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { Loc.tag ~loc (Tacexp tac) } ]];
+ ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
END
@@ -1724,7 +1724,7 @@ let ssrautoprop gl =
let tacname =
try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
- let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
+ let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
with Not_found -> V82.of_tactic (Auto.full_trivial []) gl
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 12:13:41 +0000