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

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