aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml42
-rw-r--r--library/declare.mli5
-rw-r--r--library/global.ml2
-rw-r--r--library/global.mli2
-rw-r--r--library/lib.ml53
-rw-r--r--library/lib.mli11
-rw-r--r--library/library.ml346
-rw-r--r--library/library.mli49
-rwxr-xr-xlibrary/nametab.ml326
-rwxr-xr-xlibrary/nametab.mli52
10 files changed, 572 insertions, 316 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 34e0c1a12f..b360d8e01b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -23,6 +23,7 @@ open Lib
open Impargs
open Indrec
open Nametab
+open Library
type strength =
| NotDeclare
@@ -81,7 +82,7 @@ let cache_variable (sp,(id,(d,_,_) as vd)) =
| SectionLocalAssum ty -> Global.push_named_assum (id,ty)
| SectionLocalDef c -> Global.push_named_def (id,c)
end;
- Nametab.push_local sp (VarRef sp);
+ Nametab.push_short_name id (VarRef sp);
vartab := let (m,l) = !vartab in (Spmap.add sp vd m, sp::l)
let (in_variable, out_variable) =
@@ -105,11 +106,17 @@ let cache_parameter (sp,c) =
errorlabstrm "cache_parameter"
[< pr_id (basename sp); 'sTR " already exists" >];
Global.add_parameter sp c (current_section_context ());
- Nametab.push sp (ConstRef sp)
+ Nametab.push sp (ConstRef sp);
+ Nametab.push_short_name (basename sp) (ConstRef sp)
-let load_parameter _ = ()
+let load_parameter (sp,_) =
+ if Nametab.exists_cci sp then
+ errorlabstrm "cache_parameter"
+ [< pr_id (basename sp); 'sTR " already exists" >];
+ Nametab.push sp (ConstRef sp)
-let open_parameter (sp,_) = ()
+let open_parameter (sp,_) =
+ Nametab.push_short_name (basename sp) (ConstRef sp)
let export_parameter x = Some x
@@ -155,13 +162,19 @@ let cache_constant (sp,(cdt,stre,op)) =
| ConstantRecipe r -> Global.add_discharged_constant sp r sc
end;
Nametab.push sp (ConstRef sp);
+ Nametab.push_short_name (basename sp) (ConstRef sp);
if op then Global.set_opaque sp;
csttab := Spmap.add sp stre !csttab
let load_constant (sp,(ce,stre,op)) =
- csttab := Spmap.add sp stre !csttab
+ if Nametab.exists_cci sp then
+ errorlabstrm "cache_constant"
+ [< pr_id (basename sp); 'sTR " already exists" >] ;
+ csttab := Spmap.add sp stre !csttab;
+ Nametab.push sp (ConstRef sp)
-let open_constant (sp,_) = ()
+let open_constant (sp,_) =
+ Nametab.push_short_name (basename sp) (ConstRef sp)
let export_constant x = Some x
@@ -216,11 +229,17 @@ let cache_inductive (sp,mie) =
let names = inductive_names sp mie in
List.iter check_exists_inductive names;
Global.add_mind sp mie (current_section_context ());
- List.iter (fun (sp, ref) -> Nametab.push sp ref) names
+ List.iter (fun (sp, ref) -> Nametab.push sp ref; Nametab.push_short_name
+ (basename sp) ref) names
-let load_inductive _ = ()
+let load_inductive (sp,mie) =
+ let names = inductive_names sp mie in
+ List.iter check_exists_inductive names;
+ List.iter (fun (sp, ref) -> Nametab.push sp ref) names
-let open_inductive (sp,mie) = ()
+let open_inductive (sp,mie) =
+ let names = inductive_names sp mie in
+ List.iter (fun (sp, ref) -> Nametab.push_short_name (basename sp) ref) names
let export_inductive x = Some x
@@ -481,8 +500,7 @@ let elimination_suffix = function
| Prop Null -> "_ind"
| Prop Pos -> "_rec"
-let make_elimination_ident id s =
- id_of_string ((string_of_id id) ^ (elimination_suffix s))
+let make_elimination_ident id s = add_suffix id (elimination_suffix s)
let declare_one_elimination mispec =
let mindstr = string_of_id (mis_typename mispec) in
@@ -524,7 +542,7 @@ let declare_eliminations sp =
let lookup_eliminator env path s =
let dir, base,k = repr_path path in
- let id = id_of_string ((string_of_id base)^(elimination_suffix s)) in
+ let id = add_suffix base (elimination_suffix s) in
(* Try first to get an eliminator defined in the same section as the *)
(* inductive type *)
try construct_absolute_reference env (Names.make_path dir id k)
diff --git a/library/declare.mli b/library/declare.mli
index ad462534f3..9bbd0b8f40 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -14,6 +14,7 @@ open Term
open Sign
open Declarations
open Inductive
+open Library
(*i*)
(* This module provides the official functions to declare new variables,
@@ -23,7 +24,7 @@ open Inductive
reset works properly --- and will fill some global tables such as
[Nametab] and [Impargs]. *)
-type strength =
+type strength =
| NotDeclare
| DischargeAt of dir_path
| NeverDischarge
@@ -64,7 +65,7 @@ val declare_eliminations : mutual_inductive_path -> unit
val out_inductive : Libobject.obj -> mutual_inductive_entry
-val make_strength : string list -> strength
+val make_strength : dir_path -> strength
val make_strength_0 : unit -> strength
val make_strength_1 : unit -> strength
val make_strength_2 : unit -> strength
diff --git a/library/global.ml b/library/global.ml
index b4f45ad69c..ea5506969a 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -31,7 +31,7 @@ let _ =
{ freeze_function = (fun () -> !global_env);
unfreeze_function = (fun fr -> global_env := fr);
init_function = (fun () -> global_env := empty_environment);
- survive_section = true }
+ survive_section = false }
(* Then we export the functions of [Typing] on that environment. *)
diff --git a/library/global.mli b/library/global.mli
index c463bd1534..51acc840ee 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -50,7 +50,7 @@ val lookup_mind_specif : inductive -> inductive_instance
val set_opaque : section_path -> unit
val set_transparent : section_path -> unit
-val export : string -> compiled_env
+val export : dir_path -> compiled_env
val import : compiled_env -> unit
(*s Some functions of [Environ] instanciated on the global environment. *)
diff --git a/library/lib.ml b/library/lib.ml
index 9438713d6c..8fc7a4e9cb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -17,9 +17,9 @@ open Summary
type node =
| Leaf of obj
| Module of dir_path
- | OpenedSection of string * Summary.frozen
+ | OpenedSection of module_ident * Summary.frozen
(* bool is to tell if the section must be opened automatically *)
- | ClosedSection of bool * string * library_segment
+ | ClosedSection of bool * module_ident * library_segment
| FrozenState of Summary.frozen
and library_entry = section_path * node
@@ -36,16 +36,16 @@ and library_segment = library_entry list
let lib_stk = ref ([] : (section_path * node) list)
+let default_module = make_dirpath [id_of_string "Scratch"]
let module_name = ref None
-let path_prefix = ref ([Nametab.default_root] : dir_path)
+let path_prefix = ref (default_module : dir_path)
let module_sp () =
- match !module_name with Some m -> m | None -> [Nametab.default_root]
+ match !module_name with Some m -> m | None -> default_module
let recalc_path_prefix () =
let rec recalc = function
- | (sp, OpenedSection _) :: _ ->
- let (pl,id,_) = repr_path sp in pl@[string_of_id id]
+ | (sp, OpenedSection (modid,_)) :: _ -> (dirpath sp)@[modid]
| _::l -> recalc l
| [] -> module_sp ()
in
@@ -112,12 +112,13 @@ let contents_after = function
(* Sections. *)
-let open_section s =
- let sp = make_path (id_of_string s) OBJ in
- if Nametab.exists_module sp then
- errorlabstrm "open_section" [< 'sTR (s^" already exists") >];
- add_entry sp (OpenedSection (s, freeze_summaries()));
- path_prefix := !path_prefix @ [s];
+let open_section id =
+ let dir = !path_prefix @ [id] in
+ let sp = make_path id OBJ in
+ if Nametab.exists_section dir then
+ errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
+ add_entry sp (OpenedSection (id, freeze_summaries()));
+ path_prefix := dir;
sp
let check_for_module () =
@@ -130,13 +131,23 @@ let check_for_module () =
let start_module s =
if !module_name <> None then
error "a module is already started";
- if !path_prefix <> [Nametab.default_root] then
+ if !path_prefix <> default_module then
error "some sections are already opened";
module_name := Some s;
+ (match split_dirpath s with [],id -> Nametab.push_library_root id | _ -> ());
Univ.set_module s;
let _ = add_anonymous_entry (Module s) in
path_prefix := s
+let end_module s =
+ match !module_name with
+ | None -> error "no module declared"
+ | Some m ->
+ let bm = snd (split_dirpath m) in
+ if bm <> s then
+ error ("The current open module has basename "^(string_of_id bm));
+ m
+
let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
let sections_are_opened () =
@@ -156,11 +167,11 @@ let export_segment seg =
in
clean [] seg
-let close_section export s =
+let close_section export id =
let sp,fs =
try match find_entry_p is_opened_section with
- | sp,OpenedSection (s',fs) ->
- if s <> s' then error "this is not the last opened section"; (sp,fs)
+ | sp,OpenedSection (id',fs) ->
+ if id<>id' then error "this is not the last opened section"; (sp,fs)
| _ -> assert false
with Not_found ->
error "no opened section"
@@ -169,16 +180,14 @@ let close_section export s =
lib_stk := before;
let after' = export_segment after in
pop_path_prefix ();
- add_entry
- (make_path (id_of_string s) OBJ) (ClosedSection (export, s,after'));
+ add_entry (make_path id OBJ) (ClosedSection (export, id, after'));
(sp,after,fs)
(* The following function exports the whole library segment, that will be
saved as a module. Objects are presented in chronological order, and
frozen states are removed. *)
-let export_module f =
- if !module_name = None then error "no module declared";
+let export_module s =
export_segment !lib_stk
(* Backtracking. *)
@@ -214,8 +223,8 @@ let reset_name id =
(* [dir] is a section dir if [module] < [dir] <= [path_prefix] *)
let is_section_p sp =
- not (dirpath_prefix_of sp (module_sp ()))
- & (dirpath_prefix_of sp !path_prefix)
+ not (is_dirpath_prefix_of sp (module_sp ()))
+ & (is_dirpath_prefix_of sp !path_prefix)
(* State and initialization. *)
diff --git a/library/lib.mli b/library/lib.mli
index 9b5326db1e..b22839a3da 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -21,8 +21,8 @@ open Summary
type node =
| Leaf of obj
| Module of dir_path
- | OpenedSection of string * Summary.frozen
- | ClosedSection of bool * string * library_segment
+ | OpenedSection of module_ident * Summary.frozen
+ | ClosedSection of bool * module_ident * library_segment
| FrozenState of Summary.frozen
and library_entry = section_path * node
@@ -47,9 +47,9 @@ val contents_after : section_path option -> library_segment
(*s Opening and closing a section. *)
-val open_section : string -> section_path
+val open_section : identifier -> section_path
val close_section :
- export:bool -> string -> section_path * library_segment * Summary.frozen
+ export:bool -> identifier -> section_path * library_segment * Summary.frozen
val sections_are_opened : unit -> bool
val make_path : identifier -> path_kind -> section_path
@@ -57,7 +57,8 @@ val cwd : unit -> dir_path
val is_section_p : dir_path -> bool
val start_module : dir_path -> unit
-val export_module : unit -> library_segment
+val end_module : module_ident -> dir_path
+val export_module : dir_path -> library_segment
(*s Backtracking (undo). *)
diff --git a/library/library.ml b/library/library.ml
index a6b7b50127..5556bf32ee 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -10,7 +10,7 @@
open Pp
open Util
-open System
+
open Names
open Environ
open Libobject
@@ -19,72 +19,112 @@ open Nametab
(*s Load path. *)
-let load_path = ref ([] : load_path)
+type logical_path = dir_path
+
+let load_path = ref ([],[] : System.physical_path list * logical_path list)
-let get_load_path () = !load_path
+let get_load_path () = fst !load_path
-let add_load_path_entry lpe = load_path := lpe :: !load_path
+let find_logical_path dir =
+ match list_filter2 (fun p d -> p = dir) !load_path with
+ | _,[dir] -> dir
+ | _ -> anomaly ("Two logical paths are associated to "^dir)
let remove_path dir =
- load_path := List.filter (fun lpe -> lpe.directory <> dir) !load_path
+ load_path := list_filter2 (fun p d -> p <> dir) !load_path
+
+let add_load_path_entry (phys_path,coq_path) =
+ match list_filter2 (fun p d -> p = phys_path) !load_path with
+ | _,[dir] ->
+ if dir <> coq_path && coq_path <> Nametab.default_root_prefix then
+ (* Assume the user is concerned by module naming *)
+ begin
+ if dir <> Nametab.default_root_prefix then
+ warning (phys_path^" was previously bound to "
+ ^(string_of_dirpath dir)
+ ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
+ remove_path phys_path;
+ load_path := (phys_path::fst !load_path, coq_path::snd !load_path)
+ end
+ | _,[] ->
+ load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path)
+ | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+
+let physical_paths (dp,lp) = dp
+
+let load_path_of_logical_path dir =
+ fst (list_filter2 (fun p d -> d = dir) !load_path)
+
+let get_full_load_path () = List.combine (fst !load_path) (snd !load_path)
(*s Modules on disk contain the following informations (after the magic
number, and before the digest). *)
+type compilation_unit_name = dir_path
+
type module_disk = {
- md_name : string;
+ md_name : compilation_unit_name;
md_compiled_env : compiled_env;
md_declarations : library_segment;
- md_nametab : module_contents;
- md_deps : (string * Digest.t * bool) list }
+ md_deps : (compilation_unit_name * Digest.t * bool) list }
(*s Modules loaded in memory contain the following informations. They are
kept in the global table [modules_table]. *)
type module_t = {
- module_name : string;
- module_filename : load_path_entry * string;
+ module_name : compilation_unit_name;
+ module_filename : System.physical_path;
module_compiled_env : compiled_env;
module_declarations : library_segment;
- module_nametab : module_contents;
mutable module_opened : bool;
mutable module_exported : bool;
- module_deps : (string * Digest.t * bool) list;
+ module_deps : (compilation_unit_name * Digest.t * bool) list;
module_digest : Digest.t }
-let modules_table = ref Stringmap.empty
+module CompUnitOrdered =
+ struct
+ type t = dir_path
+ let compare = Pervasives.compare
+ end
+
+module CompUnitmap = Map.Make(CompUnitOrdered)
+
+let modules_table = ref CompUnitmap.empty
let _ =
Summary.declare_summary "MODULES"
{ Summary.freeze_function = (fun () -> !modules_table);
Summary.unfreeze_function = (fun ft -> modules_table := ft);
- Summary.init_function = (fun () -> modules_table := Stringmap.empty);
- Summary.survive_section = true }
+ Summary.init_function = (fun () -> modules_table := CompUnitmap.empty);
+ Summary.survive_section = false }
let find_module s =
try
- Stringmap.find s !modules_table
+ CompUnitmap.find s !modules_table
with Not_found ->
- error ("Unknown module " ^ s)
+ error ("Unknown module " ^ (string_of_dirpath s))
-let module_is_loaded s =
- try let _ = Stringmap.find s !modules_table in true with Not_found -> false
+let module_is_loaded dir =
+ try let _ = CompUnitmap.find dir !modules_table in true
+ with Not_found -> false
-let module_is_opened s = (find_module s).module_opened
+let module_is_opened s = (find_module [id_of_string s]).module_opened
let loaded_modules () =
- Stringmap.fold (fun s _ l -> s :: l) !modules_table []
+ CompUnitmap.fold (fun s _ l -> s :: l) !modules_table []
let opened_modules () =
- Stringmap.fold
+ CompUnitmap.fold
(fun s m l -> if m.module_opened then s :: l else l)
!modules_table []
+let compunit_cache = ref Stringmap.empty
+
let module_segment = function
| None -> contents_after None
| Some m -> (find_module m).module_declarations
-let module_filename m = (find_module m).module_filename
+let module_full_filename m = (find_module m).module_filename
let vo_magic_number = 0700
@@ -106,7 +146,9 @@ let segment_iter f =
let rec apply = function
| sp,Leaf obj -> f (sp,obj)
| _,OpenedSection _ -> assert false
- | _,ClosedSection (export,s,seg) -> if export then iter seg
+ | sp,ClosedSection (export,s,seg) ->
+ push_section (wd_of_sp sp);
+ if export then iter seg
| _,(FrozenState _ | Module _) -> ()
and iter seg =
List.iter apply seg
@@ -125,7 +167,6 @@ let rec open_module force s =
if force or not m.module_opened then begin
List.iter (fun (m,_,exp) -> if exp then open_module force m) m.module_deps;
open_objects m.module_declarations;
- open_module_contents (make_qualid [] (id_of_string s));
m.module_opened <- true
end
@@ -138,60 +179,198 @@ let import_module = open_module true
then same value as for caller is reused in recursive loadings). *)
let load_objects decls =
- segment_rec_iter load_object decls
+(* segment_rec_iter load_object decls*)
+ segment_iter load_object decls
+
+exception LibUnmappedDir
+exception LibNotFound
+type library_location = LibLoaded | LibInPath
-let rec load_module_from s f =
+let locate_absolute_library dir =
+ (* Look if loaded *)
try
- Stringmap.find s !modules_table
+ let m = CompUnitmap.find dir !modules_table in
+ (LibLoaded, dir, m.module_filename)
with Not_found ->
- let (lpe,fname,ch) =
- try raw_intern_module (get_load_path ()) f
- with System.Bad_magic_number fname ->
- errorlabstrm "load_module_from"
- [< 'sTR"file "; 'sTR fname; 'sPC; 'sTR"has bad magic number.";
- 'sPC; 'sTR"It is corrupted"; 'sPC;
- 'sTR"or was compiled with another version of Coq." >] in
- let md = System.marshal_in ch in
- let digest = System.marshal_in ch in
- close_in ch;
- let m = { module_name = md.md_name;
- module_filename = (lpe,fname);
- module_compiled_env = md.md_compiled_env;
- module_declarations = md.md_declarations;
- module_nametab = md.md_nametab;
- module_opened = false;
- module_exported = false;
- module_deps = md.md_deps;
- module_digest = digest } in
- if s <> md.md_name then
- error ("The file " ^ fname ^ " does not contain module " ^ s);
- List.iter (load_mandatory_module s) m.module_deps;
- Global.import m.module_compiled_env;
- load_objects m.module_declarations;
- let sp = Names.make_path lpe.coq_dirpath (id_of_string s) CCI in
- push_module sp m.module_nametab;
- modules_table := Stringmap.add s m !modules_table;
- m
-
-and load_mandatory_module caller (s,d,_) =
- let m = load_module_from s s in
+ (* Look if in loadpath *)
+ try
+ let pref, base = split_dirpath dir in
+ let loadpath = load_path_of_logical_path pref in
+ if loadpath = [] then raise LibUnmappedDir;
+ let name = (string_of_id base)^".vo" in
+ let _, file = System.where_in_path loadpath name in
+ (LibInPath, dir, file)
+ with Not_found -> raise LibNotFound
+
+let with_magic_number_check f a =
+ try f a
+ with System.Bad_magic_number fname ->
+ errorlabstrm "load_module_from"
+ [< 'sTR"file "; 'sTR fname; 'sPC; 'sTR"has bad magic number.";
+ 'sPC; 'sTR"It is corrupted"; 'sPC;
+ 'sTR"or was compiled with another version of Coq." >]
+
+let rec load_module = function
+ | (LibLoaded, dir, _) ->
+ CompUnitmap.find dir !modules_table
+ | (LibInPath, dir, f) ->
+ (* [dir] is an absolute name which matches [f] *)
+ let md, digest =
+ try Stringmap.find f !compunit_cache
+ with Not_found ->
+ let ch = with_magic_number_check raw_intern_module f in
+ let md = System.marshal_in ch in
+ let digest = System.marshal_in ch in
+ close_in ch;
+ if dir <> md.md_name then
+ errorlabstrm "load_module"
+ [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
+ pr_dirpath md.md_name; 'sPC; 'sTR "and not module"; 'sPC;
+ pr_dirpath dir >];
+ (match split_dirpath dir with
+ | [], id -> Nametab.push_library_root id
+ | _ -> ());
+ compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
+ (md, digest) in
+ intern_module digest f md
+
+and intern_module digest fname md =
+ let m = { module_name = md.md_name;
+ module_filename = fname;
+ module_compiled_env = md.md_compiled_env;
+ module_declarations = md.md_declarations;
+ module_opened = false;
+ module_exported = false;
+ module_deps = md.md_deps;
+ module_digest = digest } in
+ List.iter (load_mandatory_module md.md_name) m.module_deps;
+ Global.import m.module_compiled_env;
+ load_objects m.module_declarations;
+ modules_table := CompUnitmap.add md.md_name m !modules_table;
+ Nametab.push_loaded_library md.md_name;
+ m
+
+and load_mandatory_module caller (dir,d,_) =
+ let m = load_absolute_module_from dir in
if d <> m.module_digest then
- error ("module "^caller^" makes inconsistent assumptions over module "^s)
-
-let load_module s = function
- | None -> ignore (load_module_from s s)
- | Some f -> ignore (load_module_from s f)
+ error ("compiled module "^(string_of_dirpath caller)^
+ " makes inconsistent assumptions over module "
+ ^(string_of_dirpath dir))
+and load_absolute_module_from dir =
+ try
+ load_module (locate_absolute_library dir)
+ with
+ | LibUnmappedDir ->
+ let prefix, dir = fst (split_dirpath dir), string_of_dirpath dir in
+ errorlabstrm "load_module"
+ [< 'sTR ("Cannot load "^dir^":"); 'sPC;
+ 'sTR "no physical path bound to"; 'sPC; pr_dirpath prefix; 'fNL >]
+ | LibNotFound ->
+ errorlabstrm "load_module"
+ [< 'sTR"Cannot find module "; pr_dirpath dir; 'sTR" in loadpath">]
+ | _ -> assert false
+
+let try_locate_qualified_library qid =
+ (* Look if loaded *)
+ try
+ let dir = Nametab.locate_loaded_library qid in
+ (LibLoaded, dir, module_full_filename dir)
+ with Not_found ->
+ (* Look if in loadpath *)
+ try
+ let dir, base = repr_qualid qid in
+ let loadpath =
+ if dir = [] then get_load_path ()
+ else if is_absolute_dirpath dir then
+ load_path_of_logical_path dir
+ else
+ error
+ ("Not loaded partially qualified library names not implemented: "
+ ^(string_of_qualid qid))
+ in
+ if loadpath = [] then raise LibUnmappedDir;
+ let name = (string_of_id base)^".vo" in
+ let path, file = System.where_in_path loadpath name in
+ (LibInPath, find_logical_path path@[base], file)
+ with Not_found -> raise LibNotFound
+
+let locate_qualified_library qid =
+ try
+ try_locate_qualified_library qid
+ with
+ | LibUnmappedDir ->
+ let prefix, id = repr_qualid qid in
+ errorlabstrm "load_module"
+ [< 'sTR ("Cannot load "^(string_of_id id)^":"); 'sPC;
+ 'sTR "no physical path bound to"; 'sPC; pr_dirpath prefix; 'fNL >]
+ | LibNotFound ->
+ errorlabstrm "load_module"
+ [< 'sTR"Cannot find module "; pr_qualid qid; 'sTR" in loadpath">]
+ | _ -> assert false
+
+let check_module_short_name f dir = function
+ | Some id when id <> snd (split_dirpath dir) ->
+ errorlabstrm "load_module"
+ [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
+ pr_dirpath dir; 'sPC; 'sTR "and not module"; 'sPC;
+ pr_id id >]
+ | _ -> ()
+
+let locate_by_filename_only id f =
+ let ch = with_magic_number_check raw_intern_module f in
+ let md = System.marshal_in ch in
+ let digest = System.marshal_in ch in
+ close_in ch;
+ (* Only the base name is expected to match *)
+ check_module_short_name f md.md_name id;
+ (* We check no other file containing same module is loaded *)
+ try
+ let m = CompUnitmap.find md.md_name !modules_table in
+ warning ((string_of_dirpath md.md_name)^" is already loaded from file "^
+ m.module_filename);
+ (LibLoaded, md.md_name, m.module_filename)
+ with Not_found ->
+ (match split_dirpath md.md_name with
+ | [], id -> Nametab.push_library_root id
+ | _ -> ());
+ compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
+ (LibInPath, md.md_name, f)
+
+let locate_module qid = function
+ | Some f ->
+ (* A name is specified, we have to check it contains module id *)
+ let prefix, id = repr_qualid qid in
+ assert (prefix = []);
+ let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
+ locate_by_filename_only (Some id) f
+ | None ->
+ (* No name, we need to find the file name *)
+ locate_qualified_library qid
+
+let read_module qid =
+ ignore (load_module (locate_qualified_library qid))
+
+let read_module_from_file f =
+ let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
+ ignore (load_module (locate_by_filename_only None f))
+
+let reload_module (modref, export) =
+ let m = load_module modref in
+ if export then m.module_exported <- true;
+ open_module false m.module_name
(*s [require_module] loads and opens a module. This is a synchronized
operation. *)
-let cache_require (_,(name,file,export)) =
- let m = load_module_from name file in
+type module_reference = (library_location * CompUnitmap.key * Util.Stringmap.key) * bool
+
+let cache_require (_,(modref,export)) =
+ let m = load_module modref in
if export then m.module_exported <- true;
- open_module false name
+ open_module false m.module_name
-let (in_require, _) =
+let (in_require, out_require) =
declare_object
("REQUIRE",
{ cache_function = cache_require;
@@ -199,32 +378,28 @@ let (in_require, _) =
open_function = (fun _ -> ());
export_function = (fun _ -> None) })
-let require_module spec name fileopt export =
+let require_module spec qid fileopt export =
(* Trop contraignant
if sections_are_opened () then
warning ("Objets of "^name^" not surviving sections (e.g. Grammar \nand Hints) will be removed at the end of the section");
*)
- let file = match fileopt with
- | None -> name
- | Some f -> f
- in
- add_anonymous_leaf (in_require (name,file,export));
+ let modref = locate_module qid fileopt in
+ add_anonymous_leaf (in_require (modref,export));
add_frozen_state ()
(*s [save_module s] saves the module [m] to the disk. *)
let current_imports () =
- Stringmap.fold
+ CompUnitmap.fold
(fun _ m l -> (m.module_name, m.module_digest, m.module_exported) :: l)
!modules_table []
-let save_module_to process s f =
- let seg = export_module () in
+let save_module_to s f =
+ let seg = export_module s in
let md = {
md_name = s;
md_compiled_env = Global.export s;
md_declarations = seg;
- md_nametab = process seg;
md_deps = current_imports () } in
let (f',ch) = raw_extern_module f in
try
@@ -234,6 +409,7 @@ let save_module_to process s f =
System.marshal_out ch di;
close_out ch
with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e)
+
(*s Iterators. *)
let fold_all_segments insec f x =
@@ -244,7 +420,7 @@ let fold_all_segments insec f x =
| _ -> acc
in
let acc' =
- Stringmap.fold
+ CompUnitmap.fold
(fun _ m acc -> List.fold_left apply acc m.module_declarations)
!modules_table x
in
@@ -256,7 +432,7 @@ let iter_all_segments insec f =
| _, ClosedSection (_,_,seg) -> if insec then List.iter apply seg
| _ -> ()
in
- Stringmap.iter
+ CompUnitmap.iter
(fun _ m -> List.iter apply m.module_declarations) !modules_table;
List.iter apply (Lib.contents_after None)
@@ -266,9 +442,9 @@ let fmt_modules_state () =
let opened = opened_modules ()
and loaded = loaded_modules () in
[< 'sTR "Imported (open) Modules: " ;
- prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) opened ; 'fNL ;
- 'sTR "Loaded Modules: " ;
- prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) loaded ; 'fNL >]
+ prlist_with_sep pr_spc pr_dirpath opened ; 'fNL ;
+ 'sTR "Loaded Modules: ";
+ prlist_with_sep pr_spc pr_dirpath loaded ; 'fNL >]
(*s Display the memory use of a module. *)
@@ -276,6 +452,6 @@ open Printf
let mem s =
let m = find_module s in
- h 0 [< 'sTR (sprintf "%dk (cenv = %dk / seg = %dk / nmt = %dk)"
+ h 0 [< 'sTR (sprintf "%dk (cenv = %dk / seg = %dk)"
(size_kb m) (size_kb m.module_compiled_env)
- (size_kb m.module_declarations) (size_kb m.module_nametab)) >]
+ (size_kb m.module_declarations)) >]
diff --git a/library/library.mli b/library/library.mli
index e5ad55e48c..3274f7361f 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -20,14 +20,15 @@ open Libobject
provides a high level function [require] which corresponds to the
vernacular command [Require]. *)
-val load_module : string -> string option -> unit
-val import_module : string -> unit
+val read_module : Nametab.qualid -> unit
+val read_module_from_file : System.physical_path -> unit
+val import_module : dir_path -> unit
-val module_is_loaded : string -> bool
+val module_is_loaded : dir_path -> bool
val module_is_opened : string -> bool
-val loaded_modules : unit -> string list
-val opened_modules : unit -> string list
+val loaded_modules : unit -> dir_path list
+val opened_modules : unit -> dir_path list
val fmt_modules_state : unit -> Pp.std_ppcmds
@@ -37,21 +38,21 @@ val fmt_modules_state : unit -> Pp.std_ppcmds
([false]), if not [None]. And [export] specifies if the module must be
exported. *)
-val require_module : bool option -> string -> string option -> bool -> unit
+val require_module :
+ bool option -> Nametab.qualid -> string option -> bool -> unit
(*s [save_module_to s f] saves the current environment as a module [s]
in the file [f]. *)
-val save_module_to : (Lib.library_segment -> Nametab.module_contents) ->
- string -> string -> unit
+val save_module_to : dir_path -> string -> unit
(*s [module_segment m] returns the segment of the loaded module
[m]; if not given, the segment of the current module is returned
(which is then the same as [Lib.contents_after None]).
- [module_filename] returns the full filename of a loaded module. *)
+ [module_full_filename] returns the full filename of a loaded module. *)
-val module_segment : string option -> Lib.library_segment
-val module_filename : string -> System.load_path_entry * string
+val module_segment : dir_path option -> Lib.library_segment
+val module_full_filename : dir_path -> string
(*s [fold_all_segments] and [iter_all_segments] iterate over all
segments, the modules' segments first and then the current
@@ -63,10 +64,28 @@ val fold_all_segments : bool -> ('a -> section_path -> obj -> 'a) -> 'a -> 'a
val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit
(*s Global load path *)
-val get_load_path : unit -> System.load_path
-val add_load_path_entry : System.load_path_entry -> unit
-val remove_path : string -> unit
+type logical_path = dir_path
+
+val get_load_path : unit -> System.physical_path list
+val get_full_load_path : unit -> (System.physical_path * logical_path) list
+val add_load_path_entry : System.physical_path * logical_path -> unit
+val remove_path : System.physical_path -> unit
+val find_logical_path : System.physical_path -> logical_path
+val load_path_of_logical_path : dir_path -> System.physical_path list
+
+exception LibUnmappedDir
+exception LibNotFound
+type library_location = LibLoaded | LibInPath
+
+val locate_qualified_library :
+ Nametab.qualid -> library_location * dir_path * System.physical_path
(*s Displays the memory use of a module. *)
-val mem : string -> Pp.std_ppcmds
+val mem : dir_path -> Pp.std_ppcmds
+
+(* For discharge *)
+type module_reference
+
+val out_require : Libobject.obj -> module_reference
+val reload_module : module_reference -> unit
diff --git a/library/nametab.ml b/library/nametab.ml
index aec5da6f90..3d7ca98f4e 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -16,16 +16,20 @@ open Declarations
open Term
(*s qualified names *)
-type qualid = string list * identifier
+type qualid = dir_path * identifier
let make_qualid p id = (p,id)
let repr_qualid q = q
-let string_of_qualid (l,id) = String.concat "." (l@[string_of_id id])
-let pr_qualid (l,id) =
- prlist_with_sep (fun () -> pr_str ".") pr_str (l@[string_of_id id])
+let string_of_qualid (l,id) =
+ let dir = if l = [] then "" else string_of_dirpath l ^ "." in
+ dir ^ string_of_id id
+let pr_qualid p = pr_str (string_of_qualid p)
let qualid_of_sp sp = make_qualid (dirpath sp) (basename sp)
+let qualid_of_dirpath dir =
+ let a,l = list_sep_last (repr_qualid dir) in
+ make_qualid l a
exception GlobalizationError of qualid
@@ -39,141 +43,161 @@ let error_global_not_found q = raise (GlobalizationError q)
let roots = ref []
let push_library_root s = roots := list_add_set s !roots
-let coq_root = "Coq"
-let default_root = "Scratch"
-
-(* Names tables *)
-type cci_table = global_reference Idmap.t
-type obj_table = (section_path * obj) Idmap.t
-type mod_table = (section_path * module_contents) Stringmap.t
-and module_contents = Closed of cci_table * obj_table * mod_table
-
-let empty =
- Closed (Idmap.empty, Idmap.empty, Stringmap.empty)
-
-let persistent_nametab = ref (empty : module_contents)
-let local_nametab = ref (empty : module_contents)
-
-let push_cci (Closed (ccitab, objtab, modtab)) s ref =
- Closed (Idmap.add s ref ccitab, objtab, modtab)
-
-let push_obj (Closed (ccitab, objtab, modtab)) s obj =
- Closed (ccitab, Idmap.add s obj objtab, modtab)
-
-let push_mod (Closed (ccitab, objtab, modtab)) s mc =
- (* devrait pas mais ca plante en décommentant la ligne ci-dessous *)
- (* assert (not (Stringmap.mem s modtab)); *)
- Closed (ccitab, objtab, Stringmap.add s mc modtab)
-
-let push_tree push dir id o =
- let rec search (Closed (ccitab, objtab, modtab) as tabs) pref = function
- | id :: dir' ->
- let sp, mc =
- try Stringmap.find id modtab
- with Not_found ->
- let pref = List.rev pref in
- (make_path dir (id_of_string id) CCI, empty)
+let coq_root = id_of_string "Coq"
+let default_root_prefix = []
+
+(* Constructions and syntactic definitions live in the same space *)
+type extended_global_reference =
+ | TrueGlobal of global_reference
+ | SyntacticDef of section_path
+
+type 'a nametree = ('a option * 'a nametree ModIdmap.t)
+type ccitab = extended_global_reference nametree Idmap.t
+type objtab = section_path nametree Idmap.t
+type dirtab = dir_path nametree ModIdmap.t
+
+let the_ccitab = ref (Idmap.empty : ccitab)
+let the_libtab = ref (ModIdmap.empty : dirtab)
+let the_sectab = ref (ModIdmap.empty : dirtab)
+let the_objtab = ref (Idmap.empty : objtab)
+
+(* How necessarily_open works: concretely, roots and directory are
+ always open but libraries are open only during their interactive
+ construction or on demand if a precompiled one; then for a name
+ "Root.Rep.Lib.name", then "Lib.name", "Rep.Lib.name" and
+ "Root.Rep.Lib.name", but not "name" are pushed *)
+
+(* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *)
+(* We proceed in the reverse way, looking first to [id] *)
+let push_tree tab dir o =
+ let rec push necessarily_open (current,dirmap) = function
+ | modid :: path as dir ->
+ let mc =
+ try ModIdmap.find modid dirmap
+ with Not_found -> (None, ModIdmap.empty)
in
- Closed (ccitab, objtab,
- Stringmap.add id (sp,search mc (id::pref) dir') modtab)
- | [] ->
- push tabs id o in
- persistent_nametab := search !persistent_nametab [] dir
-
-(* This pushes a name at the current level (for relative qualified use) *)
-let push_cci_current = push_tree push_cci []
-let push_obj_current = push_tree push_obj []
-let push_mod_current = push_tree push_mod []
-
-(* This pushes a name at the root level (for absolute access) *)
-let push_cci_absolute = push_tree push_cci
-let push_obj_absolute = push_tree push_obj
-let push_mod_absolute = push_tree push_mod
+ let this = if necessarily_open then Some o else current in
+ (this, ModIdmap.add modid (push true mc path) dirmap)
+ | [] -> (Some o,dirmap) in
+ push false tab (List.rev dir)
+
+let push_idtree tab dir id o =
+ let modtab =
+ try Idmap.find id !tab
+ with Not_found -> (None, ModIdmap.empty) in
+ tab := Idmap.add id (push_tree modtab dir o) !tab
+
+let push_long_names_ccipath = push_idtree the_ccitab
+let push_short_name_ccipath = push_idtree the_ccitab
+let push_short_name_objpath = push_idtree the_objtab
+
+let push_modidtree tab dir id o =
+ let modtab =
+ try ModIdmap.find id !tab
+ with Not_found -> (None, ModIdmap.empty) in
+ tab := ModIdmap.add id (push_tree modtab dir o) !tab
+
+let push_long_names_secpath = push_modidtree the_sectab
+let push_long_names_libpath = push_modidtree the_libtab
(* These are entry points for new declarations at toplevel *)
-(* Do not use with "open" since it pushes an absolute name too *)
-let push sp ref =
- let dir, s = repr_qualid (qualid_of_sp sp) in
- push_cci_absolute dir s ref;
- push_cci_current s ref
-let push_object sp obj =
- let dir, s = repr_qualid (qualid_of_sp sp) in
- push_obj_absolute dir s (sp,obj);
- push_obj_current s (sp,obj)
+(* This is for permanent constructions (never discharged -- but with
+ possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
+ Parameter but also Remark and Fact) *)
-let push_module sp mc =
- let dir, s = repr_qualid (qualid_of_sp sp) in
- let s = string_of_id s in
- push_mod_absolute dir s (sp,mc);
- if List.mem s !roots then
- warning ("Cannot allow access to "^s^" by relative paths: it is already registered as a root of the Coq library")
- else push_mod_current s (sp,mc)
-
-(* Sections are not accessible by basename *)
-let push_section sp mc =
+let push_cci sp ref =
let dir, s = repr_qualid (qualid_of_sp sp) in
- push_mod_absolute dir (string_of_id s) (sp,mc)
+ (* We push partially qualified name (with at least one prefix) *)
+ push_long_names_ccipath dir s (TrueGlobal ref)
-(* This is an entry point for local declarations at toplevel *)
-(* Do not use with "open" since it pushes an absolute name too *)
+let push = push_cci
-let push_cci_local s ref =
- local_nametab := push_cci !local_nametab s ref
+let push_short_name id ref =
+ (* We push a volatile unqualified name *)
+ push_short_name_ccipath [] id (TrueGlobal ref)
-let push_obj_local s o =
- local_nametab := push_obj !local_nametab s o
+(* This is for Syntactic Definitions *)
-let push_local sp ref =
+let push_syntactic_definition sp =
let dir, s = repr_qualid (qualid_of_sp sp) in
- push_cci_absolute dir s ref;
- push_cci_local s ref
+ push_long_names_ccipath dir s (SyntacticDef sp)
-let push_local_object sp obj =
- let dir, s = repr_qualid (qualid_of_sp sp) in
- push_obj_absolute dir s (sp,obj);
- push_obj_local s (sp,obj)
+let push_short_name_syntactic_definition sp =
+ let _, s = repr_qualid (qualid_of_sp sp) in
+ push_short_name_ccipath [] s (SyntacticDef sp)
+
+(* This is for dischargeable non-cci objects (removed at the end of the
+ section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
+
+let push_short_name_object sp =
+ push_short_name_objpath [] (basename sp) sp
+
+(* This is to remember absolute Section/Module names and to avoid redundancy *)
+
+let push_section fulldir =
+ let dir, s = split_dirpath fulldir in
+ (* We push all partially qualified name *)
+ push_long_names_secpath dir s fulldir;
+ push_long_names_secpath [] s fulldir
(* These are entry points to locate names *)
(* If the name starts with the coq_root name, then it is an absolute name *)
-let locate qid =
- let (dir,id) = repr_qualid qid in
- let rec search (Closed (ccitab,_,modtab)) = function
- | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
- | [] -> Idmap.find id ccitab
+let locate_in_tree tab dir =
+ let dir = List.rev dir in
+ let rec search (current,modidtab) = function
+ | modid :: path -> search (ModIdmap.find modid modidtab) path
+ | [] -> match current with Some o -> o | _ -> raise Not_found
in
- try search !local_nametab dir
- with Not_found -> search !persistent_nametab dir
+ search tab dir
+
+let locate_cci qid =
+ let (dir,id) = repr_qualid qid in
+ locate_in_tree (Idmap.find id !the_ccitab) dir
+
+(* This should be used when syntactic definitions are allowed *)
+let extended_locate = locate_cci
+
+(* This should be used when no syntactic definitions is expected *)
+let locate qid = match locate_cci qid with
+ | TrueGlobal ref -> ref
+ | SyntacticDef _ -> raise Not_found
let locate_obj qid =
let (dir,id) = repr_qualid qid in
- let rec search (Closed (_,objtab,modtab)) = function
- | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
- | [] -> Idmap.find id objtab
- in
- try search !local_nametab dir
- with Not_found -> search !persistent_nametab dir
+ locate_in_tree (Idmap.find id !the_objtab) dir
+
+(* Actually, this table has only two levels, since only basename and *)
+(* fullname are registered *)
+let push_loaded_library fulldir =
+ let dir, s = split_dirpath fulldir in
+ push_long_names_libpath dir s fulldir;
+ push_long_names_libpath [] s fulldir
-let locate_module qid =
+let locate_loaded_library qid =
let (dir,id) = repr_qualid qid in
- let s = string_of_id id in
- let rec search (Closed (_,_,modtab)) = function
- | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
- | [] -> Stringmap.find s modtab
- in
- try search !local_nametab dir
- with Not_found -> search !persistent_nametab dir
+ locate_in_tree (ModIdmap.find id !the_libtab) dir
+
+let locate_section qid =
+ let (dir,id) = repr_qualid qid in
+ locate_in_tree (ModIdmap.find id !the_sectab) dir
+
+(* Derived functions *)
let locate_constant qid =
- match locate qid with
- | ConstRef sp -> sp
+ match locate_cci qid with
+ | TrueGlobal (ConstRef sp) -> sp
| _ -> raise Not_found
-let sp_of_id _ id = locate (make_qualid [] id)
+let sp_of_id _ id = match locate_cci (make_qualid [] id) with
+ | TrueGlobal ref -> ref
+ | SyntacticDef _ ->
+ anomaly ("sp_of_id: "^(string_of_id id)
+ ^" is not a true global reference but a syntactic definition")
let constant_sp_of_id id =
- match locate (make_qualid [] id) with
- | ConstRef sp -> sp
+ match locate_cci (make_qualid [] id) with
+ | TrueGlobal (ConstRef sp) -> sp
| _ -> raise Not_found
let check_absoluteness dir =
@@ -181,29 +205,19 @@ let check_absoluteness dir =
| a::_ when List.mem a !roots -> ()
| _ -> anomaly ("Not an absolute dirpath: "^(string_of_dirpath dir))
+let is_absolute_dirpath = function
+ | a::_ when List.mem a !roots -> true
+ | _ -> false
+
let absolute_reference sp =
check_absoluteness (dirpath sp);
locate (qualid_of_sp sp)
-exception Found of global_reference
-let locate_in_module dir id =
- let rec exists_in id (Closed (ccitab,_,modtab)) =
- try raise (Found (Idmap.find id ccitab))
- with Not_found ->
- Stringmap.iter (fun _ (sp,mc) -> exists_in id mc) modtab
- in
- let rec search (Closed (ccitab,_,modtab) as mc) = function
- | modid :: dir' -> search (snd (Stringmap.find modid modtab)) dir'
- | [] ->
- try exists_in id mc; raise Not_found
- with Found ref -> ref
- in
- search !persistent_nametab dir
-
let locate_in_absolute_module dir id =
check_absoluteness dir;
- locate_in_module dir id
+ locate (make_qualid dir id)
+(*
(* These are entry points to make the contents of a module/section visible *)
(* in the current env (does not affect the absolute name space `coq_root') *)
let open_module_contents qid =
@@ -229,40 +243,46 @@ let rec rec_open_module_contents qid =
push_mod_current m mt;
rec_open_module_contents (qualid_of_sp sp))
modtab
-
+*)
let exists_cci sp =
- try let _ = locate (qualid_of_sp sp) in true with Not_found -> false
+ try let _ = locate_cci (qualid_of_sp sp) in true
+ with Not_found -> false
-let exists_module sp =
- try let _ = locate_module (qualid_of_sp sp) in true with Not_found -> false
+let exists_section dir =
+ try let _ = locate_section (qualid_of_dirpath dir) in true
+ with Not_found -> false
(********************************************************************)
-(* Registration of persistent tables as a global table and rollback *)
-
-type frozen = module_contents
-
-let init () = persistent_nametab := empty; roots := []
-let freeze () = !persistent_nametab, !roots
-let unfreeze (mc,r) = persistent_nametab := mc; roots := r
-
-let _ =
- Summary.declare_summary "persistent-names"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init;
- Summary.survive_section = true }
(********************************************************************)
-(* Registration of persistent tables as a global table and rollback *)
-
-let init () = local_nametab := empty
-let freeze () = !local_nametab
-let unfreeze mc = local_nametab := mc
+(* Registration of tables as a global table and rollback *)
+
+type frozen = ccitab * dirtab * dirtab * objtab * identifier list
+
+let init () =
+ the_ccitab := Idmap.empty;
+ the_libtab := ModIdmap.empty;
+ the_sectab := ModIdmap.empty;
+ the_objtab := Idmap.empty;
+ roots := []
+
+let freeze () =
+ !the_ccitab,
+ !the_libtab,
+ !the_sectab,
+ !the_objtab,
+ !roots
+
+let unfreeze (mc,ml,ms,mo,r) =
+ the_ccitab := mc;
+ the_libtab := ml;
+ the_sectab := ms;
+ the_objtab := mo;
+ roots := r
let _ =
- Summary.declare_summary "local-names"
+ Summary.declare_summary "names"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init;
Summary.survive_section = false }
-
diff --git a/library/nametab.mli b/library/nametab.mli
index 8506c7a5b5..927205dea9 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -18,6 +18,10 @@ open Term
(*s This module contains the table for globalization, which associates global
names (section paths) to qualified names. *)
+type extended_global_reference =
+ | TrueGlobal of global_reference
+ | SyntacticDef of section_path
+
(*s A [qualid] is a partially qualified ident; it includes fully
qualified names (= absolute names) and all intermediate partial
qualifications of absolute names, including single identifiers *)
@@ -38,19 +42,17 @@ exception GlobalizationError of qualid
val error_global_not_found_loc : loc -> qualid -> 'a
val error_global_not_found : qualid -> 'a
-(*s Names tables *)
-type cci_table = global_reference Idmap.t
-type obj_table = (section_path * Libobject.obj) Idmap.t
-type mod_table = (section_path * module_contents) Stringmap.t
-and module_contents = Closed of cci_table * obj_table * mod_table
-
-(*s Registers absolute paths *)
+(*s Register visibility of absolute paths by qualified names *)
val push : section_path -> global_reference -> unit
-val push_object : section_path -> Libobject.obj -> unit
-val push_module : section_path -> module_contents -> unit
+val push_syntactic_definition : section_path -> unit
+
+(*s Register visibility of absolute paths by short names *)
+val push_short_name : identifier -> global_reference -> unit
+val push_short_name_syntactic_definition : section_path -> unit
+val push_short_name_object : section_path -> unit
-val push_local : section_path -> global_reference -> unit
-val push_local_object : section_path -> Libobject.obj -> unit
+(*s Register visibility by all qualifications *)
+val push_section : dir_path -> unit
(* This should eventually disappear *)
val sp_of_id : path_kind -> identifier -> global_reference
@@ -61,37 +63,47 @@ val sp_of_id : path_kind -> identifier -> global_reference
val constant_sp_of_id : identifier -> section_path
val locate : qualid -> global_reference
-val locate_obj : qualid -> (section_path * Libobject.obj)
+
+(* This locates also syntactic definitions *)
+val extended_locate : qualid -> extended_global_reference
+
+val locate_obj : qualid -> section_path
+
val locate_constant : qualid -> constant_path
-val locate_module : qualid -> section_path * module_contents
+val locate_section : qualid -> dir_path
(* [exists sp] tells if [sp] is already bound to a cci term *)
val exists_cci : section_path -> bool
-val exists_module : section_path -> bool
-
+val exists_section : dir_path -> bool
+(*
val open_module_contents : qualid -> unit
val rec_open_module_contents : qualid -> unit
(*s Entry points for sections *)
val open_section_contents : qualid -> unit
val push_section : section_path -> module_contents -> unit
-
+*)
(*s Roots of the space of absolute names *)
(* This is the root of the standard library of Coq *)
-val coq_root : string
+val coq_root : module_ident
-(* This is the default root for developments which doesn't mention a root *)
-val default_root : string
+(* This is the default root prefix for developments which doesn't mention a root *)
+val default_root_prefix : dir_path
(* This is to declare a new root *)
-val push_library_root : string -> unit
+val push_library_root : module_ident -> unit
(* This turns a "user" absolute name into a global reference;
especially, constructor/inductive names are turned into internal
references inside a block of mutual inductive *)
val absolute_reference : section_path -> global_reference
+val is_absolute_dirpath : dir_path -> bool
+
(* [locate_in_absolute_module dir id] finds [id] in module [dir] or in
one of its section/subsection *)
val locate_in_absolute_module : dir_path -> identifier -> global_reference
+
+val push_loaded_library : dir_path -> unit
+val locate_loaded_library : qualid -> dir_path
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:34:06 +0000