From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 2 Mar 2009 23:35:31 +0000 (+0000)
Subject: New version.
X-Git-Tag: make_still_working~4178
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=79a489c46c77de80979d68a512d1f640f8273f9e;p=helm.git

New version.
---

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 7c7cd3ecd..59807ed69 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -33,31 +33,23 @@ let rec new_dir dir =
   | (C|I)::tl -> new_dir dir tl
 ;;
 
-let string_of_dir = function Le -> "<=" | Ge -> ">=";;
-
 let string_of_w w =
  String.concat ""
   (List.map (function I -> "i" | C -> "c" | M -> "-") w)
 ;;
 
-let string_of_eqclass eqc =
- let eqc = List.sort compare eqc in
-  String.concat "=" (List.map string_of_w eqc)
-;;
-
-let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));;
-
 exception NoMatch;;
 
 let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2;;
 
 let uniq l =
- let rec aux l =
-  function
-     [] -> l
-   | he::tl -> aux (if List.mem he l then l else he::l) tl
+ let rec aux acc = function
+  | [] -> acc
+  | h::[] -> h::acc
+  | h1::h2::tl when h1=h2 -> aux (h2::acc) tl
+  | h1::tl (* when h1 <> h2 *) -> aux (h1::acc) tl
  in
-  aux [] l
+  List.rev (aux [] (List.sort compare l))
 ;;
 
 let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) =
@@ -97,110 +89,152 @@ let step (l : w list) =
     (List.map
      (function w ->
        List.map (fun x -> x@w)
-       (if List.mem M w then
+       (if List.length (List.filter (fun w -> w = M) w) >= 2 then
          [[I];[C];[]]
         else
-         [[I];[C](*;[M]*);[]])
+         [[I];[C];[M];[]])
      ) l))
 ;;
 
