From 765510929b2255d9c56fcdfce4a3ea555b07b340 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 31 Mar 2015 18:25:45 +0200 Subject: A more reasonable implementation of Loadpath. The new behaviour is simple: either a path is in the loadpaths or it is not. No more wild expansions of paths! This should not affect -R and -Q, but it does change the semantics of -I -as. Still, there are no more users of it and it only does so in a subtle way. --- library/loadpath.ml | 48 ++++++++++++++---------------------------------- 1 file changed, 14 insertions(+), 34 deletions(-) (limited to 'library') diff --git a/library/loadpath.ml b/library/loadpath.ml index ab8b0a3078..0f7c2fb465 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -93,47 +93,27 @@ let expand_root_path dir = let rec aux = function | [] -> [] | p :: l -> - if p.path_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 + if DirPath.equal p.path_logical dir then p.path_physical :: 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 is_suffix dir1 dir2 = + let dir1 = DirPath.repr dir1 in + let dir2 = DirPath.repr dir2 in + List.prefix_of Id.equal dir1 dir2 let expand_path dir = let rec aux = function | [] -> [] | p :: l -> - match p.path_implicit, p.path_root with - | true, false -> expand p dir :: aux l - | true, true -> - let inters = intersections p.path_logical dir in - List.map (expand p) inters @ aux l - | false, true -> - if is_dirpath_prefix_of p.path_logical dir then - expand p (drop_dirpath_prefix p.path_logical dir) :: aux l - else aux l - | false, false -> - (* nothing to do, an explicit root path should also match above - if [is_dirpath_prefix_of p.path_logical dir] were true here *) - aux l in + let { path_physical = ph; path_logical = lg } = p in + match p.path_implicit with + | true -> + (** The path is implicit, so that we only want match the logical suffix *) + if is_suffix dir lg then (ph, lg) :: aux l else aux l + | false -> + (** Otherwise we must match exactly *) + if DirPath.equal dir lg then (ph, lg) :: aux l else aux l + in aux !load_paths -- cgit v1.2.3 From 43a0a3147073b12b038c55c27fd6f0adcb900ac9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 31 Mar 2015 19:24:10 +0200 Subject: Removing the unused root flag from loadpaths. --- library/loadpath.ml | 4 +--- library/loadpath.mli | 8 ++++---- 2 files changed, 5 insertions(+), 7 deletions(-) (limited to 'library') diff --git a/library/loadpath.ml b/library/loadpath.ml index 0f7c2fb465..ca22801021 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -17,7 +17,6 @@ open Libnames type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_root : bool; path_implicit : bool; } @@ -53,13 +52,12 @@ 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 coq_path ~root ~implicit = +let add_load_path phys_path coq_path ~implicit = 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_root = root; path_implicit = implicit; } in match List.filter filter !load_paths with diff --git a/library/loadpath.mli b/library/loadpath.mli index d4029303d2..ae54b3183a 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -30,8 +30,8 @@ val get_load_paths : unit -> t list 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 -> DirPath.t -> root:bool -> implicit:bool -> unit -(** [add_load_path phys type log] adds the binding [phys := log] to the current +val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit +(** [add_load_path phys log type] adds the binding [phys := log] to the current loadpaths. *) val remove_load_path : CUnix.physical_path -> unit @@ -47,7 +47,7 @@ val is_in_load_paths : CUnix.physical_path -> bool 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. *) + logical paths which are possible matches of it. *) val expand_root_path : DirPath.t -> CUnix.physical_path list -(** As [expand_path] but restricts to root loadpaths. *) +(** As [expand_path] but ignores the implicit status. *) -- cgit v1.2.3 From f15506263b0f85039b0b3c25c93406b9f9a5f241 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 1 Apr 2015 11:14:21 +0200 Subject: Removing a probably incorrect on-the-fly require in a tactic. Also removed the require function it was using, as it is absent from the remaining of the code. --- library/library.ml | 4 ---- library/library.mli | 1 - 2 files changed, 5 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 2b607e1a38..2ebf4e5c31 100644 --- a/library/library.ml +++ b/library/library.ml @@ -592,10 +592,6 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library qidl export = - let modrefl = List.map try_locate_qualified_library qidl in - require_library_from_dirpath modrefl export - let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev_map snd needed in diff --git a/library/library.mli b/library/library.mli index 75b256258f..150896783e 100644 --- a/library/library.mli +++ b/library/library.mli @@ -21,7 +21,6 @@ open Libnames (** {6 ... } *) (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) -val require_library : qualid located list -> bool option -> unit val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit -- cgit v1.2.3 From 7c41bc9bdc883aacbc015954a89ff13fe9c9c1c0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 1 Apr 2015 10:51:32 +0200 Subject: From X Require Y looks for X with absolute path, disregarding -R. --- library/libnames.ml | 5 +++++ library/libnames.mli | 2 ++ library/library.ml | 25 ++++++++++++++----------- library/library.mli | 10 ++++++++-- library/loadpath.ml | 11 +++-------- library/loadpath.mli | 5 +++-- 6 files changed, 35 insertions(+), 23 deletions(-) (limited to 'library') diff --git a/library/libnames.ml b/library/libnames.ml index f2a9d041d1..cdaec6a3de 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -32,6 +32,11 @@ let is_dirpath_prefix_of d1 d2 = List.prefix_of Id.equal (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) +let is_dirpath_suffix_of dir1 dir2 = + let dir1 = DirPath.repr dir1 in + let dir2 = DirPath.repr dir2 in + List.prefix_of Id.equal dir1 dir2 + let chop_dirpath n d = let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in DirPath.make (List.rev d1), DirPath.make (List.rev d2) diff --git a/library/libnames.mli b/library/libnames.mli index 3b5feb94e8..b95c088715 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -37,6 +37,8 @@ val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool +val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool + module Dirset : Set.S with type elt = DirPath.t module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset diff --git a/library/library.ml b/library/library.ml index 2ebf4e5c31..9d0ccb972a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -268,8 +268,9 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = Loadpath.expand_root_path pref in + let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let loadpath = List.map fst loadpath in let find ext = try let name = Id.to_string base ^ ext in @@ -286,10 +287,20 @@ let locate_absolute_library dir = | [vo;vi] -> dir, vo | _ -> assert false -let locate_qualified_library warn qid = +let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path dir in + let loadpath = match root with + | None -> Loadpath.expand_path dir + | Some root -> + let filter path = + if is_dirpath_prefix_of root path then + let path = drop_dirpath_prefix root path in + is_dirpath_suffix_of dir path + else false + in + Loadpath.filter_path filter + in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try @@ -333,14 +344,6 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) -let try_locate_qualified_library (loc,qid) = - try - let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in - dir,f - with - | LibUnmappedDir -> error_unmapped_dir qid - | LibNotFound -> error_lib_not_found qid - (************************************************************************) (** {6 Tables of opaque proof terms} *) diff --git a/library/library.mli b/library/library.mli index 150896783e..3506706809 100644 --- a/library/library.mli +++ b/library/library.mli @@ -72,8 +72,14 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - bool -> qualid -> library_location * DirPath.t * CUnix.physical_path -val try_locate_qualified_library : qualid located -> DirPath.t * string + ?root:DirPath.t -> ?warn:bool -> qualid -> + library_location * DirPath.t * CUnix.physical_path +(** Locates a library by implicit name. + + @raise LibUnmappedDir if the library is not in the path + @raise LibNotFound if there is no corresponding file in the path + +*) (** {6 Statistics: display the memory use of a library. } *) val mem : DirPath.t -> Pp.std_ppcmds diff --git a/library/loadpath.ml b/library/loadpath.ml index ca22801021..54ea0be4f9 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -87,20 +87,15 @@ 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 filter_path f = let rec aux = function | [] -> [] | p :: l -> - if DirPath.equal p.path_logical dir then p.path_physical :: aux l + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l else aux l in aux !load_paths -let is_suffix dir1 dir2 = - let dir1 = DirPath.repr dir1 in - let dir2 = DirPath.repr dir2 in - List.prefix_of Id.equal dir1 dir2 - let expand_path dir = let rec aux = function | [] -> [] @@ -109,7 +104,7 @@ let expand_path dir = match p.path_implicit with | true -> (** The path is implicit, so that we only want match the logical suffix *) - if is_suffix dir lg then (ph, lg) :: aux l else aux l + if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l | false -> (** Otherwise we must match exactly *) if DirPath.equal dir lg then (ph, lg) :: aux l else aux l diff --git a/library/loadpath.mli b/library/loadpath.mli index ae54b3183a..3251b8c60c 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -49,5 +49,6 @@ 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 matches of it. *) -val expand_root_path : DirPath.t -> CUnix.physical_path list -(** As [expand_path] but ignores the implicit status. *) +val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list +(** As {!expand_path} but uses a filter function instead, and ignores the + implicit status of loadpaths. *) -- cgit v1.2.3 From 049f329908ab6702c3a933ddc45ae6b6f5160065 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 2 Apr 2015 13:36:43 +0200 Subject: Make it possible for -R to override the existing implicit setting of a path. Without this commit, passing "-R theories Coq" to "coqtop -nois" has no effect since "-Q theories Coq" has already been done implicitly. --- library/loadpath.ml | 36 +++++++++++++++++++----------------- 1 file changed, 19 insertions(+), 17 deletions(-) (limited to 'library') diff --git a/library/loadpath.ml b/library/loadpath.ml index 54ea0be4f9..26af809e78 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -63,21 +63,24 @@ let add_load_path phys_path coq_path ~implicit = 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 + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DirPath.equal coq_path old_path then + implicit <> old_implicit + else if DirPath.equal coq_path (Nameops.default_root_prefix) + && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then + false (* This is the default "-I ." path, don't override the old path *) + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DirPath.equal old_path Nameops.default_root_prefix) then + msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath old_path ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path) in + true in + if replace then begin - (* Assume the user is concerned by library naming *) - if not (DirPath.equal dir Nameops.default_root_prefix) then - 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 @@ -99,9 +102,8 @@ let filter_path f = let expand_path dir = let rec aux = function | [] -> [] - | p :: l -> - let { path_physical = ph; path_logical = lg } = p in - match p.path_implicit with + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + match implicit with | true -> (** The path is implicit, so that we only want match the logical suffix *) if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l -- cgit v1.2.3