matita/components/binaries/matitadep/matitadep.ml

   1 module StringSet = Set.Make (String)
   2
   3 type file = {
   4    ddeps: string list;
   5    rdeps: StringSet.t option
   6 }
   7
   8 let graph = Hashtbl.create 503
   9
  10 let rec purge dname bdeps = match bdeps with
  11    | []       -> bdeps
  12    | hd :: tl -> if hd = dname then bdeps else purge dname tl
  13
  14 let add fname =
  15    if Hashtbl.mem graph fname then () else
  16    Hashtbl.add graph fname {ddeps = []; rdeps = None}
  17
  18 let add_ddep fname dname =
  19    let file = Hashtbl.find graph fname in
  20    Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps}
  21
  22 let init fname dname =
  23    add fname; add dname; add_ddep fname dname
  24
  25 let rec compute bdeps fname file = match file.rdeps with
  26    | Some rdeps -> rdeps
  27    | None       ->
  28       let bdeps = fname :: bdeps in
  29       let rdeps = List.fold_left (iter fname bdeps) StringSet.empty file.ddeps in
  30       Hashtbl.replace graph fname {file with rdeps = Some rdeps};
  31       rdeps
  32
  33 and iter fname bdeps rdeps dname =
  34    if StringSet.mem dname rdeps then begin
  35       Printf.printf "%s: redundant %s\n" fname dname;
  36       rdeps
  37    end else if List.mem dname bdeps then begin
  38       let loop = purge dname (List.rev bdeps) in
  39       Printf.printf "circular: %s\n" (String.concat " " loop);
  40       StringSet.add dname rdeps
  41    end else
  42      let file = Hashtbl.find graph dname in
  43      StringSet.add dname (StringSet.union (compute bdeps dname file) rdeps)
  44
  45 let check () =
  46    let iter fname file = ignore (compute [] fname file) in
  47    Hashtbl.iter iter graph
  48
  49 let get_unions () =
  50    let map1 ddeps dname = StringSet.add dname ddeps in
  51    let map2 fname file (fnames, ddeps) =
  52       StringSet.add fname fnames, List.fold_left map1 ddeps file.ddeps
  53    in
  54    Hashtbl.fold map2 graph (StringSet.empty, StringSet.empty)
  55
  56 let top () =
  57    let iter dname = Printf.printf "top: %s\n" dname in
  58    let fnames, ddeps = get_unions () in
  59    StringSet.iter iter (StringSet.diff fnames ddeps)
  60
  61 let rec read ich =
  62    let _ = Scanf.sscanf (input_line ich) "%s@:include \"%s@\"." init in
  63    read ich
  64
  65 let _ =
  66    let show_top = ref false in
  67    let process_file name = () in
  68    let help   = "" in
  69    let help_t = " Print the top nodes of the dependences graph" in
  70    Arg.parse [
  71       "-t", Arg.Set show_top, help_t;
  72    ] process_file help;
  73    try read stdin with End_of_file ->
  74    if !show_top then top () else check ()