X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Fcomb.ml;h=f998b88a98934ee324b0c7516fe9f55d34ff5d5a;hb=5dcae34c6e44a40e236db641f59ddb096d1a16ec;hp=7c7cd3ecd94b238ac6a8dbdecd0553963ad2d670;hpb=74769ee535a1a3f019e04da7501b183c15e348da;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 7c7cd3ecd..f998b88a9 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -1,3 +1,33 @@
+(* 0: 7       4    0.312    3 5 7
+   1: 29      6    0.549    3 8 16 24 29
+   2: 120    10   25.525    3 8 19 39 66  95 113 119 120
+   3: > 327  >9             3 8 19 39 75 134 208 274
+   4: > 657  >9             3 8 19 39 75 139 245
+   5: > 526  >8             3 8 19 39 75 139 245
+   6: > 529  >8
+   7: > 529  >8
+   8: > 529  >8
+
+(CMM?)+ | (MM?C)+
+
+cCw = Cw
+-Cw = MCw
+cMw = CMw
+-MMw = -w
+-MCw = MMCw
+iw = w
+
+
+  s <= s'            s <= s'         s <= s'           s <= s'
+===========        ===========     ============      ==========
+ ws <= Cws'         Cs <= Cs'       CMs' <= Ms       Ms' <= MCs
+
+  s <= s'          s <= s'
+===========     ============
+ s <= MMs'        Ms' <= Ms
+
+*)
+
 type t = M | I | C
 type w = t list
 type eqclass = w list
@@ -21,9 +51,40 @@ let rules =
    [M;M],   Ge, [];
    [M],     Le, [M];
    [M],     Ge, [M];
+   (* classical
+   [M;M],   Le, [];
+   [C;M],   Ge, [M;I];
+   *)
  ]
 ;;
 
+let inject =
+ let cache = Hashtbl.create 5393 in
+ function w ->
+  try
+   Hashtbl.find cache w
+  with
+   Not_found ->
+    let rec aux acc =
+     function
+        [] -> acc
+      | he::tl -> aux (4 * acc + (match he with I -> 1 | C -> 2 | M -> 3)) tl
+    in
+     let res = 0, aux 0 w, w in
+      Hashtbl.add cache w res;
+      res
+;;
+
+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 +94,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 s =
+  String.concat ""
+   (List.map (function I -> "i" | C -> "c" | M -> "-") w)
+ in
+  if s = "" then "." else s
 ;;
 
-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 =
+ let s =
+  String.concat ""
+   (List.map (function I -> "i" | C -> "c" | M -> "m") w)
+ in
+  if s = "" then "E" else s
 ;;
 
-let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));;
+let string_of_eqclass l = String.concat "=" (List.map string_of_w l);;
+
+let name_of_eqclass l = String.concat "_" (List.map string_of_w' l);;
 
 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) =
@@ -68,9 +136,10 @@ let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) =
    function
       [],w -> w
     | x::lhs,x'::w when x = x' -> aux (lhs,w)
-    | _,_ -> raise NoMatch
-  in
-   rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs)
+    | _,_ -> raise NoMatch in
+  let w' = aux (lhs,w) in
+   if List.length rhs < List.length lhs then rhs @@ [w']
+   else rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs)
 and apply_rules (w,_ as w_and_dir) =
  if w = [] then [[]]
  else
