diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 34 | ||||
| -rw-r--r-- | lib/system.mli | 15 | ||||
| -rw-r--r-- | lib/util.ml | 7 | ||||
| -rw-r--r-- | lib/util.mli | 1 |
4 files changed, 27 insertions, 30 deletions
diff --git a/lib/system.ml b/lib/system.ml index cf48f0e4b4..bb3c711307 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -13,22 +13,18 @@ open Util open Unix (* Files and load path. *) -(* All subdirectories, recursively *) -type load_path_entry = { - directory : string; - coq_dirpath : string list } +type physical_path = string +type load_path = physical_path list -type load_path = load_path_entry list +(* All subdirectories, recursively *) let exists_dir dir = try let _ = opendir dir in true with Unix_error _ -> false -let all_subdirs root alias = +let all_subdirs root = let l = ref [] in - let add f rel = - l := { directory = f; coq_dirpath = rel } :: !l - in + let add f rel = l := (f, rel) :: !l in let rec traverse dir rel = let dirh = opendir dir in try @@ -49,12 +45,8 @@ let all_subdirs root alias = in if exists_dir root then begin - let alias = match alias with - | Some a -> a - | None -> [Filename.basename root] - in - add root alias; - traverse root alias + add root []; + traverse root [] end ; List.rev !l @@ -73,7 +65,7 @@ let glob s = s let search_in_path path filename = let rec search = function | lpe :: rem -> - let f = glob (Filename.concat lpe.directory filename) in + let f = glob (Filename.concat lpe filename) in if Sys.file_exists f then (lpe,f) else search rem | [] -> raise Not_found @@ -86,7 +78,7 @@ let find_file_in_path paths name = let globname = glob name in if not (Filename.is_relative globname) then let root = Filename.dirname globname in - { directory = root; coq_dirpath = [] }, globname + root, globname else try search_in_path paths name @@ -129,12 +121,11 @@ let raw_extern_intern magic suffix = open_trapping_failure (fun n -> n,open_out_bin n) name suffix in output_binary_int channel magic; filec - and intern_state paths name = - let lpe,fname = find_file_in_path paths (make_suffix name suffix) in + and intern_state fname = let channel = open_in_bin fname in if input_binary_int channel <> magic then raise (Bad_magic_number fname); - (lpe,fname,channel) + channel in (extern_state,intern_state) @@ -151,7 +142,8 @@ let extern_intern magic suffix = with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try - let (_,fname,channel) = raw_intern paths name in + let _,fname = find_file_in_path paths (make_suffix name suffix) in + let channel = raw_intern fname in let v = marshal_in channel in close_in channel; v diff --git a/lib/system.mli b/lib/system.mli index ee2dca4905..e6eb921883 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -12,15 +12,13 @@ given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) -type load_path_entry = { - directory : string; - coq_dirpath : string list } -type load_path = load_path_entry list +type physical_path = string +type load_path = physical_path list -val all_subdirs : unix_path:string -> string list option -> load_path +val all_subdirs : unix_path:string -> (physical_path * string list) list val is_in_path : load_path -> string -> bool -val where_in_path : load_path -> string -> load_path_entry * string +val where_in_path : load_path -> string -> physical_path * string val make_suffix : string -> string -> string val file_readable_p : string -> bool @@ -31,7 +29,7 @@ val home : string val exists_dir : string -> bool -val find_file_in_path : load_path -> string -> load_path_entry * string +val find_file_in_path : load_path -> string -> physical_path * string (*s Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] @@ -43,8 +41,7 @@ val marshal_in : in_channel -> 'a exception Bad_magic_number of string val raw_extern_intern : int -> string -> - (string -> string * out_channel) * - (load_path -> string -> load_path_entry * string * in_channel) + (string -> string * out_channel) * (string -> in_channel) val extern_intern : int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a) diff --git a/lib/util.ml b/lib/util.ml index 0c3c038dd2..cf5b58b49e 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -223,6 +223,13 @@ let rec list_distinct = function | h::t -> (not (List.mem h t)) && list_distinct t | _ -> true +let rec list_filter2 f = function + | [], [] as p -> p + | d::dp, l::lp -> + let (dp',lp' as p) = list_filter2 f (dp,lp) in + if f d l then d::dp', l::lp' else p + | _ -> invalid_arg "list_filter2" + let list_subset l1 l2 = let t2 = Hashtbl.create 151 in List.iter (fun x -> Hashtbl.add t2 x ()) l2; diff --git a/lib/util.mli b/lib/util.mli index d5976baf1d..a57803c5e2 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -64,6 +64,7 @@ val list_chop : int -> 'a list -> 'a list * 'a list val list_tabulate : (int -> 'a) -> int -> 'a list val list_assign : 'a list -> int -> 'a -> 'a list val list_distinct : 'a list -> bool +val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list val list_map2_i : (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list |