diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/lib.ml | 30 | ||||
| -rw-r--r-- | library/lib.mli | 4 | ||||
| -rw-r--r-- | library/libobject.ml | 97 | ||||
| -rw-r--r-- | library/summary.ml | 105 | ||||
| -rw-r--r-- | library/summary.mli | 2 |
7 files changed, 106 insertions, 138 deletions
diff --git a/library/global.ml b/library/global.ml index d4262683bb..fbbe09301b 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) @@ -206,7 +206,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..a38fde41a5 100644 --- a/library/global.mli +++ b/library/global.mli @@ -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 *) diff --git a/library/lib.ml b/library/lib.ml index c3c480aee4..9cce9b92ad 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 -> diff --git a/library/lib.mli b/library/lib.mli index a313a62c2e..0d03046dc2 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 *) diff --git a/library/libobject.ml b/library/libobject.ml index a632a426fd..c9ea6bcff8 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -82,79 +82,58 @@ 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 } - let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t -let cache_tab = - (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t) +module DynMap = Dyn.Map (struct type 'a t = 'a object_declaration end) + +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 - | 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)) + let tag = Dyn.create na in + let () = cache_tab := DynMap.add tag odecl !cache_tab in + let infun v = Dyn.Dyn (tag, v) in + let outfun v = match Dyn.Easy.prj v tag with + | None -> assert false + | Some v -> v 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 (sp, Dyn.Dyn (tag, v)) = + let decl = DynMap.find tag !cache_tab in + decl.cache_function (sp, v) -let cache_object ((_,lobj) as node) = - apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj +let load_object i (sp, Dyn.Dyn (tag, v)) = + let decl = DynMap.find tag !cache_tab in + decl.load_function i (sp, v) -let load_object i ((_,lobj) as node) = - apply_dyn_fun (fun d -> d.dyn_load_function i node) lobj +let open_object i (sp, Dyn.Dyn (tag, v)) = + let decl = DynMap.find tag !cache_tab in + decl.open_function i (sp, v) -let open_object i ((_,lobj) as node) = - apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj +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 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 +let classify_object (Dyn.Dyn (tag, v)) = + let decl = DynMap.find tag !cache_tab in + match decl.classify_function v with + | Dispose -> Dispose + | 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/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. *) |