blob: 60799a8a7e9f2012af81b14e46740f78b5818f74 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
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 load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
let logical p = p.path_logical
let physical p = p.path_physical
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
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
|
