aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/loadpath.ml
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