diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 97 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 49 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 14 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 13 | ||||
| -rw-r--r-- | tactics/redexpr.ml | 15 |
6 files changed, 75 insertions, 115 deletions
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) |