- lambdadelta: tentative definition of lazy equivalence for closures +

[helm.git] / matita / components / binaries / matitadep / matitadep.ml

diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml
index 0415a5111f1b02821ad8612d68dc1f43997e4fa8..4e0651be4e19541e473b1c11db3b3bb3ac0de09a 100644 (file)
--- a/matita/components/binaries/matitadep/matitadep.ml
+++ b/matita/components/binaries/matitadep/matitadep.ml
@@ -1,15 +1,17 @@
 module StringSet = Set.Make (String) 
 
 type file = {
-   ddeps: string list;
-   rdeps: StringSet.t option
+   ddeps: string list;        (* direct dependences *)
+   rdeps: StringSet.t option  (* recursive dependences *)
 }
 
 let graph = Hashtbl.create 503
 
-let rec purge dname bdeps = match bdeps with
-   | []       -> bdeps
-   | hd :: tl -> if hd = dname then bdeps else purge dname tl 
+let debug = ref 0
+
+let rec purge dname vdeps = match vdeps with
+   | []       -> vdeps
+   | hd :: tl -> if hd = dname then tl else hd :: purge dname tl 
 
 let add fname =
    if Hashtbl.mem graph fname then () else
@@ -20,30 +22,39 @@ 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;
    add fname; add dname; add_ddep fname dname 
 
-let rec compute bdeps fname file = match file.rdeps with
+(* vdeps: visited dependences for loop detection *)
+let rec compute_from_file vdeps fname file = match file.rdeps with
    | Some rdeps -> rdeps
-   | None       ->
-      let bdeps = fname :: bdeps in
-      let rdeps = List.fold_left (iter fname bdeps) StringSet.empty file.ddeps in
-      Hashtbl.replace graph fname {file with rdeps = Some 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
 
-and iter fname bdeps rdeps dname =
-   if StringSet.mem dname rdeps then begin
-      Printf.printf "%s: redundant %s\n" fname dname;
-      rdeps 
-   end else if List.mem dname bdeps then begin
-      let loop = purge dname (List.rev bdeps) in
+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 bdeps dname file) rdeps)
+     StringSet.add dname (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
 
 let check () = 
-   let iter fname file = ignore (compute [] fname file) in
+   let iter fname file = ignore (compute_from_file [] fname file) in
    Hashtbl.iter iter graph 
 
 let get_unions () =
@@ -53,22 +64,45 @@ let get_unions () =
    in
    Hashtbl.fold map2 graph (StringSet.empty, StringSet.empty)
 
+let get_leafs () =
+   let map fname file fnames =
+      if file.ddeps = [] then StringSet.add fname fnames else fnames
+   in
+   Hashtbl.fold map graph StringSet.empty
+
 let top () =
-   let iter dname = Printf.printf "top: %s\n" dname in
+   let iter fname = Printf.printf "top: %s\n" fname in
    let fnames, ddeps = get_unions () in
    StringSet.iter iter (StringSet.diff fnames ddeps) 
 
+let leaf () =
+   let iter fname = Printf.printf "leaf: %s\n" fname in
+   let fnames = get_leafs () in
+   StringSet.iter iter fnames
+
 let rec read ich = 
    let _ = Scanf.sscanf (input_line ich) "%s@:include \"%s@\"." init in
    read ich
    
 let _ =
+   let show_check = ref false in
    let show_top = ref false in
+   let show_leaf = ref false in   
    let process_file name = () in
+   let show () =
+      if !show_check then check ();
+      if !show_top then top ();
+      if !show_leaf then leaf ()   
+   in
    let help   = "" 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_l = " Print the leaf nodes of the dependences graph" in
    let help_t = " Print the top nodes of the dependences graph" in
    Arg.parse [
+      "-c", Arg.Set show_check, help_c;
+      "-d", Arg.Int (fun x -> debug := x), help_d;
+      "-l", Arg.Set show_leaf, help_l;
       "-t", Arg.Set show_top, help_t;
    ] process_file help;
-   try read stdin with End_of_file ->
-   if !show_top then top () else check ()
+   try read stdin with End_of_file -> show ()