aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli3
-rw-r--r--library/globnames.ml7
-rw-r--r--library/globnames.mli7
-rw-r--r--library/goptions.ml67
-rw-r--r--library/goptions.mli7
-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
11 files changed, 128 insertions, 41 deletions
diff --git a/library/global.ml b/library/global.ml
index abc04a5e14..5c847fda96 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -99,7 +99,9 @@ let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c)
let set_check_positive c = globalize0 (Safe_typing.set_check_positive c)
let set_check_universes c = globalize0 (Safe_typing.set_check_universes c)
let typing_flags () = Environ.typing_flags (env ())
-let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
+let set_cumulative_sprop b =
+ set_typing_flags {(typing_flags()) with Declarations.cumulative_sprop = b}
+let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop
let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
let sprop_allowed () = Environ.sprop_allowed (env())
let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
diff --git a/library/global.mli b/library/global.mli
index e7133a1034..2acd7e2a67 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -36,7 +36,8 @@ val set_check_guarded : bool -> unit
val set_check_positive : bool -> unit
val set_check_universes : bool -> unit
val typing_flags : unit -> Declarations.typing_flags
-val make_sprop_cumulative : unit -> unit
+val set_cumulative_sprop : bool -> unit
+val is_cumulative_sprop : unit -> bool
val set_allow_sprop : bool -> unit
val sprop_allowed : unit -> bool
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 73132868d7..f096c5d749 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;
@@ -387,9 +413,10 @@ let declare_interpreted_string_option_and_ref ~depr ~key ~(value:'a) from_string
(* 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
@@ -398,38 +425,38 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v =
| Some (depr, (read,write,append)) ->
write locality (check_and_cast v (read ()))
-let show_value_type = function
- | BoolValue _ -> "bool"
- | IntValue _ -> "int"
- | StringValue _ -> "string"
- | StringOptValue _ -> "string"
-
-let bad_type_error opt_value actual_type =
+let bad_type_error ~expected ~got =
user_err Pp.(str "Bad type of value for this option:" ++ spc() ++
- str "expected " ++ str (show_value_type opt_value) ++
- str ", got " ++ str actual_type ++ str ".")
+ str "expected " ++ str expected ++
+ str ", got " ++ str got ++ str ".")
+
+let error_flag () =
+ user_err Pp.(str "This is a flag. It does not take a value.")
let check_int_value v = function
+ | BoolValue _ -> error_flag ()
| IntValue _ -> IntValue v
- | optv -> bad_type_error optv "int"
+ | StringValue _ | StringOptValue _ ->
+ bad_type_error ~expected:"string" ~got:"int"
let check_bool_value v = function
| BoolValue _ -> BoolValue v
- | optv -> bad_type_error optv "bool"
+ | _ -> user_err Pp.(str "This is an option. A value must be provided.")
let check_string_value v = function
+ | BoolValue _ -> error_flag ()
+ | IntValue _ -> bad_type_error ~expected:"int" ~got:"string"
| StringValue _ -> StringValue v
| StringOptValue _ -> StringOptValue (Some v)
- | optv -> bad_type_error optv "string"
let check_unset_value v = function
| BoolValue _ -> BoolValue false
| IntValue _ -> IntValue None
| StringOptValue _ -> StringOptValue None
- | optv -> bad_type_error optv "nothing"
+ | StringValue _ -> user_err Pp.(str "This option does not support the \"Unset\" command.")
(* Nota: For compatibility reasons, some errors are treated as
- warning. This allows a script to refer to an option that doesn't
+ warnings. This allows a script to refer to an option that doesn't
exist anymore *)
let set_int_option_value_gen ?locality =
diff --git a/library/goptions.mli b/library/goptions.mli
index 336cae420c..150954cbac 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -187,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
@@ -204,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-05-04 07:15:38 +0000