swh:1:snp:9f9174fb54ac68d4510837c2f930cf0558bce5b6
Tip revision: 863066bded664a5e2aba7f89c4fb7bc2afd0e28d authored by Pierre-Yves Strub on 23 September 2015, 08:28:02 UTC
Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec`
Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec`
Tip revision: 863066b
ecLoader.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2015 - IMDEA Software Institute
* Copyright (c) - 2012--2015 - Inria
*
* 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 (Pcre.pmatch ~pat:"^[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