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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
let to_relative_path : string -> string = fun full_path ->
if Filename.is_relative full_path then full_path else
let re_delim = if Sys.win32 then "[/\\]" else "/" in
let cwd = Str.split_delim (Str.regexp re_delim) (Sys.getcwd ()) in
let path = Str.split_delim (Str.regexp re_delim) full_path in
let rec remove_common_prefix l1 l2 =
match (l1, l2) with
| (x1 :: l1, x2 :: l2) when x1 = x2 -> remove_common_prefix l1 l2
| (_ , _ ) -> (l1, String.concat "/" l2)
in
let (cwd, path) = remove_common_prefix cwd path in
let add_parent path _ = Filename.concat Filename.parent_dir_name path in
List.fold_left add_parent path cwd
let normalize_path : string -> string = fun path ->
let re_delim = if Sys.win32 then "[/\\]" else "/" in
let path = Str.split_delim (Str.regexp re_delim) path in
let rec normalize acc path =
match (path, acc) with
| ([] , _ ) -> List.rev acc
| ("." :: path, _ ) -> normalize acc path
| (".." :: path, [] ) -> normalize (".." :: []) path
| (".." :: path, ".." :: _ ) -> normalize (".." :: acc) path
| (".." :: path, _ :: acc) -> normalize acc path
| (dir :: path, _ ) -> normalize (dir :: acc) path
in
match normalize [] path with
| [] -> "."
| path -> String.concat "/" path
|