-let leq rels x y =
- let rec aux avoid x y =
-  x = y ||
-   List.exists
-    (fun (x',z) -> x=x' && not (List.mem z avoid) && aux (z::avoid) z y) rels
- in
-  aux [x] x y
-;;
-
-let in_class rels eqc he =
- match eqc with
-    [] -> assert false
-  | k::_ -> leq rels k he && leq rels he k
-;;
-
-let add_class rels classes he =
-prerr_endline "Add";
- let rec aux visited =
+let mapi f l =
+ let rec aux acc i =
   function
-     [] -> [he]::visited
-   | eqc::tl ->
-      if in_class rels eqc he then
-       (he::eqc)::tl@visited
-      else
-       aux (eqc::visited) tl
+     [] -> acc
+   | he::tl -> aux (f i he :: acc) (i+1) tl
  in
-  aux [] classes
+  List.rev (aux [] 1 l)
 ;;
 
-let classify (l : w list) =
-prerr_endline ("Classify: " ^ string_of_int (List.length l));
+let normalize (l : w list) =
+ print_endline (string_of_int (List.length l) ^ " nodes to be normalized");
  let rels =
-  List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
- in
-  uniq
-   (List.map
-    (function (x,rel,y) -> match rel with Le -> x,y | Ge -> y,x) 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 ();
+ 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
 ;;
 
-let visualize graph =
-  let dot = "" in
-  (*Graph.Pack.Digraph.dot_output graph dot;*)
-  Graph.Pack.Digraph.display_with_gv graph;
-exit 1;
-(*
+let visualize describe graph =
+ let module G =
+  struct
+   include Graph.Pack.Digraph;;
+   let edge_attributes _ = []
+   let default_edge_attributes _ = []
+   let get_subgraph _ = None
+   let vertex_attributes v = [`Label (describe (Graph.Pack.Digraph.V.label v))]
+   let vertex_name v = "v" ^ string_of_int (Graph.Pack.Digraph.V.label v)
+   let default_vertex_attributes _ = []
+   let graph_attributes _ = []
+  end in
+ let module D = Graph.Graphviz.Dot(G) in
   let ch = open_out "/tmp/comb.dot" in
-   output_string ch dot;
+   D.output_graph ch graph;
    close_out ch;
-   Unix.system ("tred /tmp/comb.dot > /tmp/red.dot");
-   Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps");
-   Unix.system ("ggv /tmp/red.ps");
-*) ()
-;;
-
-let analyze arcs =
- let mk_vertex =
-  let cache = ref [] in
-  function w ->
-   try
-    List.assoc w !cache
-   with
-    Not_found ->
-     let n =
-      let rec aux acc =
-       function
-          [] -> acc
-        | he::tl -> aux (acc * 4 + (match he with I -> 1 | C -> 2 | M -> 3)) tl
+   ignore (Unix.system ("tred /tmp/comb.dot > /tmp/red.dot"));
+   ignore (Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps"));
+   (*Unix.system ("ggv /tmp/red.ps");*)
+;;
+
+let mk_vertex_and_dsc_vertex =
+ function () ->
+  let cache1 = Hashtbl.create 37 in
+  let cache2 = Hashtbl.create 37 in
+  (function w ->
+    try
+     Hashtbl.find cache1 w
+    with
+     Not_found ->
+      let n =
+       let rec aux acc =
+        function
+           [] -> acc
+         | he::tl -> aux (acc * 4 + (match he with I -> 1 | C -> 2 | M -> 3)) tl
+       in
+        aux 0 w
       in
-       aux 0 w
-     in
-prerr_endline (string_of_w w ^ " => " ^ string_of_int n);
-      let v = Graph.Pack.Digraph.V.create n in
-       cache := (w,v)::!cache;
-       v in
+       let v = Graph.Pack.Digraph.V.create n in
+        Hashtbl.add cache1 w v;
+        Hashtbl.add cache2 v w;
+        v),
+   (Hashtbl.find cache2)
+;;
+
+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
+  (function n ->
+    let v = mk_vertex n in
+    let normalized = norm v in
+    let dsc = dsc_vertex v in
+     if not (List.mem dsc (Hashtbl.find_all cache normalized)) then
+      Hashtbl.add cache normalized dsc;
+     normalized),
+  (function v ->
+    let vertexes = uniq (Hashtbl.fold (fun k _ l -> k::l) cache []) in
+    let ll =
+     List.map
+      (fun v ->
+        v,
+         List.sort string_compare
+          (List.map string_of_w (Hashtbl.find_all cache v))
+      ) vertexes in
+    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)
+    in
+    let l = List.filter is_not_redundant (List.assoc v ll) in
+    let s = String.concat "=" l in
+     if s = "" then "." else s)
+;;
+
+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) ->
     Graph.Pack.Digraph.add_edge graph (mk_vertex x) (mk_vertex y)) arcs;
-prerr_endline ("<CLASSI>");
- let classes =  Graph.Pack.Digraph.Components.scc_list graph in
-List.iter (function l -> prerr_endline (String.concat "=" (List.map string_of_int (List.map Graph.Pack.Digraph.V.label l)))) classes;
-prerr_endline ("</CLASSI>");
- let classes,normalize =  Graph.Pack.Digraph.Components.scc graph in
-prerr_endline (string_of_int classes ^ " CLASSI");
- let arcs = uniq (List.map (fun (x,y) -> normalize (mk_vertex x),normalize (mk_vertex y)) arcs) in
+ print_endline ("<scc>");
+ let classes,norm =  Graph.Pack.Digraph.Components.scc graph in
+ print_endline (string_of_int classes ^ " classes");
+ 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
  let cgraph = Graph.Pack.Digraph.create () in
  List.iter
   (function (x,y) ->
-    Graph.Pack.Digraph.add_edge cgraph (Graph.Pack.Digraph.V.create x) (Graph.Pack.Digraph.V.create y)) arcs;
- visualize cgraph
+    if x <> y then
+     Graph.Pack.Digraph.add_edge cgraph (Graph.Pack.Digraph.V.create x
+  ) (Graph.Pack.Digraph.V.create y)) arcs;
+ print_endline "visualize";
+ visualize describe cgraph;
+ print_endline ("-----");
 ;;
 
 let rec iter n l =
- let arcs = analyze (classify l) in
- (*print_graph' (analyze arcs);*)
+ let pkg = classify (normalize l) in
  if n > 0 then
   iter (n - 1) (step l)
+ else
+  analyze pkg
 in
- iter 4 [[]]
+ iter 10 [[]]
 ;;