From 1654d0ad0d8ba9e03ab403b59fd0893ed8ebd4f6 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 2 Mar 2009 23:36:26 +0000
Subject: [PATCH] New version.

---
 .../contribs/formal_topology/bin/comb.ml      | 99 ++++++++++---------
 1 file changed, 55 insertions(+), 44 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 19874951b..2f4d46fca 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -1,7 +1,7 @@
 (* 0: 7
-   1: 29      6?
+   1: 29      6
    2: 120    10
-   3: > 319
+   3: > 327  >9
    4: ???
 *)
 
@@ -35,8 +35,35 @@ let rules =
  ]
 ;;
 
-module V = struct type t = eqclass end;;
-module G = Graph.Imperative.Digraph.Abstract(V);;
+let inject =
+ function w ->
+  let rec aux acc =
+   function
+      [] -> acc
+    | he::tl -> aux (4 * acc + (match he with I -> 1 | C -> 2 | M -> 3)) tl
+  in
+   0, aux 0 w, w
+;;
+
+module V =
+ struct
+  type t = int * int * w
+  let compare (h1,l1,_) (h2,l2,_) = compare (h1,l1) (h2,l2)
+  let hash (_,l,_) = l
+  let equal ((h1 : int),(l1 : int),_) (h2,l2,_) = l1=l2 && h1=h2
+ end
+
+module G = Graph.Imperative.Digraph.Concrete(V);;
+
+module VL =
+ struct
+  type t = eqclass
+  let compare = compare
+  let hash = Hashtbl.hash
+  let equal = (=)
+ end
+
+module GL = Graph.Imperative.Digraph.Concrete(VL);;
 
 let swap = function Le -> Ge | Ge -> Le;;
 
@@ -118,7 +145,7 @@ let step (l : w list) =
     (List.map
      (function w ->
        List.map (fun x -> x@w)
-       (if List.length (List.filter (fun w -> w = M) w) >= 2 then
+       (if List.length (List.filter (fun w -> w = M) w) >= 3 then
          [[I];[C];[]]
         else
          [[I];[C];[M];[]])
@@ -164,25 +191,28 @@ let normalize (l : w list) =
   List.flatten
    (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in
  let arcs =
-  List.rev (List.rev_map
-   (function (x,rel,y) -> match rel with Le -> [x],[y] | Ge -> [y],[x]) rels) in
- let res = uniq arcs in
- res
+  mapi
+   (function (x,rel,y) ->
+     let x = inject x in
+     let y = inject y in
+      match rel with Le -> x,y | Ge -> y,x) rels
+ in
+  uniq arcs
 ;;
 
 let visualize graph =
- let module G =
+ let module GL =
   struct
-   include G;;
+   include GL;;
    let edge_attributes _ = []
    let default_edge_attributes _ = []
    let get_subgraph _ = None
-   let vertex_attributes v = [`Label (string_of_eqclass (G.V.label v))]
-   let vertex_name v = name_of_eqclass (G.V.label v)
+   let vertex_attributes v = [`Label (string_of_eqclass (GL.V.label v))]
+   let vertex_name v = name_of_eqclass (GL.V.label v)
    let default_vertex_attributes _ = []
    let graph_attributes _ = []
   end in
- let module D = Graph.Graphviz.Dot(G) in
+ let module D = Graph.Graphviz.Dot(GL) in
   let ch = open_out "/tmp/comb.dot" in
    D.output_graph ch graph;
    close_out ch;
@@ -191,18 +221,6 @@ let visualize graph =
    (*Unix.system ("ggv /tmp/red.ps");*)
 ;;
 
-let mk_vertex () =
- let cache1 = Hashtbl.create 5393 in
- (function w ->
-   try
-    Hashtbl.find cache1 w
-   with
-    Not_found ->
-      let v = G.V.create w in
-       Hashtbl.add cache1 w v;
-       v)
-;;
-
 let w_compare s1 s2 =
  let c = compare (List.length s1) (List.length s2) in
   if c = 0 then compare s1 s2 else c
@@ -214,11 +232,7 @@ let normalize_and_describe norm =
  let descriptions = Hashtbl.create 5393 in
   (function v ->
     let normalized = norm v in
-    let dsc =
-     match G.V.label v with
-        [d] -> d
-      | _ -> assert false
-    in
+    let _,_,dsc = G.V.label v in
      if not (List.mem dsc (Hashtbl.find_all cache normalized)) then
       Hashtbl.add cache normalized dsc;
      normalized),
@@ -242,42 +256,39 @@ let normalize_and_describe norm =
 
 let classify arcs =
  print_endline (string_of_int (List.length arcs) ^ " arcs to be classified");
- let mk_vertex = mk_vertex () in
  let graph = G.create () in
- let varcs = mapi (fun (x,y) -> mk_vertex x,mk_vertex y) arcs in
- iteri (fun (x,y) -> G.add_edge graph x y) varcs;
+ iteri (fun (x,y) -> G.add_edge graph x y) arcs;
  print_endline ("<scc>");
  let classes,norm =
   let module SCC = Graph.Components.Make(G) in SCC.scc graph in
  print_endline (string_of_int classes ^ " classes");
  print_endline ("-----");
- norm,varcs
+ norm,arcs
 ;;
 
 let analyze (norm,arcs) =
  print_endline ("building class graph (" ^ string_of_int (List.length arcs) ^ ")");
  let normalize,finish,describe = normalize_and_describe norm in
- let arcs =
-  uniq (mapi (fun (x,y) -> normalize x,normalize y) arcs) in
+ let arcs = uniq (mapi (fun (x,y) -> normalize x,normalize y) arcs) in
  print_endline "finish";
  finish ();
- let cgraph = G.create () in
- let mk_vertex = mk_vertex () in
- List.iter
-  (function (x,y) ->
-    if x <> y then
-     G.add_edge cgraph (mk_vertex (describe x)) (mk_vertex (describe y))) arcs;
+ print_endline ("collapse " ^ string_of_int (List.length arcs) ^ " arcs");
+ let arcs = uniq (mapi (function (x,y) -> describe x,describe y) arcs) in
+ print_endline ("build (" ^ string_of_int (List.length arcs) ^ " arcs)");
+ let cgraph = GL.create () in
+ iteri (function (x,y) -> if x <> y then GL.add_edge cgraph x y) arcs;
  print_endline "visualize";
  visualize cgraph;
  print_endline ("/////");
 ;;
 
 let rec iter n l =
+ print_endline ("STEP " ^ string_of_int n);
  let pkg = classify (normalize l) in
  if n > 0 then
   iter (n - 1) (step l)
  else
   analyze pkg
 in
- iter 10 [[]]
+ iter 15 [[]]
 ;;
-- 
2.39.2