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