aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/global.ml6
-rw-r--r--library/global.mli7
-rw-r--r--library/globnames.ml12
-rw-r--r--library/globnames.mli6
-rw-r--r--library/goptions.ml32
-rw-r--r--library/goptions.mli5
-rw-r--r--library/lib.ml32
-rw-r--r--library/lib.mli6
-rw-r--r--library/libobject.ml111
-rw-r--r--library/libobject.mli8
-rw-r--r--library/states.ml2
-rw-r--r--library/summary.ml105
-rw-r--r--library/summary.mli2
13 files changed, 138 insertions, 196 deletions
diff --git a/library/global.ml b/library/global.ml
index d4262683bb..8706238f5a 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -90,7 +90,7 @@ let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
let push_named_def d = globalize0 (Safe_typing.push_named_def d)
let push_section_context c = globalize0 (Safe_typing.push_section_context c)
let add_constraints c = globalize0 (Safe_typing.add_constraints c)
-let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
+let push_context_set ~strict c = globalize0 (Safe_typing.push_context_set ~strict c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
@@ -192,8 +192,6 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r
let is_template_polymorphic r = is_template_polymorphic (env ()) r
-let is_template_checked r = is_template_checked (env ()) r
-
let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r
let is_type_in_type r = is_type_in_type (env ()) r
@@ -206,7 +204,7 @@ let current_dirpath () =
let with_global f =
let (a, ctx) = f (env ()) (current_dirpath ()) in
- push_context_set false ctx; a
+ push_context_set ~strict:true ctx; a
let register_inline c = globalize0 (Safe_typing.register_inline c)
let register_inductive c r = globalize0 (Safe_typing.register_inductive c r)
diff --git a/library/global.mli b/library/global.mli
index db0f87df7e..0198ac5952 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -47,8 +47,8 @@ val push_named_def : (Id.t * Entries.section_def_entry) -> unit
val push_section_context : (Name.t array * Univ.UContext.t) -> unit
val export_private_constants :
- Safe_typing.private_constants Entries.proof_output ->
- Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
+ Safe_typing.private_constants ->
+ Safe_typing.exported_private_constant list
val add_constant :
Id.t -> Safe_typing.global_declaration -> Constant.t
@@ -60,7 +60,7 @@ val add_mind :
(** Extra universe constraints *)
val add_constraints : Univ.Constraint.t -> unit
-val push_context_set : bool -> Univ.ContextSet.t -> unit
+val push_context_set : strict:bool -> Univ.ContextSet.t -> unit
(** Non-interactive modules and module types *)
@@ -150,7 +150,6 @@ val is_joined_environment : unit -> bool
val is_polymorphic : GlobRef.t -> bool
val is_template_polymorphic : GlobRef.t -> bool
-val is_template_checked : GlobRef.t -> bool
val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list
val is_type_in_type : GlobRef.t -> bool
diff --git a/library/globnames.ml b/library/globnames.ml
index acb05f9ac0..e55a7b5499 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -73,13 +73,7 @@ let global_of_constr c = match kind c with
| Var id -> VarRef id
| _ -> raise Not_found
-let is_global c t =
- match c, kind t with
- | ConstRef c, Const (c', _) -> Constant.equal c c'
- | IndRef i, Ind (i', _) -> eq_ind i i'
- | ConstructRef i, Construct (i', _) -> eq_constructor i i'
- | VarRef id, Var id' -> Id.equal id id'
- | _ -> false
+let is_global = Constr.isRefX
let printable_constr_of_global = function
| VarRef id -> mkVar id
@@ -123,7 +117,3 @@ module ExtRefOrdered = struct
| SynDef kn -> combinesmall 2 (KerName.hash kn)
end
-
-type global_reference_or_constr =
- | IsGlobal of GlobRef.t
- | IsConstr of constr
diff --git a/library/globnames.mli b/library/globnames.mli
index 48cbb11b66..fb59cbea4e 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -32,6 +32,7 @@ val destIndRef : GlobRef.t -> inductive
val destConstructRef : GlobRef.t -> constructor
val is_global : GlobRef.t -> constr -> bool
+[@@ocaml.deprecated "Use [Constr.isRefX] instead."]
val subst_constructor : substitution -> constructor -> constructor
val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
@@ -44,6 +45,7 @@ val printable_constr_of_global : GlobRef.t -> constr
(** Turn a construction denoting a global reference into a global reference;
raise [Not_found] if not a global reference *)
val global_of_constr : constr -> GlobRef.t
+[@@ocaml.deprecated "Use [Constr.destRef] instead (throws DestKO instead of Not_found)."]
(** {6 Extended global references } *)
@@ -59,7 +61,3 @@ module ExtRefOrdered : sig
val equal : t -> t -> bool
val hash : t -> int
end
-
-type global_reference_or_constr =
- | IsGlobal of GlobRef.t
- | IsConstr of constr
diff --git a/library/goptions.ml b/library/goptions.ml
index 6e53bed349..616f6edf72 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -27,7 +27,6 @@ type option_value =
(** Summary of an option status *)
type option_state = {
opt_depr : bool;
- opt_name : string;
opt_value : option_value;
}
@@ -190,7 +189,6 @@ module MakeRefTable =
type 'a option_sig = {
optdepr : bool;
- optname : string;
optkey : option_name;
optread : unit -> 'a;
optwrite : 'a -> unit }
@@ -229,7 +227,7 @@ let warn_deprecated_option =
strbrk " is deprecated")
let declare_option cast uncast append ?(preprocess = fun x -> x)
- { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
+ { optdepr=depr; optkey=key; optread=read; optwrite=write } =
check_key key;
let default = read() in
let change =
@@ -275,7 +273,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
let cread () = cast (read ()) in
let cwrite l v = warn (); change l OptSet (uncast v) in
let cappend l v = warn (); change l OptAppend (uncast v) in
- value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab
+ value_tab := OptionMap.add key (depr, (cread,cwrite,cappend)) !value_tab
let declare_int_option =
declare_option
@@ -298,13 +296,12 @@ let declare_stringopt_option =
(function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
(fun _ _ -> anomaly (Pp.str "async_option."))
-let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) =
+let declare_bool_option_and_ref ~depr ~key ~(value:bool) =
let r_opt = ref value in
let optwrite v = r_opt := v in
let optread () = !r_opt in
let _ = declare_bool_option {
optdepr = depr;
- optname = name;
optkey = key;
optread; optwrite
} in
@@ -323,7 +320,7 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (read,write,append)) ->
+ | Some (depr, (read,write,append)) ->
write locality (check_and_cast v (read ()))
let show_value_type = function
@@ -373,7 +370,7 @@ let set_string_option_append_value_gen ?(locality = OptDefault) key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (read,write,append)) ->
+ | Some (depr, (read,write,append)) ->
append locality (check_string_value v (read ()))
let set_int_option_value opt v = set_int_option_value_gen opt v
@@ -382,7 +379,7 @@ let set_string_option_value opt v = set_string_option_value_gen opt v
(* Printing options/tables *)
-let msg_option_value (name,v) =
+let msg_option_value v =
match v with
| BoolValue true -> str "on"
| BoolValue false -> str "off"
@@ -394,19 +391,18 @@ let msg_option_value (name,v) =
(* | IdentValue r -> pr_global_env Id.Set.empty r *)
let print_option_value key =
- let (name, depr, (read,_,_)) = get_option key in
+ let (depr, (read,_,_)) = get_option key in
let s = read () in
match s with
| BoolValue b ->
- Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+ Feedback.msg_notice (prlist_with_sep spc str key ++ str " is " ++ str (if b then "on" else "off"))
| _ ->
- Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+ Feedback.msg_notice (str "Current value of " ++ prlist_with_sep spc str key ++ str " is " ++ msg_option_value s)
let get_tables () =
let tables = !value_tab in
- let fold key (name, depr, (read,_,_)) accu =
+ let fold key (depr, (read,_,_)) accu =
let state = {
- opt_name = name;
opt_depr = depr;
opt_value = read ();
} in
@@ -415,15 +411,15 @@ let get_tables () =
OptionMap.fold fold tables OptionMap.empty
let print_tables () =
- let print_option key name value depr =
- let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in
+ let print_option key value depr =
+ let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value value in
if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
else msg ++ fnl ()
in
str "Options:" ++ fnl () ++
OptionMap.fold
- (fun key (name, depr, (read,_,_)) p ->
- p ++ print_option key name (read ()) depr)
+ (fun key (depr, (read,_,_)) p ->
+ p ++ print_option key (read ()) depr)
!value_tab (mt ()) ++
str "Tables:" ++ fnl () ++
List.fold_right
diff --git a/library/goptions.mli b/library/goptions.mli
index 29af196654..e3791dffb1 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -111,8 +111,6 @@ end
type 'a option_sig = {
optdepr : bool;
(** whether the option is DEPRECATED *)
- optname : string;
- (** a short string describing the option *)
optkey : option_name;
(** the low-level name of this option *)
optread : unit -> 'a;
@@ -133,7 +131,7 @@ val declare_stringopt_option: ?preprocess:(string option -> string option) ->
(** Helper to declare a reference controlled by an option. Read-only
as to avoid races. *)
-val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool)
+val declare_bool_option_and_ref : depr:bool -> key:option_name -> value:bool -> (unit -> bool)
(** {6 Special functions supposed to be used only in vernacentries.ml } *)
@@ -181,7 +179,6 @@ val set_option_value : ?locality:option_locality ->
(** Summary of an option status *)
type option_state = {
opt_depr : bool;
- opt_name : string;
opt_value : option_value;
}
diff --git a/library/lib.ml b/library/lib.ml
index c3c480aee4..7f96adeecf 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -133,7 +133,10 @@ let cwd () = !lib_state.path_prefix.Nametab.obj_dir
let current_mp () = !lib_state.path_prefix.Nametab.obj_mp
let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env())
-let sections_depth () = Section.depth (current_sections())
+let sections_depth () = match current_sections() with
+ | None -> 0
+ | Some sec -> Section.depth sec
+
let sections_are_opened = Global.sections_are_opened
let cwd_except_section () =
@@ -240,15 +243,6 @@ let add_discharged_leaf id obj =
cache_object (oname,newobj);
add_entry oname (Leaf (AtomicObject newobj))
-let add_leaves id objs =
- let oname = make_foname id in
- let add_obj obj =
- add_entry oname (Leaf (AtomicObject obj));
- load_object 1 (oname,obj)
- in
- List.iter add_obj objs;
- oname
-
let add_anonymous_leaf ?(cache_first = true) obj =
let id = anonymous_id () in
let oname = make_foname id in
@@ -417,14 +411,18 @@ let extract_worklist info =
let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
+let force_sections () = match Safe_typing.sections_of_safe_env (Global.safe_env()) with
+ | Some s -> s
+ | None -> CErrors.user_err Pp.(str "No open section.")
+
let replacement_context () =
- Section.replacement_context (Global.env ()) (sections ())
+ Section.replacement_context (Global.env ()) (force_sections ())
let section_segment_of_constant con =
- Section.segment_of_constant (Global.env ()) con (sections ())
+ Section.segment_of_constant (Global.env ()) con (force_sections ())
let section_segment_of_mutual_inductive kn =
- Section.segment_of_inductive (Global.env ()) kn (sections ())
+ Section.segment_of_inductive (Global.env ()) kn (force_sections ())
let empty_segment = Section.empty_segment
@@ -437,8 +435,10 @@ let section_segment_of_reference = let open GlobRef in function
let variable_section_segment_of_reference gr =
(section_segment_of_reference gr).Section.abstr_ctx
-let is_in_section ref =
- Section.is_in_section (Global.env ()) ref (sections ())
+let is_in_section ref = match sections () with
+ | None -> false
+ | Some sec ->
+ Section.is_in_section (Global.env ()) ref sec
let section_instance = let open GlobRef in function
| VarRef id ->
@@ -500,7 +500,7 @@ let close_section () =
type frozen = lib_state
-let freeze ~marshallable = !lib_state
+let freeze () = !lib_state
let unfreeze st = lib_state := st
diff --git a/library/lib.mli b/library/lib.mli
index a313a62c2e..1fe72389f6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -65,10 +65,6 @@ val add_anonymous_entry : node -> unit
val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name
val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
-(** this operation adds all objects with the same name and calls [load_object]
- for each of them *)
-val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name
-
(** {6 ... } *)
(** The function [contents] gives access to the current entire segment *)
@@ -155,7 +151,7 @@ val close_section : unit -> unit
type frozen
-val freeze : marshallable:bool -> frozen
+val freeze : unit -> frozen
val unfreeze : frozen -> unit
(** Keep only the libobject structure, not the objects themselves *)
diff --git a/library/libobject.ml b/library/libobject.ml
index a632a426fd..28d0654444 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -82,79 +82,54 @@ and objects = (Names.Id.t * t) list
and substitutive_objects = MBId.t list * algebraic_objects
-type dynamic_object_declaration = {
- dyn_cache_function : object_name * obj -> unit;
- dyn_load_function : int -> object_name * obj -> unit;
- dyn_open_function : int -> object_name * obj -> unit;
- dyn_subst_function : Mod_subst.substitution * obj -> obj;
- dyn_classify_function : obj -> obj substitutivity;
- dyn_discharge_function : object_name * obj -> obj option;
- dyn_rebuild_function : obj -> obj }
+module DynMap = Dyn.Map (struct type 'a t = 'a object_declaration end)
-let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
-
-let cache_tab =
- (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t)
+let cache_tab = ref DynMap.empty
let declare_object_full odecl =
let na = odecl.object_name in
- let (infun, outfun) = Dyn.Easy.make_dyn na in
- let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj)
- and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj)
- and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj)
- and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj))
- and classifier lobj = match odecl.classify_function (outfun lobj) with
+ let tag = Dyn.create na in
+ let () = cache_tab := DynMap.add tag odecl !cache_tab in
+ tag
+
+let declare_object odecl =
+ let tag = declare_object_full odecl in
+ let infun v = Dyn.Dyn (tag, v) in
+ infun
+
+let cache_object (sp, Dyn.Dyn (tag, v)) =
+ let decl = DynMap.find tag !cache_tab in
+ decl.cache_function (sp, v)
+
+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 decl = DynMap.find tag !cache_tab in
+ decl.open_function i (sp, v)
+
+let subst_object (subs, Dyn.Dyn (tag, v)) =
+ let decl = DynMap.find tag !cache_tab in
+ Dyn.Dyn (tag, decl.subst_function (subs, v))
+
+let classify_object (Dyn.Dyn (tag, v)) =
+ let decl = DynMap.find tag !cache_tab in
+ match decl.classify_function v with
| Dispose -> Dispose
- | Substitute atomic_obj -> Substitute (infun atomic_obj)
- | Keep atomic_obj -> Keep (infun atomic_obj)
- | Anticipate (atomic_obj) -> Anticipate (infun atomic_obj)
- and discharge (oname,lobj) =
- Option.map infun (odecl.discharge_function (oname,outfun lobj))
- and rebuild lobj = infun (odecl.rebuild_function (outfun lobj))
- in
- Hashtbl.add cache_tab na { dyn_cache_function = cacher;
- dyn_load_function = loader;
- dyn_open_function = opener;
- dyn_subst_function = substituter;
- dyn_classify_function = classifier;
- dyn_discharge_function = discharge;
- dyn_rebuild_function = rebuild };
- (infun,outfun)
-
-let declare_object odecl = fst (declare_object_full odecl)
-let declare_object_full odecl = declare_object_full odecl
-
-(* this function describes how the cache, load, open, and export functions
- are triggered. *)
-
-let apply_dyn_fun f lobj =
- let tag = object_tag lobj in
- let dodecl =
- try Hashtbl.find cache_tab tag
- with Not_found -> assert false
- in
- f dodecl
-
-let cache_object ((_,lobj) as node) =
- apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
-
-let load_object i ((_,lobj) as node) =
- apply_dyn_fun (fun d -> d.dyn_load_function i node) lobj
-
-let open_object i ((_,lobj) as node) =
- apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj
-
-let subst_object ((_,lobj) as node) =
- apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj
-
-let classify_object lobj =
- apply_dyn_fun (fun d -> d.dyn_classify_function lobj) lobj
-
-let discharge_object ((_,lobj) as node) =
- apply_dyn_fun (fun d -> d.dyn_discharge_function node) lobj
-
-let rebuild_object lobj =
- apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj
+ | Substitute v -> Substitute (Dyn.Dyn (tag, v))
+ | Keep v -> Keep (Dyn.Dyn (tag, v))
+ | Anticipate v -> Anticipate (Dyn.Dyn (tag, v))
+
+let discharge_object (sp, Dyn.Dyn (tag, v)) =
+ let decl = DynMap.find tag !cache_tab in
+ match decl.discharge_function (sp, v) with
+ | None -> None
+ | Some v -> Some (Dyn.Dyn (tag, v))
+
+let rebuild_object (Dyn.Dyn (tag, v)) =
+ let decl = DynMap.find tag !cache_tab in
+ Dyn.Dyn (tag, decl.rebuild_function v)
let dump = Dyn.dump
diff --git a/library/libobject.mli b/library/libobject.mli
index 146ccc293f..c25345994a 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -101,7 +101,9 @@ val ident_subst_function : substitution * 'a -> 'a
will hand back two functions, the "injection" and "projection"
functions for dynamically typed library-objects. *)
-type obj
+module Dyn : Dyn.S
+
+type obj = Dyn.t
type algebraic_objects =
| Objs of objects
@@ -120,13 +122,11 @@ and objects = (Names.Id.t * t) list
and substitutive_objects = Names.MBId.t list * algebraic_objects
val declare_object_full :
- 'a object_declaration -> ('a -> obj) * (obj -> 'a)
+ 'a object_declaration -> 'a Dyn.tag
val declare_object :
'a object_declaration -> ('a -> obj)
-val object_tag : obj -> string
-
val cache_object : object_name * obj -> unit
val load_object : int -> object_name * obj -> unit
val open_object : int -> object_name * obj -> unit
diff --git a/library/states.ml b/library/states.ml
index 0be153d96a..90303a2a5c 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -18,7 +18,7 @@ let replace_summary (lib,_) st = lib, st
let replace_lib (_,st) lib = lib, st
let freeze ~marshallable =
- (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
+ (Lib.freeze (), Summary.freeze_summaries ~marshallable)
let unfreeze (fl,fs) =
Lib.unfreeze fl;
diff --git a/library/summary.ml b/library/summary.ml
index d3ae42694a..2afccda847 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -19,57 +19,47 @@ type 'a summary_declaration = {
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
-let sum_mod = ref None
-let sum_map = ref String.Map.empty
+module DynMap = Dyn.Map(struct type 'a t = 'a summary_declaration end)
+
+type ml_modules = (string * string option) list
+
+let sum_mod : ml_modules summary_declaration option ref = ref None
+let sum_map = ref DynMap.empty
let mangle id = id ^ "-SUMMARY"
-let unmangle id = String.(sub id 0 (length id - 8))
-
-let ml_modules = "ML-MODULES"
-
-let internal_declare_summary fadd sumname sdecl =
- let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
- let dyn_freeze ~marshallable = infun (sdecl.freeze_function ~marshallable)
- and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
- and dyn_init = sdecl.init_function in
- let ddecl = {
- freeze_function = dyn_freeze;
- unfreeze_function = dyn_unfreeze;
- init_function = dyn_init }
- in
- fadd sumname ddecl;
- tag
let declare_ml_modules_summary decl =
- let ml_add _ ddecl = sum_mod := Some ddecl in
- internal_declare_summary ml_add ml_modules decl
+ sum_mod := Some decl
-let declare_ml_modules_summary decl =
- ignore(declare_ml_modules_summary decl)
+let check_name sumname = match Dyn.name sumname with
+| None -> ()
+| Some (Dyn.Any tag) ->
+ anomaly ~label:"Summary.declare_summary"
+ (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str (Dyn.repr tag) ++ str ".")
let declare_summary_tag sumname decl =
- let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in
- let () = if String.Map.mem sumname !sum_map then
- anomaly ~label:"Summary.declare_summary"
- (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".")
- in
- internal_declare_summary fadd sumname decl
+ let () = check_name (mangle sumname) in
+ let tag = Dyn.create (mangle sumname) in
+ let () = sum_map := DynMap.add tag decl !sum_map in
+ tag
let declare_summary sumname decl =
ignore(declare_summary_tag sumname decl)
+module Frozen = Dyn.Map(struct type 'a t = 'a end)
+
type frozen = {
- summaries : Dyn.t String.Map.t;
+ summaries : Frozen.t;
(** Ordered list w.r.t. the first component. *)
- ml_module : Dyn.t option;
+ ml_module : ml_modules option;
(** Special handling of the ml_module summary. *)
}
-let empty_frozen = { summaries = String.Map.empty; ml_module = None }
+let empty_frozen = { summaries = Frozen.empty; ml_module = None }
let freeze_summaries ~marshallable : frozen =
- let smap decl = decl.freeze_function ~marshallable in
- { summaries = String.Map.map smap !sum_map;
+ let fold (DynMap.Any (tag, decl)) accu = Frozen.add tag (decl.freeze_function ~marshallable) accu in
+ { summaries = DynMap.fold fold !sum_map Frozen.empty;
ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod;
}
@@ -87,23 +77,23 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
(* The unfreezing of [ml_modules_summary] has to be anticipated since it
* may modify the content of [summaries] by loading new ML modules *)
begin match !sum_mod with
- | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
- | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
+ | None -> anomaly (str "Undeclared ML-MODULES summary.")
+ | Some decl -> Option.iter decl.unfreeze_function ml_module
end;
(* We must be independent on the order of the map! *)
- let ufz name decl =
- try decl.unfreeze_function String.Map.(find name summaries)
+ let ufz (DynMap.Any (name, decl)) =
+ try decl.unfreeze_function Frozen.(find name summaries)
with Not_found ->
if not partial then begin
- warn_summary_out_of_scope name;
+ warn_summary_out_of_scope (Dyn.repr name);
decl.init_function ()
end;
in
(* String.Map.iter unfreeze_single !sum_map *)
- String.Map.iter ufz !sum_map
+ DynMap.iter ufz !sum_map
let init_summaries () =
- String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map
+ DynMap.iter (fun (DynMap.Any (_, decl)) -> decl.init_function ()) !sum_map
(** For global tables registered statically before the end of coqtop
launch, the following empty [init_function] could be used. *)
@@ -112,18 +102,15 @@ let nop () = ()
(** Summary projection *)
let project_from_summary { summaries } tag =
- let id = unmangle (Dyn.repr tag) in
- let state = String.Map.find id summaries in
- Option.get (Dyn.Easy.prj state tag)
+ Frozen.find tag summaries
let modify_summary st tag v =
- let id = unmangle (Dyn.repr tag) in
- let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in
+ let () = assert (Frozen.mem tag st.summaries) in
+ let summaries = Frozen.add tag v st.summaries in
{st with summaries}
let remove_from_summary st tag =
- let id = unmangle (Dyn.repr tag) in
- let summaries = String.Map.remove id st.summaries in
+ let summaries = Frozen.remove tag st.summaries in
{st with summaries}
(** All-in-one reference declaration + registration *)
@@ -140,26 +127,32 @@ let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x
module Local = struct
-type 'a local_ref = ('a CEphemeron.key * string) ref
+type 'a local_ref = ('a CEphemeron.key * 'a Dyn.tag) ref
-let (:=) r v = r := (CEphemeron.create v, snd !r)
+let set r v = r := (CEphemeron.create v, snd !r)
-let (!) r =
+let get r =
let key, name = !r in
try CEphemeron.get key
with CEphemeron.InvalidKey ->
- let { init_function } = String.Map.find name !sum_map in
+ let { init_function } = DynMap.find name !sum_map in
init_function ();
CEphemeron.get (fst !r)
let ref ?(freeze=fun x -> x) ~name init =
- let r = pervasives_ref (CEphemeron.create init, name) in
- declare_summary name
- { freeze_function = (fun ~marshallable -> freeze !r);
- unfreeze_function = ((:=) r);
- init_function = (fun () -> r := init) };
+ let () = check_name (mangle name) in
+ let tag : 'a Dyn.tag = Dyn.create (mangle name) in
+ let r = pervasives_ref (CEphemeron.create init, tag) in
+ let () = sum_map := DynMap.add tag
+ { freeze_function = (fun ~marshallable -> freeze (get r));
+ unfreeze_function = (set r);
+ init_function = (fun () -> set r init) } !sum_map
+ in
r
+let (!) = get
+let (:=) = set
+
end
let dump = Dyn.dump
diff --git a/library/summary.mli b/library/summary.mli
index 3a122edf3d..f4550b38f9 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -63,7 +63,7 @@ end
because its unfreeze may load ML code and hence add summary
entries. Thus is has to be recognizable, and handled properly.
*)
-val declare_ml_modules_summary : 'a summary_declaration -> unit
+val declare_ml_modules_summary : (string * string option) list summary_declaration -> unit
(** For global tables registered statically before the end of coqtop
launch, the following empty [init_function] could be used. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 11:16:45 +0000