https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: 5e06824340dbecd78d36e3ddde952e505e85061f authored by Pierre-Yves Strub on 27 April 2018, 12:07:39 UTC
Merge branch '1.0' into deploy-trivial-in-low-api
Tip revision: 5e06824
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
back to top