@@ -97,110 +166,153 @@ let step (l : w list) =
     (List.map
      (function w ->
        List.map (fun x -> x@w)
-       (if List.mem M w then
-         [[I];[C];[]]
+       (if List.length (List.filter (fun w -> w = M) w) >= 5 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
+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
-  aux [x] x y
+  let res = List.rev (aux [] 1 l) in
+   print_newline ();
+   res
 ;;
 
-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 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 rels =
-  List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
+let normalize canonical (l : w list) =
+ print_endline (string_of_int (List.length l) ^ " nodes to be normalized");
+ let rec aux all l =
+  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 = canonical x(*(inject x)*) in
+      let y = canonical y(*(inject y)*) in
+       match rel with Le -> x,y | Ge -> y,x) rels in
+  let res = uniq arcs in
+  let nodes = uniq (l @ List.map (fun (_,_,n) -> n) rels) in
+  let new_nodes = List.filter (fun n -> not (List.mem n all)) nodes in
+  let new_nodes = List.filter (function n -> [n] = canonical n) new_nodes in
+   if new_nodes = [] then
+    res
+   else
+    uniq (res @ aux nodes new_nodes)
  in
-  uniq
-   (List.map
-    (function (x,rel,y) -> match rel with Le -> x,y | Ge -> y,x) rels)
+  aux l l
 ;;
 
 let visualize graph =
-  let dot = "" in
-  (*Graph.Pack.Digraph.dot_output graph dot;*)
-  Graph.Pack.Digraph.display_with_gv graph;
-exit 1;
-(*
+ 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
-   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");
-*) ()
+   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 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 w_compare s1 s2 =
+ let c = compare (List.length s1) (List.length s2) in
+  if c = 0 then compare s1 s2 else c
 ;;
 
-let rec iter n l =
- let arcs = analyze (classify l) in
- (*print_graph' (analyze arcs);*)
- if n > 0 then
-  iter (n - 1) (step l)
+exception Found of GL.V.t;;
+
+let rec iter n cgraph (canonical: w -> GL.V.t) =
+ print_endline ("STEP " ^ string_of_int n);
+ let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in
+ let nodes = step (List.map List.hd nodes) in
+(*let nodes = [[C;M];[C;M;C;M];[C;M;C;M;C;M];[C;M;C;M;C;M;C;M];[C;M;C;M;C;M;C;M;C;M]] in*)
+(*let nodes = [[C;I;C;I;C;I]] in*)
+ (*let nodes = step (List.concat nodes) in*)
+(*List.iter (fun x -> prerr_endline ("#@ " ^ string_of_w x)) nodes;*)
+ let arcs = normalize canonical nodes in
+  iteri (fun (x,y) -> if x <> y then GL.add_edge cgraph x y) arcs;
+(*List.iter (fun (x,y) -> prerr_endline (string_of_eqclass x ^ " -> " ^ string_of_eqclass y)) arcs;*)
+
+  print_endline ("<scc>");
+  let classes,norm =
+   let module SCC = Graph.Components.Make(GL) in SCC.scc cgraph in
+  let xxx =
+   let module SCC = Graph.Components.Make(GL) in SCC.scc_array cgraph in
+  print_endline ("</scc>");
+  let get_canonical n =
+   try List.sort w_compare (List.concat (xxx.(norm n)))
+   with Not_found -> n
+  in
+  let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in
+  print_endline "get_canonical";
+  let nodes = mapi (fun n -> n,get_canonical n) nodes in
+  print_endline "/get_canonical";
+  print_endline ("collapse " ^ string_of_int (List.length nodes));
+  iteri
+   (function (n,n') ->
+     let succ = GL.succ cgraph n in
+     let pred = GL.pred cgraph n in
+      GL.remove_vertex cgraph n;
+      let add_edge s t = if s <> t then GL.add_edge cgraph s t in
+      List.iter (fun s -> add_edge n' (get_canonical s)) succ;
+      List.iter (fun p -> add_edge (get_canonical p) n') pred)
+   nodes;
+  print_endline (string_of_int classes ^ " classes");
+  print_endline ("-----");
+  print_endline "visualize";
+  visualize cgraph;
+  print_endline ("/////");
+  GL.iter_vertex (fun l -> print_endline ("?" ^ string_of_eqclass l)) cgraph;
+  let canonical =
+   function (*_,_,*)w ->
+    try
+     GL.iter_vertex (fun l -> if List.mem w l then raise (Found l)) cgraph;
+     [w]
+    with
+     Found l -> l in
+  if n > 0 then
+   iter (n - 1) cgraph canonical
+  else
+   ()
 in
- iter 4 [[]]
+ let cgraph = GL.create () in
+  GL.add_vertex cgraph [[]];
+  iter 9 cgraph (fun w(*(_,_,w)*) -> [w])
 ;;