blob: bc6ea8910ecea8a22b67063c02360d2529852e21 (
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
130
131
132
133
134
135
|
(************************************************************************)
(* 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
type path_type = ImplicitPath | ImplicitRootPath | RootPath
(** Load paths. Mapping from physical to logical paths. *)
type t = {
path_physical : CUnix.physical_path;
path_logical : DirPath.t;
path_type : path_type;
}
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 path_type 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_type = path_type;
} 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_type <> ImplicitPath && 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 ->
match p.path_type with
| ImplicitPath -> expand p dir :: aux l
| ImplicitRootPath ->
let inters = intersections p.path_logical dir in
List.map (expand p) inters @ aux l
| RootPath ->
if is_dirpath_prefix_of p.path_logical dir then
expand p (drop_dirpath_prefix p.path_logical dir) :: aux l
else aux l in
aux !load_paths
|
