X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatitadep%2Fmatitadep.ml;h=426ab69267043da6cbe60c8d710fab518030ad0b;hp=d21af12a3fd635320655f2c6a7e1bf9d832ef161;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hpb=bfd440cc2a790741616cae6b375609c6bbdc3b24

diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml
index d21af12a3..426ab6926 100644
--- a/matita/components/binaries/matitadep/matitadep.ml
+++ b/matita/components/binaries/matitadep/matitadep.ml
@@ -5,6 +5,12 @@ type file = {
   rdeps: StringSet.t option  (* recursive dependences *)
 }
 
+let show_check = ref false
+let show_top = ref false
+let show_leaf = ref false
+let show_back = ref ""
+let iset = ref StringSet.empty
+
 let graph = Hashtbl.create 503
 
 let debug = ref 0
@@ -24,36 +30,41 @@ let add_ddep fname dname =
   Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps}
 
 let init fname dname =
-  if !debug land 1 > 0 then Printf.eprintf "init: %s: %s.\n" fname dname;
+  if !debug land 1 > 0 then Printf.printf "init: %s: %s.\n" fname dname;
   add fname; add dname; add_ddep fname dname
 
 (* vdeps: visited dependences for loop detection *)
 let rec compute_from_file vdeps fname file = match file.rdeps with
   | Some rdeps -> rdeps
   | None       ->
-    if !debug land 2 > 0 then Printf.eprintf "  compute file: %s\n" fname;
-    let vdeps = fname :: vdeps in
-    List.iter (redundant vdeps fname file.ddeps) file.ddeps;
-    let rdeps = compute_from_ddeps vdeps file.ddeps in
-    Hashtbl.replace graph fname {file with rdeps = Some rdeps};
-    rdeps
+    if !debug land 2 > 0 then Printf.printf "  (%u) compute object: %s\n%!" (List.length vdeps) fname;
+    if !debug land 2 > 0 then Printf.printf "  ddeps: %s\n%!" (String.concat " " file.ddeps);
+    if !debug land 8 > 0 then Printf.printf "  vdeps: %s\n%!" (String.concat " " vdeps);
+    if List.mem fname vdeps then begin
+      if !show_check then Printf.printf "circular: %s\n%!" (String.concat " " vdeps);
+      StringSet.empty
+    end else begin
+      let vdeps = fname :: vdeps in
+      List.iter (redundant vdeps fname file.ddeps) file.ddeps;
+      let rdeps = compute_from_ddeps vdeps file.ddeps in
+      Hashtbl.replace graph fname {file with rdeps = Some rdeps};
+      rdeps
+    end
 
 and compute_from_dname vdeps rdeps dname =
-  if List.mem dname vdeps then begin
-    let loop = purge dname (List.rev vdeps) in
-    Printf.printf "circular: %s\n" (String.concat " " loop);
-    StringSet.add dname rdeps
-  end else
-    let file = Hashtbl.find graph dname in
-    StringSet.add dname (StringSet.union (compute_from_file vdeps dname file) rdeps)
+  if !debug land 4 > 0 then Printf.printf "  (%u) compute dep: %s\n%!" (List.length vdeps) dname;
+  if !debug land 8 > 0 then Printf.printf "  vdeps: %s\n%!" (String.concat " " vdeps);
+  let file = Hashtbl.find graph dname in
+  let rdeps = StringSet.add dname rdeps in
+  StringSet.union (compute_from_file vdeps dname file) rdeps
 
 and compute_from_ddeps vdeps ddeps =
   List.fold_left (compute_from_dname vdeps) StringSet.empty ddeps
 
 and redundant vdeps fname ddeps dname =
   let rdeps = compute_from_ddeps vdeps (purge dname ddeps) in
-  if StringSet.mem dname rdeps then
-    Printf.printf "%s: redundant %s\n" fname dname
+  if !show_check && StringSet.mem dname rdeps then
+    Printf.printf "%S: redundant %S\n%!" fname dname
 
 let check () =
   let iter fname file = ignore (compute_from_file [] fname file) in
@@ -82,52 +93,90 @@ let leaf () =
   let fnames = get_leafs () in
   StringSet.iter iter fnames
 
