Proofrecording/diffs/depgraph.ml

   1 module Label = struct
   2
   3   type t = string
   4
   5   let compare = String.compare
   6
   7   let hash s =
   8     let n = String.length s in
   9     let p = 9 in
  10     if n >= p then
  11       try
  12         int_of_string (String.sub s p (n-p))
  13       with | Failure _ -> n
  14     else
  15       n
  16
  17   let equal a b = a = b
  18
  19 end
  20
  21
  22 module Dep = struct
  23
  24   include Graph.Imperative.Digraph.ConcreteBidirectional(Label)
  25
  26   let graph_attributes _ = []
  27
  28   let default_vertex_attributes _ = []
  29
  30   let vertex_name v = V.label v
  31
  32   let vertex_attributes _ = []
  33
  34   let get_subgraph _ = None
  35
  36   let default_edge_attributes _ = []
  37
  38   let edge_attributes _ = []
  39
  40   let add_thm dep thm = add_vertex dep (V.create thm)
  41
  42   let add_dep dep thm1 thm2 =
  43     let v1 = V.create thm1 in
  44     let v2 = V.create thm2 in
  45     if ((mem_vertex dep v1) && (mem_vertex dep v2)) then
  46       add_edge dep v1 v2
  47
  48   let min_max_moy_in_deg dep =
  49     let max = ref 0 in
  50     let lab_max = ref "" in
  51     let min = ref 1073741823 in
  52     let lab_min = ref "" in
  53     let nb = ref 0 in
  54     let sum = ref 0 in
  55     let calc v =
  56       let deg = in_degree dep v in
  57       if deg < !min then (
  58         min := deg;
  59         lab_min := V.label v
  60       );
  61       if deg > !max then (
  62         max := deg;
  63         lab_max := V.label v
  64       );
  65       incr nb;
  66       sum := !sum + deg in
  67     iter_vertex calc dep;
  68     let moy = (float_of_int !sum) /. (float_of_int !nb) in
  69     (!min, !lab_min, !max, !lab_max, moy)
  70
  71   let min_max_moy_out_deg dep =
  72     let max = ref 0 in
  73     let lab_max = ref "" in
  74     let min = ref 1073741823 in
  75     let lab_min = ref "" in
  76     let nb = ref 0 in
  77     let sum = ref 0 in
  78     let calc v =
  79       let deg = out_degree dep v in
  80       if deg < !min then (
  81         min := deg;
  82         lab_min := V.label v
  83       );
  84       if deg > !max then (
  85         max := deg;
  86         lab_max := V.label v
  87       );
  88       incr nb;
  89       sum := !sum + deg in
  90     iter_vertex calc dep;
  91     let moy = (float_of_int !sum) /. (float_of_int !nb) in
  92     (!min, !lab_min, !max, !lab_max, moy)
  93
  94 end
  95
  96
  97 module Dep_top = struct
  98
  99   include Graph.Topological.Make(Dep)
 100
 101   let iter_top f dep = iter (fun v -> f (Dep.V.label v)) dep
 102
 103 end
 104
 105
 106 module Dep_dot = struct
 107
 108   include Graph.Graphviz.Dot(Dep)
 109
 110   let output_dot name dep =
 111     let file = open_out name in
 112     output_graph file dep;
 113     close_out file
 114
 115 end