aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/globnames.ml7
-rw-r--r--library/globnames.mli7
-rw-r--r--library/goptions.ml114
-rw-r--r--library/goptions.mli38
-rw-r--r--library/lib.ml2
-rw-r--r--library/lib.mli3
-rw-r--r--library/libobject.ml37
-rw-r--r--library/libobject.mli18
-rw-r--r--library/nametab.ml14
9 files changed, 209 insertions, 31 deletions
diff --git a/library/globnames.ml b/library/globnames.ml
index 9126a467bf..bc24fbf096 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -117,3 +117,10 @@ module ExtRefOrdered = struct
| SynDef kn -> combinesmall 2 (KerName.hash kn)
end
+
+module ExtRefMap = HMap.Make(ExtRefOrdered)
+module ExtRefSet = ExtRefMap.Set
+
+let subst_extended_reference sub = function
+ | SynDef kn -> SynDef (subst_kn sub kn)
+ | TrueGlobal gr -> TrueGlobal (subst_global_reference sub gr)
diff --git a/library/globnames.mli b/library/globnames.mli
index fb1583e16c..8acea5ef28 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -61,3 +61,10 @@ module ExtRefOrdered : sig
val equal : t -> t -> bool
val hash : t -> int
end
+
+module ExtRefSet : CSig.SetS with type elt = extended_global_reference
+module ExtRefMap : CMap.ExtS
+ with type key = extended_global_reference
+ and module Set := ExtRefSet
+
+val subst_extended_reference : substitution -> extended_global_reference -> extended_global_reference
diff --git a/library/goptions.ml b/library/goptions.ml
index 75eef5b411..666ba8ee2e 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -24,6 +24,10 @@ type option_value =
| StringValue of string
| StringOptValue of string option
+type table_value =
+ | StringRefValue of string
+ | QualidRefValue of qualid
+
(** Summary of an option status *)
type option_state = {
opt_depr : bool;
@@ -35,8 +39,13 @@ type option_state = {
let nickname table = String.concat " " table
+let error_no_table_of_this_type ~kind key =
+ user_err ~hdr:"Goptions"
+ (str ("There is no " ^ kind ^ "-valued table with this name: \"" ^ nickname key ^ "\"."))
+
let error_undeclared_key key =
- user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type")
+ user_err ~hdr:"Goptions"
+ (str ("There is no flag, option or table with this name: \"" ^ nickname key ^ "\"."))
(****************************************************************************)
(* 1- Tables *)
@@ -90,7 +99,7 @@ module MakeTable =
let inGo : option_mark * A.t -> obj =
Libobject.declare_object {(Libobject.default_object nick) with
Libobject.load_function = load_options;
- Libobject.open_function = load_options;
+ Libobject.open_function = simple_open load_options;
Libobject.cache_function = cache_options;
Libobject.subst_function = subst_options;
Libobject.classify_function = (fun x -> Substitute x)}
@@ -184,6 +193,23 @@ end
module MakeRefTable =
functor (A : RefConvertArg) -> MakeTable (RefConvert(A))
+type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit }
+
+let iter_table f key lv =
+ let aux = function
+ | StringRefValue s ->
+ begin
+ try f.aux (get_string_table key) (Global.env()) s
+ with Not_found -> error_no_table_of_this_type ~kind:"string" key
+ end
+ | QualidRefValue locqid ->
+ begin
+ try f.aux (get_ref_table key) (Global.env()) locqid
+ with Not_found -> error_no_table_of_this_type ~kind:"qualid" key
+ end
+ in
+ List.iter aux lv
+
(****************************************************************************)
(* 2- Flags. *)
@@ -262,7 +288,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
declare_object
{ (default_object (nickname key)) with
load_function = load_options;
- open_function = open_options;
+ open_function = simple_open open_options;
cache_function = cache_options;
subst_function = subst_options;
discharge_function = discharge_options;
@@ -296,6 +322,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,14 +375,48 @@ 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 *)
let warn_unknown_option =
- CWarnings.create ~name:"unknown-option" ~category:"option"
- (fun key -> strbrk "There is no option " ++
- str (nickname key) ++ str ".")
+ CWarnings.create
+ ~name:"unknown-option" ~category:"option"
+ (fun key -> strbrk "There is no flag or option with this name: \"" ++
+ str (nickname key) ++ str "\".")
let set_option_value ?(locality = OptDefault) check_and_cast key v =
let opt = try Some (get_option key) with Not_found -> None in
diff --git a/library/goptions.mli b/library/goptions.mli
index 8fcc258d47..150954cbac 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 } *)
@@ -168,6 +187,10 @@ type option_value =
| StringValue of string
| StringOptValue of string option
+type table_value =
+ | StringRefValue of string
+ | QualidRefValue of qualid
+
val set_option_value : ?locality:option_locality ->
('a -> option_value -> option_value) -> option_name -> 'a -> unit
(** [set_option_value ?locality f name v] sets [name] to the result of
@@ -185,4 +208,7 @@ type option_state = {
val get_tables : unit -> option_state OptionMap.t
val print_tables : unit -> Pp.t
+type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit }
+val iter_table : iter_table_aux -> option_name -> table_value list -> unit
+
val error_undeclared_key : option_name -> 'a
diff --git a/library/lib.ml b/library/lib.ml
index e7e6dc640a..830777003b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -46,7 +46,7 @@ let iter_objects f i prefix =
List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
let load_atomic_objects i pr = iter_objects load_object i pr
-let open_atomic_objects i pr = iter_objects open_object i pr
+let open_atomic_objects f i pr = iter_objects (open_object f) i pr
let subst_atomic_objects subst seg =
let subst_one = fun (id,obj as node) ->
diff --git a/library/lib.mli b/library/lib.mli
index 949b5e26c2..56ea35ec60 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -35,7 +35,8 @@ type lib_objects = (Id.t * Libobject.t) list
(** {6 Object iteration functions. } *)
-val open_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit
+val open_atomic_objects : Libobject.open_filter
+ -> int -> Nametab.object_prefix -> lib_atomic_objects -> unit
val load_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit
val subst_atomic_objects : Mod_subst.substitution -> lib_atomic_objects -> lib_atomic_objects
(*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
diff --git a/library/libobject.ml b/library/libobject.ml
index 0681e12449..c38e0d891b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -18,11 +18,36 @@ type 'a substitutivity =
type object_name = Libnames.full_path * Names.KerName.t
+module NSet = Globnames.ExtRefSet
+
+type open_filter =
+ | Unfiltered
+ | Names of NSet.t
+
+let simple_open f filter i o = match filter with
+ | Unfiltered -> f i o
+ | Names _ -> ()
+
+let filter_and f1 f2 = match f1, f2 with
+ | Unfiltered, f | f, Unfiltered -> Some f
+ | Names n1, Names n2 ->
+ let n = NSet.inter n1 n2 in
+ if NSet.is_empty n then None
+ else Some (Names n)
+
+let filter_or f1 f2 = match f1, f2 with
+ | Unfiltered, f | f, Unfiltered -> Unfiltered
+ | Names n1, Names n2 -> Names (NSet.union n1 n2)
+
+let in_filter_ref gr = function
+ | Unfiltered -> true
+ | Names ns -> NSet.mem (Globnames.TrueGlobal gr) ns
+
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
load_function : int -> object_name * 'a -> unit;
- open_function : int -> object_name * 'a -> unit;
+ open_function : open_filter -> int -> object_name * 'a -> unit;
classify_function : 'a -> 'a substitutivity;
subst_function : Mod_subst.substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
@@ -32,7 +57,7 @@ let default_object s = {
object_name = s;
cache_function = (fun _ -> ());
load_function = (fun _ _ -> ());
- open_function = (fun _ _ -> ());
+ open_function = (fun _ _ _ -> ());
subst_function = (fun _ ->
CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
classify_function = (fun atomic_obj -> Keep atomic_obj);
@@ -75,7 +100,7 @@ and t =
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
- | ExportObject of { mpl : ModPath.t list }
+ | ExportObject of { mpl : (open_filter * ModPath.t) list }
| AtomicObject of obj
and objects = (Names.Id.t * t) list
@@ -105,9 +130,9 @@ let load_object i (sp, Dyn.Dyn (tag, v)) =
let decl = DynMap.find tag !cache_tab in
decl.load_function i (sp, v)
-let open_object i (sp, Dyn.Dyn (tag, v)) =
+let open_object f i (sp, Dyn.Dyn (tag, v)) =
let decl = DynMap.find tag !cache_tab in
- decl.open_function i (sp, v)
+ decl.open_function f i (sp, v)
let subst_object (subs, Dyn.Dyn (tag, v)) =
let decl = DynMap.find tag !cache_tab in
@@ -147,7 +172,7 @@ let global_object_nodischarge s ~cache ~subst =
let import i o = if Int.equal i 1 then cache o in
{ (default_object s) with
cache_function = cache;
- open_function = import;
+ open_function = simple_open import;
subst_function = (match subst with
| None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
| Some subst -> subst;
diff --git a/library/libobject.mli b/library/libobject.mli
index 24cadc2223..1c82349bb6 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -72,16 +72,28 @@ type 'a substitutivity =
type object_name = full_path * Names.KerName.t
+type open_filter = Unfiltered | Names of Globnames.ExtRefSet.t
+
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
load_function : int -> object_name * 'a -> unit;
- open_function : int -> object_name * 'a -> unit;
+ open_function : open_filter -> int -> object_name * 'a -> unit;
classify_function : 'a -> 'a substitutivity;
subst_function : substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
rebuild_function : 'a -> 'a }
+val simple_open : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit
+(** Combinator for making objects which are only opened by unfiltered Import *)
+
+val filter_and : open_filter -> open_filter -> open_filter option
+(** Returns [None] when the intersection is empty. *)
+
+val filter_or : open_filter -> open_filter -> open_filter
+
+val in_filter_ref : Names.GlobRef.t -> open_filter -> bool
+
(** The default object is a "Keep" object with empty methods.
Object creators are advised to use the construction
[{(default_object "MY_OBJECT") with
@@ -114,7 +126,7 @@ and t =
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
- | ExportObject of { mpl : Names.ModPath.t list }
+ | ExportObject of { mpl : (open_filter * Names.ModPath.t) list }
| AtomicObject of obj
and objects = (Names.Id.t * t) list
@@ -129,7 +141,7 @@ val declare_object :
val cache_object : object_name * obj -> unit
val load_object : int -> object_name * obj -> unit
-val open_object : int -> object_name * obj -> unit
+val open_object : open_filter -> int -> object_name * obj -> unit
val subst_object : substitution * obj -> obj
val classify_object : obj -> obj substitutivity
val discharge_object : object_name * obj -> obj option
diff --git a/library/nametab.ml b/library/nametab.ml
index 523fe8af50..d9b4dc9122 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -352,10 +352,8 @@ let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
(* Reversed name tables ***************************************************)
(* This table translates extended_global_references back to section paths *)
-module Globrevtab = HMap.Make(ExtRefOrdered)
-
-type globrevtab = full_path Globrevtab.t
-let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab)
+type globrevtab = full_path ExtRefMap.t
+let the_globrevtab = Summary.ref ~name:"globrevtab" (ExtRefMap.empty : globrevtab)
type mprevtab = DirPath.t MPmap.t
@@ -386,7 +384,7 @@ let push_xref visibility sp xref =
match visibility with
| Until _ ->
the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
- the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+ the_globrevtab := ExtRefMap.add xref sp !the_globrevtab
| _ ->
begin
if ExtRefTab.exists sp !the_ccitab then
@@ -520,7 +518,7 @@ let path_of_global ref =
let open GlobRef in
match ref with
| VarRef id -> make_path DirPath.empty id
- | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
+ | _ -> ExtRefMap.find (TrueGlobal ref) !the_globrevtab
let dirpath_of_global ref =
fst (repr_path (path_of_global ref))
@@ -529,7 +527,7 @@ let basename_of_global ref =
snd (repr_path (path_of_global ref))
let path_of_syndef kn =
- Globrevtab.find (SynDef kn) !the_globrevtab
+ ExtRefMap.find (SynDef kn) !the_globrevtab
let dirpath_of_module mp =
MPmap.find mp !the_modrevtab
@@ -547,7 +545,7 @@ let shortest_qualid_of_global ?loc ctx ref =
match ref with
| VarRef id -> make_qualid ?loc DirPath.empty id
| _ ->
- let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
+ let sp = ExtRefMap.find (TrueGlobal ref) !the_globrevtab in
ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
let shortest_qualid_of_syndef ?loc ctx kn =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 04:23:19 +0000