-let back fname =
-  Printf.printf "backward: %s\n" fname;
-  try match (Hashtbl.find graph fname).rdeps with
+let rec file_iter map ich =
+  let line = input_line ich in
+  if line <> "" then map line;
+  file_iter map ich
+
+let back name =
+  Printf.printf "\"%s\":\n" name;
+  try match (Hashtbl.find graph name).rdeps with
     | None       -> ()
     | Some rdeps ->
-      let iter fname = Printf.printf "%s\n" fname in
-      StringSet.iter iter rdeps
-  with Not_found -> ()
+      let rdeps =
+        if !iset = StringSet.empty then rdeps
+        else StringSet.inter rdeps !iset
+      in
+      let iter name = Printf.printf "  \"%s\"\n" name in
+      StringSet.iter iter rdeps;
+      Printf.printf "\n"
+  with Not_found -> Printf.printf "* not found\n\n"
 
-let rec read ich =
+let back fname =
+  if Librarian.is_uri fname then back fname else
+  let ich = open_in fname in
+  try file_iter back ich with End_of_file -> close_in ich
+
+let set_iset fname =
+  if Librarian.is_uri fname then iset := StringSet.singleton fname else
+  let map name = iset := StringSet.add name !iset in
+  let ich = open_in fname in
+  try file_iter map ich with End_of_file -> close_in ich
+
+let rec read_many ich s =
   let line = input_line ich in
-  begin try Scanf.sscanf line "%s@:include \"%s@\"." init
-  with Scanf.Scan_failure _ ->
-    begin try Scanf.sscanf line "./%s@:include \"%s@\"." init
-    with Scanf.Scan_failure _ ->
+  if line = "" then () else begin
+    begin try Scanf.sscanf line " %S" (init s)
+    with Scanf.Scan_failure _ | End_of_file ->
+      Printf.eprintf "unknown line: %s.\n" line
+    end;
+    read_many ich s
+  end
+
+let rec read_deps ich =
+  let line = input_line ich in
+  begin try Scanf.sscanf line "%s@:include %S." init
+  with Scanf.Scan_failure _ | End_of_file ->
+    begin try Scanf.sscanf line "./%s@:include %S." init
+    with Scanf.Scan_failure _ | End_of_file ->
       begin try Scanf.sscanf line "%s@:(*%s@*)" (fun _ _ -> ())
-      with Scanf.Scan_failure _ ->
-	   Printf.eprintf "unknown line: %s.\n" line
+      with Scanf.Scan_failure _ | End_of_file ->
+        begin try Scanf.sscanf line "%S:%!" (read_many ich)
+        with Scanf.Scan_failure _ | End_of_file ->
+          begin try Scanf.sscanf line "%S: %S" init
+          with Scanf.Scan_failure _ | End_of_file ->
+            Printf.eprintf "unknown line: %s.\n" line
+          end
+        end
       end
     end
   end;
-  read ich
+  read_deps ich
 
 let _ =
-  let show_check = ref false in
-  let show_top = ref false in
-  let show_leaf = ref false in
-  let show_back = ref "" in
-  let process_file name = () in
+  let process_file name =
+    let ich = open_in name in
+    try read_deps ich with End_of_file -> close_in ich
+  in
   let show () =
-    if !show_check then check ();
+    if !show_check || !show_back <> "" then check ();
     if !show_top then top ();
     if !show_leaf then leaf ();
     if !show_back <> "" then back !show_back
   in
-  let help   = "matitadep [-clt | -d <int> | -b <string> ] < <file>" in
-  let help_b = "<string> Print the backward dependences of this node" in
+  let help   = "matitadep [ -clt | -d <int> | -bi [ <uri> | <file> ] | <file> ]*" in
+  let help_b = "<uri>|<file>  Print the backward dependences of these nodes" in
   let help_c = " Print the redundant and looping arcs of the dependences graph" in
   let help_d = "<flags>  Set these debug options" in
+  let help_i = "<uri>|<file>  Intersect with these nodes" in
   let help_l = " Print the leaf nodes of the dependences graph" in
   let help_t = " Print the top nodes of the dependences graph" in
   Arg.parse [
     "-b", Arg.String ((:=) show_back), help_b;
     "-c", Arg.Set show_check, help_c;
     "-d", Arg.Int ((:=) debug), help_d;
+    "-i", Arg.String set_iset, help_i;
     "-l", Arg.Set show_leaf, help_l;
     "-t", Arg.Set show_top, help_t;
   ] process_file help;
-  try read stdin with End_of_file -> show ()
+  show ()