diff options
-rw-r--r-- | library/library.ml | 118 | ||||
-rw-r--r-- | library/library.mli | 12 | ||||
-rw-r--r-- | library/library.mllib | 1 | ||||
-rw-r--r-- | library/loadpath.ml | 129 | ||||
-rw-r--r-- | library/loadpath.mli | 54 | ||||
-rw-r--r-- | library/states.ml | 4 | ||||
-rw-r--r-- | toplevel/ide_slave.ml | 2 | ||||
-rw-r--r-- | toplevel/mltop.ml | 11 | ||||
-rw-r--r-- | toplevel/vernac.ml | 5 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 26 |
10 files changed, 229 insertions, 133 deletions
diff --git a/library/library.ml b/library/library.ml index edb86bc4c..dc0981497 100644 --- a/library/library.ml +++ b/library/library.ml @@ -17,99 +17,6 @@ open Safe_typing open Libobject open Lib -(*************************************************************************) -(*s Load path. Mapping from physical to logical paths etc.*) - -type logical_path = DirPath.t - -let load_paths = ref ([] : (CUnix.physical_path * logical_path * bool) list) - -let get_load_paths () = List.map pi1 !load_paths - -let find_logical_path phys_dir = - let phys_dir = CUnix.canonical_path_name phys_dir in - let filter (p, _, _) = String.equal p phys_dir in - let paths = List.filter filter !load_paths in - match paths with - | [_,dir,_] -> dir - | [] -> Nameops.default_root_prefix - | l -> anomaly (str "Two logical paths are associated to" ++ spc () ++ str phys_dir) - -let is_in_load_paths phys_dir = - let dir = CUnix.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 - -let remove_load_path dir = - load_paths := List.filter (fun (p,_,_) -> not (String.equal p dir)) !load_paths - -let add_load_path isroot (phys_path,coq_path) = - let phys_path = CUnix.canonical_path_name phys_path in - let filter (p, _, _) = String.equal p phys_path in - match List.filter filter !load_paths with - | [_,dir,_] -> - if not (DirPath.equal coq_path dir) - (* If this is not the default -I . to coqtop *) - && not - (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) - && DirPath.equal coq_path (Nameops.default_root_prefix)) - then - begin - (* Assume the user is concerned by library naming *) - if not (DirPath.equal dir Nameops.default_root_prefix) then - Flags.if_warn msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath dir ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path); - remove_load_path phys_path; - load_paths := (phys_path,coq_path,isroot) :: !load_paths; - end - | [] -> - load_paths := (phys_path,coq_path,isroot) :: !load_paths; - | _ -> anomaly (str "Two logical paths are associated to" ++ spc () ++ str phys_path) - -let extend_path_with_dirpath p dir = - List.fold_left Filename.concat p - (List.rev_map Id.to_string (DirPath.repr dir)) - -let root_paths_matching_dir_path dir = - let rec aux = function - | [] -> [] - | (p,d,true) :: l when is_dirpath_prefix_of d dir -> - let suffix = drop_dirpath_prefix d dir in - extend_path_with_dirpath p suffix :: aux l - | _ :: l -> aux l in - aux !load_paths - -(* Root p is bound to A.B.C.D and we require file C.D.E.F *) -(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *) - -(* Root p is bound to A.B.C.C and we require file C.C.E.F *) -(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *) - -let intersections d1 d2 = - let rec aux d1 = - if DirPath.is_empty d1 then [d2] else - let rest = aux (snd (chop_dirpath 1 d1)) in - if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest - else rest in - aux d1 - -let loadpaths_matching_dir_path dir = - let rec aux = function - | [] -> [] - | (p,d,true) :: l -> - let inters = intersections d dir in - List.map (fun tl -> (extend_path_with_dirpath p tl,append_dirpath d tl)) - inters @ - aux l - | (p,d,_) :: l -> - (extend_path_with_dirpath p dir,append_dirpath d dir) :: aux l in - aux !load_paths - -let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths - (************************************************************************) (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) @@ -330,7 +237,7 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = root_paths_matching_dir_path pref in + let loadpath = Loadpath.expand_root_path pref in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in try let name = (Id.to_string base)^".vo" in @@ -347,7 +254,7 @@ let locate_qualified_library warn qid = try (* Search library in loadpath *) let dir, base = repr_qualid qid in - let loadpath = loadpaths_matching_dir_path dir in + let loadpath = Loadpath.expand_path dir in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let name = Id.to_string base ^ ".vo" in let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in @@ -480,7 +387,7 @@ 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 paths = get_load_paths () in + let paths = Loadpath.get_paths () in let _, f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in rec_intern_by_filename_only idopt f @@ -609,10 +516,15 @@ let check_coq_overwriting p id = ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) let start_library f = - let paths = get_load_paths () in - let _,longf = + let paths = Loadpath.get_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 + let ldir0 = + try + let lp = Loadpath.find_load_path (Filename.dirname longf) in + Loadpath.logical lp + with Not_found -> Nameops.default_root_prefix + in let id = Id.of_string (Filename.basename f) in check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in @@ -661,7 +573,9 @@ let save_library_to dir f = System.marshal_out ch table; close_out ch; if not !Flags.no_native_compiler then begin - let lp = List.map CUnix.string_of_physical_path (get_load_paths ()) in + let lp = Loadpath.get_load_paths () in + let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in + let lp = List.map map_path lp in let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in match Nativelibrary.compile_library dir ast lp fn with | 0 -> () @@ -686,6 +600,8 @@ let mem s = (CObj.size_kb m.library_objects))) let get_load_paths_str () = - List.map CUnix.string_of_physical_path (get_load_paths ()) + let lp = Loadpath.get_load_paths () in + let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in + List.map map_path lp let _ = Nativelib.get_load_paths := get_load_paths_str diff --git a/library/library.mli b/library/library.mli index 11253087a..22b94e521 100644 --- a/library/library.mli +++ b/library/library.mli @@ -58,18 +58,6 @@ val overwrite_library_filenames : string -> unit (** {6 Hook for the xml exportation of libraries } *) val set_xml_require : (DirPath.t -> unit) -> unit -(** {6 ... } *) -(** Global load paths: a load path is a physical path in the file - system; to each load path is associated a Coq [DirPath.t] (the "logical" - path of the physical path) *) - -val get_load_paths : unit -> CUnix.physical_path list -val get_full_load_paths : unit -> (CUnix.physical_path * DirPath.t) list -val add_load_path : bool -> CUnix.physical_path * DirPath.t -> unit -val remove_load_path : CUnix.physical_path -> unit -val find_logical_path : CUnix.physical_path -> DirPath.t -val is_in_load_paths : CUnix.physical_path -> bool - (** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound diff --git a/library/library.mllib b/library/library.mllib index 2d03f14cb..2568bcc18 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -7,6 +7,7 @@ Nametab Global Lib Declaremods +Loadpath Library States Kindops diff --git a/library/loadpath.ml b/library/loadpath.ml new file mode 100644 index 000000000..44b53c09a --- /dev/null +++ b/library/loadpath.ml @@ -0,0 +1,129 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Errors +open Names +open Libnames + +(** Load paths. Mapping from physical to logical paths. *) + +type t = { + path_physical : CUnix.physical_path; + path_logical : DirPath.t; + path_is_root : bool; +} + +let logical p = p.path_logical + +let physical p = p.path_physical + +let load_paths = ref ([] : t list) + +let get_load_paths () = !load_paths + +let get_paths () = List.map physical !load_paths + +let anomaly_too_many_paths path = + anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) + +let find_load_path phys_dir = + let phys_dir = CUnix.canonical_path_name phys_dir in + let filter p = String.equal p.path_physical phys_dir in + let paths = List.filter filter !load_paths in + match paths with + | [] -> raise Not_found + | [p] -> p + | _ -> anomaly_too_many_paths phys_dir + +let is_in_load_paths phys_dir = + let dir = CUnix.canonical_path_name phys_dir in + let lp = get_load_paths () in + let check_p p = String.equal dir p.path_physical in + List.exists check_p lp + +let remove_load_path dir = + let filter p = not (String.equal p.path_physical dir) in + load_paths := List.filter filter !load_paths + +let add_load_path phys_path isroot coq_path = + let phys_path = CUnix.canonical_path_name phys_path in + let filter p = String.equal p.path_physical phys_path in + let binding = { + path_logical = coq_path; + path_physical = phys_path; + path_is_root = isroot; + } in + match List.filter filter !load_paths with + | [] -> + load_paths := binding :: !load_paths; + | [p] -> + let dir = p.path_logical in + if not (DirPath.equal coq_path dir) + (* If this is not the default -I . to coqtop *) + && not + (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) + && DirPath.equal coq_path (Nameops.default_root_prefix)) + then + begin + (* Assume the user is concerned by library naming *) + if not (DirPath.equal dir Nameops.default_root_prefix) then + Flags.if_warn msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath dir ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path); + remove_load_path phys_path; + load_paths := binding :: !load_paths; + end + | _ -> anomaly_too_many_paths phys_path + +let extend_path_with_dirpath p dir = + List.fold_left Filename.concat p + (List.rev_map Id.to_string (DirPath.repr dir)) + +let expand_root_path dir = + let rec aux = function + | [] -> [] + | p :: l -> + if p.path_is_root && is_dirpath_prefix_of p.path_logical dir then + let suffix = drop_dirpath_prefix p.path_logical dir in + extend_path_with_dirpath p.path_physical suffix :: aux l + else aux l + in + aux !load_paths + +(* Root p is bound to A.B.C.D and we require file C.D.E.F *) +(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *) + +(* Root p is bound to A.B.C.C and we require file C.C.E.F *) +(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *) + +let intersections d1 d2 = + let rec aux d1 = + if DirPath.is_empty d1 then [d2] else + let rest = aux (snd (chop_dirpath 1 d1)) in + if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest + else rest in + aux d1 + +let expand p dir = + let ph = extend_path_with_dirpath p.path_physical dir in + let log = append_dirpath p.path_logical dir in + (ph, log) + +let expand_path dir = + let rec aux = function + | [] -> [] + | p :: l -> + if p.path_is_root then + let inters = intersections p.path_logical dir in + List.map (expand p) inters @ aux l + else + expand p dir :: aux l in + aux !load_paths diff --git a/library/loadpath.mli b/library/loadpath.mli new file mode 100644 index 000000000..8928542a6 --- /dev/null +++ b/library/loadpath.mli @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names + +(** * Load paths. + + A load path is a physical path in the file system; to each load path is + associated a Coq [DirPath.t] (the "logical" path of the physical path). + +*) + +type t +(** Type of loadpath bindings. *) + +val physical : t -> CUnix.physical_path +(** Get the physical path (filesystem location) of a loadpath. *) + +val logical : t -> DirPath.t +(** Get the logical path (Coq module hierarchy) of a loadpath. *) + +val get_load_paths : unit -> t list +(** Get the current loadpath association. *) + +val get_paths : unit -> CUnix.physical_path list +(** Same as [get_load_paths] but only get the physical part. *) + +val add_load_path : CUnix.physical_path -> bool -> DirPath.t -> unit +(** [add_load_path root phys log] adds the binding [phys := log] to the current + loadpaths. The [root] flag indicates whether this loadpath has to be treated + as a root one. *) + +val remove_load_path : CUnix.physical_path -> unit +(** Remove the current logical path binding associated to a given physical path, + if any. *) + +val find_load_path : CUnix.physical_path -> t +(** Get the binding associated to a physical path. Raises [Not_found] if there + is none. *) + +val is_in_load_paths : CUnix.physical_path -> bool +(** Whether a physical path is currently bound. *) + +val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list +(** Given a relative logical path, associate the list of absolute physical and + logical paths which are possible expansions of it. *) + +val expand_root_path : DirPath.t -> CUnix.physical_path list +(** As [expand_path] but restricts to root loadpaths. *) diff --git a/library/states.ml b/library/states.ml index 906ebdacc..9d15dfc6c 100644 --- a/library/states.ml +++ b/library/states.ml @@ -28,8 +28,8 @@ let (extern_state,intern_state) = raw_extern s (freeze())), (fun s -> let s = ensure_suffix s in - unfreeze - (with_magic_number_check (raw_intern (Library.get_load_paths ())) s); + let paths = Loadpath.get_paths () in + unfreeze (with_magic_number_check (raw_intern paths) s); Library.overwrite_library_filenames s) (* Rollback. *) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index ce74b361d..6e7ed6e7f 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -228,7 +228,7 @@ let hints () = (** Other API calls *) let inloadpath dir = - Library.is_in_load_paths (CUnix.physical_path_of_string dir) + Loadpath.is_in_load_paths (CUnix.physical_path_of_string dir) let status () = (** We remove the initial part of the current [DirPath.t] diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index e0daf53f1..4ad1940cc 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -156,7 +156,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = if exists_dir dir then begin add_ml_dir dir; - Library.add_load_path true (dir,coq_dirpath) + Loadpath.add_load_path dir true coq_dirpath end else msg_warning (str ("Cannot open " ^ dir)) @@ -178,10 +178,11 @@ let add_rec_path ~unix_path ~coq_root = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; - add_ml_dir unix_path; - List.iter (Library.add_load_path false) dirs; - Library.add_load_path true (unix_path, coq_root) + let () = List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs in + let () = add_ml_dir unix_path in + let add (path, dir) = Loadpath.add_load_path path false dir in + let () = List.iter add dirs in + Loadpath.add_load_path unix_path true coq_root else msg_warning (str ("Cannot open " ^ unix_path)) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index faf4f1bdd..84968c3d4 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -182,7 +182,7 @@ let open_utf8_file_in fname = the file we parse seems a bit risky to me. B.B. *) let open_file_twice_if verbosely fname = - let paths = Library.get_load_paths () in + let paths = Loadpath.get_paths () in let _,longfname = find_file_in_path ~warn:(Flags.is_verbose()) paths fname in let in_chan = open_utf8_file_in longfname in @@ -269,8 +269,9 @@ let rec vernac_com interpfun checknav (loc,com) = let st = save_translator_coqdoc () in if !Flags.beautify_file then begin + let paths = Loadpath.get_paths () in let _,f = find_file_in_path ~warn:(Flags.is_verbose()) - (Library.get_load_paths ()) + paths (CUnix.make_suffix fname ".v") in chan_beautify := open_out (f^beautify_suffix); Pp.comments := [] diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e8fef0060..d713fdcc2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -200,17 +200,22 @@ let show_match id = (* "Print" commands *) -let print_path_entry (s,l) = - (str (DirPath.to_string l) ++ str " " ++ tbrk (0,0) ++ str s) +let print_path_entry p = + let dir = str (DirPath.to_string (Loadpath.logical p)) in + let path = str (Loadpath.physical p) in + (dir ++ str " " ++ tbrk (0, 0) ++ path) let print_loadpath dir = - let l = Library.get_full_load_paths () in + let l = Loadpath.get_load_paths () in let l = match dir with - | None -> l - | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in - Pp.t (str "Logical Path: " ++ - tab () ++ str "Physical path:" ++ fnl () ++ - prlist_with_sep fnl print_path_entry l) + | None -> l + | Some dir -> + let filter p = is_dirpath_prefix_of dir (Loadpath.logical p) in + List.filter filter l + in + Pp.t (str "Logical Path: " ++ + tab () ++ str "Physical path:" ++ fnl () ++ + prlist_with_sep fnl print_path_entry l) let print_modules () = let opened = Library.opened_libraries () @@ -365,7 +370,8 @@ let dump_universes sorted s = (* "Locate" commands *) let locate_file f = - let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in + let paths = Loadpath.get_paths () in + let _, file = System.find_file_in_path ~warn:false paths f in str file let msg_found_library = function @@ -857,7 +863,7 @@ let vernac_add_loadpath isrec pdir ldiropt = ~unix_path:pdir ~coq_root:alias let vernac_remove_loadpath path = - Library.remove_load_path (expand path) + Loadpath.remove_load_path (expand path) (* Coq syntax for ML or system commands *) |