diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 22 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 49 | ||||
| -rw-r--r-- | library/global.mli | 7 | ||||
| -rw-r--r-- | library/lib.ml | 59 | ||||
| -rw-r--r-- | library/lib.mli | 38 | ||||
| -rw-r--r-- | library/libnames.ml | 31 | ||||
| -rw-r--r-- | library/libnames.mli | 40 | ||||
| -rw-r--r-- | library/libobject.ml | 5 | ||||
| -rw-r--r-- | library/libobject.mli | 6 | ||||
| -rw-r--r-- | library/nametab.ml | 69 | ||||
| -rw-r--r-- | library/nametab.mli | 51 |
12 files changed, 194 insertions, 185 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index e01a99f731..d20775a0d7 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -139,7 +139,7 @@ let expand_sobjs (_,aobjs) = expand_aobjs aobjs Module M:SIG. ... End M. have the keep list empty. *) -type module_objects = object_prefix * Lib.lib_objects * Lib.lib_objects +type module_objects = Nametab.object_prefix * Lib.lib_objects * Lib.lib_objects module ModObjs : sig @@ -185,7 +185,7 @@ let consistency_checks exists dir dirinfo = user_err ~hdr:"consistency_checks" (DirPath.print dir ++ str " should already exist!") in - assert (eq_global_dir_reference globref dirinfo) + assert (Nametab.GlobDirRef.equal globref dirinfo) else if Nametab.exists_dir dir then user_err ~hdr:"consistency_checks" @@ -197,8 +197,8 @@ let compute_visibility exists i = (** Iterate some function [iter_objects] on all components of a module *) let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = - let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in - let dirinfo = DirModule prefix in + let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let dirinfo = Nametab.GlobDirRef.DirModule prefix in consistency_checks exists obj_dir dirinfo; Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; ModSubstObjs.set obj_mp sobjs; @@ -239,19 +239,19 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!") let load_keep i ((sp,kn),kobjs) = (* Invariant : seg isn't empty *) let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in let prefix',sobjs,kobjs0 = try ModObjs.get obj_mp with Not_found -> assert false (* a substobjs should already be loaded *) in - assert (eq_op prefix' prefix); + assert Nametab.(eq_op prefix' prefix); assert (List.is_empty kobjs0); ModObjs.set obj_mp (prefix,sobjs,kobjs); Lib.load_objects i prefix kobjs let open_keep i ((sp,kn),kobjs) = let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in Lib.open_objects i prefix kobjs let in_modkeep : Lib.lib_objects -> obj = @@ -302,7 +302,7 @@ let (in_modtype : substitutive_objects -> obj), let do_include do_load do_open i ((sp,kn),aobjs) = let obj_dir = Libnames.dirpath sp in let obj_mp = KerName.modpath kn in - let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in let o = expand_aobjs aobjs in if do_load then Lib.load_objects i prefix o; if do_open then Lib.open_objects i prefix o @@ -605,7 +605,7 @@ let start_module interp_modast export id args res fs = let () = Global.push_context_set true cst in openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in - Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModule prefix); + Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); mp let end_module () = @@ -723,7 +723,7 @@ let start_modtype interp_modast id args mtys fs = let () = Global.push_context_set true cst in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in - Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix); + Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix)); mp let end_modtype () = @@ -977,7 +977,7 @@ let iter_all_segments f = | "INCLUDE" -> let objs = expand_aobjs (out_include obj) in List.iter (apply_obj prefix) objs - | _ -> f (make_oname prefix id) obj + | _ -> f (Lib.make_oname prefix id) obj in let apply_mod_obj _ (prefix,substobjs,keepobjs) = List.iter (apply_obj prefix) substobjs; diff --git a/library/declaremods.mli b/library/declaremods.mli index b42a59bfbd..7aa4bc30ce 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -130,7 +130,7 @@ val declare_include : (together with their section path). *) val iter_all_segments : - (Libnames.object_name -> Libobject.obj -> unit) -> unit + (Libobject.object_name -> Libobject.obj -> unit) -> unit val debug_print_modtab : unit -> Pp.t diff --git a/library/global.ml b/library/global.ml index 3781ff3230..4ea5969a6f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -128,19 +128,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let instantiate cb c = - let open Declarations in - match cb.const_universes with - | Monomorphic_const _ -> c, Univ.AUContext.empty - | Polymorphic_const ctx -> c, ctx - -let body_of_constant_body cb = - let open Declarations in - let otab = opaque_tables () in - match cb.const_body with - | Undef _ -> None - | Def c -> Some (instantiate cb (Mod_subst.force_constr c)) - | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) +let body_of_constant_body ce = body_of_constant_body (env ()) ce let body_of_constant cst = body_of_constant_body (lookup_constant cst) @@ -165,8 +153,6 @@ let import c u d = globalize (Safe_typing.import c u d) let env_of_context hyps = reset_with_named_context hyps (env()) -open Globnames - let constr_of_global_in_context = Typeops.constr_of_global_in_context let type_of_global_in_context = Typeops.type_of_global_in_context @@ -175,21 +161,9 @@ let universes_of_global gr = let is_polymorphic r = Environ.is_polymorphic (env()) r -let is_template_polymorphic r = - let env = env() in - match r with - | VarRef id -> false - | ConstRef c -> false - | IndRef ind -> Environ.template_polymorphic_ind ind env - | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env - -let is_type_in_type r = - let env = env() in - match r with - | VarRef id -> false - | ConstRef c -> Environ.type_in_type_constant c env - | IndRef ind -> Environ.type_in_type_ind ind env - | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env +let is_template_polymorphic r = is_template_polymorphic (env ()) r + +let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = Safe_typing.current_modpath (safe_env ()) @@ -208,11 +182,10 @@ let register field value = let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = - GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) - -let set_reduction_sharing b = - let env = safe_env () in - let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in - let flags = { flags with Declarations.share_reduction = b } in - let env = Safe_typing.set_typing_flags flags env in - GlobalSafeEnv.set_safe_env env + globalize0 (Safe_typing.set_strategy k l) + +let set_share_reduction b = + globalize0 (Safe_typing.set_share_reduction b) + +let set_VM b = globalize0 (Safe_typing.set_VM b) +let set_native_compiler b = globalize0 (Safe_typing.set_native_compiler b) diff --git a/library/global.mli b/library/global.mli index 42a8005a4f..01ee695c49 100644 --- a/library/global.mli +++ b/library/global.mli @@ -150,7 +150,12 @@ val register_inline : Constant.t -> unit val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit -val set_reduction_sharing : bool -> unit +(** {6 Conversion settings } *) + +val set_share_reduction : bool -> unit + +val set_VM : bool -> unit +val set_native_compiler : bool -> unit (* Modifies the global state, registering new universes *) diff --git a/library/lib.ml b/library/lib.ml index 27c5056a7f..690a4fd53d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -22,11 +22,16 @@ module NamedDecl = Context.Named.Declaration type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) +(* let make_oname (dirpath,(mp,dir)) id = *) +let make_oname Nametab.{ obj_dir; obj_mp } id = + Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id)) + +(* let make_oname (dirpath,(mp,dir)) id = *) type node = | Leaf of obj - | CompilingLibrary of object_prefix - | OpenedModule of is_type * export * object_prefix * Summary.frozen - | OpenedSection of object_prefix * Summary.frozen + | CompilingLibrary of Nametab.object_prefix + | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen + | OpenedSection of Nametab.object_prefix * Summary.frozen type library_entry = object_name * node @@ -89,7 +94,7 @@ let segment_of_objects prefix = sections, but on the contrary there are many constructions of section paths based on the library path. *) -let initial_prefix = { +let initial_prefix = Nametab.{ obj_dir = default_library; obj_mp = ModPath.initial; obj_sec = DirPath.empty; @@ -98,7 +103,7 @@ let initial_prefix = { type lib_state = { comp_name : DirPath.t option; lib_stk : library_segment; - path_prefix : object_prefix; + path_prefix : Nametab.object_prefix; } let initial_lib_state = { @@ -115,9 +120,9 @@ let library_dp () = (* [path_prefix] is a pair of absolute dirpath and a pair of current module path and relative section path *) -let cwd () = !lib_state.path_prefix.obj_dir -let current_mp () = !lib_state.path_prefix.obj_mp -let current_sections () = !lib_state.path_prefix.obj_sec +let cwd () = !lib_state.path_prefix.Nametab.obj_dir +let current_mp () = !lib_state.path_prefix.Nametab.obj_mp +let current_sections () = !lib_state.path_prefix.Nametab.obj_sec let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) @@ -138,7 +143,7 @@ let make_kn id = let mp = current_mp () in Names.KerName.make mp (Names.Label.of_id id) -let make_oname id = Libnames.make_oname !lib_state.path_prefix id +let make_foname id = make_oname !lib_state.path_prefix id let recalc_path_prefix () = let rec recalc = function @@ -153,9 +158,9 @@ let recalc_path_prefix () = let pop_path_prefix () = let op = !lib_state.path_prefix in lib_state := { !lib_state - with path_prefix = { op with obj_dir = pop_dirpath op.obj_dir; - obj_sec = pop_dirpath op.obj_sec; - } } + with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir; + obj_sec = pop_dirpath op.obj_sec; + } } let find_entry_p p = let rec find = function @@ -214,24 +219,24 @@ let anonymous_id = fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) let add_anonymous_entry node = - add_entry (make_oname (anonymous_id ())) node + add_entry (make_foname (anonymous_id ())) node let add_leaf id obj = if ModPath.equal (current_mp ()) ModPath.initial then user_err Pp.(str "No session module started (use -top dir)"); - let oname = make_oname id in + let oname = make_foname id in cache_object (oname,obj); add_entry oname (Leaf obj); oname let add_discharged_leaf id obj = - let oname = make_oname id in + let oname = make_foname id in let newobj = rebuild_object obj in cache_object (oname,newobj); add_entry oname (Leaf newobj) let add_leaves id objs = - let oname = make_oname id in + let oname = make_foname id in let add_obj obj = add_entry oname (Leaf obj); load_object 1 (oname,obj) @@ -241,7 +246,7 @@ let add_leaves id objs = let add_anonymous_leaf ?(cache_first = true) obj = let id = anonymous_id () in - let oname = make_oname id in + let oname = make_foname id in if cache_first then begin cache_object (oname,obj); add_entry oname (Leaf obj) @@ -269,15 +274,15 @@ let current_mod_id () = let start_mod is_type export id mp fs = - let dir = add_dirpath_suffix (!lib_state.path_prefix.obj_dir) id in - let prefix = { obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in + let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in + let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in let exists = if is_type then Nametab.exists_cci (make_path id) else Nametab.exists_module dir in if exists then user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); - add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs)); + add_entry (make_foname id) (OpenedModule (is_type,export,prefix,fs)); lib_state := { !lib_state with path_prefix = prefix} ; prefix @@ -318,9 +323,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after let start_compilation s mp = if !lib_state.comp_name != None then user_err Pp.(str "compilation unit is already started"); - if not (Names.DirPath.is_empty (!lib_state.path_prefix.obj_sec)) then + if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then user_err Pp.(str "some sections are already opened"); - let prefix = Libnames.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in add_anonymous_entry (CompilingLibrary prefix); lib_state := { !lib_state with comp_name = Some s; path_prefix = prefix } @@ -544,14 +549,14 @@ let is_in_section ref = (* Sections. *) let open_section id = let opp = !lib_state.path_prefix in - let obj_dir = add_dirpath_suffix opp.obj_dir id in - let prefix = { obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in + let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in + let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in if Nametab.exists_section obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:`No in - add_entry (make_oname id) (OpenedSection (prefix, fs)); + add_entry (make_foname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) - Nametab.push_dir (Nametab.Until 1) obj_dir (DirOpenSection prefix); + Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); lib_state := { !lib_state with path_prefix = prefix }; add_section () @@ -611,7 +616,7 @@ let init () = (* Misc *) let mp_of_global = function - | VarRef id -> !lib_state.path_prefix.obj_mp + | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp | ConstRef cst -> Names.Constant.modpath cst | IndRef ind -> Names.ind_modpath ind | ConstructRef constr -> Names.constr_modpath constr diff --git a/library/lib.mli b/library/lib.mli index 686e6a0e2d..d1b4977dd5 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -19,22 +19,24 @@ open Names type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) +val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name + type node = | Leaf of Libobject.obj - | CompilingLibrary of Libnames.object_prefix - | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen - | OpenedSection of Libnames.object_prefix * Summary.frozen + | CompilingLibrary of Nametab.object_prefix + | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen + | OpenedSection of Nametab.object_prefix * Summary.frozen -type library_segment = (Libnames.object_name * node) list +type library_segment = (Libobject.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list (** {6 Object iteration functions. } *) -val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit -val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit +val open_objects : int -> Nametab.object_prefix -> lib_objects -> unit +val load_objects : int -> Nametab.object_prefix -> lib_objects -> unit val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects -(*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) +(*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) (** [classify_segment seg] verifies that there are no OpenedThings, clears ClosedSections and FrozenStates and divides Leafs according @@ -46,20 +48,20 @@ val classify_segment : (** [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : - Libnames.object_prefix -> lib_objects -> library_segment + Nametab.object_prefix -> lib_objects -> library_segment (** {6 ... } *) (** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name +val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit -val pull_to_head : Libnames.object_name -> unit +val pull_to_head : Libobject.object_name -> 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 -> Libnames.object_name +val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name (** {6 ... } *) @@ -70,7 +72,7 @@ val contents : unit -> library_segment (** The function [contents_after] returns the current library segment, starting from a given section path. *) -val contents_after : Libnames.object_name -> library_segment +val contents_after : Libobject.object_name -> library_segment (** {6 Functions relative to current path } *) @@ -105,28 +107,28 @@ val find_opening_node : Id.t -> node val start_module : export -> module_ident -> ModPath.t -> - Summary.frozen -> Libnames.object_prefix + Summary.frozen -> Nametab.object_prefix val start_modtype : module_ident -> ModPath.t -> - Summary.frozen -> Libnames.object_prefix + Summary.frozen -> Nametab.object_prefix val end_module : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Nametab.object_prefix * Summary.frozen * library_segment val end_modtype : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Nametab.object_prefix * Summary.frozen * library_segment (** {6 Compilation units } *) val start_compilation : DirPath.t -> ModPath.t -> unit -val end_compilation_checks : DirPath.t -> Libnames.object_name +val end_compilation_checks : DirPath.t -> Libobject.object_name val end_compilation : - Libnames.object_name-> Libnames.object_prefix * library_segment + Libobject.object_name-> Nametab.object_prefix * library_segment (** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) diff --git a/library/libnames.ml b/library/libnames.ml index bd2ca550b9..87c4de42e8 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,37 +162,6 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath -type object_name = full_path * KerName.t - -type object_prefix = { - obj_dir : DirPath.t; - obj_mp : ModPath.t; - obj_sec : DirPath.t; -} - -(* let make_oname (dirpath,(mp,dir)) id = *) -let make_oname { obj_dir; obj_mp } id = - make_path obj_dir id, KerName.make obj_mp (Label.of_id id) - -(* to this type are mapped DirPath.t's in the nametab *) -type global_dir_reference = - | DirOpenModule of object_prefix - | DirOpenModtype of object_prefix - | DirOpenSection of object_prefix - | DirModule of object_prefix - -let eq_op op1 op2 = - DirPath.equal op1.obj_dir op2.obj_dir && - DirPath.equal op1.obj_sec op2.obj_sec && - ModPath.equal op1.obj_mp op2.obj_mp - -let eq_global_dir_reference r1 r2 = match r1, r2 with -| DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2 -| DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 -| DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 -| DirModule op1, DirModule op2 -> eq_op op1 op2 -| _ -> false - (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/libnames.mli b/library/libnames.mli index 447eecbb5c..9960603cbb 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,46 +88,6 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t -(** Both names are passed to objects: a "semantic" [kernel_name], which - can be substituted and a "syntactic" [full_path] which can be printed -*) - -type object_name = full_path * KerName.t - -(** Object prefix morally contains the "prefix" naming of an object to - be stored by [library], where [obj_dir] is the "absolute" path, - [obj_mp] is the current "module" prefix and [obj_sec] is the - "section" prefix. - - Thus, for an object living inside [Module A. Section B.] the - prefix would be: - - [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ] - - Note that both [obj_dir] and [obj_sec] are "paths" that is to say, - as opposed to [obj_mp] which is a single module name. - - *) -type object_prefix = { - obj_dir : DirPath.t; - obj_mp : ModPath.t; - obj_sec : DirPath.t; -} - -val eq_op : object_prefix -> object_prefix -> bool - -val make_oname : object_prefix -> Id.t -> object_name - -(** to this type are mapped [DirPath.t]'s in the nametab *) -type global_dir_reference = - | DirOpenModule of object_prefix - | DirOpenModtype of object_prefix - | DirOpenSection of object_prefix - | DirModule of object_prefix - -val eq_global_dir_reference : - global_dir_reference -> global_dir_reference -> bool - (** {6 ... } *) (** some preset paths *) diff --git a/library/libobject.ml b/library/libobject.ml index 79a3fed1b9..c153e9a09a 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Libnames open Pp module Dyn = Dyn.Make () @@ -16,6 +15,8 @@ module Dyn = Dyn.Make () type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a +type object_name = Libnames.full_path * Names.KerName.t + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; @@ -65,7 +66,7 @@ type dynamic_object_declaration = { let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = - (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) + (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t) let declare_object_full odecl = let na = odecl.object_name in diff --git a/library/libobject.mli b/library/libobject.mli index aefa81b225..32ffc5b79e 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -66,6 +66,12 @@ open Mod_subst type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a +(** Both names are passed to objects: a "semantic" [kernel_name], which + can be substituted and a "syntactic" [full_path] which can be printed +*) + +type object_name = full_path * Names.KerName.t + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; diff --git a/library/nametab.ml b/library/nametab.ml index 06ace373c3..e29c7b2960 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -15,6 +15,39 @@ open Names open Libnames open Globnames +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} + +let eq_op op1 op2 = + DirPath.equal op1.obj_dir op2.obj_dir && + DirPath.equal op1.obj_sec op2.obj_sec && + ModPath.equal op1.obj_mp op2.obj_mp + +(* to this type are mapped DirPath.t's in the nametab *) +module GlobDirRef = struct + type t = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + + let equal r1 r2 = match r1, r2 with + | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2 + | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 + | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 + | DirModule op1, DirModule op2 -> eq_op op1 op2 + | _ -> false + +end + +type global_dir_reference = GlobDirRef.t +[@@ocaml.deprecated "Use [GlobDirRef.t]"] + +let eq_global_dir_reference = GlobDirRef.equal +[@@ocaml.deprecated "Use [GlobDirRef.equal]"] exception GlobalizationError of qualid @@ -74,6 +107,8 @@ module type NAMETREE = sig val user_name : qualid -> t -> user_name val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list + (** Matches a prefix of [qualid], useful for completion *) + val match_prefixes : qualid -> t -> elt list end module Make (U : UserName) (E : EqualityType) : NAMETREE @@ -259,9 +294,19 @@ let find_prefixes qid tab = search_prefixes (Id.Map.find id tab) (DirPath.repr dir) with Not_found -> [] -end - +let match_prefixes = + let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in + fun qid tab -> + try + let (dir,id) = repr_qualid qid in + let id_prefix = cprefix Id.(to_string id) in + let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in + let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in + (* Coq's flatten is "magical", so this is not so bad perf-wise *) + CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches []) + with Not_found -> [] +end (* Global name tables *************************************************) @@ -295,13 +340,7 @@ struct | id :: l -> (id, l) end -module GlobDir = -struct - type t = global_dir_reference - let equal = eq_global_dir_reference -end - -module DirTab = Make(DirPath')(GlobDir) +module DirTab = Make(DirPath')(GlobDirRef) (* If we have a (closed) module M having a submodule N, than N does not have the entry in [the_dirtab]. *) @@ -390,7 +429,7 @@ let push_modtype vis sp kn = let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; match dir_ref with - | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab + | GlobDirRef.DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab | _ -> () (* This is for global universe names *) @@ -424,17 +463,17 @@ let locate_dir qid = DirTab.locate qid !the_dirtab let locate_module qid = match locate_dir qid with - | DirModule { obj_mp ; _} -> obj_mp + | GlobDirRef.DirModule { obj_mp ; _} -> obj_mp | _ -> raise Not_found let full_name_module qid = match locate_dir qid with - | DirModule { obj_dir ; _} -> obj_dir + | GlobDirRef.DirModule { obj_dir ; _} -> obj_dir | _ -> raise Not_found let locate_section qid = match locate_dir qid with - | DirOpenSection { obj_dir; _ } -> obj_dir + | GlobDirRef.DirOpenSection { obj_dir; _ } -> obj_dir | _ -> raise Not_found let locate_all qid = @@ -447,6 +486,10 @@ let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab +(* Completion *) +let completion_canditates qualid = + ExtRefTab.match_prefixes qualid !the_ccitab + (* Derived functions *) let locate_constant qid = diff --git a/library/nametab.mli b/library/nametab.mli index 1c3322bfb1..24af07619d 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -57,6 +57,44 @@ open Globnames *) +(** Object prefix morally contains the "prefix" naming of an object to + be stored by [library], where [obj_dir] is the "absolute" path, + [obj_mp] is the current "module" prefix and [obj_sec] is the + "section" prefix. + + Thus, for an object living inside [Module A. Section B.] the + prefix would be: + + [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ] + + Note that both [obj_dir] and [obj_sec] are "paths" that is to say, + as opposed to [obj_mp] which is a single module name. + + *) +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} + +val eq_op : object_prefix -> object_prefix -> bool + +(** to this type are mapped [DirPath.t]'s in the nametab *) +module GlobDirRef : sig + type t = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + val equal : t -> t -> bool +end + +type global_dir_reference = GlobDirRef.t +[@@ocaml.deprecated "Use [GlobDirRef.t]"] + +val eq_global_dir_reference : + GlobDirRef.t -> GlobDirRef.t -> bool +[@@ocaml.deprecated "Use [GlobDirRef.equal]"] exception GlobalizationError of qualid @@ -79,7 +117,7 @@ val map_visibility : (int -> int) -> visibility -> visibility val push : visibility -> full_path -> GlobRef.t -> unit val push_modtype : visibility -> full_path -> ModPath.t -> unit -val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit +val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit type universe_id = DirPath.t * int @@ -98,7 +136,7 @@ val locate_extended : qualid -> extended_global_reference val locate_constant : qualid -> Constant.t val locate_syndef : qualid -> syndef_name val locate_modtype : qualid -> ModPath.t -val locate_dir : qualid -> global_dir_reference +val locate_dir : qualid -> GlobDirRef.t val locate_module : qualid -> ModPath.t val locate_section : qualid -> DirPath.t val locate_universe : qualid -> universe_id @@ -115,9 +153,15 @@ val global_inductive : qualid -> inductive val locate_all : qualid -> GlobRef.t list val locate_extended_all : qualid -> extended_global_reference list -val locate_extended_all_dir : qualid -> global_dir_reference list +val locate_extended_all_dir : qualid -> GlobDirRef.t list val locate_extended_all_modtype : qualid -> ModPath.t list +(** Experimental completion support, API is _unstable_ *) +val completion_canditates : qualid -> extended_global_reference list +(** [completion_canditates qualid] will return the list of global + references that have [qualid] as a prefix. UI usually will want to + compose this with [shortest_qualid_of_global] *) + (** Mapping a full path to a global reference *) val global_of_path : full_path -> GlobRef.t @@ -211,6 +255,7 @@ module type NAMETREE = sig val user_name : qualid -> t -> user_name val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list + val match_prefixes : qualid -> t -> elt list end module Make (U : UserName) (E : EqualityType) : |