sysutil.ml 6.31 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7
8
9
10
11
12
13
14
15
16
17
18
19
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
21
22
23
24
25
26
let backup_file f =
  if Sys.file_exists f then begin
    let fb = f ^ ".bak" in
    if Sys.file_exists fb then Sys.remove fb;
    Sys.rename f fb
  end

27
28
29
30
31
32
33
34
35
36
37
let channel_contents_fmt cin fmt =
  let buff = String.make 1024 ' ' in
  let n = ref 0 in
  while n := input cin buff 0 1024; !n <> 0 do
    Format.pp_print_string fmt
      (if !n = 1024 then
         buff
       else
         String.sub buff 0 !n)
  done

38
39
40
41
let channel_contents_buf cin =
  let buf = Buffer.create 1024
  and buff = String.make 1024 ' ' in
  let n = ref 0 in
42
  while n := input cin buff 0 1024; !n <> 0 do
43
44
45
46
47
48
    Buffer.add_substring buf buff 0 !n
  done;
  buf

let channel_contents cin = Buffer.contents (channel_contents_buf cin)

49
50
51
52
53
let rec fold_channel f acc cin =
  try
    fold_channel f (f acc (input_line cin)) cin
  with End_of_file -> acc

54
55
56
57
58
let file_contents_fmt f fmt =
  try
    let cin = open_in f in
    channel_contents_fmt cin fmt;
    close_in cin
59
  with _ ->
60
61
    invalid_arg (Printf.sprintf "(cannot open %s)" f)

62
let file_contents_buf f =
63
  try
64
65
66
67
    let cin = open_in f in
    let buf = channel_contents_buf cin in
    close_in cin;
    buf
68
  with _ ->
69
70
71
72
    invalid_arg (Printf.sprintf "(cannot open %s)" f)

let file_contents f = Buffer.contents (file_contents_buf f)

Francois Bobot's avatar
Francois Bobot committed
73
let open_temp_file ?(debug=false) filesuffix usefile =
74
75
76
  let file,cout = Filename.open_temp_file "why" filesuffix in
  try
    let res = usefile file cout in
Francois Bobot's avatar
Francois Bobot committed
77
    if not debug then Sys.remove file;
78
79
80
    close_out cout;
    res
  with
81
    | e ->
Francois Bobot's avatar
Francois Bobot committed
82
        if not debug then Sys.remove file;
83
84
        close_out cout;
        raise e
85

Francois Bobot's avatar
Francois Bobot committed
86
87
88
89
90
91
92
93
type 'a result =
  | Result of 'a
  | Exception of exn

open Unix

exception Bad_execution of process_status

94
let call_asynchronous (f : unit -> 'a) =
Francois Bobot's avatar
Francois Bobot committed
95
96
97
98
  let cin,cout = pipe () in
  let cin = in_channel_of_descr cin in
  let cout = out_channel_of_descr cout in
  match fork () with
99
100
    | 0 ->
        let result =
Francois Bobot's avatar
Francois Bobot committed
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
          try
            Result (f ())
          with exn -> Exception exn in
        Marshal.to_channel cout (result : 'a result) [];
        close_out cout;
        exit 0
    | pid ->
        let f () =
          let result = (Marshal.from_channel cin: 'a result) in
          close_in cin;
          let _, ps = waitpid [] pid in
          match ps with
            | WEXITED 0 ->
                begin match result with
                  | Result res -> res
                  | Exception exn -> raise exn
                end
            | _ -> raise (Bad_execution ps) in
        f
120

François Bobot's avatar
François Bobot committed
121
122
123
124
125
126
127
128
let copy_file from to_ =
  let cin = open_in from in
  let cout = open_out to_ in
  let buff = String.make 1024 ' ' in
  let n = ref 0 in
  while n := input cin buff 0 1024; !n <> 0 do
    output cout buff 0 !n
  done
129

130
131
132
133
134
135
136
137
138
139
140
141
let rec copy_dir from to_ =
  if not (Sys.file_exists to_) then Unix.mkdir to_ 0o755;
  let files = Sys.readdir from in
  let copy fname =
    let src = Filename.concat from fname in
    let dst = Filename.concat to_ fname in
    if Sys.is_directory src
    then copy_dir src dst
    else copy_file src dst in
  Array.iter copy files


142
143
144
145
146
147
148
149
150
151
152
153
(* return the absolute path of a given file name.
   this code has been designed to be architecture-independant so
   be very careful if you modify this *)
let path_of_file f =
  let rec aux acc f =
(*
    Format.printf "aux %s@." f;
    let _ = read_line () in
*)
    let d = Filename.dirname f in
    if d = Filename.current_dir_name then
      (* f is relative to the current dir *)
154
155
156
157
158
      let b = Filename.basename f in
      aux (b::acc) (Sys.getcwd ())
    else if f=d then
      (* we are at the root *)
      acc
159
160
    else
      let b = Filename.basename f in
161
162
        if f=b then b::acc else
          aux (b::acc) d
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
  in
  aux [] f

(*
let test x = (Filename.dirname x, Filename.basename x)

let _ = test "file"
let _ = test "/file"
let _ = test "/"
let _ = test "f1/f2"
let _ = test "/f1/f2"

let p1 = path_of_file "/bin/bash"

let p1 = path_of_file "../src/f.why"
  *)

let relativize_filename base f =
  let rec aux ab af =
182
    match ab,af with
183
      | x::rb, y::rf when x=y -> aux rb rf
184
      | _ ->
185
186
187
188
189
          let rec aux2 acc p =
            match p with
              | [] -> acc
              | _::rb -> aux2 (Filename.parent_dir_name::acc) rb
          in aux2 af ab
190
191
192
193
194
195
196
197
198
  in
  let rec rebuild l =
    match l with
      | [] -> ""
      | [x] -> x
      | x::l -> Filename.concat x (rebuild l)
  in
  rebuild (aux (path_of_file base) (path_of_file f))

199
200
201
202
203
204
let absolutize_filename dirname f =
  if Filename.is_relative f then
    Filename.concat dirname f
  else
    f

205
206
207
(*
let p1 = relativize_filename "/bin/bash" "src/f.why"

208
209
let p1 = relativize_filename "test"
  "/home/cmarche/recherche/why3/src/ide/f.why"
210
*)
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226

let uniquify file =
  (* Uniquify the filename if it exists on disk *)
  let i =
    try String.rindex file '.'
    with _ -> String.length file
  in
  let name = String.sub file 0 i in
  let ext = String.sub file i (String.length file - i) in
  let i = ref 1 in
  while Sys.file_exists
    (name ^ "_" ^ (string_of_int !i) ^ ext) do
    incr i
  done;
  let file = name ^ "_" ^ (string_of_int !i) ^ ext in
  file