aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/dune (renamed from plugins/ltac/plugin_base.dune)2
-rw-r--r--plugins/ltac/extratactics.mlg22
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg18
-rw-r--r--plugins/ltac/leminv.ml297
-rw-r--r--plugins/ltac/leminv.mli21
-rw-r--r--plugins/ltac/ltac_plugin.mlpack1
-rw-r--r--plugins/ltac/profile_ltac.ml108
-rw-r--r--plugins/ltac/rewrite.ml61
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacenv.ml2
-rw-r--r--plugins/ltac/tacinterp.ml10
-rw-r--r--plugins/ltac/tactic_option.ml11
13 files changed, 438 insertions, 119 deletions
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/dune
index 5611f5ba16..6558ecbfe8 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/dune
@@ -11,3 +11,5 @@
(synopsis "Coq's tauto tactic")
(modules tauto)
(libraries coq.plugins.ltac))
+
+(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 9b80cbd803..0bad3cbe5b 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -47,7 +47,7 @@ DECLARE PLUGIN "ltac_plugin"
let with_delayed_uconstr ist c tac =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -312,7 +312,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
if poly then ctx
else (* This is a global universe context that shouldn't be
refreshed at every use of the hint, declare it globally. *)
- (Declare.declare_universe_context ~poly:false ctx;
+ (DeclareUctx.declare_universe_context ~poly:false ctx;
Univ.ContextSet.empty)
in
CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
@@ -345,8 +345,8 @@ open EConstr
open Vars
let constr_flags () = {
- Pretyping.use_typeclasses = true;
- Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
+ Pretyping.use_typeclasses = Pretyping.UseTC;
+ Pretyping.solve_unification_constraints = Proof.use_unification_heuristics ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
Pretyping.program_mode = false;
@@ -375,22 +375,22 @@ let refine_tac ist simple with_classes c =
TACTIC EXTEND refine
| [ "refine" uconstr(c) ] ->
- { refine_tac ist false true c }
+ { refine_tac ist false Pretyping.UseTC c }
END
TACTIC EXTEND simple_refine
| [ "simple" "refine" uconstr(c) ] ->
- { refine_tac ist true true c }
+ { refine_tac ist true Pretyping.UseTC c }
END
TACTIC EXTEND notcs_refine
| [ "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist false false c }
+ { refine_tac ist false Pretyping.NoUseTC c }
END
TACTIC EXTEND notcs_simple_refine
| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist true false c }
+ { refine_tac ist true Pretyping.NoUseTC c }
END
(* Solve unification constraints using heuristics or fail if any remain *)
@@ -918,7 +918,7 @@ END
VERNAC COMMAND EXTEND GrabEvars STATE proof
| [ "Grab" "Existential" "Variables" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+ -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
END
(* Shelves all the goals under focus. *)
@@ -950,7 +950,7 @@ END
VERNAC COMMAND EXTEND Unshelve STATE proof
| [ "Unshelve" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.unshelve p) pstate }
+ -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.unshelve p) pstate }
END
(* Gives up on the goals under focus: the goals are considered solved,
@@ -1102,7 +1102,7 @@ END
VERNAC COMMAND EXTEND OptimizeProof
| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
- { fun ~pstate -> Proof_global.compact_the_proof pstate }
+ { fun ~pstate -> Declare.Proof.compact pstate }
| [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
{ Gc.compact () }
END
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3c30c881fb..b4527694ae 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -53,7 +53,7 @@ END
let eval_uconstrs ist cs =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 50c3ed1248..5baa23b3e9 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
hint:
[ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
tac = Pltac.tactic ->
- { Hints.HintsExtern (n,c, in_tac tac) } ] ]
+ { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
;
operconstr: LEVEL "0"
[ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
@@ -359,23 +359,17 @@ open Vernacextend
open Goptions
open Libnames
-let print_info_trace = ref None
-
-let () = declare_int_option {
- optdepr = false;
- optkey = ["Info" ; "Level"];
- optread = (fun () -> !print_info_trace);
- optwrite = fun n -> print_info_trace := n;
-}
+let print_info_trace =
+ declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
- let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
+ let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p ->
let with_end_tac = if b then Some etac else None in
let global = match n with SelectAll | SelectList _ -> true | _ -> false in
- let info = Option.append info !print_info_trace in
+ let info = Option.append info (print_info_trace ()) in
let (p,status) =
- Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+ Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
in
(* in case a strict subtree was completed,
go back to the top of the prooftree *)
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
new file mode 100644
index 0000000000..5a8ec404ee
--- /dev/null
+++ b/plugins/ltac/leminv.ml
@@ -0,0 +1,297 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Termops
+open Environ
+open Constr
+open Context
+open EConstr
+open Vars
+open Namegen
+open Evd
+open Printer
+open Reductionops
+open Inductiveops
+open Tacmach.New
+open Clenv
+open Tacticals.New
+open Tactics
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
+
+let no_inductive_inconstr env sigma constr =
+ (str "Cannot recognize an inductive predicate in " ++
+ pr_leconstr_env env sigma constr ++
+ str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
+ spc () ++ str "or of the type of constructors" ++ spc () ++
+ str "is hidden by constant definitions.")
+
+(* Inversion stored in lemmas *)
+
+(* ALGORITHM:
+
+ An inversion stored in a lemma is computed from a term-pattern, in
+ a signature, as follows:
+
+ Suppose we have an inductive relation, (I abar), in a signature Gamma:
+
+ Gamma |- (I abar)
+
+ Then we compute the free-variables of abar. Suppose that Gamma is
+ thinned out to only include these.
+
+ [We need technically to require that all free-variables of the
+ types of the free variables of abar are themselves free-variables
+ of abar. This needs to be checked, but it should not pose a
+ problem - it is hard to imagine cases where it would not hold.]
+
+ Now, we pose the goal:
+
+ (P:(Gamma)Prop)(Gamma)(I abar)->(P vars[Gamma]).
+
+ We execute the tactic:
+
+ REPEAT Intro THEN (OnLastHyp (Inv NONE false o outSOME))
+
+ This leaves us with some subgoals. All the assumptions after "P"
+ in these subgoals are new assumptions. I.e. if we have a subgoal,
+
+ P:(Gamma)Prop, Gamma, Hbar:Tbar |- (P ybar)
+
+ then the assumption we needed to have was
+
+ (Hbar:Tbar)(P ybar)
+
+ So we construct all the assumptions we need, and rebuild the goal
+ with these assumptions. Then, we can re-apply the same tactic as
+ above, but instead of stopping after the inversion, we just apply
+ the respective assumption in each subgoal.
+
+ *)
+
+(* returns the sub_signature of sign corresponding to those identifiers that
+ * are not global. *)
+(*
+let get_local_sign sign =
+ let lid = ids_of_sign sign in
+ let globsign = Global.named_context() in
+ let add_local id res_sign =
+ if not (mem_sign globsign id) then
+ add_sign (lookup_sign id sign) res_sign
+ else
+ res_sign
+ in
+ List.fold_right add_local lid nil_sign
+*)
+(* returns the identifier of lid that was the latest declared in sign.
+ * (i.e. is the identifier id of lid such that
+ * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) >
+ * for any id'<>id in lid).
+ * it returns both the pair (id,(sign_prefix id sign)) *)
+(*
+let max_prefix_sign lid sign =
+ let rec max_rec (resid,prefix) = function
+ | [] -> (resid,prefix)
+ | (id::l) ->
+ let pre = sign_prefix id sign in
+ if sign_length pre > sign_length prefix then
+ max_rec (id,pre) l
+ else
+ max_rec (resid,prefix) l
+ in
+ match lid with
+ | [] -> nil_sign
+ | id::l -> snd (max_rec (id, sign_prefix id sign) l)
+*)
+let rec add_prods_sign env sigma t =
+ match EConstr.kind sigma (whd_all env sigma t) with
+ | Prod (na,c1,b) ->
+ let id = id_of_name_using_hdchar env sigma t na.binder_name in
+ let b'= subst1 (mkVar id) b in
+ add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
+ | LetIn (na,c1,t1,b) ->
+ let id = id_of_name_using_hdchar env sigma t na.binder_name in
+ let b'= subst1 (mkVar id) b in
+ add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
+ | _ -> (env,t)
+
+(* [dep_option] indicates whether the inversion lemma is dependent or not.
+ If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
+ the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
+ where P:(x_bar:T_bar)(H:(I x_bar))[sort].
+ The generalisation of such a goal at the moment of the dependent case should
+ be easy.
+
+ If it is non dependent, then if [I]=(I t_bar) and (x_bar:T_bar) are the
+ variables occurring in [I], then the stated goal will be:
+ (x_bar:T_bar)(I t_bar)->(P x_bar)
+ where P: P:(x_bar:T_bar)[sort].
+*)
+
+let compute_first_inversion_scheme env sigma ind sort dep_option =
+ let indf,realargs = dest_ind_type ind in
+ let allvars = vars_of_env env in
+ let p = next_ident_away (Id.of_string "P") allvars in
+ let pty,goal =
+ if dep_option then
+ let pty = make_arity env sigma true indf sort in
+ let r = relevance_of_inductive_type env ind in
+ let goal =
+ mkProd
+ (make_annot Anonymous r, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
+ in
+ pty,goal
+ else
+ let i = mkAppliedInd ind in
+ let ivars = global_vars env sigma i in
+ let revargs,ownsign =
+ fold_named_context
+ (fun env d (revargs,hyps) ->
+ let d = map_named_decl EConstr.of_constr d in
+ let id = NamedDecl.get_id d in
+ if Id.List.mem id ivars then
+ ((mkVar id)::revargs, Context.Named.add d hyps)
+ else
+ (revargs,hyps))
+ env ~init:([],[])
+ in
+ let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
+ let goal = mkArrow i Sorts.Relevant (applist(mkVar p, List.rev revargs)) in
+ (pty,goal)
+ in
+ let npty = nf_all env sigma pty in
+ let extenv = push_named (LocalAssum (make_annot p Sorts.Relevant,npty)) env in
+ extenv, goal
+
+(* [inversion_scheme sign I]
+
+ Given a local signature, [sign], and an instance of an inductive
+ relation, [I], inversion_scheme will prove the associated inversion
+ scheme on sort [sort]. Depending on the value of [dep_option] it will
+ build a dependent lemma or a non-dependent one *)
+
+let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
+ let (env,i) = add_prods_sign env sigma t in
+ let ind =
+ try find_rectype env sigma i
+ with Not_found ->
+ user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
+ in
+ let (invEnv,invGoal) =
+ compute_first_inversion_scheme env sigma ind sort dep_option
+ in
+ assert
+ (List.subset
+ (global_vars env sigma invGoal)
+ (ids_of_named_context (named_context invEnv)));
+ (*
+ user_err ~hdr:"lemma_inversion"
+ (str"Computed inversion goal was not closed in initial signature.");
+ *)
+ let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
+ let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
+ let pfterm = List.hd (Proof.partial_proof pf) in
+ let global_named_context = Global.named_context_val () in
+ let ownSign = ref begin
+ fold_named_context
+ (fun env d sign ->
+ let d = map_named_decl EConstr.of_constr d in
+ if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
+ else Context.Named.add d sign)
+ invEnv ~init:Context.Named.empty
+ end in
+ let avoid = ref Id.Set.empty in
+ let Proof.{sigma} = Proof.data pf in
+ let sigma = Evd.minimize_universes sigma in
+ let rec fill_holes c =
+ match EConstr.kind sigma c with
+ | Evar (e,args) ->
+ let h = next_ident_away (Id.of_string "H") !avoid in
+ let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
+ avoid := Id.Set.add h !avoid;
+ ownSign := Context.Named.add (LocalAssum (make_annot h Sorts.Relevant,ty)) !ownSign;
+ applist (mkVar h, inst)
+ | _ -> EConstr.map sigma fill_holes c
+ in
+ let c = fill_holes pfterm in
+ (* warning: side-effect on ownSign *)
+ let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
+ let p = EConstr.to_constr sigma invProof in
+ p, sigma
+
+let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
+ let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
+ let univs = Evd.univ_entry ~poly sigma in
+ let entry = Declare.definition_entry ~univs invProof in
+ let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
+ ()
+
+(* inv_op = Inv (derives de complete inv. lemma)
+ * inv_op = InvNoThining (derives de semi inversion lemma) *)
+
+let add_inversion_lemma_exn ~poly na com comsort bool tac =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
+ let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
+ try
+ add_inversion_lemma ~poly na env sigma c sort bool tac
+ with
+ | UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
+ user_err ~hdr:"Inv needs Nodep Prop Set" s
+
+(* ================================= *)
+(* Applying a given inversion lemma *)
+(* ================================= *)
+
+let lemInv id c =
+ Proofview.Goal.enter begin fun gls ->
+ try
+ let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in
+ let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
+ Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
+ with
+ | NoSuchBinding ->
+ user_err
+ (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
+ | UserError (a,b) ->
+ user_err ~hdr:"LemInv"
+ (str "Cannot refine current goal with the lemma " ++
+ pr_leconstr_env (pf_env gls) (project gls) c)
+ end
+
+let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
+
+let lemInvIn id c ids =
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
+ let intros_replace_ids =
+ let concl = Proofview.Goal.concl gl in
+ let sigma = project gl in
+ let nb_of_new_hyp = nb_prod sigma concl - List.length ids in
+ if nb_of_new_hyp < 1 then
+ intros_replacing ids
+ else
+ (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
+ in
+ ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
+ (intros_replace_ids)))
+ end
+
+let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
+
+let lemInv_clause id c = function
+ | [] -> lemInv_gen id c
+ | l -> lemInvIn_gen id c l
diff --git a/plugins/ltac/leminv.mli b/plugins/ltac/leminv.mli
new file mode 100644
index 0000000000..5a5de7b58f
--- /dev/null
+++ b/plugins/ltac/leminv.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open EConstr
+open Constrexpr
+open Tactypes
+
+val lemInv_clause :
+ quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
+
+val add_inversion_lemma_exn : poly:bool ->
+ Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
+ unit
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index e83eab20dc..f31361279c 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -9,6 +9,7 @@ Tactic_debug
Tacintern
Profile_ltac
Tactic_matching
+Leminv
Tacinterp
Tacentries
Evar_tactics
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 14fab251d0..0dbf16a821 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -25,27 +25,20 @@ let is_profiling = Flags.profile_ltac
let set_profiling b = is_profiling := b
let get_profiling () = !is_profiling
-(** LtacProf cannot yet handle backtracking into multi-success tactics.
- To properly support this, we'd have to somehow recreate our location in the
- call-stack, and stop/restart the intervening timers. This is tricky and
- possibly expensive, so instead we currently just emit a warning that
- profiling results will be off. *)
-let encountered_multi_success_backtracking = ref false
-
-let warn_profile_backtracking =
- CWarnings.create ~name:"profile-backtracking" ~category:"ltac"
- (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \
- into multi-success tactics; profiling results may be wildly inaccurate.")
-
-let warn_encountered_multi_success_backtracking () =
- if !encountered_multi_success_backtracking then
- warn_profile_backtracking ()
-
-let encounter_multi_success_backtracking () =
- if not !encountered_multi_success_backtracking
+let encountered_invalid_stack_no_self = ref false
+
+let warn_invalid_stack_no_self =
+ CWarnings.create ~name:"profile-invalid-stack-no-self" ~category:"ltac"
+ (fun () -> strbrk
+ "Ltac Profiler encountered an invalid stack (no self \
+ node). This can happen if you reset the profile during \
+ tactic execution.")
+
+let encounter_invalid_stack_no_self () =
+ if not !encountered_invalid_stack_no_self
then begin
- encountered_multi_success_backtracking := true;
- warn_encountered_multi_success_backtracking ()
+ encountered_invalid_stack_no_self := true;
+ warn_invalid_stack_no_self ()
end
@@ -76,8 +69,7 @@ module Local = Summary.Local
let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root]
let reset_profile_tmp () =
- Local.(stack := [empty_treenode root]);
- encountered_multi_success_backtracking := false
+ Local.(stack := [empty_treenode root])
(* ************** XML Serialization ********************* *)
@@ -218,7 +210,6 @@ let to_string ~filter ?(cutoff=0.0) node =
cumulate tree;
!global
in
- warn_encountered_multi_success_backtracking ();
let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
let msg =
h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
@@ -296,13 +287,15 @@ let exit_tactic ~count_call start_time c =
match Local.(!stack) with
| [] | [_] ->
(* oops, our stack is invalid *)
- encounter_multi_success_backtracking ();
+ encounter_invalid_stack_no_self ();
reset_profile_tmp ()
| node :: (parent :: rest as full_stack) ->
let name = string_of_call c in
if not (String.equal name node.name) then
(* oops, our stack is invalid *)
- encounter_multi_success_backtracking ();
+ CErrors.anomaly
+ (Pp.strbrk "Ltac Profiler encountered an invalid stack (wrong self node) \
+ likely due to backtracking into multi-success tactics.");
let node = { node with
total = node.total +. diff;
local = node.local +. diff;
@@ -332,38 +325,56 @@ let exit_tactic ~count_call start_time c =
(* Calls are over, we reset the stack and send back data *)
if rest == [] && get_profiling () then begin
assert(String.equal root parent.name);
+ encountered_invalid_stack_no_self := false;
reset_profile_tmp ();
feedback_results parent
end
-let tclFINALLY tac (finally : unit Proofview.tactic) =
+(** [tclWRAPFINALLY before tac finally] runs [before] before each
+ entry-point of [tac] and passes the result of [before] to
+ [finally], which is then run at each exit-point of [tac],
+ regardless of whether it succeeds or fails. Said another way, if
+ [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
+ ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
+ [e], it behaves as [before >>= fun v -> finally v <*> tclZERO
+ e]. *)
+let rec tclWRAPFINALLY before tac finally =
+ let open Proofview in
let open Proofview.Notations in
- Proofview.tclIFCATCH
- tac
- (fun v -> finally <*> Proofview.tclUNIT v)
- (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
+ before >>= fun v -> tclCASE tac >>= function
+ | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
+ | Next (ret, tac') -> tclOR
+ (finally v >>= fun () -> tclUNIT ret)
+ (fun e -> tclWRAPFINALLY before (tac' e) finally)
let do_profile s call_trace ?(count_call=true) tac =
let open Proofview.Notations in
- Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
- if !is_profiling then
- match call_trace, Local.(!stack) with
- | (_, c) :: _, parent :: rest ->
- let name = string_of_call c in
- let node = get_child name parent in
- Local.(stack := node :: parent :: rest);
- Some (time ())
- | _ :: _, [] -> assert false
- | _ -> None
- else None)) >>= function
- | Some start_time ->
- tclFINALLY
- tac
+ (* We do an early check to [is_profiling] so that we save the
+ overhead of [tclWRAPFINALLY] when profiling is not set
+ *)
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function
+ | false -> tac
+ | true ->
+ tclWRAPFINALLY
(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
- (match call_trace with
- | (_, c) :: _ -> exit_tactic ~count_call start_time c
- | [] -> ()))))
- | None -> tac
+ if !is_profiling then
+ match call_trace, Local.(!stack) with
+ | (_, c) :: _, parent :: rest ->
+ let name = string_of_call c in
+ let node = get_child name parent in
+ Local.(stack := node :: parent :: rest);
+ Some (time ())
+ | _ :: _, [] -> assert false
+ | _ -> None
+ else None)))
+ tac
+ (function
+ | Some start_time ->
+ (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+ (match call_trace with
+ | (_, c) :: _ -> exit_tactic ~count_call start_time c
+ | [] -> ()))))
+ | None -> Proofview.tclUNIT ())
(* ************** Accumulation of data from workers ************************* *)
@@ -396,6 +407,7 @@ let _ =
| _ -> ()))
let reset_profile () =
+ encountered_invalid_stack_no_self := false;
reset_profile_tmp ();
data := SM.empty
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 321b05b97c..3834b21a14 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -639,7 +639,7 @@ let solve_remaining_by env sigma holes by =
let env = Environ.reset_with_named_context evi.evar_hyps env in
let ty = evi.evar_concl in
let name, poly = Id.of_string "rewrite", false in
- let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in
+ let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma ty solve_tac in
Evd.define evk (EConstr.of_constr c) sigma
in
List.fold_left solve sigma indep
@@ -952,10 +952,11 @@ let fold_match env sigma c =
then case_dep_scheme_kind_from_type
else case_scheme_kind_from_type)
in
- let exists = Ind_tables.check_scheme sk ci.ci_ind in
- if exists then
- dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind
- else raise Not_found
+ match Ind_tables.lookup_scheme sk ci.ci_ind with
+ | Some cst ->
+ dep, pred, true, cst
+ | None ->
+ raise Not_found
in
let app =
let ind, args = Inductiveops.find_mrectype env sigma cty in
@@ -1559,7 +1560,7 @@ let assert_replacing id newt tac =
if Id.equal n id then ev' else mkVar n
in
let (e, _) = destEvar sigma ev in
- (sigma, mkEvar (e, Array.map_of_list map nc))
+ (sigma, mkEvar (e, List.map map nc))
end
end in
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
@@ -1864,14 +1865,14 @@ let proper_projection env sigma r ty =
Array.append args [| instarg |]) in
it_mkLambda_or_LetIn app ctx
-let declare_projection n instance_id r =
+let declare_projection name instance_id r =
let poly = Global.is_polymorphic r in
let env = Global.env () in
let sigma = Evd.from_env env in
let sigma,c = Evd.fresh_global env sigma r in
let ty = Retyping.get_type_of env sigma c in
- let term = proper_projection env sigma c ty in
- let sigma, typ = Typing.type_of env sigma term in
+ let body = proper_projection env sigma c ty in
+ let sigma, typ = Typing.type_of env sigma body in
let ctx, typ = decompose_prod_assum sigma typ in
let typ =
let n =
@@ -1892,14 +1893,11 @@ let declare_projection n instance_id r =
let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ
in it_mkProd_or_LetIn ccl ctx
in
- let typ = it_mkProd_or_LetIn typ ctx in
- let univs = Evd.univ_entry ~poly sigma in
- let typ = EConstr.to_constr sigma typ in
- let term = EConstr.to_constr sigma term in
- let cst = Declare.definition_entry ~types:typ ~univs term in
- let _ : Constant.t =
- Declare.declare_constant ~name:n ~kind:Decls.(IsDefinition Definition)
- (Declare.DefinitionEntry cst)
+ let types = Some (it_mkProd_or_LetIn typ ctx) in
+ let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let impargs, udecl = [], UState.default_univ_decl in
+ let _r : GlobRef.t =
+ DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
in ()
let build_morphism_signature env sigma m =
@@ -1927,10 +1925,7 @@ let build_morphism_signature env sigma m =
in
let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
let evd = solve_constraints env !evd in
- let evd = Evd.minimize_universes evd in
- let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
- Pretyping.check_evars env evd (EConstr.of_constr m);
- Evd.evar_universe_context evd, m
+ evd, morph
let default_morphism sign m =
let env = Global.env () in
@@ -1965,22 +1960,24 @@ let add_morphism_as_parameter atts m n : unit =
let instance_id = add_suffix n "_Proper" in
let env = Global.env () in
let evd = Evd.from_env env in
- let uctx, instance = build_morphism_signature env evd m in
- let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
- let cst = Declare.declare_constant ~name:instance_id
- ~kind:Decls.(IsAssumption Logical)
- (Declare.ParameterEntry (None,(instance,uctx),None))
- in
- Classes.add_instance (Classes.mk_instance
- (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (GlobRef.ConstRef cst));
- declare_projection n instance_id (GlobRef.ConstRef cst)
+ let poly = atts.polymorphic in
+ let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let impargs, udecl = [], UState.default_univ_decl in
+ let evd, types = build_morphism_signature env evd m in
+ let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+ let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
+ let cst = GlobRef.ConstRef cst in
+ Classes.add_instance
+ (Classes.mk_instance
+ (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst);
+ declare_projection n instance_id cst
let add_morphism_interactive atts m n : Lemmas.t =
init_setoid ();
let instance_id = add_suffix n "_Proper" in
let env = Global.env () in
let evd = Evd.from_env env in
- let uctx, instance = build_morphism_signature env evd m in
+ let evd, morph = build_morphism_signature env evd m in
let poly = atts.polymorphic in
let kind = Decls.(IsDefinition Instance) in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -1996,7 +1993,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
let info = Lemmas.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
- let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4127d28bae..9910796d9c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -299,7 +299,7 @@ let classify_tactic_notation tacobj = Substitute tacobj
let inTacticGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "TacticGrammar") with
- open_function = open_tactic_notation;
+ open_function = simple_open open_tactic_notation;
load_function = load_tactic_notation;
cache_function = cache_tactic_notation;
subst_function = subst_tactic_notation;
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index ce9189792e..76d47f5482 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -182,7 +182,7 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
- open_function = open_md;
+ open_function = simple_open open_md;
subst_function = subst_md;
classify_function = classify_md}
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9e0b9d3254..dda7f0742c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -546,7 +546,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
(evd,c)
let constr_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = true;
expand_evars = true;
@@ -564,7 +564,7 @@ let interp_constr = interp_constr_gen WithoutTypeConstraint
let interp_type = interp_constr_gen IsType
let open_constr_use_classes_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -573,7 +573,7 @@ let open_constr_use_classes_flags () = {
}
let open_constr_no_classes_flags () = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -582,7 +582,7 @@ let open_constr_no_classes_flags () = {
}
let pure_open_constr_flags = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = false;
@@ -2070,7 +2070,7 @@ let _ =
*)
let name, poly = Id.of_string "ltac_gen", poly in
let name, poly = Id.of_string "ltac_gen", poly in
- let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
+ let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
(EConstr.of_constr c, sigma)
in
GlobEnv.register_constr_interp0 wit_tactic eval
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index c72a527537..922d2f7792 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -13,15 +13,11 @@ open Pp
let declare_tactic_option ?(default=Tacexpr.TacId []) name =
let locality = Summary.ref false ~name:(name^"-locality") in
- let default_tactic_expr : Tacexpr.glob_tactic_expr ref =
- Summary.ref default ~name:(name^"-default-tacexpr")
- in
let default_tactic : Tacexpr.glob_tactic_expr ref =
- Summary.ref !default_tactic_expr ~name:(name^"-default-tactic")
+ Summary.ref default ~name:(name^"-default-tactic")
in
let set_default_tactic local t =
locality := local;
- default_tactic_expr := t;
default_tactic := t
in
let cache (_, (local, tac)) = set_default_tactic local tac in
@@ -36,18 +32,17 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
{ (default_object name) with
cache_function = cache;
load_function = (fun _ -> load);
- open_function = (fun _ -> load);
+ open_function = simple_open (fun _ -> load);
classify_function = (fun (local, tac) ->
if local then Dispose else Substitute (local, tac));
subst_function = subst}
in
let put local tac =
- set_default_tactic local tac;
Lib.add_anonymous_leaf (input (local, tac))
in
let get () = !locality, Tacinterp.eval_tactic !default_tactic in
let print () =
- Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
+ Pptactic.pr_glob_tactic (Global.env ()) !default_tactic ++
(if !locality then str" (locally defined)" else str" (globally defined)")
in
put, get, print
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 19:24:07 +0000