matita/components/binaries/matitadep/matitadep.ml

   1 module StringSet = Set.Make (String)
   2
   3 type file = {
   4    ddeps: string list;        (* direct dependences *)
   5    rdeps: StringSet.t option  (* recursive dependences *)
   6 }
   7
   8 let graph = Hashtbl.create 503
   9
  10 let debug = ref 0
  11
  12 let rec purge dname vdeps = match vdeps with
  13    | []       -> vdeps
  14    | hd :: tl -> if hd = dname then tl else hd :: purge dname tl
  15
  16 let add fname =
  17    if Hashtbl.mem graph fname then () else
  18    Hashtbl.add graph fname {ddeps = []; rdeps = None}
  19
  20 let add_ddep fname dname =
  21    let file = Hashtbl.find graph fname in
  22    Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps}
  23
  24 let init fname dname =
  25    if !debug land 1 > 0 then Printf.eprintf "init: %s: %s.\n" fname dname;
  26    add fname; add dname; add_ddep fname dname
  27
  28 (* vdeps: visited dependences for loop detection *)
  29 let rec compute_from_file vdeps fname file = match file.rdeps with
  30    | Some rdeps -> rdeps
  31    | None       ->
  32       if !debug land 2 > 0 then Printf.eprintf "  compute file: %s\n" fname;
  33       let vdeps = fname :: vdeps in
  34       List.iter (redundant vdeps fname file.ddeps) file.ddeps;
  35       let rdeps = compute_from_ddeps vdeps file.ddeps in
  36       Hashtbl.replace graph fname {file with rdeps = Some rdeps};
  37       rdeps
  38
  39 and compute_from_dname vdeps rdeps dname =
  40    if List.mem dname vdeps then begin
  41       let loop = purge dname (List.rev vdeps) in
  42       Printf.printf "circular: %s\n" (String.concat " " loop);
  43       StringSet.add dname rdeps
  44    end else
  45      let file = Hashtbl.find graph dname in
  46      StringSet.add dname (StringSet.union (compute_from_file vdeps dname file) rdeps)
  47
  48 and compute_from_ddeps vdeps ddeps =
  49    List.fold_left (compute_from_dname vdeps) StringSet.empty ddeps
  50
  51 and redundant vdeps fname ddeps dname =
  52    let rdeps = compute_from_ddeps vdeps (purge dname ddeps) in
  53    if StringSet.mem dname rdeps then
  54       Printf.printf "%s: redundant %s\n" fname dname
  55
  56 let check () =
  57    let iter fname file = ignore (compute_from_file [] fname file) in
  58    Hashtbl.iter iter graph
  59
  60 let get_unions () =
  61    let map1 ddeps dname = StringSet.add dname ddeps in
  62    let map2 fname file (fnames, ddeps) =
  63       StringSet.add fname fnames, List.fold_left map1 ddeps file.ddeps
  64    in
  65    Hashtbl.fold map2 graph (StringSet.empty, StringSet.empty)
  66
  67 let get_leafs () =
  68    let map fname file fnames =
  69       if file.ddeps = [] then StringSet.add fname fnames else fnames
  70    in
  71    Hashtbl.fold map graph StringSet.empty
  72
  73 let top () =
  74    let iter fname = Printf.printf "top: %s\n" fname in
  75    let fnames, ddeps = get_unions () in
  76    StringSet.iter iter (StringSet.diff fnames ddeps)
  77
  78 let leaf () =
  79    let iter fname = Printf.printf "leaf: %s\n" fname in
  80    let fnames = get_leafs () in
  81    StringSet.iter iter fnames
  82
  83 let rec read ich =
  84    let line = input_line ich in
  85    begin try Scanf.sscanf line "%s@:include \"%s@\"." init
  86    with Scanf.Scan_failure _ ->
  87       begin try Scanf.sscanf line "./%s@:include \"%s@\"." init
  88       with Scanf.Scan_failure _ ->
  89          begin try Scanf.sscanf line "%s@:(*%s@*)" (fun _ _ -> ())
  90          with Scanf.Scan_failure _ ->
  91             Printf.eprintf "unknown line: %s.\n" line
  92          end
  93       end
  94    end;
  95    read ich
  96
  97 let _ =
  98    let show_check = ref false in
  99    let show_top = ref false in
 100    let show_leaf = ref false in
 101    let process_file name = () in
 102    let show () =
 103       if !show_check then check ();
 104       if !show_top then top ();
 105       if !show_leaf then leaf ()
 106    in
 107    let help   = "" in
 108    let help_c = " Print the redundant and looping arcs of the dependences graph" in
 109    let help_d = "<flags>  Set these debug options" in
 110    let help_l = " Print the leaf nodes of the dependences graph" in
 111    let help_t = " Print the top nodes of the dependences graph" in
 112    Arg.parse [
 113       "-c", Arg.Set show_check, help_c;
 114       "-d", Arg.Int (fun x -> debug := x), help_d;
 115       "-l", Arg.Set show_leaf, help_l;
 116       "-t", Arg.Set show_top, help_t;
 117    ] process_file help;
 118    try read stdin with End_of_file -> show ()