aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml6
-rw-r--r--pretyping/cbv.ml19
-rw-r--r--pretyping/classops.ml20
-rw-r--r--pretyping/coercion.ml22
-rw-r--r--pretyping/detyping.ml16
-rw-r--r--pretyping/evarconv.ml14
-rw-r--r--pretyping/inferCumulativity.ml4
-rw-r--r--pretyping/pretyping.ml16
-rw-r--r--pretyping/program.ml6
-rw-r--r--pretyping/reductionops.ml28
-rw-r--r--pretyping/typeclasses.ml51
-rw-r--r--pretyping/typeclasses.mli5
-rw-r--r--pretyping/unification.ml28
13 files changed, 113 insertions, 122 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e02fb33276..fe67f5767b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -995,7 +995,7 @@ let expand_arg tms (p,ccl) ((_,t),_,na) =
let use_unit_judge env evd =
let j, ctx = coq_unit_judge !!env in
- let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in
+ let evd' = Evd.merge_context_set Evd.univ_flexible evd ctx in
evd', j
let add_assert_false_case pb tomatch =
@@ -2037,7 +2037,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
| None ->
(* No type constraint: we first create a generic evar type constraint *)
let src = (loc, Evar_kinds.CasesType false) in
- let sigma, (t, _) = Evarutil.new_type_evar !!env sigma univ_flexible_alg ~src in
+ let sigma, (t, _) = Evarutil.new_type_evar !!env sigma univ_flexible ~src in
sigma, t in
(* First strategy: we build an "inversion" predicate, also replacing the *)
(* dependencies with existential variables *)
@@ -2061,7 +2061,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
| Some rtntyp ->
(* We extract the signature of the arity *)
let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
- let sigma, newt = new_sort_variable univ_flexible_alg sigma in
+ let sigma, newt = new_sort_variable univ_flexible sigma in
let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in
let predccl = nf_evar sigma predcclj.uj_val in
[sigma, predccl, building_arsign]
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 5061aeff88..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 {
- Goptions.optdepr = false;
- Goptions.optname = "cbv visited constants display";
- Goptions.optkey = ["Debug";"Cbv"];
- Goptions.optread = (fun () -> !debug_cbv);
- Goptions.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 2c2a8fe49e..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 e21c2fda85..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
@@ -183,7 +179,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
with UnableToUnify _ ->
let (n, eqT), restT = dest_prod typ in
let (n', eqT'), restT' = dest_prod typ' in
- let _ =
+ let () =
try evdref := the_conv_x_leq env eqT eqT' !evdref
with UnableToUnify _ -> raise NoSubtacCoercion
in
@@ -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/detyping.ml b/pretyping/detyping.ml
index 072ac9deed..33ced6d6e0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -138,7 +138,7 @@ open Goptions
let wildcard_value = ref true
let force_wildcard () = !wildcard_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "forced wildcard";
optkey = ["Printing";"Wildcard"];
@@ -148,7 +148,7 @@ let _ = declare_bool_option
let synth_type_value = ref true
let synthetize_type () = !synth_type_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "pattern matching return type synthesizability";
optkey = ["Printing";"Synth"];
@@ -158,7 +158,7 @@ let _ = declare_bool_option
let reverse_matching_value = ref true
let reverse_matching () = !reverse_matching_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "pattern-matching reversibility";
optkey = ["Printing";"Matching"];
@@ -168,7 +168,7 @@ let _ = declare_bool_option
let print_primproj_params_value = ref false
let print_primproj_params () = !print_primproj_params_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "printing of primitive projection parameters";
optkey = ["Printing";"Primitive";"Projection";"Parameters"];
@@ -178,7 +178,7 @@ let _ = declare_bool_option
let print_primproj_compatibility_value = ref false
let print_primproj_compatibility () = !print_primproj_compatibility_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "backwards-compatible printing of primitive projections";
optkey = ["Printing";"Primitive";"Projection";"Compatibility"];
@@ -257,8 +257,7 @@ let lookup_index_as_renamed env sigma t n =
let print_factorize_match_patterns = ref true
-let _ =
- let open Goptions in
+let () =
declare_bool_option
{ optdepr = false;
optname = "factorization of \"match\" patterns in printing";
@@ -268,8 +267,7 @@ let _ =
let print_allow_match_default_clause = ref true
-let _ =
- let open Goptions in
+let () =
declare_bool_option
{ optdepr = false;
optname = "possible use of \"match\" default pattern in printing";
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f370ad7ae2..6c268de3b3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -33,14 +33,14 @@ type unify_fun = TransparentState.t ->
env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
let debug_unification = ref (false)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname =
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
"Print states sent to Evarconv unification";
- Goptions.optkey = ["Debug";"Unification"];
- Goptions.optread = (fun () -> !debug_unification);
- Goptions.optwrite = (fun a -> debug_unification:=a);
-}
+ optkey = ["Debug";"Unification"];
+ optread = (fun () -> !debug_unification);
+ optwrite = (fun a -> debug_unification:=a);
+})
(*******************************************)
(* Functions to deal with impossible cases *)
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index 9762d0f1d9..e46d03b743 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -110,9 +110,9 @@ let rec infer_fterm cv_pb infos variances hd stk =
let (_,ty,bd) = destFLambda mk_clos hd in
let variances = infer_fterm CONV infos variances ty [] in
infer_fterm CONV infos variances bd []
- | FProd (_,dom,codom) ->
+ | FProd (_,dom,codom,e) ->
let variances = infer_fterm CONV infos variances dom [] in
- infer_fterm cv_pb infos variances codom []
+ infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) []
| FInd (ind, u) ->
let variances =
if Instance.is_empty u then variances
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index abf52d2893..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/program.ml b/pretyping/program.ml
index bbabbefdc3..7e38c09189 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -75,7 +75,7 @@ let is_program_cases () = !program_cases
open Goptions
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "preferred transparency of Program obligations";
@@ -83,7 +83,7 @@ let _ =
optread = get_proofs_transparency;
optwrite = set_proofs_transparency; }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "program cases";
@@ -91,7 +91,7 @@ let _ =
optread = (fun () -> !program_cases);
optwrite = (:=) program_cases }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "program generalized coercion";
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e632976ae5..a57ee6e292 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,14 +29,14 @@ exception Elimconst
their parameters in its stack.
*)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname =
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
"Generate weak constraints between Irrelevant universes";
- Goptions.optkey = ["Cumulativity";"Weak";"Constraints"];
- Goptions.optread = (fun () -> not !UState.drop_weak_constraints);
- Goptions.optwrite = (fun a -> UState.drop_weak_constraints:=not a);
-}
+ optkey = ["Cumulativity";"Weak";"Constraints"];
+ optread = (fun () -> not !UState.drop_weak_constraints);
+ optwrite = (fun a -> UState.drop_weak_constraints:=not a);
+})
(** Support for reduction effects *)
@@ -830,14 +830,14 @@ let fix_recarg ((recindices,bodynum),_) stack =
*)
let debug_RAKAM = ref (false)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname =
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
"Print states of the Reductionops abstract machine";
- Goptions.optkey = ["Debug";"RAKAM"];
- Goptions.optread = (fun () -> !debug_RAKAM);
- Goptions.optwrite = (fun a -> debug_RAKAM:=a);
-}
+ optkey = ["Debug";"RAKAM"];
+ optread = (fun () -> !debug_RAKAM);
+ optwrite = (fun a -> debug_RAKAM:=a);
+})
let equal_stacks sigma (x, l) (y, l') =
let f_equal x y = eq_constr sigma x y in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4aea2c3db9..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.
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8c1aae26ae..094fcd923e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -43,25 +43,25 @@ module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname = "Unification is keyed";
- Goptions.optkey = ["Keyed";"Unification"];
- Goptions.optread = (fun () -> !keyed_unification);
- Goptions.optwrite = (fun a -> keyed_unification:=a);
-}
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname = "Unification is keyed";
+ 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 {
- Goptions.optdepr = false;
- Goptions.optname =
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
"Print states sent to tactic unification";
- Goptions.optkey = ["Debug";"Tactic";"Unification"];
- Goptions.optread = (fun () -> !debug_unification);
- Goptions.optwrite = (fun a -> debug_unification:=a);
-}
+ optkey = ["Debug";"Tactic";"Unification"];
+ optread = (fun () -> !debug_unification);
+ optwrite = (fun a -> debug_unification:=a);
+})
(** Making this unification algorithm correct w.r.t. the evar-map abstraction
breaks too much stuff. So we redefine incorrect functions here. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 10:29:23 +0000