summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml17
-rw-r--r--library/decl_kinds.mli12
-rw-r--r--library/declaremods.ml145
-rw-r--r--library/impargs.ml10
-rw-r--r--library/impargs.mli8
-rw-r--r--library/lib.ml118
-rw-r--r--library/lib.mli118
-rw-r--r--library/libnames.ml26
-rw-r--r--library/libnames.mli3
-rw-r--r--library/libobject.ml7
-rw-r--r--library/library.ml130
-rw-r--r--library/library.mli6
12 files changed, 326 insertions, 274 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 8f2525b8..d6dfbb6b 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_kinds.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: decl_kinds.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
open Util
open Libnames
@@ -112,3 +112,18 @@ let strength_of_global = function
let string_of_strength = function
| Local -> "Local"
| Global -> "Global"
+
+
+(* Recursive power *)
+
+(* spiwack: this definition might be of use in the kernel, for now I do not
+ push them deeper than needed, though. *)
+type recursivity_kind =
+ | Finite (* = inductive *)
+ | CoFinite (* = coinductive *)
+ | BiFinite (* = non-recursive, like in "Record" definitions *)
+
+(* helper, converts to "finiteness flag" booleans *)
+let recursivity_flag_of_kind = function
+ | Finite | BiFinite -> true
+ | CoFinite -> false
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 9358c4b5..70c63c39 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_kinds.mli 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: decl_kinds.mli 11809 2009-01-20 11:39:55Z aspiwack $ *)
open Util
open Libnames
@@ -82,3 +82,13 @@ val string_of_definition_kind :
val strength_of_global : global_reference -> locality
val string_of_strength : locality -> string
+
+(* About recursive power of type declarations *)
+
+type recursivity_kind =
+ | Finite (* = inductive *)
+ | CoFinite (* = coinductive *)
+ | BiFinite (* = non-recursive, like in "Record" definitions *)
+
+(* helper, converts to "finiteness flag" booleans *)
+val recursivity_flag_of_kind : recursivity_kind -> bool
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b630b5dc..de1893c7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declaremods.ml 11246 2008-07-22 15:10:05Z soubiran $ i*)
+(*i $Id: declaremods.ml 11703 2008-12-18 15:54:41Z soubiran $ i*)
open Pp
open Util
open Names
@@ -151,37 +151,60 @@ let check_subtypes mp sub_mtb =
in
() (* The constraints are checked and forgot immediately! *)
-let subst_substobjs dir mp (subst,mbids,msid,objs) =
+let compute_subst_objects mp (subst,mbids,msid,objs) =
match mbids with
- | [] ->
+ | [] ->
+ let subst' = join_alias (map_msid msid mp) subst in
+ Some (join (map_msid msid mp) (join subst' subst), objs)
+ | _ ->
+ None
+
+let subst_substobjs dir mp substobjs =
+ match compute_subst_objects mp substobjs with
+ | Some (subst, objs) ->
let prefix = dir,(mp,empty_dirpath) in
- let subst' = join_alias (map_msid msid mp) subst in
- let subst = join subst' subst in
- Some (subst_objects prefix (join (map_msid msid mp) subst) objs)
- | _ -> None
+ Some (subst_objects prefix subst objs)
+ | None -> None
+
+(* These functions register the visibility of the module and iterates
+ through its components. They are called by plenty module functions *)
+
+let compute_visibility exists what i dir dirinfo =
+ if exists then
+ if
+ try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
+ with Not_found -> false
+ then
+ Nametab.Exactly i
+ else
+ errorlabstrm (what^"_module")
+ (pr_dirpath dir ++ str " should already exist!")
+ else
+ if Nametab.exists_dir dir then
+ errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
+ else
+ Nametab.Until i
-(* This function registers the visibility of the module and iterates
- through its components. It is called by plenty module functions *)
+let do_load_and_subst_module i dir mp substobjs keep =
+ let prefix = (dir,(mp,empty_dirpath)) in
+ let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
+ let vis = compute_visibility false "load_and_subst" i dir dirinfo in
+ let objects = compute_subst_objects mp substobjs in
+ Nametab.push_dir vis dir dirinfo;
+ modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
+ match objects with
+ | Some (subst,seg) ->
+ let seg = load_and_subst_objects (i+1) prefix subst seg in
+ modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
+ load_objects (i+1) prefix keep;
+ Some (seg@keep)
+ | None ->
+ None
let do_module exists what iter_objects i dir mp substobjs objects =
let prefix = (dir,(mp,empty_dirpath)) in
let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
- let vis =
- if exists then
- if
- try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
- with Not_found -> false
- then
- Nametab.Exactly i
- else
- errorlabstrm (what^"_module")
- (pr_dirpath dir ++ str " should already exist!")
- else
- if Nametab.exists_dir dir then
- errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
- else
- Nametab.Until i
- in
+ let vis = compute_visibility exists what i dir dirinfo in
Nametab.push_dir vis dir dirinfo;
modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
match objects with
@@ -324,22 +347,7 @@ and do_module_alias exists what iter_objects i dir mp alias substobjs objects =
try Some (MPmap.find alias !modtab_objects) with
Not_found -> None in
let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
- let vis =
- if exists then
- if
- try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
- with Not_found -> false
- then
- Nametab.Exactly i
- else
- errorlabstrm (what^"_module")
- (pr_dirpath dir ++ str " should already exist!")
- else
- if Nametab.exists_dir dir then
- errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
- else
- Nametab.Until i
- in
+ let vis = compute_visibility exists what i dir dirinfo in
Nametab.push_dir vis dir dirinfo;
modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
match alias_objects,objects with
@@ -588,16 +596,21 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp =
let rec replace_idl = function
| _,[] -> []
| id::idl,(id',obj)::tail when id = id' ->
- if object_tag obj = "MODULE" then
+ let tag = object_tag obj in
+ if tag = "MODULE" or tag ="MODULE ALIAS" then
(match idl with
[] -> (id, in_module_alias (Some
({mod_entry_type = None;
mod_entry_expr = Some (MSEident mp)},None)
,modobjs,None))::tail
| _ ->
- let (_,substobjs,_) = out_module obj in
+ let (a,substobjs,_) = if tag = "MODULE ALIAS" then
+ out_module_alias obj else out_module obj in
let substobjs' = replace_module_object idl substobjs modobjs mp in
- (id, in_module (None,substobjs',None))::tail
+ if tag = "MODULE ALIAS" then
+ (id, in_module_alias (a,substobjs',None))::tail
+ else
+ (id, in_module (None,substobjs',None))::tail
)
else error "MODULE expected!"
| idl,lobj::tail -> lobj::replace_idl (idl,tail)
@@ -645,8 +658,8 @@ let rec get_modtype_substobjs env = function
(* application outside the kernel, only for substitutive
objects (that are all non-logical objects) *)
((join
- (join subst (map_mbid mbid mp (Some resolve)))
- sub3)
+ (join subst sub3)
+ (map_mbid mbid mp (Some resolve)))
, mbids, msid, objs)
| [] -> match mexpr with
| MSEident _ -> error "Application of a non-functor"
@@ -662,8 +675,7 @@ let process_module_bindings argids args =
let dir = make_dirpath [id] in
let mp = MPbound mbid in
let substobjs = get_modtype_substobjs (Global.env()) mty in
- let substituted = subst_substobjs dir mp substobjs in
- do_module false "start" load_objects 1 dir mp substobjs substituted
+ ignore (do_load_and_subst_module 1 dir mp substobjs [])
in
List.iter2 process_arg argids args
@@ -677,8 +689,7 @@ let intern_args interp_modtype (idl,arg) =
(fun dir mbid ->
Global.add_module_parameter mbid mty;
let mp = MPbound mbid in
- let substituted = subst_substobjs dir mp substobjs in
- do_module false "interp" load_objects 1 dir mp substobjs substituted;
+ ignore (do_load_and_subst_module 1 dir mp substobjs []);
(mbid,mty))
dirs mbids
@@ -792,25 +803,19 @@ type library_objects =
let register_library dir cenv objs digest =
let mp = MPfile dir in
- let substobjs, objects =
- try
- ignore(Global.lookup_module mp);
- (* if it's in the environment, the cached objects should be correct *)
- Dirmap.find dir !library_cache
- with
- Not_found ->
- if mp <> Global.import cenv digest then
- anomaly "Unexpected disk module name";
- let msid,substitute,keep = objs in
- let substobjs = empty_subst, [], msid, substitute in
- let substituted = subst_substobjs dir mp substobjs in
- let objects = Option.map (fun seg -> seg@keep) substituted in
- let modobjs = substobjs, objects in
- library_cache := Dirmap.add dir modobjs !library_cache;
- modobjs
- in
+ try
+ ignore(Global.lookup_module mp);
+ (* if it's in the environment, the cached objects should be correct *)
+ let substobjs, objects = Dirmap.find dir !library_cache in
do_module false "register_library" load_objects 1 dir mp substobjs objects
-
+ with Not_found ->
+ if mp <> Global.import cenv digest then
+ anomaly "Unexpected disk module name";
+ let msid,substitute,keep = objs in
+ let substobjs = empty_subst, [], msid, substitute in
+ let objects = do_load_and_subst_module 1 dir mp substobjs keep in
+ let modobjs = substobjs, objects in
+ library_cache := Dirmap.add dir modobjs !library_cache
let start_library dir =
let mp = Global.start_library dir in
@@ -960,8 +965,8 @@ let rec get_module_substobjs env = function
(* application outside the kernel, only for substitutive
objects (that are all non-logical objects) *)
((join
- (join subst (map_mbid mbid mp (Some resolve)))
- sub3)
+ (join subst sub3)
+ (map_mbid mbid mp (Some resolve)))
, mbids, msid, objs)
| [] -> match mexpr with
| MSEident _ -> error "Application of a non-functor"
diff --git a/library/impargs.ml b/library/impargs.ml
index 3a505ddb..2b2c607c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: impargs.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: impargs.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
open Util
open Names
@@ -71,6 +71,7 @@ let make_maximal_implicit_args flag =
let is_implicit_args () = !implicit_args.main
let is_manual_implicit_args () = !implicit_args.manual
+let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ())
let is_strict_implicit_args () = !implicit_args.strict
let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -577,10 +578,11 @@ type manual_explicitation = Topconstr.explicitation * (bool * bool)
let compute_implicits_with_manual env typ enriching l =
compute_manual_implicits env !implicit_args typ enriching l
-let declare_manual_implicits local ref enriching l =
+let declare_manual_implicits local ref ?enriching l =
let flags = !implicit_args in
let env = Global.env () in
let t = Global.type_of_global ref in
+ let enriching = Option.default (is_auto_implicit_args ()) enriching in
let l' = compute_manual_implicits env flags t enriching l in
let req =
if local or isVarRef ref then ImplLocal
@@ -588,9 +590,9 @@ let declare_manual_implicits local ref enriching l =
in
add_anonymous_leaf (inImplicits (req,[ref,l']))
-let maybe_declare_manual_implicits local ref enriching l =
+let maybe_declare_manual_implicits local ref ?enriching l =
if l = [] then ()
- else declare_manual_implicits local ref enriching l
+ else declare_manual_implicits local ref ?enriching l
let lift_implicits n =
List.map (fun x ->
diff --git a/library/impargs.mli b/library/impargs.mli
index 705efd31..a363effa 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: impargs.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: impargs.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -83,14 +83,16 @@ val declare_implicits : bool -> global_reference -> unit
(* [declare_manual_implicits local ref enriching l]
Manual declaration of which arguments are expected implicit.
+ If not set, we decide if it should enrich by automatically inferd
+ implicits depending on the current state.
Unsets implicits if [l] is empty. *)
-val declare_manual_implicits : bool -> global_reference -> bool ->
+val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
manual_explicitation list -> unit
(* If the list is empty, do nothing, otherwise declare the implicits. *)
-val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
+val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
manual_explicitation list -> unit
val implicits_of_global : global_reference -> implicits_list
diff --git a/library/lib.ml b/library/lib.ml
index fa71bb2f..88bcd0b8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,11 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: lib.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: lib.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
open Pp
open Util
-open Names
open Libnames
open Nameops
open Libobject
@@ -33,7 +32,7 @@ and library_entry = object_name * node
and library_segment = library_entry list
-type lib_objects = (identifier * obj) list
+type lib_objects = (Names.identifier * obj) list
let iter_objects f i prefix =
List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
@@ -49,11 +48,18 @@ let subst_objects prefix subst seg =
in
list_smartmap subst_one seg
+let load_and_subst_objects i prefix subst seg =
+ List.rev (List.fold_left (fun seg (id,obj as node) ->
+ let obj' = subst_object (make_oname prefix id, subst, obj) in
+ let node = if obj == obj' then node else (id, obj') in
+ load_object i (make_oname prefix id, obj');
+ node :: seg) [] seg)
+
let classify_segment seg =
let rec clean ((substl,keepl,anticipl) as acc) = function
| (_,CompilingLibrary _) :: _ | [] -> acc
| ((sp,kn as oname),Leaf o) :: stk ->
- let id = id_of_label (label kn) in
+ let id = Names.id_of_label (Names.label kn) in
(match classify_object (oname,o) with
| Dispose -> clean acc stk
| Keep o' ->
@@ -85,7 +91,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 = default_library,(initial_path,empty_dirpath)
+let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath)
let lib_stk = ref ([] : library_segment)
@@ -98,8 +104,21 @@ let library_dp () =
module path and relative section path *)
let path_prefix = ref initial_prefix
+let sections_depth () =
+ List.length (Names.repr_dirpath (snd (snd !path_prefix)))
+
+let sections_are_opened () =
+ match Names.repr_dirpath (snd (snd !path_prefix)) with
+ [] -> false
+ | _ -> true
+
let cwd () = fst !path_prefix
+let current_dirpath sec =
+ Libnames.drop_dirpath_prefix (library_dp ())
+ (if sec then cwd ()
+ else Libnames.extract_dirpath_prefix (sections_depth ()) (cwd ()))
+
let make_path id = Libnames.make_path (cwd ()) id
let path_of_include () =
@@ -112,25 +131,15 @@ let current_prefix () = snd !path_prefix
let make_kn id =
let mp,dir = current_prefix () in
- Names.make_kn mp dir (label_of_id id)
+ Names.make_kn mp dir (Names.label_of_id id)
let make_con id =
let mp,dir = current_prefix () in
- Names.make_con mp dir (label_of_id id)
+ Names.make_con mp dir (Names.label_of_id id)
let make_oname id = make_path id, make_kn id
-
-let sections_depth () =
- List.length (repr_dirpath (snd (snd !path_prefix)))
-
-let sections_are_opened () =
- match repr_dirpath (snd (snd !path_prefix)) with
- [] -> false
- | _ -> true
-
-
let recalc_path_prefix () =
let rec recalc = function
| (sp, OpenedSection (dir,_)) :: _ -> dir
@@ -194,7 +203,7 @@ let add_entry sp node =
let anonymous_id =
let n = ref 0 in
- fun () -> incr n; id_of_string ("_" ^ (string_of_int !n))
+ fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n))
let add_anonymous_entry node =
let id = anonymous_id () in
@@ -207,7 +216,7 @@ let add_absolutely_named_leaf sp obj =
add_entry sp (Leaf obj)
let add_leaf id obj =
- if fst (current_prefix ()) = initial_path then
+ if fst (current_prefix ()) = Names.initial_path then
error ("No session module started (use -top dir)");
let oname = make_oname id in
cache_object (oname,obj);
@@ -261,7 +270,7 @@ let current_mod_id () =
let start_module export id mp nametab =
let dir = extend_dirpath (fst !path_prefix) id in
- let prefix = dir,(mp,empty_dirpath) in
+ let prefix = dir,(mp,Names.empty_dirpath) in
let oname = make_path id, make_kn id in
if Nametab.exists_module dir then
errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
@@ -306,7 +315,7 @@ let end_module id =
let start_modtype id mp nametab =
let dir = extend_dirpath (fst !path_prefix) id in
- let prefix = dir,(mp,empty_dirpath) in
+ let prefix = dir,(mp,Names.empty_dirpath) in
let sp = make_path id in
let name = sp, make_kn id in
if Nametab.exists_cci sp then
@@ -363,9 +372,9 @@ let check_for_comp_unit () =
let start_compilation s mp =
if !comp_name <> None then
error "compilation unit is already started";
- if snd (snd (!path_prefix)) <> empty_dirpath then
+ if snd (snd (!path_prefix)) <> Names.empty_dirpath then
error "some sections are already opened";
- let prefix = s, (mp, empty_dirpath) in
+ let prefix = s, (mp, Names.empty_dirpath) in
let _ = add_anonymous_entry (CompilingLibrary prefix) in
comp_name := Some s;
path_prefix := prefix
@@ -395,8 +404,8 @@ let end_compilation dir =
| None -> anomaly "There should be a module name..."
| Some m ->
if m <> dir then anomaly
- ("The current open module has name "^ (string_of_dirpath m) ^
- " and not " ^ (string_of_dirpath m));
+ ("The current open module has name "^ (Names.string_of_dirpath m) ^
+ " and not " ^ (Names.string_of_dirpath m));
in
let (after,_,before) = split_lib oname in
comp_name := None;
@@ -446,7 +455,7 @@ let sectab =
ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
let add_section () =
- sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
+ sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
let add_section_variable id impl keep =
match !sectab with
@@ -489,10 +498,10 @@ let replacement_context () = pi2 (List.hd !sectab)
let variables_context () = pi1 (List.hd !sectab)
let section_segment_of_constant con =
- Cmap.find con (fst (pi3 (List.hd !sectab)))
+ Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
let section_segment_of_mutual_inductive kn =
- KNmap.find kn (snd (pi3 (List.hd !sectab)))
+ Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
let rec list_mem_assoc_in_triple x = function
[] -> raise Not_found
@@ -503,9 +512,9 @@ let section_instance = function
if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||]
else raise Not_found
| ConstRef con ->
- Cmap.find con (fst (pi2 (List.hd !sectab)))
+ Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
- KNmap.find kn (snd (pi2 (List.hd !sectab)))
+ Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
let is_in_section ref =
try ignore (section_instance ref); true with Not_found -> false
@@ -566,11 +575,11 @@ let close_section id =
| oname,OpenedSection (_,fs) ->
let id' = basename (fst oname) in
if id <> id' then
- errorlabstrm "close_section" (str "last opened section is " ++ pr_id id');
+ errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str ".");
(oname,fs)
| _ -> assert false
with Not_found ->
- error "no opened section"
+ error "No opened section."
in
let (secdecls,secopening,before) = split_lib oname in
lib_stk := before;
@@ -730,7 +739,7 @@ let back n = reset_to (back_stk n !lib_stk)
(* State and initialization. *)
-type frozen = dir_path option * library_segment
+type frozen = Names.dir_path option * library_segment
let freeze () = (!comp_name, !lib_stk)
@@ -774,16 +783,37 @@ let reset_initial () =
let mp_of_global ref =
match ref with
| VarRef id -> fst (current_prefix ())
- | ConstRef cst -> con_modpath cst
- | IndRef ind -> ind_modpath ind
- | ConstructRef constr -> constr_modpath constr
+ | ConstRef cst -> Names.con_modpath cst
+ | IndRef ind -> Names.ind_modpath ind
+ | ConstructRef constr -> Names.constr_modpath constr
let rec dp_of_mp modp =
match modp with
- | MPfile dp -> dp
- | MPbound _ | MPself _ -> library_dp ()
- | MPdot (mp,_) -> dp_of_mp mp
-
+ | Names.MPfile dp -> dp
+ | Names.MPbound _ | Names.MPself _ -> library_dp ()
+ | Names.MPdot (mp,_) -> dp_of_mp mp
+
+let rec split_mp mp =
+ match mp with
+ | Names.MPfile dp -> dp, Names.empty_dirpath
+ | Names.MPdot (prfx, lbl) ->
+ let mprec, dprec = split_mp prfx in
+ mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
+ | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in library_dp(), Names.make_dirpath [Names.id_of_string id]
+ | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id]
+
+let split_modpath mp =
+ let rec aux = function
+ | Names.MPfile dp -> dp, []
+ | Names.MPbound mbid ->
+ library_dp (), [Names.id_of_mbid mbid]
+ | Names.MPself msid -> library_dp (), [Names.id_of_msid msid]
+ | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
+ (mp', Names.id_of_label l :: lab)
+ in
+ let (mp, l) = aux mp in
+ mp, l
+
let library_part ref =
match ref with
| VarRef id -> library_dp ()
@@ -815,12 +845,12 @@ let pop_con con =
Names.make_con mp (dirpath_prefix dir) l
let con_defined_in_sec kn =
- let _,dir,_ = repr_con kn in
- dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+ let _,dir,_ = Names.repr_con kn in
+ dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
let defined_in_sec kn =
- let _,dir,_ = repr_kn kn in
- dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+ let _,dir,_ = Names.repr_kn kn in
+ dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
let discharge_global = function
| ConstRef kn when con_defined_in_sec kn ->
diff --git a/library/lib.mli b/library/lib.mli
index d35fcc09..23af7c17 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,41 +6,34 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: lib.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: lib.mli 11671 2008-12-12 12:43:03Z herbelin $ i*)
-(*i*)
-open Util
-open Names
-open Libnames
-open Libobject
-open Summary
-open Mod_subst
-(*i*)
(*s This module provides a general mechanism to keep a trace of all operations
and to backtrack (undo) those operations. It provides also the section
mechanism (at a low level; discharge is not known at this step). *)
type node =
- | Leaf of obj
- | CompilingLibrary of object_prefix
- | OpenedModule of bool option * object_prefix * Summary.frozen
+ | Leaf of Libobject.obj
+ | CompilingLibrary of Libnames.object_prefix
+ | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen
| ClosedModule of library_segment
- | OpenedModtype of object_prefix * Summary.frozen
+ | OpenedModtype of Libnames.object_prefix * Summary.frozen
| ClosedModtype of library_segment
- | OpenedSection of object_prefix * Summary.frozen
+ | OpenedSection of Libnames.object_prefix * Summary.frozen
| ClosedSection of library_segment
| FrozenState of Summary.frozen
-and library_segment = (object_name * node) list
+and library_segment = (Libnames.object_name * node) list
-type lib_objects = (identifier * obj) list
+type lib_objects = (Names.identifier * Libobject.obj) list
(*s Object iteratation functions. *)
-val open_objects : int -> object_prefix -> lib_objects -> unit
-val load_objects : int -> object_prefix -> lib_objects -> unit
-val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
+val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
+val load_and_subst_objects : int -> Libnames.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
@@ -48,23 +41,23 @@ val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
[Substitute], [Keep], [Anticipate] respectively. The order of each
returned list is the same as in the input list. *)
val classify_segment :
- library_segment -> lib_objects * lib_objects * obj list
+ library_segment -> lib_objects * lib_objects * Libobject.obj list
(* [segment_of_objects prefix objs] forms a list of Leafs *)
val segment_of_objects :
- object_prefix -> lib_objects -> library_segment
+ Libnames.object_prefix -> lib_objects -> library_segment
(*s Adding operations (which call the [cache] method, and getting the
current list of operations (most recent ones coming first). *)
-val add_leaf : identifier -> obj -> object_name
-val add_absolutely_named_leaf : object_name -> obj -> unit
-val add_anonymous_leaf : obj -> unit
+val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name
+val add_absolutely_named_leaf : Libnames.object_name -> Libobject.obj -> unit
+val add_anonymous_leaf : Libobject.obj -> unit
(* 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
+val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
val add_frozen_state : unit -> unit
@@ -81,19 +74,20 @@ val reset_label : int -> unit
starting from a given section path. If not given, the entire segment
is returned. *)
-val contents_after : object_name option -> library_segment
+val contents_after : Libnames.object_name option -> library_segment
(*s Functions relative to current path *)
(* User-side names *)
-val cwd : unit -> dir_path
-val make_path : identifier -> section_path
-val path_of_include : unit -> section_path
+val cwd : unit -> Names.dir_path
+val current_dirpath : bool -> Names.dir_path
+val make_path : Names.identifier -> Libnames.section_path
+val path_of_include : unit -> Libnames.section_path
(* Kernel-side names *)
-val current_prefix : unit -> module_path * dir_path
-val make_kn : identifier -> kernel_name
-val make_con : identifier -> constant
+val current_prefix : unit -> Names.module_path * Names.dir_path
+val make_kn : Names.identifier -> Names.kernel_name
+val make_con : Names.identifier -> Names.constant
(* Are we inside an opened section *)
val sections_are_opened : unit -> bool
@@ -102,53 +96,55 @@ val sections_depth : unit -> int
(* Are we inside an opened module type *)
val is_modtype : unit -> bool
val is_module : unit -> bool
-val current_mod_id : unit -> module_ident
+val current_mod_id : unit -> Names.module_ident
(* Returns the most recent OpenedThing node *)
-val what_is_opened : unit -> object_name * node
+val what_is_opened : unit -> Libnames.object_name * node
(*s Modules and module types *)
val start_module :
- bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix
-val end_module : module_ident
- -> object_name * object_prefix * Summary.frozen * library_segment
+ bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
+val end_module : Names.module_ident
+ -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
val start_modtype :
- module_ident -> module_path -> Summary.frozen -> object_prefix
-val end_modtype : module_ident
- -> object_name * object_prefix * Summary.frozen * library_segment
+ Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
+val end_modtype : Names.module_ident
+ -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
(* [Lib.add_frozen_state] must be called after each of the above functions *)
(*s Compilation units *)
-val start_compilation : dir_path -> module_path -> unit
-val end_compilation : dir_path -> object_prefix * library_segment
+val start_compilation : Names.dir_path -> Names.module_path -> unit
+val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment
(* The function [library_dp] returns the [dir_path] of the current
compiling library (or [default_library]) *)
-val library_dp : unit -> dir_path
+val library_dp : unit -> Names.dir_path
(* Extract the library part of a name even if in a section *)
-val dp_of_mp : module_path -> dir_path
-val library_part : global_reference -> dir_path
-val remove_section_part : global_reference -> dir_path
+val dp_of_mp : Names.module_path -> Names.dir_path
+val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
+val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list
+val library_part : Libnames.global_reference -> Names.dir_path
+val remove_section_part : Libnames.global_reference -> Names.dir_path
(*s Sections *)
-val open_section : identifier -> unit
-val close_section : identifier -> unit
+val open_section : Names.identifier -> unit
+val close_section : Names.identifier -> unit
(*s Backtracking (undo). *)
-val reset_to : object_name -> unit
-val reset_name : identifier located -> unit
-val remove_name : identifier located -> unit
-val reset_mod : identifier located -> unit
-val reset_to_state : object_name -> unit
+val reset_to : Libnames.object_name -> unit
+val reset_name : Names.identifier Util.located -> unit
+val remove_name : Names.identifier Util.located -> unit
+val reset_mod : Names.identifier Util.located -> unit
+val reset_to_state : Libnames.object_name -> unit
-val has_top_frozen_state : unit -> object_name option
+val has_top_frozen_state : unit -> Libnames.object_name option
(* [back n] resets to the place corresponding to the $n$-th call of
[mark_end_of_command] (counting backwards) *)
@@ -168,8 +164,8 @@ val reset_initial : unit -> unit
(* XML output hooks *)
-val set_xml_open_section : (identifier -> unit) -> unit
-val set_xml_close_section : (identifier -> unit) -> unit
+val set_xml_open_section : (Names.identifier -> unit) -> unit
+val set_xml_close_section : (Names.identifier -> unit) -> unit
type binding_kind = Explicit | Implicit
@@ -190,13 +186,13 @@ val add_section_variable : Names.identifier -> binding_kind -> Term.types option
val add_section_constant : Names.constant -> Sign.named_context -> unit
val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
val replacement_context : unit ->
- (identifier array Cmap.t * identifier array KNmap.t)
+ (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t)
(*s Discharge: decrease the section level if in the current section *)
-val discharge_kn : kernel_name -> kernel_name
-val discharge_con : constant -> constant
-val discharge_global : global_reference -> global_reference
-val discharge_inductive : inductive -> inductive
+val discharge_kn : Names.kernel_name -> Names.kernel_name
+val discharge_con : Names.constant -> Names.constant
+val discharge_global : Libnames.global_reference -> Libnames.global_reference
+val discharge_inductive : Names.inductive -> Names.inductive
diff --git a/library/libnames.ml b/library/libnames.ml
index d0c6e8b9..3f226179 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: libnames.ml 11209 2008-07-05 10:17:49Z herbelin $ i*)
+(*i $Id: libnames.ml 11750 2009-01-05 20:47:34Z herbelin $ i*)
open Pp
open Util
@@ -24,6 +24,11 @@ type global_reference =
let isVarRef = function VarRef _ -> true | _ -> false
+let subst_constructor subst ((kn,i),j as ref) =
+ let kn' = subst_kn subst kn in
+ if kn==kn' then ref, mkConstruct ref
+ else ((kn',i),j), mkConstruct ((kn',i),j)
+
let subst_global subst ref = match ref with
| VarRef var -> ref, mkVar var
| ConstRef kn ->
@@ -32,10 +37,9 @@ let subst_global subst ref = match ref with
| IndRef (kn,i) ->
let kn' = subst_kn subst kn in
if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
- | ConstructRef ((kn,i),j) ->
- let kn' = subst_kn subst kn in
- if kn==kn' then ref, mkConstruct ((kn,i),j)
- else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j)
+ | ConstructRef ((kn,i),j as c) ->
+ let c',t = subst_constructor subst c in
+ if c'==c then ref,t else ConstructRef c', t
let global_of_constr c = match kind_of_term c with
| Const sp -> ConstRef sp
@@ -119,21 +123,21 @@ let path_of_inductive env (sp,tyi) =
let parse_dir s =
let len = String.length s in
let rec decoupe_dirs dirs n =
- if n>=len then dirs else
+ if n = len && n > 0 then error (s ^ " is an invalid path.");
+ if n >= len then dirs else
let pos =
try
String.index_from s n '.'
with Not_found -> len
in
+ if pos = n then error (s ^ " is an invalid path.");
let dir = String.sub s n (pos-n) in
- decoupe_dirs ((id_of_string dir)::dirs) (pos+1)
+ decoupe_dirs ((id_of_string dir)::dirs) (pos+1)
in
decoupe_dirs [] 0
-let dirpath_of_string s =
- match parse_dir s with
- [] -> invalid_arg "dirpath_of_string"
- | dir -> make_dirpath dir
+let dirpath_of_string s =
+ make_dirpath (if s = "" then [] else parse_dir s)
module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
diff --git a/library/libnames.mli b/library/libnames.mli
index 76c406db..cc664a08 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 11209 2008-07-05 10:17:49Z herbelin $ i*)
+(*i $Id: libnames.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Pp
@@ -25,6 +25,7 @@ type global_reference =
val isVarRef : global_reference -> bool
+val subst_constructor : substitution -> constructor -> constructor * constr
val subst_global : substitution -> global_reference -> global_reference * constr
(* Turn a global reference into a construction *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 6b302447..b455e2b3 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: libobject.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: libobject.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
open Util
open Names
@@ -148,8 +148,9 @@ let apply_dyn_fun deflt f lobj =
if !relax_flag then
failwith "local to_apply_dyn_fun"
else
- anomaly
- ("Cannot find library functions for an object with tag "^tag) in
+ error
+ ("Cannot find library functions for an object with tag "^tag^
+ " (maybe a plugin is missing)") in
f dodecl
with
Failure "local to_apply_dyn_fun" -> deflt;;
diff --git a/library/library.ml b/library/library.ml
index 73928a9b..9f3478f0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml 11313 2008-08-07 11:15:03Z barras $ *)
+(* $Id: library.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
open Pp
open Util
@@ -18,7 +18,6 @@ open Safe_typing
open Libobject
open Lib
open Nametab
-open Declaremods
(*************************************************************************)
(*s Load path. Mapping from physical to logical paths etc.*)
@@ -29,43 +28,15 @@ let load_paths = ref ([] : (System.physical_path * logical_path * bool) list)
let get_load_paths () = List.map pi1 !load_paths
-(* Hints to partially detects if two paths refer to the same repertory *)
-let rec remove_path_dot p =
- let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
- let n = String.length curdir in
- if String.length p > n && String.sub p 0 n = curdir then
- remove_path_dot (String.sub p n (String.length p - n))
- else
- p
-
-let strip_path p =
- let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
- let n = String.length cwd in
- if String.length p > n && String.sub p 0 n = cwd then
- remove_path_dot (String.sub p n (String.length p - n))
- else
- remove_path_dot p
-
-let canonical_path_name p =
- let current = Sys.getcwd () in
- try
- Sys.chdir p;
- let p' = Sys.getcwd () in
- Sys.chdir current;
- p'
- with Sys_error _ ->
- (* We give up to find a canonical name and just simplify it... *)
- strip_path p
-
let find_logical_path phys_dir =
- let phys_dir = canonical_path_name phys_dir in
+ let phys_dir = System.canonical_path_name phys_dir in
match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with
| [_,dir,_] -> dir
| [] -> Nameops.default_root_prefix
| l -> anomaly ("Two logical paths are associated to "^phys_dir)
let is_in_load_paths phys_dir =
- let dir = canonical_path_name phys_dir in
+ let dir = System.canonical_path_name phys_dir in
let lp = get_load_paths () in
let check_p = fun p -> (String.compare dir p) == 0 in
List.exists check_p lp
@@ -74,13 +45,13 @@ let remove_load_path dir =
load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
let add_load_path isroot (phys_path,coq_path) =
- let phys_path = canonical_path_name phys_path in
+ let phys_path = System.canonical_path_name phys_path in
match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
| [_,dir,_] ->
if coq_path <> dir
(* If this is not the default -I . to coqtop *)
&& not
- (phys_path = canonical_path_name Filename.current_dir_name
+ (phys_path = System.canonical_path_name Filename.current_dir_name
&& coq_path = Nameops.default_root_prefix)
then
begin
@@ -149,7 +120,7 @@ type compilation_unit_name = dir_path
type library_disk = {
md_name : compilation_unit_name;
md_compiled : compiled_library;
- md_objects : library_objects;
+ md_objects : Declaremods.library_objects;
md_deps : (compilation_unit_name * Digest.t) list;
md_imports : compilation_unit_name list }
@@ -159,7 +130,7 @@ type library_disk = {
type library_t = {
library_name : compilation_unit_name;
library_compiled : compiled_library;
- library_objects : library_objects;
+ library_objects : Declaremods.library_objects;
library_deps : (compilation_unit_name * Digest.t) list;
library_imports : compilation_unit_name list;
library_digest : Digest.t }
@@ -324,14 +295,14 @@ let open_libraries export modl =
(**********************************************************************)
(* import and export - synchronous operations*)
-let cache_import (_,(dir,export)) =
- open_libraries export [try_find_library dir]
-
-let open_import i (_,(dir,_) as obj) =
+let open_import i (_,(dir,export)) =
if i=1 then
(* even if the library is already imported, we re-import it *)
(* if not (library_is_opened dir) then *)
- cache_import obj
+ open_libraries export [try_find_library dir]
+
+let cache_import obj =
+ open_import 1 obj
let subst_import (_,_,o) = o
@@ -379,7 +350,7 @@ let locate_absolute_library dir =
if loadpath = [] then raise LibUnmappedDir;
try
let name = (string_of_id base)^".vo" in
- let _, file = System.where_in_path false loadpath name in
+ let _, file = System.where_in_path ~warn:false loadpath name in
(dir, file)
with Not_found ->
(* Last chance, removed from the file system but still in memory *)
@@ -395,7 +366,7 @@ let locate_qualified_library warn qid =
let loadpath = loadpaths_matching_dir_path dir in
if loadpath = [] then raise LibUnmappedDir;
let name = string_of_id base ^ ".vo" in
- let lpath, file = System.where_in_path warn (List.map fst loadpath) name in
+ let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
let dir = extend_dirpath (List.assoc lpath loadpath) base in
(* Look if loaded *)
if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
@@ -506,12 +477,14 @@ let rec_intern_by_filename_only id f =
let rec_intern_library_from_file idopt f =
(* A name is specified, we have to check it contains library id *)
- let _, f = System.find_file_in_path (get_load_paths ()) (f^".vo") in
+ let paths = get_load_paths () in
+ let _, f =
+ System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
rec_intern_by_filename_only idopt f
(**********************************************************************)
-(*s [require_library] loads and opens a library. This is a synchronized
- operation. It is performed as follows:
+(*s [require_library] loads and possibly opens a library. This is a
+ synchronized operation. It is performed as follows:
preparation phase: (functions require_library* ) the library and its
dependencies are read from to disk (using intern_* )
@@ -524,10 +497,6 @@ let rec_intern_library_from_file idopt f =
the library is loaded in the environment and Nametab, the objects are
registered etc, using functions from Declaremods (via load_library,
which recursively loads its dependencies)
-
-
- The [read_library] operation is very similar, but does not "open"
- the library
*)
type library_reference = dir_path list * bool option
@@ -540,14 +509,21 @@ let register_library (dir,m) =
m.library_digest;
register_loaded_library m
- (* [needed] is the ordered list of libraries not already loaded *)
-let cache_require (_,(needed,modl,export)) =
- List.iter register_library needed;
+(* Follow the semantics of Anticipate object:
+ - called at module or module type closing when a Require occurs in
+ the module or module type
+ - not called from a library (i.e. a module identified with a file) *)
+let load_require _ (_,(needed,modl,_)) =
+ List.iter register_library needed
+
+let open_require i (_,(_,modl,export)) =
Option.iter (fun exp -> open_libraries exp (List.map find_library modl))
export
-let load_require _ (_,(needed,modl,_)) =
- List.iter register_library needed
+ (* [needed] is the ordered list of libraries not already loaded *)
+let cache_require o =
+ load_require 1 o;
+ open_require 1 o
(* keeps the require marker for closed section replay but removes
OS dependent fields from .vo files for cross-platform compatibility *)
@@ -555,10 +531,13 @@ let export_require (_,l,e) = Some ([],l,e)
let discharge_require (_,o) = Some o
+(* open_function is never called from here because an Anticipate object *)
+
let (in_require, out_require) =
declare_object {(default_object "REQUIRE") with
cache_function = cache_require;
load_function = load_require;
+ open_function = (fun _ _ -> assert false);
export_function = export_require;
discharge_function = discharge_require;
classify_function = (fun (_,o) -> Anticipate o) }
@@ -566,8 +545,6 @@ let (in_require, out_require) =
(* Require libraries, import them if [export <> None], mark them for export
if [export = Some true] *)
-(* read = require without opening *)
-
let xml_require = ref (fun d -> ())
let set_xml_require f = xml_require := f
@@ -575,19 +552,16 @@ let require_library qidl export =
let modrefl = List.map try_locate_qualified_library qidl in
let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
let modrefl = List.map fst modrefl in
- if Lib.is_modtype () || Lib.is_module () then begin
- add_anonymous_leaf (in_require (needed,modrefl,None));
- Option.iter (fun exp ->
- List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
- export
- end
+ if Lib.is_modtype () || Lib.is_module () then
+ begin
+ add_anonymous_leaf (in_require (needed,modrefl,None));
+ Option.iter (fun exp ->
+ List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
+ export
+ end
else
add_anonymous_leaf (in_require (needed,modrefl,export));
- if !Flags.dump then List.iter2 (fun (loc, _) dp ->
- Flags.dump_string (Printf.sprintf "R%d %s <> <> %s\n"
- (fst (unloc loc)) (string_of_dirpath dp) "lib"))
- qidl modrefl;
- if !Flags.xml_export then List.iter !xml_require modrefl;
+ if !Flags.xml_export then List.iter !xml_require modrefl;
add_frozen_state ()
let require_library_from_file idopt file export =
@@ -608,25 +582,33 @@ let require_library_from_file idopt file export =
let import_module export (loc,qid) =
try
match Nametab.locate_module qid with
- MPfile dir ->
+ | MPfile dir ->
if Lib.is_modtype () || Lib.is_module () || not export then
add_anonymous_leaf (in_import (dir, export))
else
- add_anonymous_leaf (in_require ([],[dir], Some export))
+ add_anonymous_leaf (in_import (dir, export))
| mp ->
- import_module export mp
+ Declaremods.import_module export mp
with
Not_found ->
user_err_loc
- (loc,"import_library",
- str ((string_of_qualid qid)^" is not a module"))
+ (loc,"import_library",
+ str ((string_of_qualid qid)^" is not a module"))
(************************************************************************)
(*s Initializing the compilation of a library. *)
+let check_coq_overwriting p =
+ let l = repr_dirpath p in
+ if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then
+ errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library."))
+
let start_library f =
- let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in
+ let paths = get_load_paths () in
+ let _,longf =
+ System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
let ldir0 = find_logical_path (Filename.dirname longf) in
+ check_coq_overwriting ldir0;
let id = id_of_string (Filename.basename f) in
let ldir = extend_dirpath ldir0 id in
Declaremods.start_library ldir;
diff --git a/library/library.mli b/library/library.mli
index a66a77bc..d61dc4b9 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: library.mli 11209 2008-07-05 10:17:49Z herbelin $ i*)
+(*i $Id: library.mli 11750 2009-01-05 20:47:34Z herbelin $ i*)
(*i*)
open Util
@@ -76,6 +76,10 @@ type library_location = LibLoaded | LibInPath
val locate_qualified_library :
bool -> qualid -> library_location * dir_path * System.physical_path
+val try_locate_qualified_library : qualid located -> dir_path * string
+
+(* Reserve Coq prefix for the standard library *)
+val check_coq_overwriting : dir_path -> unit
(*s Statistics: display the memory use of a library. *)
val mem : dir_path -> Pp.std_ppcmds
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 23:15:57 +0000