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