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 922d39a7e4f9b21cb325843982010e37aa8a6bbc..7c7cd3ecd94b238ac6a8dbdecd0553963ad2d670 100755 (executable)
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -95,19 +95,20 @@ let step (l : w list) =
  uniq
   (List.flatten
     (List.map
-     (function w -> List.map (fun x -> x@w) [[I];[C];(*[M];*)[]])
-     l))
+     (function w ->
+       List.map (fun x -> x@w)
+       (if List.mem M w then
+         [[I];[C];[]]
+        else
+         [[I];[C](*;[M]*);[]])
+     ) l))
 ;;
 
 let leq rels x y =
  let rec aux avoid x y =
-  x = y
-  || List.exists
-      (fun (x',dir,z) ->
-        x=x' && dir = Le && not (List.mem z avoid) && aux (z::avoid) z y) rels
-  || List.exists
-      (fun (z,dir,x') ->
-        x=x' && dir = Ge && not (List.mem z avoid) && aux (z::avoid) z y) rels
+  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
 ;;
@@ -119,6 +120,7 @@ let in_class rels eqc he =
 ;;
 
 let add_class rels classes he =
+prerr_endline "Add";
  let rec aux visited =
   function
      [] -> [he]::visited
@@ -132,32 +134,71 @@ let add_class rels classes he =
 ;;
 
 let classify (l : w list) =
-(*prerr_endline ("Classify: " ^ string_of_int (List.length l));*)
+prerr_endline ("Classify: " ^ string_of_int (List.length l));
  let rels =
   List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
  in
-  let rec aux classes =
-   function
-      [] -> classes
-    | he::tl -> aux (add_class rels classes he) tl
-  in
-   aux [] l
+  uniq
+   (List.map
+    (function (x,rel,y) -> match rel with Le -> x,y | Ge -> y,x) rels)
 ;;
 
-let print_graph =
- List.iter
-  (function (w,dir,w') ->
-    prerr_endline (string_of_w w ^ string_of_dir dir ^ string_of_w w'))
+let visualize graph =
+  let dot = "" in
+  (*Graph.Pack.Digraph.dot_output graph dot;*)
+  Graph.Pack.Digraph.display_with_gv graph;
+exit 1;
+(*
+  let ch = open_out "/tmp/comb.dot" in
+   output_string ch dot;
+   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 print_graph' classes =
- prerr_endline "=============================";
- prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes));
- List.iter (function eqc -> prerr_endline (string_of_eqclass eqc)) classes
+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
+      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 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
+ 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
 ;;
 
 let rec iter n l =
- print_graph' (classify l);
+ let arcs = analyze (classify l) in
+ (*print_graph' (analyze arcs);*)
  if n > 0 then
   iter (n - 1) (step l)
 in