X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatitadep%2Fmatitadep.ml;h=d21af12a3fd635320655f2c6a7e1bf9d832ef161;hb=a454837a256907d2f83d42ced7be847e10361ea9;hp=0415a5111f1b02821ad8612d68dc1f43997e4fa8;hpb=a8c3c72dc1776997c1ce6deae88c9aa9abbf7766;p=helm.git diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml index 0415a5111..d21af12a3 100644 --- a/matita/components/binaries/matitadep/matitadep.ml +++ b/matita/components/binaries/matitadep/matitadep.ml @@ -1,74 +1,133 @@ -module StringSet = Set.Make (String) +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 - Hashtbl.add graph fname {ddeps = []; rdeps = None} + if fname = "" then () else + if Hashtbl.mem graph fname then () else + Hashtbl.add graph fname {ddeps = []; rdeps = None} let add_ddep fname dname = - let file = Hashtbl.find graph fname in - Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps} + if dname = "" then () else + let file = Hashtbl.find graph fname in + Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps} let init fname dname = - add fname; add dname; add_ddep fname dname - -let rec compute bdeps 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}; - 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 - 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) - -let check () = - let iter fname file = ignore (compute [] fname file) in - Hashtbl.iter iter graph + if !debug land 1 > 0 then Printf.eprintf "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 + +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) + +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_from_file [] fname file) in + Hashtbl.iter iter graph let get_unions () = - let map1 ddeps dname = StringSet.add dname ddeps in - let map2 fname file (fnames, ddeps) = - StringSet.add fname fnames, List.fold_left map1 ddeps file.ddeps - in - Hashtbl.fold map2 graph (StringSet.empty, StringSet.empty) + let map1 ddeps dname = StringSet.add dname ddeps in + let map2 fname file (fnames, ddeps) = + StringSet.add fname fnames, List.fold_left map1 ddeps file.ddeps + 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 fnames, ddeps = get_unions () in - StringSet.iter iter (StringSet.diff fnames ddeps) - -let rec read ich = - let _ = Scanf.sscanf (input_line ich) "%s@:include \"%s@\"." init in - read ich - + 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 back fname = + Printf.printf "backward: %s\n" fname; + try match (Hashtbl.find graph fname).rdeps with + | None -> () + | Some rdeps -> + let iter fname = Printf.printf "%s\n" fname in + StringSet.iter iter rdeps + with Not_found -> () + +let rec read ich = + 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 _ -> + begin try Scanf.sscanf line "%s@:(*%s@*)" (fun _ _ -> ()) + with Scanf.Scan_failure _ -> + Printf.eprintf "unknown line: %s.\n" line + end + end + end; + read ich + let _ = - let show_top = ref false in - let process_file name = () in - let help = "" in - let help_t = " Print the top nodes of the dependences graph" in - Arg.parse [ - "-t", Arg.Set show_top, help_t; - ] process_file help; - try read stdin with End_of_file -> - if !show_top then top () else check () + 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 show () = + if !show_check 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 | -b ] < " in + let help_b = " Print the backward dependences of this node" in + let help_c = " Print the redundant and looping arcs of the dependences graph" in + let help_d = " 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 [ + "-b", Arg.String ((:=) show_back), help_b; + "-c", Arg.Set show_check, help_c; + "-d", Arg.Int ((:=) debug), 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 -> show ()