From 6497f27021fec4e01f2182014f2bb1989b4707f9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 31 Jan 2005 14:34:14 +0000 Subject: Imported Upstream version 8.0pl2 --- library/declaremods.mli | 6 +++--- library/lib.ml | 14 +++++++++++++- library/lib.mli | 9 ++++++--- library/libnames.mli | 8 ++++---- library/libobject.mli | 4 ++-- library/library.ml | 14 ++++++++------ library/nameops.ml | 6 +++--- library/nameops.mli | 4 ++-- library/nametab.mli | 9 +++++---- 9 files changed, 46 insertions(+), 28 deletions(-) (limited to 'library') diff --git a/library/declaremods.mli b/library/declaremods.mli index f229da1e..f896310a 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.mli,v 1.8.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) +(*i $Id: declaremods.mli,v 1.8.2.2 2005/01/21 16:41:50 herbelin Exp $ i*) (*i*) open Util @@ -85,7 +85,7 @@ val end_library : (* [really_import_module mp] opens the module [mp] (in a Caml sense). - It modifies Nametab and performs the "open_object" function for + It modifies Nametab and performs the [open_object] function for every object of the module. *) val really_import_module : module_path -> unit @@ -109,7 +109,7 @@ val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit val debug_print_modtab : unit -> Pp.std_ppcmds -(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*) +(*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*) (* For translator *) val process_module_bindings : module_ident list -> diff --git a/library/lib.ml b/library/lib.ml index b9da6dea..a9f864ef 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml,v 1.63.2.2 2004/07/16 19:30:35 herbelin Exp $ *) +(* $Id: lib.ml,v 1.63.2.3 2004/11/22 14:21:23 herbelin Exp $ *) open Pp open Util @@ -564,3 +564,15 @@ let library_part ref = else (* Theorem/Lemma outside its outer section of definition *) dir + + +let rec file_of_mp = function + | MPfile dir -> Some dir + | MPself _ -> Some (library_dp ()) + | MPbound _ -> None + | MPdot (mp,_) -> file_of_mp mp + +let file_part = function + | VarRef id -> anomaly "TODO"; + | ConstRef kn | ConstructRef ((kn,_),_) | IndRef (kn,_) -> + file_of_mp (modpath kn) diff --git a/library/lib.mli b/library/lib.mli index 8981754e..aa874470 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli,v 1.41.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) +(*i $Id: lib.mli,v 1.41.2.3 2005/01/21 16:41:50 herbelin Exp $ i*) (*i*) open Util @@ -59,7 +59,7 @@ val add_leaf : identifier -> obj -> object_name val add_absolutely_named_leaf : object_name -> obj -> unit val add_anonymous_leaf : obj -> unit -(* this operation adds all objects with the same name and calls load_object +(* this operation adds all objects with the same name and calls [load_object] for each of them *) val add_leaves : identifier -> obj list -> object_name @@ -107,7 +107,7 @@ val start_modtype : module_ident -> module_path -> Summary.frozen -> object_prefix val end_modtype : module_ident -> object_name * object_prefix * Summary.frozen * library_segment -(* Lib.add_frozen_state must be called after each of the above functions *) +(* [Lib.add_frozen_state] must be called after each of the above functions *) (*s Compilation units *) @@ -121,6 +121,9 @@ val library_dp : unit -> dir_path (* Extract the library part of a name even if in a section *) val library_part : global_reference -> dir_path +(* Extract the library part of a name if not in a functor *) +val file_part : global_reference -> dir_path option + (*s Sections *) val open_section : identifier -> object_prefix diff --git a/library/libnames.mli b/library/libnames.mli index 6f05333c..a6055428 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.mli,v 1.8.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) +(*i $Id: libnames.mli,v 1.8.2.2 2005/01/21 16:41:51 herbelin Exp $ i*) (*i*) open Pp @@ -111,8 +111,8 @@ val qualid_of_dirpath : dir_path -> qualid val make_short_qualid : identifier -> qualid -(* Both names are passed to objects: a "semantic" kernel_name, which - can be substituted and a "syntactic" section_path which can be printed +(* Both names are passed to objects: a "semantic" [kernel_name], which + can be substituted and a "syntactic" [section_path] which can be printed *) type object_name = section_path * kernel_name @@ -121,7 +121,7 @@ type object_prefix = dir_path * (module_path * dir_path) val make_oname : object_prefix -> identifier -> object_name -(* to this type are mapped dir_path's in the nametab *) +(* to this type are mapped [dir_path]'s in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix diff --git a/library/libobject.mli b/library/libobject.mli index 8a3811e1..b9070f5d 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libobject.mli,v 1.9.8.1 2004/07/16 19:30:35 herbelin Exp $ i*) +(*i $Id: libobject.mli,v 1.9.8.2 2005/01/21 16:41:51 herbelin Exp $ i*) (*i*) open Names @@ -39,7 +39,7 @@ open Libnames Keep - the object is not substitutive, but survives module closing Anticipate - this is for objects which have to be explicitely - managed by the end_module function (like Require + managed by the [end_module] function (like Require and Read markers) The classification function is also an occasion for a cleanup diff --git a/library/library.ml b/library/library.ml index 0477a8f3..cbc8874a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml,v 1.79.2.1 2004/07/16 19:30:36 herbelin Exp $ *) +(* $Id: library.ml,v 1.79.2.2 2004/11/17 14:01:26 herbelin Exp $ *) open Pp open Util @@ -169,8 +169,10 @@ let _ = Summary.survive_section = false } let find_library s = - try - CompilingLibraryMap.find s !libraries_table + CompilingLibraryMap.find s !libraries_table + +let try_find_library s = + try find_library s with Not_found -> error ("Unknown library " ^ (string_of_dirpath s)) @@ -250,7 +252,7 @@ let open_libraries export modl = (fun l m -> let subimport = List.fold_left - (fun l m -> remember_last_of_each l (find_library m)) + (fun l m -> remember_last_of_each l (try_find_library m)) l m.library_imports in remember_last_of_each subimport m) [] modl in @@ -261,7 +263,7 @@ let open_libraries export modl = (* import and export - synchronous operations*) let cache_import (_,(dir,export)) = - open_libraries export [find_library dir] + open_libraries export [try_find_library dir] let open_import i (_,(dir,_) as obj) = if i=1 then @@ -698,7 +700,7 @@ let check_required_library d = open Printf let mem s = - let m = find_library s in + let m = try_find_library s in h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" (size_kb m) (size_kb m.library_compiled) (size_kb m.library_objects))) diff --git a/library/nameops.ml b/library/nameops.ml index ea40aae5..35b707a7 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml,v 1.21.2.1 2004/07/16 19:30:36 herbelin Exp $ *) +(* $Id: nameops.ml,v 1.21.2.2 2004/10/12 10:12:31 herbelin Exp $ *) open Pp open Util @@ -29,8 +29,8 @@ let cut_ident skip_quote s = (* [n'] is the position of the first non nullary digit *) let rec numpart n n' = if n = 0 then - error - ("The string " ^ s ^ " is not an identifier: it contains only digits or _") + (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *) + slen else let c = Char.code (String.get s (n-1)) in if c = code_of_0 && n <> slen then diff --git a/library/nameops.mli b/library/nameops.mli index 4b7cecda..71dbf040 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.mli,v 1.12.2.1 2004/07/16 19:30:36 herbelin Exp $ *) +(*i $Id: nameops.mli,v 1.12.2.3 2005/01/21 17:14:10 herbelin Exp $ i*) open Names @@ -18,7 +18,7 @@ val make_ident : string -> int option -> identifier val repr_ident : identifier -> string * int option val atompart_of_id : identifier -> string (* remove trailing digits *) -val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *) +val root_of_id : identifier -> identifier (* remove trailing digits, $'$ and $\_$ *) val add_suffix : identifier -> string -> identifier val add_prefix : string -> identifier -> identifier diff --git a/library/nametab.mli b/library/nametab.mli index 3a0bd670..08a9d1bb 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nametab.mli,v 1.43.2.1 2004/07/16 19:30:36 herbelin Exp $ i*) +(*i $Id: nametab.mli,v 1.43.2.2 2005/01/21 16:41:51 herbelin Exp $ i*) (*i*) open Util @@ -33,13 +33,14 @@ open Libnames \item [locate : qualid -> object_reference] - Finds the object referred to by [qualid] or raises Not_found + Finds the object referred to by [qualid] or raises [Not_found] - \item [name_of] : object_reference -> user_name + \item [name_of : object_reference -> user_name] The [user_name] can be for example the shortest non ambiguous [qualid] or the [full_user_name] or [identifier]. Such a function can also have a local context argument. + \end{itemize} *) @@ -155,7 +156,7 @@ val id_of_global : global_reference -> identifier val pr_global_env : Idset.t -> global_reference -> std_ppcmds -(* The [shortest_qualid] functions given an object with user_name +(* The [shortest_qualid] functions given an object with [user_name] Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes the same object. *) -- cgit v1.2.3