aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml5
-rw-r--r--plugins/extraction/g_extraction.ml410
-rw-r--r--plugins/firstorder/g_ground.ml46
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/indfun.ml13
-rw-r--r--plugins/funind/merge.ml6
-rw-r--r--plugins/funind/recdef.ml28
-rw-r--r--plugins/ltac/profile_ltac.ml8
-rw-r--r--plugins/ltac/profile_ltac.mli33
-rw-r--r--plugins/ltac/rewrite.ml11
-rw-r--r--plugins/ltac/tacinterp.ml6
-rw-r--r--plugins/ssr/ssrequality.ml6
12 files changed, 87 insertions, 47 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index fb65a8639..c8c4c2dad 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -38,9 +38,8 @@ let start_deriving f suchthat lemma =
let f_type = EConstr.Unsafe.to_constr f_type in
let ef = EConstr.Unsafe.to_constr ef in
let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
- let evdref = ref sigma in
- let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
- TCons ( env' , !evdref , suchthat , (fun sigma _ ->
+ let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in
+ TCons ( env' , sigma , suchthat , (fun sigma _ ->
TNil sigma))))))
in
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 23452febd..24c70bccf 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -42,14 +42,20 @@ ARGUMENT EXTEND int_or_id
END
let pr_language = function
- | Ocaml -> str "Ocaml"
+ | Ocaml -> str "OCaml"
| Haskell -> str "Haskell"
| Scheme -> str "Scheme"
| JSON -> str "JSON"
+let warn_deprecated_ocaml_spelling =
+ CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated"
+ (fun () ->
+ strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+
VERNAC ARGUMENT EXTEND language
PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
+| [ "OCaml" ] -> [ Ocaml ]
| [ "Haskell" ] -> [ Haskell ]
| [ "Scheme" ] -> [ Scheme ]
| [ "JSON" ] -> [ JSON ]
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 938bec25b..b81010c7b 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -40,17 +40,17 @@ let _=
in
declare_int_option gdopt
-let congruence_depth=ref 100
let _=
+ let congruence_depth=ref 100 in
let gdopt=
- { optdepr=false;
+ { optdepr=true; (* noop *)
optname="Congruence Depth";
optkey=["Congruence";"Depth"];
optread=(fun ()->Some !congruence_depth);
optwrite=
(function
- None->congruence_depth:=0
+ None->congruence_depth:=0
| Some i->congruence_depth:=(max i 0))}
in
declare_int_option gdopt
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fa4353630..889c064b2 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1497,7 +1497,7 @@ let do_build_inductive
let _time2 = System.get_time () in
try
with_full_print
- (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
+ (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
Decl_kinds.Finite
with
| UserError(s,msg) as e ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9e22ad306..071599d9c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -158,8 +158,8 @@ let build_newrecursive
(fun (env,impls) (((_,recname),_),bl,arityc,_) ->
let arityc = Constrexpr_ops.mkCProdN bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
- let evdref = ref (Evd.from_env env0) in
- let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
+ let evd = Evd.from_env env0 in
+ let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
let open Context.Named.Declaration in
(Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
@@ -406,7 +406,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
match fixpoint_exprl with
| [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
- Command.do_definition
+ ComDefinition.do_definition
+ ~program_mode:false
fname
(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
@@ -426,7 +427,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
in
evd,List.rev rev_pconstants
| _ ->
- Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+ ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
(fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
@@ -616,8 +617,8 @@ and rebuild_nal aux bk bl' nal typ =
let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
- let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
+ let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
+ let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
let constr_expr_typel =
with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 9e2774ff3..9fcb35f89 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
} in *)
let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
- let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,pl,impls = Command.interp_mutual_inductive indl []
+ let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in
+ let mie,pl,impls = ComInductive.interp_mutual_inductive indl []
false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
- ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
+ ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls)
(* Find infos on identifier id. *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 766adfc63..363ad5dfc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1427,7 +1427,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
- let evmap, env = Pfedit.get_current_context () in
+ let evd, env = Pfedit.get_current_context () in
Lemmas.start_proof thm_name
(Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
@@ -1479,13 +1479,13 @@ let (com_eqn : int -> Id.t ->
| ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
- let evmap, env = Pfedit.get_current_context () in
- let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
+ let evd, env = Pfedit.get_current_context () in
+ let evd = Evd.from_ctx (Evd.evar_universe_context evd) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(Lemmas.start_proof eq_name (Global, false, Proof Lemma)
~sign:(Environ.named_context_val env)
- evmap
+ evd
(EConstr.of_constr equation_lemma_type)
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (by
@@ -1528,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let open Constr in
let open CVars in
let env = Global.env() in
- let evd = ref (Evd.from_env env) in
- let function_type = interp_type_evars env evd type_of_f in
+ let evd = Evd.from_env env in
+ let evd, function_type = interp_type_evars env evd type_of_f in
let function_type = EConstr.Unsafe.to_constr function_type in
let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
- let ty = interp_type_evars env evd ~impls:rec_impls eq in
+ let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
let ty = EConstr.Unsafe.to_constr ty in
- let evm, nf = Evarutil.nf_evars_and_universes !evd in
+ let evd, nf = Evarutil.nf_evars_and_universes evd in
let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in
let function_type = nf function_type in
let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
@@ -1560,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
- let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in
+ let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in
declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
in
(* Refresh the global universes, now including those of _F *)
- let evm = Evd.from_env (Global.env ()) in
+ let evd = Evd.from_env (Global.env ()) in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
let relation, evuctx =
- interp_constr env_with_pre_rec_args evm r
+ interp_constr env_with_pre_rec_args evd r
in
- let evm = Evd.from_ctx evuctx in
+ let evd = Evd.from_ctx evuctx in
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
@@ -1599,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
and functional_ref = destConst (constr_of_global functional_ref)
and eq_ref = destConst (constr_of_global eq_ref) in
generate_induction_principle f_ref tcc_lemma_constr
- functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
+ functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation);
Flags.if_verbose
msgnl (h 1 (Ppconstr.pr_id function_name ++
spc () ++ str"is defined" )++ fnl () ++
@@ -1618,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- evm (Lemmas.mk_hook hook))
+ evd (Lemmas.mk_hook hook))
()
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 5225420dc..5e3b7cf77 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -289,7 +289,7 @@ let rec find_in_stack what acc = function
| { name } as x :: rest when String.equal name what -> Some(acc, x, rest)
| { name } as x :: rest -> find_in_stack what (x :: acc) rest
-let exit_tactic start_time c =
+let exit_tactic ~count_call start_time c =
let diff = time () -. start_time in
match Local.(!stack) with
| [] | [_] ->
@@ -304,7 +304,7 @@ let exit_tactic start_time c =
let node = { node with
total = node.total +. diff;
local = node.local +. diff;
- ncalls = node.ncalls + 1;
+ ncalls = node.ncalls + (if count_call then 1 else 0);
max_total = max node.max_total diff;
} in
(* updating the stack *)
@@ -341,7 +341,7 @@ let tclFINALLY tac (finally : unit Proofview.tactic) =
(fun v -> finally <*> Proofview.tclUNIT v)
(fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
-let do_profile s call_trace tac =
+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
@@ -359,7 +359,7 @@ let do_profile s call_trace tac =
tac
(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
(match call_trace with
- | (_, c) :: _ -> exit_tactic start_time c
+ | (_, c) :: _ -> exit_tactic ~count_call start_time c
| [] -> ()))))
| None -> tac
diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli
index 52827cb36..feb777352 100644
--- a/plugins/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
@@ -9,9 +9,39 @@
(** Ltac profiling primitives *)
+(* Note(JasonGross): Ltac semantics are a bit insane. There isn't
+ really a good notion of how many times a tactic has been "called",
+ because tactics can be partially evaluated, and it's unclear
+ whether the number of "calls" should be the number of times the
+ body is fetched and unfolded, or the number of times the code is
+ executed to a value, etc. The logic in [Tacinterp.eval_tactic]
+ gives a decent approximation, which I believe roughly corresponds
+ to the number of times that the engine runs the tactic value which
+ results from evaluating the tactic expression bound to the name
+ we're considering. However, this is a poor approximation of the
+ time spent in the tactic; we want to consider time spent evaluating
+ a tactic expression to a tactic value to be time spent in the
+ expression, not just time spent in the caller of the expression.
+ So we need to wrap some nodes in additional profiling calls which
+ don't count towards to total call count. Whether or not a call
+ "counts" is indicated by the [count_call] boolean argument.
+
+ Unfortunately, at present, we can get very strange call graphs when
+ a named tactic expression never runs as a tactic value: if we have
+ [Ltac t0 := t.] and [Ltac t1 := t0.], then [t1] is considered to
+ run 0(!) times. It evaluates to [t] during tactic expression
+ evaluation, and although the call trace records the fact that it
+ was called by [t0] which was called by [t1], the tactic running
+ phase never sees this. Thus we get one call tree (from expression
+ evaluation) that has [t1] calls [t0] calls [t], and another call
+ tree which says that the caller of [t1] calls [t] directly; the
+ expression evaluation time goes in the first tree, and the call
+ count and tactic running time goes in the second tree. Alas, I
+ suspect that fixing this requires a redesign of how the profiler
+ hooks into the tactic engine. *)
val do_profile :
string -> ('a * Tacexpr.ltac_call_kind) list ->
- 'b Proofview.tactic -> 'b Proofview.tactic
+ ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic
val set_profiling : bool -> unit
@@ -46,4 +76,3 @@ type treenode = {
(* Returns the profiling results known by the current process *)
val get_local_profiling_results : unit -> treenode
val feedback_results : treenode -> unit
-
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2e14243d8..a698b05dd 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1781,7 +1781,9 @@ let declare_an_instance n s args =
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
- new_instance (Flags.is_universe_polymorphism ())
+ let program_mode = Flags.is_program_mode () in
+ let poly = Flags.is_universe_polymorphism () in
+ new_instance ~program_mode poly
binders instance (Some (true, CAst.make @@ CRecord (fields)))
~global ~generalize:false ~refine:false Hints.empty_hint_info
@@ -2012,9 +2014,10 @@ let add_morphism glob binders m s n =
[cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
- ignore(new_instance ~global:glob poly binders instance
- (Some (true, CAst.make @@ CRecord []))
- ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
+ let program_mode = Flags.is_program_mode () in
+ ignore(new_instance ~program_mode ~global:glob poly binders instance
+ (Some (true, CAst.make @@ CRecord []))
+ ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
(** Bind to "rewrite" too *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ded902a8f..179952f28 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1272,7 +1272,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let extra = TacStore.set extra f_trace trace in
let ist = { lfun = Id.Map.empty; extra = extra; } in
let appl = GlbAppl[r,[]] in
- val_interp ~appl ist (Tacenv.interp_ltac r)
+ Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
+ (val_interp ~appl ist (Tacenv.interp_ltac r))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1338,7 +1339,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
let ist = {
lfun = newlfun;
extra = TacStore.set ist.extra f_trace []; } in
- catch_error_tac trace (val_interp ist body) >>= fun v ->
+ Profile_ltac.do_profile "interp_app" trace ~count_call:false
+ (catch_error_tac trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index bd9633afb..6032ed2af 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -143,14 +143,14 @@ let newssrcongrtac arg ist gl =
(** Coq rewrite compatibility flag *)
-let ssr_strict_match = ref false
let _ =
- Goptions.declare_bool_option
+ let ssr_strict_match = ref false in
+ Goptions.declare_bool_option
{ Goptions.optname = "strict redex matching";
Goptions.optkey = ["Match"; "Strict"];
Goptions.optread = (fun () -> !ssr_strict_match);
- Goptions.optdepr = false;
+ Goptions.optdepr = true; (* noop *)
Goptions.optwrite = (fun b -> ssr_strict_match := b) }
(** Rewrite rules *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 17:04:44 +0000