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=af5633ff35a79c19a15e9650d2abdfcfac8a025e;hpb=18711733cdd65051fa094d5a5013ac306ea1bb60;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 af5633ff3..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 string_of_eqclass l =
+ let s = String.concat "=" (List.map string_of_w l) in
+  if s = "" then "." else s
 ;;
 
-let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));;
+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,92 +143,152 @@ 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.length (List.filter (fun w -> w = M) w) >= 3 then
+         [[I];[C];[]]
+        else
+         [[I];[C];[M];[]])
+     ) l))
 ;;
 
-let classify (l : w list) =
- List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
+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 print_graph =
- List.iter
-  (function (w,dir,w') ->
-    prerr_endline (string_of_w w ^ string_of_dir dir ^ string_of_w w'))
+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 ();
 ;;
 
-print_graph (classify (step (step (step [[]]))));;
-
-(*
- let ns = ref [] in
-  List.iter (function eqc -> ns := eqc::!ns) s;
-  List.iter
-   (function eqc ->
-     List.iter
-      (function x ->
-        let eqc = simplify ([x] @@ eqc) in
-         if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
-          ns := eqc::!ns
-      ) [I;C;M]
-   ) s;
-  combine_classes !ns
+let normalize (l : w list) =
+ print_endline (string_of_int (List.length l) ^ " nodes to be normalized");
+ let rels =
+  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
+  uniq arcs
 ;;
 
-
-
-let subseteq l1 l2 =
- List.for_all (fun x -> List.mem x l2) l1
+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 (===) l1 l2 = subseteq l1 l2 && subseteq l2 l1;;
-
-let simplify eqc =
- let rec aux l =
-  let l' = uniq (List.flatten (List.map apply_rules l)) in
-  if l === l' then l else aux l'
- in
-  aux eqc
+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 combine_class_with_classes l1 =
- let rec aux =
-  function
-     [] -> [l1]
-   | l2::tl ->
-      if List.exists (fun x -> List.mem x l2) l1 then
-       uniq (l1 @ l2) :: tl
-      else
-       l2:: aux tl
- in
-  aux
+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 combine_classes l =
- let rec aux acc =
-  function
-     [] -> acc
-   | he::tl -> aux (combine_class_with_classes he acc) tl
- in
-  aux [] l
+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 step (s : eqclass list) =
- let ns = ref [] in
-  List.iter (function eqc -> ns := eqc::!ns) s;
-  List.iter
-   (function eqc ->
-     List.iter
-      (function x ->
-        let eqc = simplify ([x] @@ eqc) in
-         if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
-          ns := eqc::!ns
-      ) [I;C;M]
-   ) s;
-  combine_classes !ns
+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 classes = step (step (step (step [[[]]]))) in
- prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes));
- print classes
+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 15 [[]]
 ;;
-*)