aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/values.ml13
-rw-r--r--interp/notation.ml7
-rw-r--r--interp/syntax_def.ml2
-rw-r--r--library/globnames.ml4
-rw-r--r--library/globnames.mli2
-rw-r--r--library/goptions.ml4
-rw-r--r--library/lib.ml2
-rw-r--r--library/lib.mli3
-rw-r--r--library/libobject.ml35
-rw-r--r--library/libobject.mli18
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacenv.ml2
-rw-r--r--plugins/ltac/tactic_option.ml2
-rw-r--r--tactics/declare.ml2
-rw-r--r--tactics/hints.ml2
-rw-r--r--user-contrib/Ltac2/tac2entries.ml14
-rw-r--r--vernac/canonical.ml2
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comCoercion.ml2
-rw-r--r--vernac/declareInd.ml2
-rw-r--r--vernac/declareUniv.ml2
-rw-r--r--vernac/declaremods.ml133
-rw-r--r--vernac/declaremods.mli4
-rw-r--r--vernac/library.ml27
-rw-r--r--vernac/metasyntax.ml11
-rw-r--r--vernac/vernacentries.ml2
26 files changed, 199 insertions, 104 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 12f7135cdf..b9efce6948 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -372,6 +372,17 @@ let v_compiled_lib =
let v_obj = Dyn
+let v_globref = Sum("globref",0,[|
+ [|v_id|];
+ [|v_cst|];
+ [|v_ind|];
+ [|v_cons|]
+ |])
+
+let v_ext_gref = Sum("extended_global_reference",0,[|[|v_globref|];[|v_kn|]|])
+
+let v_open_filter = Sum ("open_filter",1,[|[|v_hset v_ext_gref|]|])
+
let rec v_aobjs = Sum("algebraic_objects", 0,
[| [|v_libobjs|];
[|v_mp;v_subst|]
@@ -383,7 +394,7 @@ and v_libobjt = Sum("Libobject.t",0,
[| v_substobjs |];
[| v_aobjs |];
[| v_libobjs |];
- [| List v_mp |];
+ [| List (v_pair v_open_filter v_mp)|];
[| v_obj |]
|])
diff --git a/interp/notation.ml b/interp/notation.ml
index 6291a88bb0..0afbb9cd62 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -206,7 +206,7 @@ let classify_scope (local,_,_ as o) =
let inScope : bool * bool * scope_item -> obj =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
- open_function = open_scope;
+ open_function = simple_open open_scope;
subst_function = subst_scope;
discharge_function = discharge_scope;
classify_function = classify_scope }
@@ -980,9 +980,12 @@ let subst_prim_token_interpretation (subs,infos) =
let classify_prim_token_interpretation infos =
if infos.pt_local then Dispose else Substitute infos
+let open_prim_token_interpretation i o =
+ if Int.equal i 1 then cache_prim_token_interpretation o
+
let inPrimTokenInterp : prim_token_infos -> obj =
declare_object {(default_object "PRIM-TOKEN-INTERP") with
- open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
+ open_function = simple_open open_prim_token_interpretation;
cache_function = cache_prim_token_interpretation;
subst_function = subst_prim_token_interpretation;
classify_function = classify_prim_token_interpretation}
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 767c69e3b6..d6aa527f4d 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -71,7 +71,7 @@ let in_syntax_constant : (bool * syndef) -> obj =
declare_object {(default_object "SYNDEF") with
cache_function = cache_syntax_constant;
load_function = load_syntax_constant;
- open_function = open_syntax_constant;
+ open_function = todo_filter open_syntax_constant;
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant }
diff --git a/library/globnames.ml b/library/globnames.ml
index 5dbc8db647..bc24fbf096 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -120,3 +120,7 @@ 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 f5ed3a3ec7..8acea5ef28 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -66,3 +66,5 @@ 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..1418407533 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -90,7 +90,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)}
@@ -262,7 +262,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;
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..392a64e5d0 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -18,11 +18,34 @@ 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 todo_filter = simple_open
+
+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)
+
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 +55,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 +98,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 +128,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 +170,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..27b47264a6 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 todo_filter : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit
+
(** 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/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4127d28bae..9910796d9c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -299,7 +299,7 @@ let classify_tactic_notation tacobj = Substitute tacobj
let inTacticGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "TacticGrammar") with
- open_function = open_tactic_notation;
+ open_function = simple_open open_tactic_notation;
load_function = load_tactic_notation;
cache_function = cache_tactic_notation;
subst_function = subst_tactic_notation;
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index ce9189792e..76d47f5482 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -182,7 +182,7 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
- open_function = open_md;
+ open_function = simple_open open_md;
subst_function = subst_md;
classify_function = classify_md}
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index 4f00f17892..922d2f7792 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -32,7 +32,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
{ (default_object name) with
cache_function = cache;
load_function = (fun _ -> load);
- open_function = (fun _ -> load);
+ open_function = simple_open (fun _ -> load);
classify_function = (fun (local, tac) ->
if local then Dispose else Substitute (local, tac));
subst_function = subst}
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 324007930a..38f6db2db3 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -135,7 +135,7 @@ let (objConstant : constant_obj Libobject.Dyn.tag) =
declare_object_full { (default_object "CONSTANT") with
cache_function = cache_constant;
load_function = load_constant;
- open_function = open_constant;
+ open_function = todo_filter open_constant;
classify_function = classify_constant;
subst_function = ident_subst_function;
discharge_function = discharge_constant }
diff --git a/tactics/hints.ml b/tactics/hints.ml
index f8a46fcb1d..2118b4f231 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1163,7 +1163,7 @@ let inAutoHint : hint_obj -> obj =
declare_object {(default_object "AUTOHINT") with
cache_function = cache_autohint;
load_function = load_autohint;
- open_function = open_autohint;
+ open_function = simple_open open_autohint;
subst_function = subst_autohint;
classify_function = classify_autohint; }
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index ebc63ddd01..3e920fcc2d 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -91,7 +91,7 @@ let inTacDef : tacdef -> obj =
declare_object {(default_object "TAC2-DEFINITION") with
cache_function = cache_tacdef;
load_function = load_tacdef;
- open_function = open_tacdef;
+ open_function = simple_open open_tacdef;
subst_function = subst_tacdef;
classify_function = classify_tacdef}
@@ -198,7 +198,7 @@ let inTypDef : typdef -> obj =
declare_object {(default_object "TAC2-TYPE-DEFINITION") with
cache_function = cache_typdef;
load_function = load_typdef;
- open_function = open_typdef;
+ open_function = simple_open open_typdef;
subst_function = subst_typdef;
classify_function = classify_typdef}
@@ -268,7 +268,7 @@ let inTypExt : typext -> obj =
declare_object {(default_object "TAC2-TYPE-EXTENSION") with
cache_function = cache_typext;
load_function = load_typext;
- open_function = open_typext;
+ open_function = simple_open open_typext;
subst_function = subst_typext;
classify_function = classify_typext}
@@ -664,7 +664,7 @@ let classify_synext o =
let inTac2Notation : synext -> obj =
declare_object {(default_object "TAC2-NOTATION") with
cache_function = cache_synext;
- open_function = open_synext;
+ open_function = simple_open open_synext;
subst_function = subst_synext;
classify_function = classify_synext}
@@ -694,7 +694,7 @@ let inTac2Abbreviation : abbreviation -> obj =
declare_object {(default_object "TAC2-ABBREVIATION") with
cache_function = cache_abbreviation;
load_function = load_abbreviation;
- open_function = open_abbreviation;
+ open_function = simple_open open_abbreviation;
subst_function = subst_abbreviation;
classify_function = classify_abbreviation}
@@ -747,7 +747,7 @@ let classify_redefinition o = Substitute o
let inTac2Redefinition : redefinition -> obj =
declare_object {(default_object "TAC2-REDEFINITION") with
cache_function = perform_redefinition;
- open_function = (fun _ -> perform_redefinition);
+ open_function = simple_open (fun _ -> perform_redefinition);
subst_function = subst_redefinition;
classify_function = classify_redefinition }
@@ -962,7 +962,7 @@ let inTac2Init : unit -> obj =
declare_object {(default_object "TAC2-INIT") with
cache_function = cache_ltac2_init;
load_function = load_ltac2_init;
- open_function = open_ltac2_init;
+ open_function = simple_open open_ltac2_init;
}
let _ = Mltop.declare_cache_obj begin fun () ->
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index 390ed62bee..eaa6c84791 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -28,7 +28,7 @@ let discharge_canonical_structure (_,((gref, _ as x), local)) =
let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
declare_object {(default_object "CANONICAL-STRUCTURE") with
- open_function = open_canonical_structure;
+ open_function = simple_open open_canonical_structure;
cache_function = cache_canonical_structure;
subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local);
classify_function = (fun x -> Substitute x);
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3d38713e09..a9425b15d2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -116,7 +116,7 @@ let instance_input : instance -> obj =
{ (default_object "type classes instances state") with
cache_function = cache_instance;
load_function = (fun _ x -> cache_instance x);
- open_function = (fun _ x -> cache_instance x);
+ open_function = simple_open (fun _ x -> cache_instance x);
classify_function = classify_instance;
discharge_function = discharge_instance;
rebuild_function = rebuild_instance;
@@ -237,7 +237,7 @@ let class_input : typeclass -> obj =
{ (default_object "type classes state") with
cache_function = cache_class;
load_function = (fun _ -> cache_class);
- open_function = (fun _ -> cache_class);
+ open_function = simple_open (fun _ -> cache_class);
classify_function = (fun x -> Substitute x);
discharge_function = (fun a -> Some (discharge_class a));
rebuild_function = rebuild_class;
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index c339c53a9b..4a8e217fc1 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -256,7 +256,7 @@ let classify_coercion obj =
let inCoercion : coercion -> obj =
declare_object {(default_object "COERCION") with
- open_function = open_coercion;
+ open_function = simple_open open_coercion;
cache_function = cache_coercion;
subst_function = (fun (subst,c) -> subst_coercion subst c);
classify_function = classify_coercion;
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 2610f16d92..203e11d6ab 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -65,7 +65,7 @@ let objInductive : inductive_obj Libobject.Dyn.tag =
declare_object_full {(default_object "INDUCTIVE") with
cache_function = cache_inductive;
load_function = load_inductive;
- open_function = open_inductive;
+ open_function = todo_filter open_inductive;
classify_function = (fun a -> Substitute a);
subst_function = ident_subst_function;
discharge_function = discharge_inductive;
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 300dfe6c35..20fa43c8e7 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -56,7 +56,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
{ (default_object "Global universe name state") with
cache_function = cache_univ_names;
load_function = load_univ_names;
- open_function = open_univ_names;
+ open_function = simple_open open_univ_names;
discharge_function = discharge_univ_names;
subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 4f527b73d0..b87d3c5681 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -81,6 +81,19 @@ module ModSubstObjs :
let sobjs_no_functor (mbids,_) = List.is_empty mbids
+let subst_filtered sub (f,mp) =
+ let f = match f with
+ | Unfiltered -> Unfiltered
+ | Names ns ->
+ let module NSet = Globnames.ExtRefSet in
+ let ns =
+ NSet.fold (fun n ns -> NSet.add (Globnames.subst_extended_reference sub n) ns)
+ ns NSet.empty
+ in
+ Names ns
+ in
+ f, subst_mp sub mp
+
let rec subst_aobjs sub = function
| Objs o as objs ->
let o' = subst_objects sub o in
@@ -109,7 +122,7 @@ and subst_objects subst seg =
let aobjs' = subst_aobjs subst aobjs in
if aobjs' == aobjs then node else (id, IncludeObject aobjs')
| ExportObject { mpl } ->
- let mpl' = List.map (subst_mp subst) mpl in
+ let mpl' = List.Smart.map (subst_filtered subst) mpl in
if mpl'==mpl then node else (id, ExportObject { mpl = mpl' })
| KeepObject _ -> assert false
in
@@ -285,86 +298,104 @@ and load_keep i ((sp,kn),kobjs) =
(** {6 Implementation of Import and Export commands} *)
-let mark_object obj (exports,acc) =
- (exports, obj::acc)
+let mark_object f obj (exports,acc) =
+ (exports, (f,obj)::acc)
-let rec collect_module_objects mp acc =
+let rec collect_module_objects (f,mp) acc =
(* May raise Not_found for unknown module and for functors *)
let modobjs = ModObjs.get mp in
let prefix = modobjs.module_prefix in
- let acc = collect_objects 1 prefix modobjs.module_keep_objects acc in
- collect_objects 1 prefix modobjs.module_substituted_objects acc
+ let acc = collect_objects f 1 prefix modobjs.module_keep_objects acc in
+ collect_objects f 1 prefix modobjs.module_substituted_objects acc
-and collect_object i (name, obj as o) acc =
+and collect_object f i (name, obj as o) acc =
match obj with
- | ExportObject { mpl; _ } -> collect_export i mpl acc
+ | ExportObject { mpl } -> collect_export f i mpl acc
| AtomicObject _ | IncludeObject _ | KeepObject _
- | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc
+ | ModuleObject _ | ModuleTypeObject _ -> mark_object f o acc
+
+and collect_objects f i prefix objs acc =
+ List.fold_right (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc
+
+and collect_one_export f (f',mp) (exports,objs as acc) =
+ match filter_and f f' with
+ | None -> acc
+ | Some f ->
+ let exports' = MPmap.update mp (function
+ | None -> Some f
+ | Some f0 -> Some (filter_or f f0))
+ exports
+ in
+ (* If the map doesn't change there is nothing new to export.
-and collect_objects i prefix objs acc =
- List.fold_right (fun (id, obj) acc -> collect_object i (Lib.make_oname prefix id, obj) acc) objs acc
+ It's possible that [filter_and] or [filter_or] mangled precise
+ filters such that we repeat uselessly, but the important
+ [Unfiltered] case is handled correctly.
+ *)
+ if exports == exports' then acc
+ else
+ collect_module_objects (f,mp) (exports', objs)
-and collect_one_export mp (exports,objs as acc) =
- if not (MPset.mem mp exports) then
- collect_module_objects mp (MPset.add mp exports, objs)
- else acc
-and collect_export i mpl acc =
+and collect_export f i mpl acc =
if Int.equal i 1 then
- List.fold_right collect_one_export mpl acc
+ List.fold_right (collect_one_export f) mpl acc
else acc
-let rec open_object i (name, obj) =
+let open_modtype i ((sp,kn),_) =
+ let mp = mp_of_kn kn in
+ let mp' =
+ try Nametab.locate_modtype (qualid_of_path sp)
+ with Not_found ->
+ anomaly (pr_path sp ++ str " should already exist!");
+ in
+ assert (ModPath.equal mp mp');
+ Nametab.push_modtype (Nametab.Exactly i) sp mp
+
+let rec open_object f i (name, obj) =
match obj with
- | AtomicObject o -> Libobject.open_object i (name, o)
+ | AtomicObject o -> Libobject.open_object f i (name, o)
| ModuleObject sobjs ->
let dir = dir_of_sp (fst name) in
let mp = mp_of_kn (snd name) in
- open_module i dir mp sobjs
+ open_module f i dir mp sobjs
| ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
- | IncludeObject aobjs -> open_include i (name, aobjs)
- | ExportObject { mpl; _ } -> open_export i mpl
- | KeepObject objs -> open_keep i (name, objs)
+ | IncludeObject aobjs -> open_include f i (name, aobjs)
+ | ExportObject { mpl } -> open_export f i mpl
+ | KeepObject objs -> open_keep f i (name, objs)
-and open_module i obj_dir obj_mp sobjs =
+and open_module f i obj_dir obj_mp sobjs =
let prefix = Nametab.{ obj_dir ; obj_mp; } in
let dirinfo = Nametab.GlobDirRef.DirModule prefix in
consistency_checks true obj_dir dirinfo;
- Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
+ (match f with
+ | Unfiltered -> Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo
+ | Names _ -> ());
(* If we're not a functor, let's iter on the internal components *)
if sobjs_no_functor sobjs then begin
let modobjs = ModObjs.get obj_mp in
- open_objects (i+1) modobjs.module_prefix modobjs.module_substituted_objects
+ open_objects f (i+1) modobjs.module_prefix modobjs.module_substituted_objects
end
-and open_objects i prefix objs =
- List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs
-
-and open_modtype i ((sp,kn),_) =
- let mp = mp_of_kn kn in
- let mp' =
- try Nametab.locate_modtype (qualid_of_path sp)
- with Not_found ->
- anomaly (pr_path sp ++ str " should already exist!");
- in
- assert (ModPath.equal mp mp');
- Nametab.push_modtype (Nametab.Exactly i) sp mp
+and open_objects f i prefix objs =
+ List.iter (fun (id, obj) -> open_object f i (Lib.make_oname prefix id, obj)) objs
-and open_include i ((sp,kn), aobjs) =
+and open_include f i ((sp,kn), aobjs) =
let obj_dir = Libnames.dirpath sp in
let obj_mp = KerName.modpath kn in
let prefix = Nametab.{ obj_dir; obj_mp; } in
let o = expand_aobjs aobjs in
- open_objects i prefix o
+ open_objects f i prefix o
-and open_export i mpl =
- let _,objs = collect_export i mpl (MPset.empty, []) in
- List.iter (open_object 1) objs
+and open_export f i mpl =
+ let _ = todo_filter in (* exports will have their own filters! *)
+ let _,objs = collect_export f i mpl (MPmap.empty, []) in
+ List.iter (fun (f,o) -> open_object f 1 o) objs
-and open_keep i ((sp,kn),kobjs) =
+and open_keep f i ((sp,kn),kobjs) =
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
let prefix = Nametab.{ obj_dir; obj_mp; } in
- open_objects i prefix kobjs
+ open_objects f i prefix kobjs
let rec cache_object (name, obj) =
match obj with
@@ -383,7 +414,7 @@ and cache_include ((sp,kn), aobjs) =
let prefix = Nametab.{ obj_dir; obj_mp; } in
let o = expand_aobjs aobjs in
load_objects 1 prefix o;
- open_objects 1 prefix o
+ open_objects Unfiltered 1 prefix o
and cache_keep ((sp,kn),kobjs) =
anomaly (Pp.str "This module should not be cached!")
@@ -1023,12 +1054,12 @@ let end_library ?except ~output_native_objects dir =
cenv,(substitute,keep),ast
let import_modules ~export mpl =
- let _,objs = List.fold_right collect_module_objects mpl (MPset.empty, []) in
- List.iter (open_object 1) objs;
+ let _,objs = List.fold_right collect_module_objects mpl (MPmap.empty, []) in
+ List.iter (fun (f,o) -> open_object f 1 o) objs;
if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
-let import_module ~export mp =
- import_modules ~export [mp]
+let import_module f ~export mp =
+ import_modules ~export [f,mp]
(** {6 Iterators} *)
@@ -1073,6 +1104,6 @@ let debug_print_modtab _ =
let mod_ops = {
- Printmod.import_module = import_module;
+ Printmod.import_module = import_module Unfiltered;
process_module_binding = process_module_binding;
}
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli
index e37299aad6..5e45957e83 100644
--- a/vernac/declaremods.mli
+++ b/vernac/declaremods.mli
@@ -97,11 +97,11 @@ val append_end_library_hook : (unit -> unit) -> unit
or when [mp] corresponds to a functor. If [export] is [true], the module is also
opened every time the module containing it is. *)
-val import_module : export:bool -> ModPath.t -> unit
+val import_module : Libobject.open_filter -> export:bool -> ModPath.t -> unit
(** Same as [import_module] but for multiple modules, and more optimized than
iterating [import_module]. *)
-val import_modules : export:bool -> ModPath.t list -> unit
+val import_modules : export:bool -> (Libobject.open_filter * ModPath.t) list -> unit
(** Include *)
diff --git a/vernac/library.ml b/vernac/library.ml
index 1b0bd4c0f7..01f5101764 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -335,7 +335,11 @@ let load_require _ (_,(needed,modl,_)) =
List.iter register_library needed
let open_require i (_,(_,modl,export)) =
- Option.iter (fun export -> Declaremods.import_modules ~export @@ List.map (fun m -> MPfile m) modl) export
+ Option.iter (fun export ->
+ let mpl = List.map (fun m -> Unfiltered, MPfile m) modl in
+ (* TODO support filters in Require *)
+ Declaremods.import_modules ~export mpl)
+ export
(* [needed] is the ordered list of libraries not already loaded *)
let cache_require o =
@@ -370,16 +374,17 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPmap.empty) modrefl in
let needed = List.rev_map (fun dir -> DPmap.find dir contents) needed in
let modrefl = List.map fst modrefl in
- if Lib.is_module_or_modtype () then
- begin
- warn_require_in_module ();
- add_anonymous_leaf (in_require (needed,modrefl,None));
- Option.iter (fun export ->
- List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modrefl)
- export
- end
- else
- add_anonymous_leaf (in_require (needed,modrefl,export));
+ if Lib.is_module_or_modtype () then
+ begin
+ warn_require_in_module ();
+ add_anonymous_leaf (in_require (needed,modrefl,None));
+ Option.iter (fun export ->
+ (* TODO import filters *)
+ List.iter (fun m -> Declaremods.import_module Unfiltered ~export (MPfile m)) modrefl)
+ export
+ end
+ else
+ add_anonymous_leaf (in_require (needed,modrefl,export));
()
(************************************************************************)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 475d5c31f7..3b9c771b93 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -877,9 +877,12 @@ let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) =
let classify_syntax_definition (local, _ as o) =
if local then Dispose else Substitute o
+let open_syntax_extension i o =
+ if Int.equal i 1 then cache_syntax_extension o
+
let inSyntaxExtension : syntax_extension_obj -> obj =
declare_object {(default_object "SYNTAX-EXTENSION") with
- open_function = (fun i o -> if Int.equal i 1 then cache_syntax_extension o);
+ open_function = simple_open open_syntax_extension;
cache_function = cache_syntax_extension;
subst_function = subst_syntax_extension;
classify_function = classify_syntax_definition}
@@ -1454,7 +1457,7 @@ let classify_notation nobj =
let inNotation : notation_obj -> obj =
declare_object {(default_object "NOTATION") with
- open_function = open_notation;
+ open_function = simple_open open_notation;
cache_function = cache_notation;
subst_function = subst_notation;
load_function = load_notation;
@@ -1765,7 +1768,7 @@ let classify_scope_command (local, _, _ as o) =
let inScopeCommand : locality_flag * scope_name * scope_command -> obj =
declare_object {(default_object "DELIMITERS") with
cache_function = cache_scope_command;
- open_function = open_scope_command;
+ open_function = simple_open open_scope_command;
load_function = load_scope_command;
subst_function = subst_scope_command;
classify_function = classify_scope_command}
@@ -1831,7 +1834,7 @@ let classify_custom_entry (local,s as o) =
let inCustomEntry : locality_flag * string -> obj =
declare_object {(default_object "CUSTOM-ENTRIES") with
cache_function = cache_custom_entry;
- open_function = open_custom_entry;
+ open_function = simple_open open_custom_entry;
load_function = load_custom_entry;
subst_function = subst_custom_entry;
classify_function = classify_custom_entry}
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3195f339b6..de781109ef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -874,7 +874,7 @@ let vernac_constraint ~poly l =
let vernac_import export refl =
let import_mod qid =
- try Declaremods.import_module ~export @@ Nametab.locate_module qid
+ try Declaremods.import_module Libobject.Unfiltered ~export @@ Nametab.locate_module qid
with Not_found ->
CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:22:07 +0000