diff options
| author | Théo Zimmermann | 2020-04-01 16:54:37 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-06 15:30:08 +0200 |
| commit | 5c5fbf68034fdd18ddfcd19c9c8b1438af6b5c92 (patch) | |
| tree | 32313fbf73082cff3da3832b0ff709c192ec28b7 | |
| parent | 2089207415565e8a28816f53b61d9292d04f4c59 (diff) | |
Clean and fix definitions of options.
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
41 files changed, 524 insertions, 717 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 370f35f6ed..c4472050f8 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -219,22 +219,22 @@ let get_mangle_names = ~key:["Mangle";"Names"] ~value:false -let mangle_names_prefix = ref (Id.of_string "_0") - -let set_prefix x = mangle_names_prefix := forget_subscript x - -let () = Goptions.( - declare_string_option - { optdepr = false; - optkey = ["Mangle";"Names";"Prefix"]; - optread = (fun () -> Id.to_string !mangle_names_prefix); - optwrite = begin fun x -> - set_prefix - (try Id.of_string x - with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) - end }) - -let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id +let mangle_names_prefix = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Mangle";"Names";"Prefix"] + ~value:(Id.of_string "_0") + (fun x -> + (try + Id.of_string x + with + | CErrors.UserError _ -> + CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\".")) + ) |> forget_subscript + ) + (fun x -> Id.to_string x) + +let mangle_id id = if get_mangle_names () then mangle_names_prefix () else id (* Looks for next "good" name by lifting subscript *) diff --git a/engine/uState.ml b/engine/uState.ml index d532129dc5..ff85f09efa 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -176,8 +176,11 @@ let instantiate_variable l b v = exception UniversesDiffer -let drop_weak_constraints = ref false - +let drop_weak_constraints = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Cumulativity";"Weak";"Constraints"] + ~value:false let process_universe_constraints ctx cstrs = let open UnivSubst in @@ -270,7 +273,7 @@ let process_universe_constraints ctx cstrs = | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local | UWeak (l, r) -> - if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local + if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local | UEq (l, r) -> equalize_universes l r local in let local = diff --git a/engine/uState.mli b/engine/uState.mli index 3959373ead..cd1c9a174e 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -69,8 +69,6 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry (** {5 Constraints handling} *) -val drop_weak_constraints : bool ref - val add_constraints : t -> Univ.Constraint.t -> t (** @raise UniversesDiffer when universes differ diff --git a/kernel/environ.ml b/kernel/environ.ml index 2d2c9a454b..de8692ff21 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -128,7 +128,7 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; - env_sprop_allowed = false; + env_sprop_allowed = true; env_universes_lbound = Univ.Level.set; env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; diff --git a/library/goptions.ml b/library/goptions.ml index 75eef5b411..73132868d7 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -296,6 +296,48 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) + +type 'a opt_decl = depr:bool -> key:option_name -> 'a + +let declare_int_option_and_ref ~depr ~key ~(value:int) = + let r_opt = ref value in + let optwrite v = r_opt := Option.default value v in + let optread () = Some !r_opt in + let _ = declare_int_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + fun () -> !r_opt + +let declare_intopt_option_and_ref ~depr ~key = + let r_opt = ref None in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_int_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + optread + +let declare_nat_option_and_ref ~depr ~key ~(value:int) = + assert (value >= 0); + let r_opt = ref value in + let optwrite v = + let v = Option.default value v in + if v < 0 then + CErrors.user_err Pp.(str "This option expects a non-negative value."); + r_opt := v + in + let optread () = Some !r_opt in + let _ = declare_int_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + fun () -> !r_opt + let declare_bool_option_and_ref ~depr ~key ~(value:bool) = let r_opt = ref value in let optwrite v = r_opt := v in @@ -307,6 +349,39 @@ let declare_bool_option_and_ref ~depr ~key ~(value:bool) = } in optread +let declare_string_option_and_ref ~depr ~key ~(value:string) = + let r_opt = ref value in + let optwrite v = r_opt := Option.default value v in + let optread () = Some !r_opt in + let _ = declare_stringopt_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + fun () -> !r_opt + +let declare_stringopt_option_and_ref ~depr ~key = + let r_opt = ref None in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_stringopt_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + optread + +let declare_interpreted_string_option_and_ref ~depr ~key ~(value:'a) from_string to_string = + let r_opt = ref value in + let optwrite v = r_opt := Option.default value @@ Option.map from_string v in + let optread () = Some (to_string !r_opt) in + let _ = declare_stringopt_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + fun () -> !r_opt + (* 3- User accessible commands *) (* Setting values of options *) diff --git a/library/goptions.mli b/library/goptions.mli index 8fcc258d47..336cae420c 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -104,9 +104,15 @@ end (** {6 Options. } *) -(** These types and function are for declaring a new option of name [key] - and access functions [read] and [write]; the parameter [name] is the option name - used when printing the option value (command "Print Toto Titi." *) +(** These types and function are for declaring a new option of name + [key] and access functions [read] and [write]; the parameter [name] + is the option name used when printing the option value (command + "Print Toto Titi." + + The declare_*_option functions are low-level, to be used when + implementing complex option workflows, e.g. when setting one option + changes the value of another. For most use cases, you should use + the helper functions declare_*_option_and_ref. *) type 'a option_sig = { optdepr : bool; @@ -118,7 +124,11 @@ type 'a option_sig = { } (** The [preprocess] function is triggered before setting the option. It can be - used to emit a warning on certain values, and clean-up the final value. *) + used to emit a warning on certain values, and clean-up the final value. + + [declare_stringopt_option] should be preferred to [declare_string_option] + because it supports "Unset". + Only "Warnings" option is declared using the latter.*) val declare_int_option : ?preprocess:(int option -> int option) -> int option option_sig -> unit @@ -129,9 +139,18 @@ val declare_string_option: ?preprocess:(string -> string) -> val declare_stringopt_option: ?preprocess:(string option -> string option) -> string option option_sig -> unit -(** Helper to declare a reference controlled by an option. Read-only +(** Helpers to declare a reference controlled by an option. Read-only as to avoid races. *) -val declare_bool_option_and_ref : depr:bool -> key:option_name -> value:bool -> (unit -> bool) +type 'a opt_decl = depr:bool -> key:option_name -> 'a + +val declare_int_option_and_ref : (value:int -> (unit -> int)) opt_decl +val declare_intopt_option_and_ref : (unit -> int option) opt_decl +val declare_nat_option_and_ref : (value:int -> (unit -> int)) opt_decl +val declare_bool_option_and_ref : (value:bool -> (unit -> bool)) opt_decl +val declare_string_option_and_ref : (value:string -> (unit -> string)) opt_decl +val declare_stringopt_option_and_ref : (unit -> string option) opt_decl +val declare_interpreted_string_option_and_ref : + (value:'a -> (string -> 'a) -> ('a -> string) -> (unit -> 'a)) opt_decl (** {6 Special functions supposed to be used only in vernacentries.ml } *) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 74043d6bc8..6f5c910297 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -25,19 +25,14 @@ open Util let init_size=5 -let cc_verbose=ref false +let cc_verbose= + declare_bool_option_and_ref + ~depr:false + ~key:["Congruence";"Verbose"] + ~value:false let debug x = - if !cc_verbose then Feedback.msg_debug (x ()) - -let () = - let gdopt= - { optdepr=false; - optkey=["Congruence";"Verbose"]; - optread=(fun ()-> !cc_verbose); - optwrite=(fun b -> cc_verbose := b)} - in - declare_bool_option gdopt + if cc_verbose () then Feedback.msg_debug (x ()) (* Signature table *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a53c2395f0..f8449bcda1 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -498,16 +498,8 @@ let info_file f = (* The objects defined below should survive an arbitrary time, so we register them to coq save/undo mechanism. *) -let my_bool_option name initval = - let flag = ref initval in - let access = fun () -> !flag in - let () = declare_bool_option - {optdepr = false; - optkey = ["Extraction"; name]; - optread = access; - optwrite = (:=) flag } - in - access +let my_bool_option name value = + declare_bool_option_and_ref ~depr:false ~key:["Extraction"; name] ~value (*s Extraction AccessOpaque *) @@ -588,25 +580,18 @@ let () = declare_int_option (* This option controls whether "dummy lambda" are removed when a toplevel constant is defined. *) -let conservative_types_ref = ref false -let conservative_types () = !conservative_types_ref - -let () = declare_bool_option - {optdepr = false; - optkey = ["Extraction"; "Conservative"; "Types"]; - optread = (fun () -> !conservative_types_ref); - optwrite = (fun b -> conservative_types_ref := b) } - +let conservative_types = + declare_bool_option_and_ref + ~depr:false + ~key:["Extraction"; "Conservative"; "Types"] + ~value:false (* Allows to print a comment at the beginning of the output files *) -let file_comment_ref = ref "" -let file_comment () = !file_comment_ref - -let () = declare_string_option - {optdepr = false; - optkey = ["Extraction"; "File"; "Comment"]; - optread = (fun () -> !file_comment_ref); - optwrite = (fun s -> file_comment_ref := s) } +let file_comment = + declare_string_option_and_ref + ~depr:false + ~key:["Extraction"; "File"; "Comment"] + ~value:"" (*s Extraction Lang *) diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 49e4c91182..6ddc6ba21e 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -31,20 +31,8 @@ DECLARE PLUGIN "ground_plugin" { -let ground_depth=ref 3 - -let ()= - let gdopt= - { optdepr=false; - optkey=["Firstorder";"Depth"]; - optread=(fun ()->Some !ground_depth); - optwrite= - (function - None->ground_depth:=3 - | Some i->ground_depth:=(max i 0))} - in - declare_int_option gdopt - +let ground_depth = + declare_nat_option_and_ref ~depr:false ~key:["Firstorder";"Depth"] ~value:3 let default_intuition_tac = let tac _ _ = Auto.h_auto None [] (Some []) in @@ -85,7 +73,7 @@ let gen_ground_tac flag taco ids bases = | None-> snd (default_solver ()) in let startseq k = Proofview.Goal.enter begin fun gl -> - let seq=empty_seq !ground_depth in + let seq=empty_seq (ground_depth ()) in let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in let seq, sigma = extend_with_auto_hints (pf_env gl) sigma bases seq in tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7d87fc0220..ec23355ce1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -107,9 +107,9 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in - let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in + let old_printallowmatchdefaultclause = Detyping.print_allow_match_default_clause () in Constrextern.print_universes := true; - Detyping.print_allow_match_default_clause := false; + Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -122,7 +122,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; - Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; + Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -132,7 +132,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; - Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; + Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise @@ -309,33 +309,18 @@ let add_Function is_general f = let pr_table env sigma = pr_table env sigma !from_function (*********************************) (* Debugging *) -let functional_induction_rewrite_dependent_proofs = ref true -let function_debug = ref false -open Goptions -let functional_induction_rewrite_dependent_proofs_sig = - { - optdepr = false; - optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; - optread = (fun () -> !functional_induction_rewrite_dependent_proofs); - optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) - } -let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig +let do_rewrite_dependent = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Functional";"Induction";"Rewrite";"Dependent"] + ~value:true -let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true - -let function_debug_sig = - { - optdepr = false; - optkey = ["Function_debug"]; - optread = (fun () -> !function_debug); - optwrite = (fun b -> function_debug := b) - } - -let () = declare_bool_option function_debug_sig - - -let do_observe () = !function_debug +let do_observe = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Function_debug"] + ~value:false let observe strm = if do_observe () @@ -405,18 +390,11 @@ let observe_tac ~header s tac = end -let strict_tcc = ref false -let is_strict_tcc () = !strict_tcc -let strict_tcc_sig = - { - optdepr = false; - optkey = ["Function_raw_tcc"]; - optread = (fun () -> !strict_tcc); - optwrite = (fun b -> strict_tcc := b) - } - -let () = declare_bool_option strict_tcc_sig - +let is_strict_tcc = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Function_raw_tcc"] + ~value:false exception Building_graph of exn exception Defining_principle of exn diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 50c3ed1248..2bd4211c90 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -359,21 +359,15 @@ 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 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 in diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 1958fff4cc..9eeba614c7 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -27,7 +27,13 @@ open NumCompat open Q.Notations open Mutils -let use_simplex = ref true +let use_simplex = + Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true + +(* If set to some [file], arithmetic goals are dumped in [file].v *) + +let dump_file = + Goptions.declare_stringopt_option_and_ref ~depr:false ~key:["Dump"; "Arith"] type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown type zres = (Mc.zArithProof, int * Mc.z list) res @@ -203,19 +209,19 @@ let fourier_linear_prover l = | Inl _ -> None let direct_linear_prover l = - if !use_simplex then Simplex.find_unsat_certificate l + if use_simplex () then Simplex.find_unsat_certificate l else fourier_linear_prover l let find_point l = let open Util in - if !use_simplex then Simplex.find_point l + if use_simplex () then Simplex.find_point l else match Mfourier.Fourier.find_point l with | Inr _ -> None | Inl cert -> Some cert let optimise v l = - if !use_simplex then Simplex.optimise v l else Mfourier.Fourier.optimise v l + if use_simplex () then Simplex.optimise v l else Mfourier.Fourier.optimise v l let dual_raw_certificate l = if debug then begin @@ -981,13 +987,11 @@ let xlia_simplex env red sys = with FoundProof prf -> compile_prf sys (Step (0, prf, Done)) let xlia env0 en red sys = - if !use_simplex then xlia_simplex env0 red sys else xlia en red sys - -let dump_file = ref None + if use_simplex () then xlia_simplex env0 red sys else xlia en red sys let gen_bench (tac, prover) can_enum prfdepth sys = let res = prover can_enum prfdepth sys in - ( match !dump_file with + ( match dump_file () with | None -> () | Some file -> let o = open_out (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli index cabd36ebb7..5b215549b0 100644 --- a/plugins/micromega/certificate.mli +++ b/plugins/micromega/certificate.mli @@ -12,16 +12,12 @@ module Mc = Micromega (** [use_simplex] is bound to the Coq option Simplex. If set, use the Simplex method, otherwise use Fourier *) -val use_simplex : bool ref +val use_simplex : unit -> bool type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown type zres = (Mc.zArithProof, int * Mc.z list) res type qres = (Mc.q Mc.psatz, int * Mc.q list) res -(** [dump_file] is bound to the Coq option Dump Arith. - If set to some [file], arithmetic goals are dumped in filexxx.v *) -val dump_file : string option ref - (** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *) val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 43f6f5a35e..7e4c4ce5c6 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -37,74 +37,31 @@ let debug = false let max_depth = max_int (* Search limit for provers over Q R *) -let lra_proof_depth = ref max_depth +let lra_proof_depth = + declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth (* Search limit for provers over Z *) -let lia_enum = ref true -let lia_proof_depth = ref max_depth -let get_lia_option () = (!Certificate.use_simplex, !lia_enum, !lia_proof_depth) -let get_lra_option () = !lra_proof_depth +let lia_enum = + declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true + +let lia_proof_depth = + declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth + +let get_lia_option () = + (Certificate.use_simplex (), lia_enum (), lia_proof_depth ()) (* Enable/disable caches *) -let use_lia_cache = ref true -let use_nia_cache = ref true -let use_nra_cache = ref true -let use_csdp_cache = ref true - -let () = - let int_opt l vref = - { optdepr = false - ; optkey = l - ; optread = (fun () -> Some !vref) - ; optwrite = - (fun x -> vref := match x with None -> max_depth | Some v -> v) } - in - let lia_enum_opt = - { optdepr = false - ; optkey = ["Lia"; "Enum"] - ; optread = (fun () -> !lia_enum) - ; optwrite = (fun x -> lia_enum := x) } - in - let solver_opt = - { optdepr = false - ; optkey = ["Simplex"] - ; optread = (fun () -> !Certificate.use_simplex) - ; optwrite = (fun x -> Certificate.use_simplex := x) } - in - let dump_file_opt = - { optdepr = false - ; optkey = ["Dump"; "Arith"] - ; optread = (fun () -> !Certificate.dump_file) - ; optwrite = (fun x -> Certificate.dump_file := x) } - in - let lia_cache_opt = - { optdepr = false - ; optkey = ["Lia"; "Cache"] - ; optread = (fun () -> !use_lia_cache) - ; optwrite = (fun x -> use_lia_cache := x) } - in - let nia_cache_opt = - { optdepr = false - ; optkey = ["Nia"; "Cache"] - ; optread = (fun () -> !use_nia_cache) - ; optwrite = (fun x -> use_nia_cache := x) } - in - let nra_cache_opt = - { optdepr = false - ; optkey = ["Nra"; "Cache"] - ; optread = (fun () -> !use_nra_cache) - ; optwrite = (fun x -> use_nra_cache := x) } - in - let () = declare_bool_option solver_opt in - let () = declare_bool_option lia_cache_opt in - let () = declare_bool_option nia_cache_opt in - let () = declare_bool_option nra_cache_opt in - let () = declare_stringopt_option dump_file_opt in - let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in - let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in - let () = declare_bool_option lia_enum_opt in - () +let use_lia_cache = + declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Cache"] ~value:true + +let use_nia_cache = + declare_bool_option_and_ref ~depr:false ~key:["Nia"; "Cache"] ~value:true + +let use_nra_cache = + declare_bool_option_and_ref ~depr:false ~key:["Nra"; "Cache"] ~value:true + +let use_csdp_cache () = true (** * Initialize a tag type to the Tag module declaration (see Mutils). @@ -2101,7 +2058,7 @@ struct let memo_opt use_cache cache_file f = let memof = memo cache_file f in - fun x -> if !use_cache then memof x else f x + fun x -> if use_cache () then memof x else f x end module CacheCsdp = MakeCache (struct @@ -2281,7 +2238,7 @@ let memo_nra = let linear_prover_Q = { name = "linear prover" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = (fun (o, l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o) l) @@ -2292,7 +2249,7 @@ let linear_prover_Q = let linear_prover_R = { name = "linear prover" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = (fun (o, l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o) l) @@ -2303,7 +2260,7 @@ let linear_prover_R = let nlinear_prover_R = { name = "nra" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = memo_nra ; hyps = hyps_of_cone ; compact = compact_cone diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 537c37810e..1371c671a2 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -45,15 +45,11 @@ let reset_info () = s_info.branch_successes <- 0; s_info.nd_branching <- 0 -let pruning = ref true - -let opt_pruning= - {optdepr=false; - optkey=["Rtauto";"Pruning"]; - optread=(fun () -> !pruning); - optwrite=(fun b -> pruning:=b)} - -let () = declare_bool_option opt_pruning +let pruning = + declare_bool_option_and_ref + ~depr:false + ~key:["Rtauto";"Pruning"] + ~value:true type form= Atom of int @@ -182,7 +178,7 @@ let rec fill stack proof = [] -> Complete proof.dep_it | slice::super -> if - !pruning && + pruning () && List.is_empty slice.proofs_done && not (slice.changes_goal && proof.dep_goal) && not (Int.Set.exists @@ -529,7 +525,7 @@ let pp = let pp_info () = let count_info = - if !pruning then + if pruning () then str "Proof steps : " ++ int s_info.created_steps ++ str " created / " ++ int s_info.pruned_steps ++ str " pruned" ++ fnl () ++ diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 63dae1417e..d464ec4c06 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -221,27 +221,17 @@ let build_env gamma= mkApp(force node_count l_push,[|mkProp;p;e|])) gamma.env (mkApp (force node_count l_empty,[|mkProp|])) -open Goptions - -let verbose = ref false - -let opt_verbose= - {optdepr=false; - optkey=["Rtauto";"Verbose"]; - optread=(fun () -> !verbose); - optwrite=(fun b -> verbose:=b)} - -let () = declare_bool_option opt_verbose - -let check = ref false - -let opt_check= - {optdepr=false; - optkey=["Rtauto";"Check"]; - optread=(fun () -> !check); - optwrite=(fun b -> check:=b)} - -let () = declare_bool_option opt_check +let verbose = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Rtauto";"Verbose"] + ~value:false + +let check = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Rtauto";"Check"] + ~value:false open Pp @@ -267,7 +257,7 @@ let rtauto_tac = let () = begin reset_info (); - if !verbose then + if verbose () then Feedback.msg_info (str "Starting proof-search ..."); end in let search_start_time = System.get_time () in @@ -276,7 +266,7 @@ let rtauto_tac = with Not_found -> user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in - let () = if !verbose then + let () = if verbose () then begin Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); @@ -292,7 +282,7 @@ let rtauto_tac = let term= applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) hyps) in let build_end_time=System.get_time () in - let () = if !verbose then + let () = if verbose () then begin Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ @@ -306,14 +296,14 @@ let rtauto_tac = let tac_start_time = System.get_time () in let term = EConstr.of_constr term in let result= - if !check then + if check () then Tactics.exact_check term else Tactics.exact_no_check term in let tac_end_time = System.get_time () in let () = - if !check then Feedback.msg_info (str "Proof term type-checking is on"); - if !verbose then + if check () then Feedback.msg_info (str "Proof term type-checking is on"); + if verbose () then Feedback.msg_info (str "Internal tactic executed in " ++ System.fmt_time_difference tac_start_time tac_end_time) in result diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 73be36d031..857918c928 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -221,53 +221,35 @@ module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet) (* Flags.for printing or not wildcard and synthetisable types *) -open Goptions - -let wildcard_value = ref true -let force_wildcard () = !wildcard_value - -let () = declare_bool_option - { optdepr = false; - optkey = ["Printing";"Wildcard"]; - optread = force_wildcard; - optwrite = (:=) wildcard_value } - -let fast_name_generation = ref false - -let () = declare_bool_option { - optdepr = false; - optkey = ["Fast";"Name";"Printing"]; - optread = (fun () -> !fast_name_generation); - optwrite = (:=) fast_name_generation; -} - -let synth_type_value = ref true -let synthetize_type () = !synth_type_value - -let () = declare_bool_option - { optdepr = false; - optkey = ["Printing";"Synth"]; - optread = synthetize_type; - optwrite = (:=) synth_type_value } - -let reverse_matching_value = ref true -let reverse_matching () = !reverse_matching_value - -let () = declare_bool_option - { optdepr = false; - optkey = ["Printing";"Matching"]; - optread = reverse_matching; - optwrite = (:=) reverse_matching_value } - -let print_primproj_params_value = ref false -let print_primproj_params () = !print_primproj_params_value - -let () = declare_bool_option - { optdepr = false; - optkey = ["Printing";"Primitive";"Projection";"Parameters"]; - optread = print_primproj_params; - optwrite = (:=) print_primproj_params_value } - +let force_wildcard = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Wildcard"] + ~value:true + +let fast_name_generation = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Fast";"Name";"Printing"] + ~value:false + +let synthetize_type = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Synth"] + ~value:true + +let reverse_matching = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Matching"] + ~value:true + +let print_primproj_params = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Primitive";"Projection";"Parameters"] + ~value:false (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) @@ -338,27 +320,23 @@ let lookup_index_as_renamed env sigma t n = (**********************************************************************) (* Factorization of match patterns *) -let print_factorize_match_patterns = ref true - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Factorizable";"Match";"Patterns"]; - optread = (fun () -> !print_factorize_match_patterns); - optwrite = (fun b -> print_factorize_match_patterns := b) } - -let print_allow_match_default_clause = ref true +let print_factorize_match_patterns = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Factorizable";"Match";"Patterns"] + ~value:true -let () = - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; - optread = (fun () -> !print_allow_match_default_clause); - optwrite = (fun b -> print_allow_match_default_clause := b) } +let print_allow_match_default_opt_name = + ["Printing";"Allow";"Match";"Default";"Clause"] +let print_allow_match_default_clause = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:print_allow_match_default_opt_name + ~value:true let rec join_eqns (ids,rhs as x) patll = function | ({CAst.loc; v=(ids',patl',rhs')} as eqn')::rest -> - if not !Flags.raw_print && !print_factorize_match_patterns && + if not !Flags.raw_print && print_factorize_match_patterns () && List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs' then join_eqns x (patl'::patll) rest @@ -404,7 +382,7 @@ let factorize_eqns eqns = let eqns = aux [] (List.rev eqns) in let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in let open CAst in - if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then + if not !Flags.raw_print && print_allow_match_default_clause () && eqns <> [] then match select_default_clause eqns with (* At least two clauses and the last one is disjunctive with no variables *) | Some {loc=gloc;v=([],patl::_::_,rhs)}, (_::_ as eqns) -> @@ -925,16 +903,16 @@ let detype_rel_context d flags where avoid env sigma sign = let detype_names isgoal avoid nenv env sigma t = let flags = { flg_isgoal = isgoal; flg_lax = false } in - let avoid = Avoid.make ~fast:!fast_name_generation avoid in + let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in detype Now flags avoid (nenv,env) sigma t let detype d ?(lax=false) isgoal avoid env sigma t = let flags = { flg_isgoal = isgoal; flg_lax = lax } in - let avoid = Avoid.make ~fast:!fast_name_generation avoid in + let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in detype d flags avoid (names_of_rel_context env, env) sigma t let detype_rel_context d ?(lax = false) where avoid env sigma sign = let flags = { flg_isgoal = false; flg_lax = lax } in - let avoid = Avoid.make ~fast:!fast_name_generation avoid in + let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in detype_rel_context d flags where avoid env sigma sign let detype_closed_glob ?lax isgoal avoid env sigma t = diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 5723b47715..254f772ff8 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -29,11 +29,12 @@ val print_evar_arguments : bool ref (** If true, contract branches with same r.h.s. and same matching variables in a disjunctive pattern *) -val print_factorize_match_patterns : bool ref +val print_factorize_match_patterns : unit -> bool -(** If true and the last non unique clause of a "match" is a +(** If this flag is true and the last non unique clause of a "match" is a variable-free disjunctive pattern, turn it into a catch-call case *) -val print_allow_match_default_clause : bool ref +val print_allow_match_default_clause : unit -> bool +val print_allow_match_default_opt_name : string list val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 26bf02aa25..3d887e1a95 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -47,21 +47,17 @@ let default_flags env = let ts = default_transparent_state env in default_flags_of ts -let debug_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"Unification"]; - optread = (fun () -> !debug_unification); - optwrite = (fun a -> debug_unification:=a); -}) - -let debug_ho_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"HO";"Unification"]; - optread = (fun () -> !debug_ho_unification); - optwrite = (fun a -> debug_ho_unification:=a); -}) +let debug_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"Unification"] + ~value:false + +let debug_ho_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"HO";"Unification"] + ~value:false (*******************************************) (* Functions to deal with impossible cases *) @@ -767,7 +763,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) - let () = if !debug_unification then + let () = if debug_unification () then let open Pp in Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term flags env evd term1 sk1, @@ -1224,16 +1220,16 @@ let apply_on_subterm env evd fixedref f test c t = (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t else - (if !debug_ho_unification then + (if debug_ho_unification () then Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t); let b, evd = try test env !evdref k c t with e when CErrors.noncritical e -> assert false in - if b then (if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded"); + if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded"); let evd', t' = f !evdref k t in evdref := evd'; t') else ( - if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed"); + if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed"); map_constr_with_binders_left_to_right !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t)) @@ -1337,7 +1333,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let env_evar = evar_filtered_env env_rhs evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs); Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar)); let args = Array.map (nf_evar evd) args in @@ -1374,7 +1370,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let rec set_holes env_rhs evd rhs = function | (id,idty,c,cty,evsref,filter,occs)::subst -> let c = nf_evar evd c in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"set holes for: " ++ prc env_rhs evd (mkVar id.binder_name) ++ spc () ++ prc env_rhs evd c ++ str" in " ++ @@ -1382,7 +1378,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let occ = ref 1 in let set_var evd k inst = let oc = !occ in - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"Found one occurrence"); Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c)); incr occ; @@ -1393,7 +1389,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | Unspecified prefer_abstraction -> let evd, evty = set_holes env_rhs evd cty subst in let evty = nf_evar evd evty in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ str" of type: " ++ prc env_evar evd evty ++ str " for " ++ prc env_rhs evd c); @@ -1413,7 +1409,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = evd, ev in let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs'); let () = check_selected_occs env_rhs evd c !occ occs in let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in @@ -1427,7 +1423,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = (* Thin evars making the term typable in env_evar *) let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs'); Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let evd,rhs' = @@ -1437,7 +1433,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = raise (TypingFailed evd) in let rhs' = nf_evar evd rhs' in (* We instantiate the evars of which the value is forced by typing *) - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs'); Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); @@ -1445,7 +1441,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | (id,idty,c,cty,evsref,_,_)::l -> let id = id.binder_name in let c = nf_evar evd c in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracting: " ++ prc env_rhs evd (mkVar id) ++ spc () ++ prc env_rhs evd c); @@ -1476,7 +1472,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | _ -> evd) with e -> user_err (Pp.str "Cannot find an instance") else - ((if !debug_ho_unification then + ((if debug_ho_unification () then let evi = Evd.find evd evk in let env = Evd.evar_env env_rhs evi in Feedback.msg_debug Pp.(str"evar is defined: " ++ @@ -1491,7 +1487,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if Evd.is_defined evd evk then (* Can happen due to dependencies: instantiating evars in the arguments of evk might instantiate evk itself. *) - (if !debug_ho_unification then + (if debug_ho_unification () then begin let evi = Evd.find evd evk in let evenv = evar_env env_rhs evi in @@ -1504,13 +1500,13 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let evi = Evd.find_undefined evd evk in let evenv = evar_env env_rhs evi in let rhs' = nf_evar evd rhs' in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ prc evenv evd rhs'); (* solve_evars is not commuting with nf_evar, because restricting an evar might provide a more specific type. *) let evd, _ = !solve_evars evenv evd rhs' in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')); let flags = default_flags_of TransparentState.full in Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs' @@ -1564,7 +1560,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in - let () = if !debug_unification then + let () = if debug_unification () then let open Pp in Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++ Termops.Internal.print_constr_env env evd t1 ++ cut () ++ diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index f989dae4c9..c1ca40329a 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -28,16 +28,22 @@ exception Find_at of int (* timing *) -let timing_enabled = ref false +let get_timing_enabled = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Timing"] + ~value:false (* profiling *) -let profiling_enabled = ref false +let get_profiling_enabled = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Profiling"] + ~value:false (* for supported platforms, filename for profiler results *) -let profile_filename = ref "native_compute_profile.data" - let profiler_platform () = match [@warning "-8"] Sys.os_type with | "Unix" -> @@ -48,10 +54,11 @@ let profiler_platform () = | "Win32" -> "Windows (Win32)" | "Cygwin" -> "Windows (Cygwin)" -let get_profile_filename () = !profile_filename - -let set_profile_filename fn = - profile_filename := fn +let get_profile_filename = + Goptions.declare_string_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Profile"; "Filename"] + ~value:"native_compute_profile.data" (* find unused profile filename *) let get_available_profile_filename () = @@ -77,18 +84,6 @@ let get_available_profile_filename () = let _ = Feedback.msg_info (Pp.str msg) in assert false -let get_profiling_enabled () = - !profiling_enabled - -let set_profiling_enabled b = - profiling_enabled := b - -let get_timing_enabled () = - !timing_enabled - -let set_timing_enabled b = - timing_enabled := b - let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 4f18174261..73a8add6ec 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -14,16 +14,6 @@ open Evd (** This module implements normalization by evaluation to OCaml code *) -val get_profile_filename : unit -> string -val set_profile_filename : string -> unit - -val get_profiling_enabled : unit -> bool -val set_profiling_enabled : bool -> unit - -val get_timing_enabled : unit -> bool -val set_timing_enabled : bool -> unit - - val native_norm : env -> evar_map -> constr -> types -> constr (** Conversion with inference of universe constraints *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 01f3537a7f..f7456ef35e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -30,14 +30,6 @@ exception Elimconst their parameters in its stack. *) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Cumulativity";"Weak";"Constraints"]; - optread = (fun () -> not !UState.drop_weak_constraints); - optwrite = (fun a -> UState.drop_weak_constraints:=not a); -}) - - (** Support for reduction effects *) open Mod_subst @@ -966,13 +958,11 @@ module CredNative = RedNative(CNativeEntries) contract_* in any case . *) -let debug_RAKAM = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"RAKAM"]; - optread = (fun () -> !debug_RAKAM); - optwrite = (fun a -> debug_RAKAM:=a); -}) +let debug_RAKAM = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"RAKAM"] + ~value:false let equal_stacks sigma (x, l) (y, l') = let f_equal x y = eq_constr sigma x y in @@ -983,7 +973,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in let open ReductionBehaviour in let rec whrec cst_l (x, stack) = - let () = if !debug_RAKAM then + let () = if debug_RAKAM () then let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in Feedback.msg_debug @@ -994,7 +984,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = in let c0 = EConstr.kind sigma x in let fold () = - let () = if !debug_RAKAM then + let () = if debug_RAKAM () then let open Pp in Feedback.msg_debug (str "<><><><><>") in ((EConstr.of_kind c0, stack),cst_l) in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 90dde01915..e168f6d1b6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -43,23 +43,17 @@ type subst0 = module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let keyed_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Keyed";"Unification"]; - optread = (fun () -> !keyed_unification); - optwrite = (fun a -> keyed_unification:=a); -}) - -let is_keyed_unification () = !keyed_unification - -let debug_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"Tactic";"Unification"]; - optread = (fun () -> !debug_unification); - optwrite = (fun a -> debug_unification:=a); -}) +let is_keyed_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Keyed";"Unification"] + ~value:false + +let debug_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"Tactic";"Unification"] + ~value:false (** Making this unification algorithm correct w.r.t. the evar-map abstraction breaks too much stuff. So we redefine incorrect functions here. *) @@ -702,7 +696,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let cM = Evarutil.whd_head_evar sigma curm and cN = Evarutil.whd_head_evar sigma curn in let () = - if !debug_unification then + if debug_unification () then Feedback.msg_debug ( Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++ Termops.Internal.print_constr_env curenv sigma cN) @@ -1127,7 +1121,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else error_cannot_unify (fst curenvnb) sigma (cM,cN) in - if !debug_unification then Feedback.msg_debug (str "Starting unification"); + if debug_unification () then Feedback.msg_debug (str "Starting unification"); let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in try let res = @@ -1152,11 +1146,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let a = match res with | Some sigma -> sigma, ms, es | None -> unirec_rec (env,0) cv_pb opt subst m n in - if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); + if debug_unification () then Feedback.msg_debug (str "Leaving unification with success"); a with e -> let e = Exninfo.capture e in - if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); + if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure"); Exninfo.iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env @@ -1745,7 +1739,7 @@ let make_abstraction env evd ccl abs = env evd c ty occs check_occs ccl let keyed_unify env evd kop = - if not !keyed_unification then fun cl -> true + if not (is_keyed_unification ()) then fun cl -> true else match kop with | None -> fun _ -> true @@ -1767,7 +1761,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = (try if closed0 evd cl && not (isEvar evd cl) && keyed_unify env evd kop cl then (try - if !keyed_unification then + if is_keyed_unification () then let f1, l1 = decompose_app_vect evd op in let f2, l2 = decompose_app_vect evd cl in w_typed_unify_array env evd flags f1 l1 f2 l2,cl @@ -1913,7 +1907,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = else let allow_K = flags.allow_K_in_toplevel_higher_order_unification in let flags = - if unsafe_occur_meta_or_existential op || !keyed_unification then + if unsafe_occur_meta_or_existential op || is_keyed_unification () then (* This is up to delta for subterms w/o metas ... *) flags else diff --git a/printing/printer.ml b/printing/printer.ml index 32dc4bb0f0..81c0a36f53 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -25,42 +25,26 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration -let enable_unfocused_goal_printing = ref false -let enable_goal_tags_printing = ref false -let enable_goal_names_printing = ref false - -let should_tag() = !enable_goal_tags_printing -let should_unfoc() = !enable_unfocused_goal_printing -let should_gname() = !enable_goal_names_printing - - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Unfocused"]; - optread = (fun () -> !enable_unfocused_goal_printing); - optwrite = (fun b -> enable_unfocused_goal_printing:=b) } - (* This is set on by proofgeneral proof-tree mode. But may be used for other purposes *) -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Goal";"Tags"]; - optread = (fun () -> !enable_goal_tags_printing); - optwrite = (fun b -> enable_goal_tags_printing:=b) } - - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Goal";"Names"]; - optread = (fun () -> !enable_goal_names_printing); - optwrite = (fun b -> enable_goal_names_printing:=b) } - +let print_goal_tag_opt_name = ["Printing";"Goal";"Tags"] +let should_tag = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:print_goal_tag_opt_name + ~value:false + +let should_unfoc = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Unfocused"] + ~value:false + +let should_gname = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Goal";"Names"] + ~value:false (**********************************************************************) (** Terms *) @@ -407,17 +391,10 @@ let pr_context_limit_compact ?n env sigma = (* The number of printed hypothesis in a goal *) (* If [None], no limit *) -let print_hyps_limit = ref (None : int option) +let print_hyps_limit = + Goptions.declare_intopt_option_and_ref ~depr:false ~key:["Hyps";"Limit"] -let () = - let open Goptions in - declare_int_option - { optdepr = false; - optkey = ["Hyps";"Limit"]; - optread = (fun () -> !print_hyps_limit); - optwrite = (fun x -> print_hyps_limit := x) } - -let pr_context_of env sigma = match !print_hyps_limit with +let pr_context_of env sigma = match print_hyps_limit () with | None -> hv 0 (pr_context_limit_compact env sigma) | Some n -> hv 0 (pr_context_limit_compact ~n env sigma) @@ -615,18 +592,14 @@ let print_evar_constraints gl sigma = str" with candidates:" ++ fnl () ++ hov 0 ppcandidates else mt () -let should_print_dependent_evars = ref false - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Dependent";"Evars";"Line"]; - optread = (fun () -> !should_print_dependent_evars); - optwrite = (fun v -> should_print_dependent_evars := v) } +let should_print_dependent_evars = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Dependent";"Evars";"Line"] + ~value:false let print_dependent_evars gl sigma seeds = - if !should_print_dependent_evars then + if should_print_dependent_evars () then let mt_pp = mt () in let evars = Evarutil.gather_dependent_evars sigma seeds in let evars_pp = Evar.Map.fold (fun e i s -> diff --git a/printing/printer.mli b/printing/printer.mli index 936426949c..8c633b5e79 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -19,9 +19,7 @@ open Notation_term (** These are the entry points for printing terms, context, tac, ... *) -val enable_unfocused_goal_printing: bool ref -val enable_goal_tags_printing : bool ref -val enable_goal_names_printing : bool ref +val print_goal_tag_opt_name : string list (** Terms *) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 3a6424ba9f..c78cc96a83 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -46,36 +46,37 @@ let write_color_enabled enabled = let color_enabled () = !term_color -let diff_option = ref `OFF +type diffOpt = DiffOff | DiffOn | DiffRemoved -let read_diffs_option () = match !diff_option with -| `OFF -> "off" -| `ON -> "on" -| `REMOVED -> "removed" +let diffs_to_string = function + | DiffOff -> "off" + | DiffOn -> "on" + | DiffRemoved -> "removed" -let write_diffs_option opt = - let enable opt = - if not (color_enabled ()) then - CErrors.user_err Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") - else - diff_option := opt - in - match opt with - | "off" -> diff_option := `OFF - | "on" -> enable `ON - | "removed" -> enable `REMOVED + +let assert_color_enabled () = + if not (color_enabled ()) then + CErrors.user_err + Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") + +let string_to_diffs = function + | "off" -> DiffOff + | "on" -> assert_color_enabled (); DiffOn + | "removed" -> assert_color_enabled (); DiffRemoved | _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".") -let () = - Goptions.(declare_string_option { - optdepr = false; - optkey = ["Diffs"]; - optread = read_diffs_option; - optwrite = write_diffs_option - }) +let opt_name = ["Diffs"] + +let diff_option = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:opt_name + ~value:DiffOff + string_to_diffs + diffs_to_string -let show_diffs () = !diff_option <> `OFF;; -let show_removed () = !diff_option = `REMOVED;; +let show_diffs () = match diff_option () with DiffOff -> false | _ -> true +let show_removed () = match diff_option () with DiffRemoved -> true | _ -> false (* DEBUG/UNIT TEST *) diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 24b171770a..ea64439456 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -10,8 +10,8 @@ (* diff options *) -(** Controls whether to show diffs. Takes values "on", "off", "removed" *) -val write_diffs_option : string -> unit +(** Name of Diffs option *) +val opt_name : string list (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index 29e19778e4..e847535aaf 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -22,11 +22,6 @@ type t = | SelectId of Id.t | SelectAll -(* Default goal selector: selector chosen when a tactic is applied - without an explicit selector. *) -let default_goal_selector = ref (SelectNth 1) -let get_default_goal_selector () = !default_goal_selector - let pr_range_selector (i, j) = if i = j then Pp.int i else Pp.(int i ++ str "-" ++ int j) @@ -53,15 +48,12 @@ let parse_goal_selector = function with Failure _ -> CErrors.user_err Pp.(str err_msg) end -let () = let open Goptions in - declare_string_option - { optdepr = false; - optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> - Pp.string_of_ppcmds - (pr_goal_selector !default_goal_selector) - end; - optwrite = begin fun n -> - default_goal_selector := parse_goal_selector n - end - } +(* Default goal selector: selector chosen when a tactic is applied + without an explicit selector. *) +let get_default_goal_selector = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Default";"Goal";"Selector"] + ~value:(SelectNth 1) + parse_goal_selector + (fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v) diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index f1f7361317..f619bc86a1 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -174,28 +174,22 @@ module Strict = struct end (* Current bullet behavior, controlled by the option *) -let current_behavior = ref Strict.strict - -let () = - Goptions.(declare_string_option { - optdepr = false; - optkey = ["Bullet";"Behavior"]; - optread = begin fun () -> - (!current_behavior).name - end; - optwrite = begin fun n -> - current_behavior := - try Hashtbl.find behaviors n - with Not_found -> - CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")) - end - }) +let current_behavior = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Bullet";"Behavior"] + ~value:Strict.strict + (fun n -> + try Hashtbl.find behaviors n + with Not_found -> + CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))) + (fun v -> v.name) let put p b = - (!current_behavior).put p b + (current_behavior ()).put p b let suggest p = - (!current_behavior).suggest p + (current_behavior ()).suggest p (* Better printing for bullet exceptions *) exception SuggestNoSuchGoals of int * Proof.t diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 92d56d2904..57eab7ddf8 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -38,33 +38,48 @@ let typeclasses_db = "typeclass_instances" (** Options handling *) let typeclasses_debug = ref 0 -let typeclasses_depth = ref None + +let typeclasses_depth_opt_name = ["Typeclasses";"Depth"] +let get_typeclasses_depth = + Goptions.declare_intopt_option_and_ref + ~depr:false + ~key:typeclasses_depth_opt_name + +let set_typeclasses_depth = + Goptions.set_int_option_value typeclasses_depth_opt_name (** When this flag is enabled, the resolution of type classes tries to avoid useless introductions. This is no longer useful since we have eta, but is here for compatibility purposes. Another compatibility issues is that the cost (in terms of search depth) can differ. *) -let typeclasses_limit_intros = ref true -let set_typeclasses_limit_intros d = (:=) typeclasses_limit_intros d -let get_typeclasses_limit_intros () = !typeclasses_limit_intros - -let typeclasses_dependency_order = ref false -let set_typeclasses_dependency_order d = (:=) typeclasses_dependency_order d -let get_typeclasses_dependency_order () = !typeclasses_dependency_order - -let typeclasses_iterative_deepening = ref false -let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d -let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening +let get_typeclasses_limit_intros = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Limit";"Intros"] + ~value:true + +let get_typeclasses_dependency_order = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Dependency";"Order"] + ~value:false + +let iterative_deepening_opt_name = ["Typeclasses";"Iterative";"Deepening"] +let get_typeclasses_iterative_deepening = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:iterative_deepening_opt_name + ~value:false (** [typeclasses_filtered_unif] governs the unification algorithm used by type classes. If enabled, a new algorithm based on pattern filtering and refine will be used. When disabled, the previous algorithm based on apply will be used. *) -let typeclasses_filtered_unification = ref false -let set_typeclasses_filtered_unification d = - (:=) typeclasses_filtered_unification d -let get_typeclasses_filtered_unification () = - !typeclasses_filtered_unification +let get_typeclasses_filtered_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Filtered";"Unification"] + ~value:false let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0) let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false @@ -75,40 +90,8 @@ let set_typeclasses_verbose = let get_typeclasses_verbose () = if !typeclasses_debug = 0 then None else Some !typeclasses_debug -let set_typeclasses_depth d = (:=) typeclasses_depth d -let get_typeclasses_depth () = !typeclasses_depth - -open Goptions - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Limit";"Intros"]; - optread = get_typeclasses_limit_intros; - optwrite = set_typeclasses_limit_intros; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Dependency";"Order"]; - optread = get_typeclasses_dependency_order; - optwrite = set_typeclasses_dependency_order; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Iterative";"Deepening"]; - optread = get_typeclasses_iterative_deepening; - optwrite = set_typeclasses_iterative_deepening; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Filtered";"Unification"]; - optread = get_typeclasses_filtered_unification; - optwrite = set_typeclasses_filtered_unification; } - let () = + let open Goptions in declare_bool_option { optdepr = false; optkey = ["Typeclasses";"Debug"]; @@ -116,24 +99,18 @@ let () = optwrite = set_typeclasses_debug; } let _ = + let open Goptions in declare_int_option { optdepr = false; optkey = ["Typeclasses";"Debug";"Verbosity"]; optread = get_typeclasses_verbose; optwrite = set_typeclasses_verbose; } -let () = - declare_int_option - { optdepr = false; - optkey = ["Typeclasses";"Depth"]; - optread = get_typeclasses_depth; - optwrite = set_typeclasses_depth; } - type search_strategy = Dfs | Bfs let set_typeclasses_strategy = function - | Dfs -> set_typeclasses_iterative_deepening false - | Bfs -> set_typeclasses_iterative_deepening true + | Dfs -> Goptions.set_bool_option_value iterative_deepening_opt_name false + | Bfs -> Goptions.set_bool_option_value iterative_deepening_opt_name true let pr_ev evs ev = Printer.pr_econstr_env (Goal.V82.env evs ev) evs (Goal.V82.concl evs ev) @@ -977,7 +954,7 @@ module Search = struct | None -> None (* This happens only because there's no evar having p *) | Some (goals, nongoals) -> let goalsl = - if !typeclasses_dependency_order then + if get_typeclasses_dependency_order () then top_sort evm goals else Evar.Set.elements goals in diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index e26338436d..b97b90d777 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -19,10 +19,8 @@ val catchable : exn -> bool [@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."] val set_typeclasses_debug : bool -> unit -val get_typeclasses_debug : unit -> bool val set_typeclasses_depth : int option -> unit -val get_typeclasses_depth : unit -> int option type search_strategy = Dfs | Bfs diff --git a/tactics/hints.ml b/tactics/hints.ml index a907b9e783..f8a46fcb1d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -188,27 +188,26 @@ type hints_expr = | HintsConstructors of qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument -type import_level = [ `LAX | `WARN | `STRICT ] - -let warn_hint : import_level ref = ref `LAX -let read_warn_hint () = match !warn_hint with -| `LAX -> "Lax" -| `WARN -> "Warn" -| `STRICT -> "Strict" - -let write_warn_hint = function -| "Lax" -> warn_hint := `LAX -| "Warn" -> warn_hint := `WARN -| "Strict" -> warn_hint := `STRICT -| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.") - -let () = - Goptions.(declare_string_option - { optdepr = false; - optkey = ["Loose"; "Hint"; "Behavior"]; - optread = read_warn_hint; - optwrite = write_warn_hint; - }) +type import_level = HintLax | HintWarn | HintStrict + +let warn_hint_to_string = function +| HintLax -> "Lax" +| HintWarn -> "Warn" +| HintStrict -> "Strict" + +let string_to_warn_hint = function +| "Lax" -> HintLax +| "Warn" -> HintWarn +| "Strict" -> HintStrict +| _ -> user_err Pp.(str "Only the following values are accepted: Lax, Warn, Strict.") + +let warn_hint = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Loose"; "Hint"; "Behavior"] + ~value:HintLax + string_to_warn_hint + warn_hint_to_string let fresh_key = let id = Summary.ref ~name:"HINT-COUNTER" 0 in @@ -1690,12 +1689,12 @@ let wrap_hint_warning_fun env sigma t = in (ans, set_extra_data store sigma) -let run_hint tac k = match !warn_hint with -| `LAX -> k tac.obj -| `WARN -> +let run_hint tac k = match warn_hint () with +| HintLax -> k tac.obj +| HintWarn -> if is_imported tac then k tac.obj else Proofview.tclTHEN (log_hint tac) (k tac.obj) -| `STRICT -> +| HintStrict -> if is_imported tac then k tac.obj else Proofview.tclZERO (UserError (None, (str "Tactic failure."))) diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 22d0ce5328..c139594f13 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -14,15 +14,11 @@ open Names open Environ open Evd -let use_unification_heuristics_ref = ref true -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Solve";"Unification";"Constraints"]; - optread = (fun () -> !use_unification_heuristics_ref); - optwrite = (fun a -> use_unification_heuristics_ref:=a); -}) - -let use_unification_heuristics () = !use_unification_heuristics_ref +let use_unification_heuristics = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Solve";"Unification";"Constraints"] + ~value:true exception NoSuchGoal let () = CErrors.register_handler begin function diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index d7dcc13e79..68de9c7a00 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -130,15 +130,10 @@ let get_open_goals ps = type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t let private_poly_univs = - let b = ref true in - let _ = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Private";"Polymorphic";"Universes"]; - optread = (fun () -> !b); - optwrite = ((:=) b); - }) - in - fun () -> !b + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Private";"Polymorphic";"Universes"] + ~value:true (* XXX: This is still separate from close_proof below due to drop_pt in the STM *) let return_proof { proof } = diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index db09a2e69e..f681e4e99e 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -53,13 +53,8 @@ let whd_cbn flags env sigma t = let strong_cbn flags = strong_with_flags whd_cbn flags -let simplIsCbn = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["SimplIsCbn"]; - optread = (fun () -> !simplIsCbn); - optwrite = (fun a -> simplIsCbn:=a); -}) +let simplIsCbn = + Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false let set_strategy_one ref l = let k = @@ -228,10 +223,10 @@ let reduction_of_red_expr env = else (e_red red_product,DEFAULTcast) | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl (f,o) -> - let whd_am = if !simplIsCbn then whd_cbn (make_flag f) else whd_simpl in - let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in + let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in + let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in let () = - if not (!simplIsCbn || List.is_empty f.rConst) then + if not (simplIsCbn () || List.is_empty f.rConst) then warn_simpl_unfolding_modifiers () in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 4963a806f5..4ffbdabf85 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -44,7 +44,6 @@ type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; toplevel_name : Stm.interactive_top; - allow_sprop : bool; cumulative_sprop : bool; } @@ -59,7 +58,6 @@ type coqargs_config = { native_include_dirs : CUnix.physical_path list; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; - diffs_set : bool; time : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; @@ -112,7 +110,6 @@ let default_logic_config = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; toplevel_name = Stm.TopLogical default_toplevel; - allow_sprop = true; cumulative_sprop = false; } @@ -127,7 +124,6 @@ let default_config = { native_include_dirs = []; stm_flags = Stm.AsyncOpts.default_opts; debug = false; - diffs_set = false; time = false; print_emacs = false; set_options = []; @@ -178,9 +174,12 @@ let add_vo_require opts d p export = let add_load_vernacular opts verb s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} +let add_set_option opts opt_name value = + { opts with config = { opts.config with set_options = (opt_name, value) :: opts.config.set_options }} + (** Options for proof general *) let set_emacs opts = - Printer.enable_goal_tags_printing := true; + Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true; { opts with config = { opts.config with color = `EMACS; print_emacs = true }} let set_logic f oval = @@ -481,14 +480,11 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with native_compiler }} | "-set" -> - let opt = next() in - let opt, v = parse_option_set opt in - { oval with config = { oval.config with set_options = (opt, OptionSet v) :: oval.config.set_options }} + let opt, v = parse_option_set @@ next() in + add_set_option oval opt (OptionSet v) | "-unset" -> - let opt = next() in - let opt = to_opt_key opt in - { oval with config = { oval.config with set_options = (opt, OptionUnset) :: oval.config.set_options }} + add_set_option oval (to_opt_key @@ next ()) OptionUnset |"-native-output-dir" -> let native_output_dir = next () in @@ -511,18 +507,16 @@ let parse_args ~help ~init arglist : t * string list = |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval - |"-diffs" -> let opt = next () in - if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then - Proof_diffs.write_diffs_option opt - else - error_wrong_arg "Error: on|off|removed expected after -diffs"; - { oval with config = { oval.config with diffs_set = true }} + |"-diffs" -> + add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ())) |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval |"-impredicative-set" -> set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval - |"-allow-sprop" -> set_logic (fun o -> { o with allow_sprop = true }) oval - |"-disallow-sprop" -> set_logic (fun o -> { o with allow_sprop = false }) oval + |"-allow-sprop" -> + add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) + |"-disallow-sprop" -> + add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset |"-sprop-cumulative" -> set_logic (fun o -> { o with cumulative_sprop = true }) oval |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 3d709db54d..8723d21bb4 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -20,7 +20,6 @@ type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; toplevel_name : Stm.interactive_top; - allow_sprop : bool; cumulative_sprop : bool; } @@ -35,7 +34,6 @@ type coqargs_config = { native_include_dirs : CUnix.physical_path list; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; - diffs_set : bool; time : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7d08244d49..1175494bad 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -199,7 +199,6 @@ let init_execution opts custom_init = Global.set_VM opts.config.enable_VM; Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); - Global.set_allow_sprop opts.config.logic.allow_sprop; if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative (); (* Native output dir *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2e509921c1..3195f339b6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1251,10 +1251,12 @@ let vernac_generalizable ~local = let local = Option.default true local in Implicit_quantifiers.declare_generalizable ~local +let allow_sprop_opt_name = ["Allow";"StrictProp"] + let () = declare_bool_option { optdepr = false; - optkey = ["Allow";"StrictProp"]; + optkey = allow_sprop_opt_name; optread = (fun () -> Global.sprop_allowed()); optwrite = Global.set_allow_sprop } @@ -1435,27 +1437,6 @@ let () = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } -let () = - declare_string_option - { optdepr = false; - optkey = ["NativeCompute"; "Profile"; "Filename"]; - optread = Nativenorm.get_profile_filename; - optwrite = Nativenorm.set_profile_filename } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["NativeCompute"; "Profiling"]; - optread = Nativenorm.get_profiling_enabled; - optwrite = Nativenorm.set_profiling_enabled } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["NativeCompute"; "Timing"]; - optread = Nativenorm.get_timing_enabled; - optwrite = Nativenorm.set_timing_enabled } - let _ = declare_bool_option { optdepr = false; diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index f5cf9702cd..2ac8458ad5 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -24,3 +24,5 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr (** Miscellaneous stuff *) val command_focus : unit Proof.focus_kind + +val allow_sprop_opt_name : string list diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 15a19c06c2..eb299222dd 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -51,24 +51,17 @@ let interp_typed_vernac c ~stack = (* Default proof mode, to be set at the beginning of proofs for programs that cannot be statically classified. *) -let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) -let get_default_proof_mode () = !default_proof_mode +let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode -let set_default_proof_mode_opt name = - default_proof_mode := - match Pvernac.lookup_proof_mode name with +let get_default_proof_mode = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:proof_mode_opt_name + ~value:(Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) + (fun name -> match Pvernac.lookup_proof_mode name with | Some pm -> pm - | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.declare_string_option Goptions.{ - optdepr = false; - optkey = proof_mode_opt_name; - optread = get_default_proof_mode_opt; - optwrite = set_default_proof_mode_opt; - } + | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))) + Pvernac.proof_mode_to_string (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) |