helm/software/matita/contribs/formal_topology/bin/comb.ml

   1 (* 0: 7
   2    1: 29      6
   3    2: 120    10
   4    3: > 327  >9
   5    4: ???
   6 *)
   7
   8 type t = M | I | C
   9 type w = t list
  10 type eqclass = w list
  11
  12 type dir = Le | Ge
  13
  14 let rules =
  15  [ [I],     Le, [];
  16    [C],     Ge, [];
  17    [I;I],   Ge, [I];
  18    [C;C],   Le, [C];
  19    [I],     Le, [I];
  20    [I],     Ge, [I];
  21    [C],     Le, [C];
  22    [C],     Ge, [C];
  23    [C;M],   Le, [M;I];
  24    [C;M;I], Le, [M;I];  (* ??? *)
  25    [I;M],   Le, [M;C];
  26    [I;M;C], Ge, [I;M];  (* ??? *)
  27    [M;M;M], Ge, [M];
  28    [M;M],   Ge, [];
  29    [M],     Le, [M];
  30    [M],     Ge, [M];
  31    (* classical
  32    [M;M],   Le, [];
  33    [C;M],   Ge, [M;I];
  34    *)
  35  ]
  36 ;;
  37
  38 let inject =
  39  function w ->
  40   let rec aux acc =
  41    function
  42       [] -> acc
  43     | he::tl -> aux (4 * acc + (match he with I -> 1 | C -> 2 | M -> 3)) tl
  44   in
  45    0, aux 0 w, w
  46 ;;
  47
  48 module V =
  49  struct
  50   type t = int * int * w
  51   let compare (h1,l1,_) (h2,l2,_) = compare (h1,l1) (h2,l2)
  52   let hash (_,l,_) = l
  53   let equal ((h1 : int),(l1 : int),_) (h2,l2,_) = l1=l2 && h1=h2
  54  end
  55
  56 module G = Graph.Imperative.Digraph.Concrete(V);;
  57
  58 module VL =
  59  struct
  60   type t = eqclass
  61   let compare = compare
  62   let hash = Hashtbl.hash
  63   let equal = (=)
  64  end
  65
  66 module GL = Graph.Imperative.Digraph.Concrete(VL);;
  67
  68 let swap = function Le -> Ge | Ge -> Le;;
  69
  70 let rec new_dir dir =
  71  function
  72     [] -> dir
  73   | M::tl -> new_dir (swap dir) tl
  74   | (C|I)::tl -> new_dir dir tl
  75 ;;
  76
  77 let string_of_w w =
  78  String.concat ""
  79   (List.map (function I -> "i" | C -> "c" | M -> "-") w)
  80 ;;
  81
  82 let string_of_w' w =
  83  String.concat ""
  84   (List.map (function I -> "i" | C -> "c" | M -> "m") w)
  85 ;;
  86
  87 let string_of_eqclass l =
  88  let s = String.concat "=" (List.map string_of_w l) in
  89   if s = "" then "." else s
  90 ;;
  91
  92 let name_of_eqclass l =
  93  let s = String.concat "_" (List.map string_of_w' l) in
  94   if s = "" then "E" else s
  95 ;;
  96
  97 exception NoMatch;;
  98
  99 let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2;;
 100
 101 let uniq l =
 102  let rec aux acc = function
 103   | [] -> acc
 104   | h::[] -> h::acc
 105   | h1::h2::tl when h1=h2 -> aux (h2::acc) tl
 106   | h1::tl (* when h1 <> h2 *) -> aux (h1::acc) tl
 107  in
 108   List.rev (aux [] (List.sort compare l))
 109 ;;
 110
 111 let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) =
 112  if dir <> dir' then
 113   raise NoMatch
 114  else
 115   let rec aux =
 116    function
 117       [],w -> w
 118     | x::lhs,x'::w when x = x' -> aux (lhs,w)
 119     | _,_ -> raise NoMatch
 120   in
 121    rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs)
 122 and apply_rules (w,_ as w_and_dir) =
 123  if w = [] then [[]]
 124  else
 125   let rec aux =
 126    function
 127       [] -> []
 128     | rule::tl ->
 129        (try apply_rule_at_beginning rule w_and_dir
 130         with NoMatch -> [])
 131        @
 132        aux tl
 133   in
 134    aux rules
 135 ;;
 136
 137 let apply_rules (w,dir as w_and_dir) =
 138  List.map (fun w' -> w,dir,w')
 139   (uniq (apply_rules w_and_dir))
 140 ;;
 141
 142 let step (l : w list) =
 143  uniq
 144   (List.flatten
 145     (List.map
 146      (function w ->
 147        List.map (fun x -> x@w)
 148        (if List.length (List.filter (fun w -> w = M) w) >= 3 then
 149          [[I];[C];[]]
 150         else
 151          [[I];[C];[M];[]])
 152      ) l))
 153 ;;
 154
 155 let mapi f l =
 156  let rec aux acc i =
 157   function
 158      [] -> acc
 159    | he::tl ->
 160       if i mod 1000 = 0 then
 161        begin
 162         print_string ("@" ^ string_of_int i ^ " ");
 163         flush stdout;
 164        end;
 165       aux (f he :: acc) (i+1) tl
 166  in
 167   let res = List.rev (aux [] 1 l) in
 168    print_newline ();
 169    res
 170 ;;
 171
 172 let iteri f l =
 173  let rec aux i =
 174   function
 175      [] -> ()
 176    | he::tl ->
 177       if i mod 1000 = 0 then
 178        begin
 179         print_string ("@" ^ string_of_int i ^ " ");
 180         flush stdout;
 181        end;
 182       f he; aux (i+1) tl
 183  in
 184   aux 1 l;
 185   print_newline ();
 186 ;;
 187
 188 let normalize (l : w list) =
 189  print_endline (string_of_int (List.length l) ^ " nodes to be normalized");
 190  let rels =
 191   List.flatten
 192    (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in
 193  let arcs =
 194   mapi
 195    (function (x,rel,y) ->
 196      let x = inject x in
 197      let y = inject y in
 198       match rel with Le -> x,y | Ge -> y,x) rels
 199  in
 200   uniq arcs
 201 ;;
 202
 203 let visualize graph =
 204  let module GL =
 205   struct
 206    include GL;;
 207    let edge_attributes _ = []
 208    let default_edge_attributes _ = []
 209    let get_subgraph _ = None
 210    let vertex_attributes v = [`Label (string_of_eqclass (GL.V.label v))]
 211    let vertex_name v = name_of_eqclass (GL.V.label v)
 212    let default_vertex_attributes _ = []
 213    let graph_attributes _ = []
 214   end in
 215  let module D = Graph.Graphviz.Dot(GL) in
 216   let ch = open_out "/tmp/comb.dot" in
 217    D.output_graph ch graph;
 218    close_out ch;
 219    ignore (Unix.system ("tred /tmp/comb.dot > /tmp/red.dot"));
 220    ignore (Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps"));
 221    (*Unix.system ("ggv /tmp/red.ps");*)
 222 ;;
 223
 224 let w_compare s1 s2 =
 225  let c = compare (List.length s1) (List.length s2) in
 226   if c = 0 then compare s1 s2 else c
 227 ;;
 228
 229 let normalize_and_describe norm =
 230  let cache = Hashtbl.create 5393 in
 231  let canonicals = Hashtbl.create 5393 in
 232  let descriptions = Hashtbl.create 5393 in
 233   (function v ->
 234     let normalized = norm v in
 235     let _,_,dsc = G.V.label v in
 236      if not (List.mem dsc (Hashtbl.find_all cache normalized)) then
 237       Hashtbl.add cache normalized dsc;
 238      normalized),
 239   (function () ->
 240     let vertexes = uniq (Hashtbl.fold (fun k _ l -> k::l) cache []) in
 241     let xx =
 242      mapi
 243       (fun v -> v, List.sort w_compare (Hashtbl.find_all cache v)) vertexes in
 244     iteri (function (_,w::_) -> Hashtbl.add canonicals w () | _ -> ()) xx;
 245     let is_not_redundant =
 246      function
 247         [] | [_] -> true
 248       | _::w ->
 249         try Hashtbl.find canonicals w; true with Not_found -> false
 250     in
 251      iteri
 252       (function (v,x) ->
 253         Hashtbl.add descriptions v ((List.filter is_not_redundant x) : eqclass)) xx),
 254   Hashtbl.find descriptions
 255 ;;
 256
 257 let classify arcs =
 258  print_endline (string_of_int (List.length arcs) ^ " arcs to be classified");
 259  let graph = G.create () in
 260  iteri (fun (x,y) -> G.add_edge graph x y) arcs;
 261  print_endline ("<scc>");
 262  let classes,norm =
 263   let module SCC = Graph.Components.Make(G) in SCC.scc graph in
 264  print_endline (string_of_int classes ^ " classes");
 265  print_endline ("-----");
 266  norm,arcs
 267 ;;
 268
 269 let analyze (norm,arcs) =
 270  print_endline ("building class graph (" ^ string_of_int (List.length arcs) ^ ")");
 271  let normalize,finish,describe = normalize_and_describe norm in
 272  let arcs = uniq (mapi (fun (x,y) -> normalize x,normalize y) arcs) in
 273  print_endline "finish";
 274  finish ();
 275  print_endline ("collapse " ^ string_of_int (List.length arcs) ^ " arcs");
 276  let arcs = uniq (mapi (function (x,y) -> describe x,describe y) arcs) in
 277  print_endline ("build (" ^ string_of_int (List.length arcs) ^ " arcs)");
 278  let cgraph = GL.create () in
 279  iteri (function (x,y) -> if x <> y then GL.add_edge cgraph x y) arcs;
 280  print_endline "visualize";
 281  visualize cgraph;
 282  print_endline ("/////");
 283 ;;
 284
 285 let rec iter n l =
 286  print_endline ("STEP " ^ string_of_int n);
 287  let pkg = classify (normalize l) in
 288  if n > 0 then
 289   iter (n - 1) (step l)
 290  else
 291   analyze pkg
 292 in
 293  iter 15 [[]]
 294 ;;