sysutil.ml 4.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12 13 14 15 16 17 18
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

19 20 21 22 23 24 25 26 27 28 29
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

30 31 32 33
let channel_contents_buf cin =
  let buf = Buffer.create 1024
  and buff = String.make 1024 ' ' in
  let n = ref 0 in
34
  while n := input cin buff 0 1024; !n <> 0 do
35 36 37 38 39 40
    Buffer.add_substring buf buff 0 !n
  done;
  buf

let channel_contents cin = Buffer.contents (channel_contents_buf cin)

41 42 43 44 45
let rec fold_channel f acc cin =
  try
    fold_channel f (f acc (input_line cin)) cin
  with End_of_file -> acc

46 47 48 49 50
let file_contents_fmt f fmt =
  try
    let cin = open_in f in
    channel_contents_fmt cin fmt;
    close_in cin
51
  with _ ->
52 53
    invalid_arg (Printf.sprintf "(cannot open %s)" f)

54
let file_contents_buf f =
55
  try
56 57 58 59
    let cin = open_in f in
    let buf = channel_contents_buf cin in
    close_in cin;
    buf
60
  with _ ->
61 62 63 64
    invalid_arg (Printf.sprintf "(cannot open %s)" f)

let file_contents f = Buffer.contents (file_contents_buf f)

65
let open_temp_file ?(debug=false) filesuffix usefile =
66 67 68
  let file,cout = Filename.open_temp_file "why" filesuffix in
  try
    let res = usefile file cout in
69
    if not debug then Sys.remove file;
70 71 72
    close_out cout;
    res
  with
73
    | e ->
74
        if not debug then Sys.remove file;
75 76
        close_out cout;
        raise e
77

François Bobot's avatar
François Bobot committed
78 79 80 81 82 83 84
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
85 86 87
  done;
  close_out cout;
  close_in  cin
88

89 90 91 92 93 94 95 96 97 98 99 100
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


101 102 103 104 105 106 107 108 109 110 111 112
(* 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 *)
113 114 115 116 117
      let b = Filename.basename f in
      aux (b::acc) (Sys.getcwd ())
    else if f=d then
      (* we are at the root *)
      acc
118 119
    else
      let b = Filename.basename f in
120 121
        if f=b then b::acc else
          aux (b::acc) d
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
  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 =
141
    match ab,af with
142
      | x::rb, y::rf when x=y -> aux rb rf
143
      | _ ->
144 145 146 147 148
          let rec aux2 acc p =
            match p with
              | [] -> acc
              | _::rb -> aux2 (Filename.parent_dir_name::acc) rb
          in aux2 af ab
149 150 151 152 153 154 155 156 157
  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))

158 159 160 161 162 163
let absolutize_filename dirname f =
  if Filename.is_relative f then
    Filename.concat dirname f
  else
    f

164 165 166
(*
let p1 = relativize_filename "/bin/bash" "src/f.why"

167 168
let p1 = relativize_filename "test"
  "/home/cmarche/recherche/why3/src/ide/f.why"
169
*)
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185

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