https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
ecLoader.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
(* -------------------------------------------------------------------- *)
type idx_t = int * int
type ecloader = {
mutable ecl_idirs : ((bool * string) * idx_t) list;
}
type kind = [`Ec | `EcA]
(* -------------------------------------------------------------------- *)
let create () = { ecl_idirs = []; }
(* -------------------------------------------------------------------- *)
let aslist (ld : ecloader) =
ld.ecl_idirs
(* -------------------------------------------------------------------- *)
let dup (ld : ecloader) = { ecl_idirs = ld.ecl_idirs; }
(* -------------------------------------------------------------------- *)
let forsys (ld : ecloader) =
{ ecl_idirs = List.filter (fun ((b, _), _) -> b) ld.ecl_idirs; }
(* -------------------------------------------------------------------- *)
let rec addidir ?(system = false) ?(recursive = false) (idir : string) (ecl : ecloader) =
if recursive then begin
let isdir filename =
let filename = Filename.concat idir filename in
try Sys.is_directory filename with Sys_error _ -> false
in
let dirs = (try EcUtils.Os.listdir idir with Unix.Unix_error _ -> []) in
let dirs = List.sort compare (List.filter isdir dirs) in
List.iter (fun filename ->
if not (String.starts_with filename ".") then
let filename = Filename.concat idir filename in
addidir ~system ~recursive filename ecl)
dirs
end;
match (try Some (Unix.stat idir) with Unix.Unix_error _ -> None) with
| None -> ()
| Some st -> begin
let idx = (st.Unix.st_dev, st.Unix.st_ino) in
match Sys.os_type with
| "Win32" ->
let test ((_, name), _) = name = idir in
if not (List.exists test ecl.ecl_idirs) then
ecl.ecl_idirs <- ((system, idir), idx) :: ecl.ecl_idirs
| _ ->
if not (List.exists ((=) idx |- snd) ecl.ecl_idirs) then
ecl.ecl_idirs <- ((system, idir), idx) :: ecl.ecl_idirs
end
(* -------------------------------------------------------------------- *)
let try_stat name =
try Some (Unix.lstat name)
with Unix.Unix_error _ -> None
(* -------------------------------------------------------------------- *)
let norm_name (mode : [`Lower | `Upper]) name =
String.init
(String.length name)
(function
| 0 when mode = `Lower -> Char.lowercase name.[0]
| 0 when mode = `Upper -> Char.uppercase name.[0]
| i -> name.[i])
(* -------------------------------------------------------------------- *)
let check_case idir name (dev, ino) =
let name = norm_name `Lower name in
let check1 tname =
match name = norm_name `Lower tname with
| false -> false
| true -> begin
try
let stat = Filename.concat idir tname in
let stat = Unix.lstat stat in
stat.Unix.st_dev = dev && stat.Unix.st_ino = ino
with Unix.Unix_error _ -> false
end
in
try List.exists check1 (EcUtils.Os.listdir idir)
with Unix.Unix_error _ -> false
(* -------------------------------------------------------------------- *)
let locate ?(onlysys = false) (name : string) (ecl : ecloader) =
if not (EcRegexp.match_ (`S "^[a-zA-Z0-9_]+$") name) then
None
else
let locate kind ((issys, idir), _) =
let name =
match kind with
| `Ec -> Printf.sprintf "%s.ec" name
| `EcA -> Printf.sprintf "%s.eca" name
in
match onlysys && not issys with
| true -> None
| false ->
let stat =
let oname = norm_name `Upper name in
let iname = norm_name `Lower name in
List.fpick
(List.map
(fun name ->
let fullname = Filename.concat idir name in
fun () -> try_stat fullname |> omap (fun s -> (s, name)))
[iname; oname])
in
match stat with
| None -> None
| Some (stat, name) ->
let stat = (stat.Unix.st_dev, stat.Unix.st_ino) in
if not (check_case idir name stat)
then None
else Some (Filename.concat idir name, kind)
in
match
List.rev_pmap
(fun kind -> List.opick (locate kind) ecl.ecl_idirs)
[`Ec; `EcA]
with
| [x] -> Some x
| _ -> None