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 show_check = ref false
   9 let show_top = ref false
  10 let show_leaf = ref false
  11 let show_back = ref ""
  12 let iset = ref StringSet.empty
  13
  14 let graph = Hashtbl.create 503
  15
  16 let debug = ref 0
  17
  18 let rec purge dname vdeps = match vdeps with
  19   | []       -> vdeps
  20   | hd :: tl -> if hd = dname then tl else hd :: purge dname tl
  21
  22 let add fname =
  23   if fname = "" then () else
  24   if Hashtbl.mem graph fname then () else
  25   Hashtbl.add graph fname {ddeps = []; rdeps = None}
  26
  27 let add_ddep fname dname =
  28   if dname = "" then () else
  29   let file = Hashtbl.find graph fname in
  30   Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps}
  31
  32 let init fname dname =
  33   if !debug land 1 > 0 then Printf.printf "init: %s: %s.\n" fname dname;
  34   add fname; add dname; add_ddep fname dname
  35
  36 (* vdeps: visited dependences for loop detection *)
  37 let rec compute_from_file vdeps fname file = match file.rdeps with
  38   | Some rdeps -> rdeps
  39   | None       ->
  40     if !debug land 2 > 0 then Printf.printf "  (%u) compute object: %s\n%!" (List.length vdeps) fname;
  41     if !debug land 2 > 0 then Printf.printf "  ddeps: %s\n%!" (String.concat " " file.ddeps);
  42     if !debug land 8 > 0 then Printf.printf "  vdeps: %s\n%!" (String.concat " " vdeps);
  43     if List.mem fname vdeps then begin
  44       if !show_check then Printf.printf "circular: %s\n%!" (String.concat " " vdeps);
  45       StringSet.empty
  46     end else begin
  47       let vdeps = fname :: vdeps in
  48       List.iter (redundant vdeps fname file.ddeps) file.ddeps;
  49       let rdeps = compute_from_ddeps vdeps file.ddeps in
  50       Hashtbl.replace graph fname {file with rdeps = Some rdeps};
  51       rdeps
  52     end
  53
  54 and compute_from_dname vdeps rdeps dname =
  55   if !debug land 4 > 0 then Printf.printf "  (%u) compute dep: %s\n%!" (List.length vdeps) dname;
  56   if !debug land 8 > 0 then Printf.printf "  vdeps: %s\n%!" (String.concat " " vdeps);
  57   let file = Hashtbl.find graph dname in
  58   let rdeps = StringSet.add dname rdeps in
  59   StringSet.union (compute_from_file vdeps dname file) rdeps
  60
  61 and compute_from_ddeps vdeps ddeps =
  62   List.fold_left (compute_from_dname vdeps) StringSet.empty ddeps
  63
  64 and redundant vdeps fname ddeps dname =
  65   let rdeps = compute_from_ddeps vdeps (purge dname ddeps) in
  66   if !show_check && StringSet.mem dname rdeps then
  67     Printf.printf "%S: redundant %S\n%!" fname dname
  68
  69 let check () =
  70   let iter fname file = ignore (compute_from_file [] fname file) in
  71   Hashtbl.iter iter graph
  72
  73 let get_unions () =
  74   let map1 ddeps dname = StringSet.add dname ddeps in
  75   let map2 fname file (fnames, ddeps) =
  76     StringSet.add fname fnames, List.fold_left map1 ddeps file.ddeps
  77   in
  78   Hashtbl.fold map2 graph (StringSet.empty, StringSet.empty)
  79
  80 let get_leafs () =
  81   let map fname file fnames =
  82     if file.ddeps = [] then StringSet.add fname fnames else fnames
  83   in
  84   Hashtbl.fold map graph StringSet.empty
  85
  86 let top () =
  87   let iter fname = Printf.printf "top: %s\n" fname in
  88   let fnames, ddeps = get_unions () in
  89   StringSet.iter iter (StringSet.diff fnames ddeps)
  90
  91 let leaf () =
  92   let iter fname = Printf.printf "leaf: %s\n" fname in
  93   let fnames = get_leafs () in
  94   StringSet.iter iter fnames
  95
  96 let rec file_iter map ich =
  97   let line = input_line ich in
  98   if line <> "" then map line;
  99   file_iter map ich
 100
 101 let back name =
 102   Printf.printf "\"%s\":\n" name;
 103   try match (Hashtbl.find graph name).rdeps with
 104     | None       -> ()
 105     | Some rdeps ->
 106       let rdeps =
 107         if !iset = StringSet.empty then rdeps
 108         else StringSet.inter rdeps !iset
 109       in
 110       let iter name = Printf.printf "  \"%s\"\n" name in
 111       StringSet.iter iter rdeps;
 112       Printf.printf "\n"
 113   with Not_found -> Printf.printf "* not found\n\n"
 114
 115 let back fname =
 116   if Librarian.is_uri fname then back fname else
 117   let ich = open_in fname in
 118   try file_iter back ich with End_of_file -> close_in ich
 119
 120 let set_iset fname =
 121   if Librarian.is_uri fname then iset := StringSet.singleton fname else
 122   let map name = iset := StringSet.add name !iset in
 123   let ich = open_in fname in
 124   try file_iter map ich with End_of_file -> close_in ich
 125
 126 let rec read_many ich s =
 127   let line = input_line ich in
 128   if line = "" then () else begin
 129     begin try Scanf.sscanf line " %S" (init s)
 130     with Scanf.Scan_failure _ | End_of_file ->
 131       Printf.eprintf "unknown line: %s.\n" line
 132     end;
 133     read_many ich s
 134   end
 135
 136 let rec read_deps ich =
 137   let line = input_line ich in
 138   begin try Scanf.sscanf line "%s@:include %S." init
 139   with Scanf.Scan_failure _ | End_of_file ->
 140     begin try Scanf.sscanf line "./%s@:include %S." init
 141     with Scanf.Scan_failure _ | End_of_file ->
 142       begin try Scanf.sscanf line "%s@:(*%s@*)" (fun _ _ -> ())
 143       with Scanf.Scan_failure _ | End_of_file ->
 144         begin try Scanf.sscanf line "%S:%!" (read_many ich)
 145         with Scanf.Scan_failure _ | End_of_file ->
 146           begin try Scanf.sscanf line "%S: %S" init
 147           with Scanf.Scan_failure _ | End_of_file ->
 148             Printf.eprintf "unknown line: %s.\n" line
 149           end
 150         end
 151       end
 152     end
 153   end;
 154   read_deps ich
 155
 156 let _ =
 157   let process_file name =
 158     let ich = open_in name in
 159     try read_deps ich with End_of_file -> close_in ich
 160   in
 161   let show () =
 162     if !show_check || !show_back <> "" then check ();
 163     if !show_top then top ();
 164     if !show_leaf then leaf ();
 165     if !show_back <> "" then back !show_back
 166   in
 167   let help   = "matitadep [ -clt | -d <int> | -bi [ <uri> | <file> ] | <file> ]*" in
 168   let help_b = "<uri>|<file>  Print the backward dependences of these nodes" in
 169   let help_c = " Print the redundant and looping arcs of the dependences graph" in
 170   let help_d = "<flags>  Set these debug options" in
 171   let help_i = "<uri>|<file>  Intersect with these nodes" in
 172   let help_l = " Print the leaf nodes of the dependences graph" in
 173   let help_t = " Print the top nodes of the dependences graph" in
 174   Arg.parse [
 175     "-b", Arg.String ((:=) show_back), help_b;
 176     "-c", Arg.Set show_check, help_c;
 177     "-d", Arg.Int ((:=) debug), help_d;
 178     "-i", Arg.String set_iset, help_i;
 179     "-l", Arg.Set show_leaf, help_l;
 180     "-t", Arg.Set show_top, help_t;
 181   ] process_file help;
 182   show ()