diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 19 | ||||
| -rw-r--r-- | pretyping/classops.ml | 20 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 20 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 16 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 51 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 5 |
6 files changed, 62 insertions, 69 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 7104b8586e..f8289f558c 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -183,14 +183,11 @@ let cofixp_reducible flgs _ stk = else false -let debug_cbv = ref false -let () = Goptions.(declare_bool_option { - optdepr = false; - optname = "cbv visited constants display"; - optkey = ["Debug";"Cbv"]; - optread = (fun () -> !debug_cbv); - optwrite = (fun a -> debug_cbv:=a); -}) +let get_debug_cbv = Goptions.declare_bool_option_and_ref + ~depr:false + ~value:false + ~name:"cbv visited constants display" + ~key:["Debug";"Cbv"] let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp @@ -325,14 +322,14 @@ and norm_head_ref k info env stack normt = if red_set_ref info.reds normt then match cbv_value_cache info normt with | Some body -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack | None -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) else begin - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) end diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 1edcc499f0..f18040accb 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -398,16 +398,12 @@ let class_params = function let add_class cl = add_new_class cl { cl_param = class_params cl } -let automatically_import_coercions = ref false - -open Goptions -let () = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic import of coercions"; - optkey = ["Automatic";"Coercions";"Import"]; - optread = (fun () -> !automatically_import_coercions); - optwrite = (:=) automatically_import_coercions } +let get_automatically_import_coercions = + Goptions.declare_bool_option_and_ref + ~depr:true (* Remove in 8.8 *) + ~name:"automatic import of coercions" + ~key:["Automatic";"Coercions";"Import"] + ~value:false let cache_coercion (_, c) = let () = add_class c.coercion_source in @@ -425,7 +421,7 @@ let cache_coercion (_, c) = add_coercion_in_graph (xf,is,it) let load_coercion _ o = - if !automatically_import_coercions then + if get_automatically_import_coercions () then cache_coercion o let set_coercion_in_scope (_, c) = @@ -435,7 +431,7 @@ let set_coercion_in_scope (_, c) = let open_coercion i o = if Int.equal i 1 then begin set_coercion_in_scope o; - if not !automatically_import_coercions then + if not (get_automatically_import_coercions ()) then cache_coercion o end diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 30eb70d0e7..4d1d405bd7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -33,16 +33,12 @@ open Evd open Termops open Globnames -let use_typeclasses_for_conversion = ref true - -let () = - Goptions.(declare_bool_option - { optdepr = false; - optname = "use typeclass resolution during conversion"; - optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"]; - optread = (fun () -> !use_typeclasses_for_conversion); - optwrite = (fun b -> use_typeclasses_for_conversion := b) } - ) +let get_use_typeclasses_for_conversion = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"use typeclass resolution during conversion" + ~key:["Typeclass"; "Resolution"; "For"; "Conversion"] + ~value:true (* Typing operations dealing with coercions *) exception NoCoercion @@ -424,7 +420,7 @@ let inh_app_fun resolve_tc env evd j = try inh_app_fun_core env evd j with | NoCoercion when not resolve_tc - || not !use_typeclasses_for_conversion -> (evd, j) + || not (get_use_typeclasses_for_conversion ()) -> (evd, j) | NoCoercion -> try inh_app_fun_core env (saturate_evd env evd) j with NoCoercion -> (evd, j) @@ -534,7 +530,7 @@ let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t = coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with - | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> + | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> error_actual_type ?loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3391750209..f5e48bcd39 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -105,16 +105,12 @@ let search_guard ?loc env possible_indexes fixdefs = (* To force universe name declaration before use *) -let strict_universe_declarations = ref true -let is_strict_universe_declarations () = !strict_universe_declarations - -let () = - Goptions.(declare_bool_option - { optdepr = false; - optname = "strict universe declaration"; - optkey = ["Strict";"Universe";"Declaration"]; - optread = is_strict_universe_declarations; - optwrite = (:=) strict_universe_declarations }) +let is_strict_universe_declarations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"strict universe declaration" + ~key:["Strict";"Universe";"Declaration"] + ~value:true (** Miscellaneous interpretation functions *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index c68890a87f..d732544c5c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -31,19 +31,12 @@ type 'a hint_info_gen = type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen -let typeclasses_unique_solutions = ref false -let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d -let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions - -open Goptions - -let () = - declare_bool_option - { optdepr = false; - optname = "check that typeclasses proof search returns unique solutions"; - optkey = ["Typeclasses";"Unique";"Solutions"]; - optread = get_typeclasses_unique_solutions; - optwrite = set_typeclasses_unique_solutions; } +let get_typeclasses_unique_solutions = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"check that typeclasses proof search returns unique solutions" + ~key:["Typeclasses";"Unique";"Solutions"] + ~value:false let (add_instance_hint, add_instance_hint_hook) = Hook.make () let add_instance_hint id = Hook.get add_instance_hint id @@ -434,28 +427,40 @@ let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl -let declare_instance info local glob = +let warning_not_a_class = + let name = "not-a-class" in + let category = "typeclasses" in + CWarnings.create ~name ~category (fun (n, ty) -> + let env = Global.env () in + let evd = Evd.from_env env in + Pp.(str "Ignored instance declaration for “" + ++ Nametab.pr_global_env Id.Set.empty n + ++ str "”: “" + ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty) + ++ str "” is not a class") + ) + +let declare_instance ?(warn = false) info local glob = let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); add_instance (new_instance tc info (not local) glob) - | None -> () + | None -> if warn then warning_not_a_class (glob, ty) let add_class cl = add_class cl; List.iter (fun (n, inst, body) -> - match inst with - | Some (Backward, info) -> - (match body with - | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") - | Some b -> declare_instance (Some info) false (ConstRef b)) - | _ -> ()) - cl.cl_projs + match inst with + | Some (Backward, info) -> + (match body with + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") + | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b)) + | _ -> ()) + cl.cl_projs - (* * interface functions *) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8bdac0a575..d00195678b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -133,7 +133,10 @@ val remove_instance_hint : GlobRef.t -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : hint_info option -> bool -> GlobRef.t -> unit +(** Declares the given global reference as an instance of its type. + Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — + when said type is not a registered type class. *) +val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit (** Build the subinstances hints for a given typeclass object. |