blob: 71956cf8f6e8fbaefd30b68e105cb4246ab737f2 (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(** Some excerpt of Util and similar files to avoid loading the whole
module and its dependencies (and hence Compat and Camlp4) *)
module Stringmap = Map.Make(String)
let list_fold_left_i f =
let rec it_list_f i a = function
| [] -> a
| b::l -> it_list_f (i+1) (f i a b) l
in
it_list_f
(* [list_chop i l] splits [l] into two lists [(l1,l2)] such that
[l1++l2=l] and [l1] has length [i].
It raises [Failure] when [i] is negative or greater than the length of [l] *)
let list_chop n l =
let rec chop_aux i acc = function
| tl when i=0 -> (List.rev acc, tl)
| h::t -> chop_aux (pred i) (h::acc) t
| [] -> failwith "list_chop"
in
chop_aux n [] l
let list_map_i f =
let rec map_i_rec i = function
| [] -> []
| x::l -> let v = f i x in v :: map_i_rec (i+1) l
in
map_i_rec
let list_index x =
let rec index_x n = function
| y::l -> if x = y then n else index_x (succ n) l
| [] -> raise Not_found
in
index_x 1
let list_index0 x l = list_index x l - 1
let list_filter_i p =
let rec filter_i_rec i = function
| [] -> []
| x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l'
in
filter_i_rec 0
let string_map f s =
let l = String.length s in
let r = String.create l in
for i= 0 to (l - 1) do r.[i] <- f (s.[i]) done;
r
let subst_command_placeholder s t =
Str.global_replace (Str.regexp_string "%s") t s
(* On win32, the home directory is probably not in $HOME, but in
some other environment variable *)
let home =
try Sys.getenv "HOME" with Not_found ->
try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
try Sys.getenv "USERPROFILE" with Not_found -> "."
let coqlib = ref ""
let coqtop_path = ref ""
(* Hints to partially detects if two paths refer to the same repertory *)
let rec remove_path_dot p =
let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
let n = String.length curdir in
if String.length p > n && String.sub p 0 n = curdir then
remove_path_dot (String.sub p n (String.length p - n))
else
p
let strip_path p =
let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
let n = String.length cwd in
if String.length p > n && String.sub p 0 n = cwd then
remove_path_dot (String.sub p n (String.length p - n))
else
remove_path_dot p
let canonical_path_name p =
let current = Sys.getcwd () in
try
Sys.chdir p;
let p' = Sys.getcwd () in
Sys.chdir current;
p'
with Sys_error _ ->
(* We give up to find a canonical name and just simplify it... *)
strip_path p
|
