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

---
 .../contribs/formal_topology/bin/comb.ml      | 98 ++++++++++++++-----
 1 file changed, 73 insertions(+), 25 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 59807ed69..e0c58dec0 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -21,6 +21,10 @@ let rules =
    [M;M],   Ge, [];
    [M],     Le, [M];
    [M],     Ge, [M];
+   (* classical
+   [M;M],   Le, [];
+   [C;M],   Ge, [M;I];
+   *)
  ]
 ;;
 
@@ -100,20 +104,40 @@ let mapi f l =
  let rec aux acc i =
   function
      [] -> acc
-   | he::tl -> aux (f i he :: acc) (i+1) tl
+   | he::tl ->
+      if i mod 1000 = 0 then
+       begin
+        print_string ("@" ^ string_of_int i ^ " ");
+        flush stdout;
+       end;
+      aux (f he :: acc) (i+1) tl
  in
-  List.rev (aux [] 1 l)
+  let res = List.rev (aux [] 1 l) in
+   print_newline ();
+   res
+;;
+
+let iteri f l =
+ let rec aux i =
+  function
+     [] -> ()
+   | he::tl ->
+      if i mod 1000 = 0 then
+       begin
+        print_string ("@" ^ string_of_int i ^ " ");
+        flush stdout;
+       end;
+      f he; aux (i+1) tl
+ in
+  aux 1 l;
+  print_newline ();
 ;;
 
 let normalize (l : w list) =
  print_endline (string_of_int (List.length l) ^ " nodes to be normalized");
  let rels =
   List.flatten
-   (mapi
-     (fun i x ->
-       if i mod 100 = 0 then print_string ("@" ^ string_of_int i ^ " ");
-        apply_rules (x,Le) @ apply_rules (x,Ge)) l) in
- print_newline ();
+   (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
@@ -144,8 +168,8 @@ let visualize describe graph =
 
 let mk_vertex_and_dsc_vertex =
  function () ->
-  let cache1 = Hashtbl.create 37 in
-  let cache2 = Hashtbl.create 37 in
+  let cache1 = Hashtbl.create 5393 in
+  let cache2 = Hashtbl.create 5393 in
   (function w ->
     try
      Hashtbl.find cache1 w
@@ -166,13 +190,28 @@ let mk_vertex_and_dsc_vertex =
    (Hashtbl.find cache2)
 ;;
 
+let mk_vertex2 =
+ function () ->
+  let cache1 = Hashtbl.create 5393 in
+  function n ->
+   try
+    Hashtbl.find cache1 n
+   with
+    Not_found ->
+     let v = Graph.Pack.Digraph.V.create n in
+      Hashtbl.add cache1 n v;
+      v
+;;
+
 let string_compare s1 s2 =
  let c = compare (String.length s1) (String.length s2) in
   if c = 0 then String.compare s1 s2 else c
 ;;
 
 let normalize_and_describe norm mk_vertex dsc_vertex =
- let cache = Hashtbl.create 37 in
+ let cache = Hashtbl.create 5393 in
+ let canonicals = Hashtbl.create 5393 in
+ let descriptions = Hashtbl.create 5393 in
   (function n ->
     let v = mk_vertex n in
     let normalized = norm v in
@@ -180,53 +219,62 @@ let normalize_and_describe norm mk_vertex dsc_vertex =
      if not (List.mem dsc (Hashtbl.find_all cache normalized)) then
       Hashtbl.add cache normalized dsc;
      normalized),
-  (function v ->
+  (function () ->
     let vertexes = uniq (Hashtbl.fold (fun k _ l -> k::l) cache []) in
-    let ll =
-     List.map
+    let xx =
+     mapi
       (fun v ->
         v,
          List.sort string_compare
           (List.map string_of_w (Hashtbl.find_all cache v))
       ) vertexes in
+    iteri (function (_,w::_) -> Hashtbl.add canonicals w () | _ -> ()) xx;
     let is_not_redundant s =
      let len = String.length s in
       if len <= 1 then true
       else
        let w = String.sub s 1 (len - 1) in
-        List.exists (function w'::_ -> w=w' | [] -> false) (List.map snd ll)
+        try Hashtbl.find canonicals w; true with Not_found -> false
     in
-    let l = List.filter is_not_redundant (List.assoc v ll) in
-    let s = String.concat "=" l in
-     if s = "" then "." else s)
+     iteri
+      (function (v,x) ->
+        Hashtbl.add descriptions v
+         (let s = String.concat "=" (List.filter is_not_redundant x) in
+           if s = "" then "." else s)) xx),
+  Hashtbl.find descriptions
 ;;
 
 let classify arcs =
  print_endline (string_of_int (List.length arcs) ^ " arcs to be classified");
  let mk_vertex,dsc_vertex = mk_vertex_and_dsc_vertex () in
  let graph = Graph.Pack.Digraph.create () in
- List.iter
-  (function (x,y) ->
+ iteri
+  (fun (x,y) ->
     Graph.Pack.Digraph.add_edge graph (mk_vertex x) (mk_vertex y)) arcs;
  print_endline ("<scc>");
  let classes,norm =  Graph.Pack.Digraph.Components.scc graph in
  print_endline (string_of_int classes ^ " classes");
+ print_endline ("-----");
  norm,mk_vertex,dsc_vertex,arcs
 ;;
 
 let analyze (norm,mk_vertex,dsc_vertex,arcs) =
- print_endline "building class graph";
- let normalize,describe = normalize_and_describe norm mk_vertex dsc_vertex in
- let arcs = uniq (List.map (fun (x,y) -> normalize x,normalize y) arcs) in
+ print_endline ("building class graph (" ^ string_of_int (List.length arcs) ^ ")");
+ let normalize,finish,describe =
+  normalize_and_describe norm mk_vertex dsc_vertex in
+ let arcs =
+  uniq (mapi (fun (x,y) -> normalize x,normalize y) arcs) in
  let cgraph = Graph.Pack.Digraph.create () in
+ let mk_vertex2 = mk_vertex2 () in
  List.iter
   (function (x,y) ->
     if x <> y then
-     Graph.Pack.Digraph.add_edge cgraph (Graph.Pack.Digraph.V.create x
-  ) (Graph.Pack.Digraph.V.create y)) arcs;
+     Graph.Pack.Digraph.add_edge cgraph (mk_vertex2 x) (mk_vertex2 y)) arcs;
+ print_endline "finish";
+ finish ();
  print_endline "visualize";
  visualize describe cgraph;
- print_endline ("-----");
+ print_endline ("/////");
 ;;
 
 let rec iter n l =
-- 
2.39.2