1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
|
(************************************************************************)
(* This file is licensed under The MIT License *)
(* See LICENSE for more information *)
(************************************************************************)
let debug = false
(* Information about a directory containing .v files *)
type 'a t =
{ prefix : string list
(** prefix of the directory, [] when root *)
; children : 'a t list
(** List of children, this could be scanned lazily *)
; modules : 'a list
(** modules [without the .v suffix] *)
}
(* Scan a single directory *)
let to_module ~dir ~prefix file =
let source = Path.make (Filename.concat dir file) in
let name = Filename.remove_extension file in
Coq_module.make ~source ~prefix ~name
let scan_dir ~prefix dir =
let contents = Sys.readdir dir |> Array.to_list in
let dirs, files = List.partition (fun f -> Filename.concat dir f |> Sys.is_directory) contents in
let files = List.filter (fun f -> Filename.(check_suffix (concat dir f) ".v")) files in
let modules = List.map (to_module ~dir ~prefix) files in
dirs, modules
(* Scan a tree *)
let rec scan_subtree ~base_dir ~prefix children =
let prefix = prefix @ [children] in
scan ~prefix (Filename.concat base_dir children)
and scan ~prefix base_dir =
if debug then
Format.eprintf "[debug] [scan] Enter: %s @\n%!" base_dir;
let children, modules = scan_dir ~prefix base_dir in
let children = List.map (scan_subtree ~base_dir ~prefix) children in
{ prefix; children; modules }
let rec map ~(f : prefix:string list -> 'a -> 'b) di =
{ di with
children = List.map (map ~f) di.children
; modules = List.map (f ~prefix:di.prefix) di.modules
}
let rec iter ~(f : prefix:string list -> 'a -> unit) di : unit =
f ~prefix:di.prefix di.modules;
List.iter (iter ~f) di.children
let rec fold ~(f : prefix:string list -> 'b list -> 'a list -> 'b) ~init di =
let res = List.map (fold ~f ~init) di.children in
f ~prefix:di.prefix res di.modules
let rec coq_modules { modules; children; _ } =
modules @ List.concat (List.map coq_modules children)
(* let rec fold ~(f : prefix:string list -> 'a -> 'b) di = *)
let rec pp pp_module fmt { prefix; children; modules } =
let open Format in
fprintf fmt "@[ { prefix = %a; children = %a; modules = %a }@]"
(pp_print_list pp_print_string) prefix
(pp_print_list (pp pp_module)) children
(pp_print_list pp_module) modules
let pp = pp Coq_module.pp
|