X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Fcomb.ml;h=2f4d46fcac930ad2456db3c522c2d12f8bbeddee;hb=c9a4185ac1fef28e5741b8671abf02e33d04ac0d;hp=922d39a7e4f9b21cb325843982010e37aa8a6bbc;hpb=fc8408a10c29e472ec05e725a36da1f71d850937;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 922d39a7e..2f4d46fca 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -1,3 +1,10 @@
+(* 0: 7
+   1: 29      6
+   2: 120    10
+   3: > 327  >9
+   4: ???
+*)
+
 type t = M | I | C
 type w = t list
 type eqclass = w list
@@ -21,9 +28,43 @@ let rules =
    [M;M],   Ge, [];
    [M],     Le, [M];
    [M],     Ge, [M];
+   (* classical
+   [M;M],   Le, [];
+   [C;M],   Ge, [M;I];
+   *)
  ]
 ;;
 
+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;;
 
 let rec new_dir dir =
@@ -33,31 +74,38 @@ 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 string_of_w' w =
+ String.concat ""
+  (List.map (function I -> "i" | C -> "c" | M -> "m") w)
 ;;
 
-let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));;
+let string_of_eqclass l =
+ let s = String.concat "=" (List.map string_of_w l) in
+  if s = "" then "." else s
+;;
+
+let name_of_eqclass l =
+ let s = String.concat "_" (List.map string_of_w' l) in
+  if s = "" then "E" else s
+;;
 
 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) =
@@ -95,71 +143,152 @@ let step (l : w list) =
  uniq
   (List.flatten
     (List.map
-     (function w -> List.map (fun x -> x@w) [[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
- in
-  aux [x] x y
+     (function w ->
+       List.map (fun x -> x@w)
+       (if List.length (List.filter (fun w -> w = M) w) >= 3 then
+         [[I];[C];[]]
+        else
+         [[I];[C];[M];[]])
+     ) l))
 ;;
 
-let in_class rels eqc he =
- match eqc with
-    [] -> assert false
-  | k::_ -> leq rels k he && leq rels he k
+let mapi f l =
+ let rec aux acc i =
+  function
+     [] -> acc
+   | 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
+  let res = List.rev (aux [] 1 l) in
+   print_newline ();
+   res
 ;;
 
-let add_class rels classes he =
- let rec aux visited =
+let iteri f l =
+ let rec aux i =
   function
-     [] -> [he]::visited
-   | eqc::tl ->
-      if in_class rels eqc he then
-       (he::eqc)::tl@visited
-      else
-       aux (eqc::visited) tl
+     [] -> ()
+   | 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 [] classes
+  aux 1 l;
+  print_newline ();
 ;;
 
-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)
+  List.flatten
+   (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in
+ let arcs =
+  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
-  let rec aux classes =
-   function
-      [] -> classes
-    | he::tl -> aux (add_class rels classes he) tl
-  in
-   aux [] l
+  uniq arcs
 ;;
 
-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 module GL =
+  struct
+   include GL;;
+   let edge_attributes _ = []
+   let default_edge_attributes _ = []
+   let get_subgraph _ = None
+   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(GL) in
+  let ch = open_out "/tmp/comb.dot" in
+   D.output_graph ch graph;
+   close_out ch;
+   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 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 w_compare s1 s2 =
+ let c = compare (List.length s1) (List.length s2) in
+  if c = 0 then compare s1 s2 else c
+;;
+
+let normalize_and_describe norm =
+ let cache = Hashtbl.create 5393 in
+ let canonicals = Hashtbl.create 5393 in
+ let descriptions = Hashtbl.create 5393 in
+  (function v ->
+    let normalized = norm v 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),
+  (function () ->
+    let vertexes = uniq (Hashtbl.fold (fun k _ l -> k::l) cache []) in
+    let xx =
+     mapi
+      (fun v -> v, List.sort w_compare (Hashtbl.find_all cache v)) vertexes in
+    iteri (function (_,w::_) -> Hashtbl.add canonicals w () | _ -> ()) xx;
+    let is_not_redundant =
+     function
+        [] | [_] -> true
+      | _::w ->
+        try Hashtbl.find canonicals w; true with Not_found -> false
+    in
+     iteri
+      (function (v,x) ->
+        Hashtbl.add descriptions v ((List.filter is_not_redundant x) : eqclass)) xx),
+  Hashtbl.find descriptions
+;;
+
+let classify arcs =
+ print_endline (string_of_int (List.length arcs) ^ " arcs to be classified");
+ let graph = G.create () in
+ 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,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
+ print_endline "finish";
+ finish ();
+ 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_graph' (classify 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 4 [[]]
+ iter 15 [[]]
 ;;