]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/formal_topology/bin/comb.ml
mod change (-x)
[helm.git] / helm / software / matita / contribs / formal_topology / bin / comb.ml
old mode 100755 (executable)
new mode 100644 (file)
index e0c58de..f998b88
@@ -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
@@ -28,6 +58,33 @@ let rules =
  ]
 ;;
 
+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 =
@@ -38,10 +95,25 @@ let rec new_dir dir =
 ;;
 
 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_w' w =
+ let s =
+  String.concat ""
+   (List.map (function I -> "i" | C -> "c" | M -> "m") w)
+ in
+  if s = "" then "E" else s
+;;
+
+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;;
@@ -64,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
@@ -93,10 +166,10 @@ let step (l : w list) =
     (List.map
      (function w ->
        List.map (fun x -> x@w)
-       (if List.length (List.filter (fun w -> w = M) w) >= 2 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))
 ;;
 
@@ -133,31 +206,43 @@ let iteri f l =
   print_newline ();
 ;;
 
-let normalize (l : w list) =
+let normalize canonical (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 =
-  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 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
+  aux l l
 ;;
 
-let visualize describe graph =
- let module G =
+let visualize graph =
+ let module GL =
   struct
-   include Graph.Pack.Digraph;;
+   include GL;;
    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 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(G) 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;
@@ -166,123 +251,68 @@ let visualize describe graph =
    (*Unix.system ("ggv /tmp/red.ps");*)
 ;;
 
-let mk_vertex_and_dsc_vertex =
- function () ->
-  let cache1 = Hashtbl.create 5393 in
-  let cache2 = Hashtbl.create 5393 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
-       let v = Graph.Pack.Digraph.V.create n in
-        Hashtbl.add cache1 w v;
-        Hashtbl.add cache2 v w;
-        v),
-   (Hashtbl.find cache2)
-;;
-
-let mk_vertex2 =
- function () ->
-  let cache1 = Hashtbl.create 5393 in
-  function n ->
-   try
-    Hashtbl.find cache1 n
-   with
-    Not_found ->
-     let v = Graph.Pack.Digraph.V.create n in
-      Hashtbl.add cache1 n v;
-      v
-;;
-
-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 5393 in
- let canonicals = Hashtbl.create 5393 in
- let descriptions = Hashtbl.create 5393 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 () ->
-    let vertexes = uniq (Hashtbl.fold (fun k _ l -> k::l) cache []) in
-    let xx =
-     mapi
-      (fun v ->
-        v,
-         List.sort string_compare
-          (List.map string_of_w (Hashtbl.find_all cache v))
-      ) vertexes in
-    iteri (function (_,w::_) -> Hashtbl.add canonicals w () | _ -> ()) xx;
-    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
-        try Hashtbl.find canonicals w; true with Not_found -> false
-    in
-     iteri
-      (function (v,x) ->
-        Hashtbl.add descriptions v
-         (let s = String.concat "=" (List.filter is_not_redundant x) in
-           if s = "" then "." else s)) xx),
-  Hashtbl.find descriptions
+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 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
- iteri
-  (fun (x,y) ->
-    Graph.Pack.Digraph.add_edge graph (mk_vertex x) (mk_vertex y)) arcs;
- print_endline ("<scc>");
- let classes,norm =  Graph.Pack.Digraph.Components.scc graph in
- print_endline (string_of_int classes ^ " classes");
- print_endline ("-----");
- norm,mk_vertex,dsc_vertex,arcs
-;;
+exception Found of GL.V.t;;
 
-let analyze (norm,mk_vertex,dsc_vertex,arcs) =
- print_endline ("building class graph (" ^ string_of_int (List.length arcs) ^ ")");
- let normalize,finish,describe =
-  normalize_and_describe norm mk_vertex dsc_vertex in
- let arcs =
-  uniq (mapi (fun (x,y) -> normalize x,normalize y) arcs) in
- let cgraph = Graph.Pack.Digraph.create () in
- let mk_vertex2 = mk_vertex2 () in
- List.iter
-  (function (x,y) ->
-    if x <> y then
-     Graph.Pack.Digraph.add_edge cgraph (mk_vertex2 x) (mk_vertex2 y)) arcs;
- print_endline "finish";
- finish ();
- print_endline "visualize";
- visualize describe cgraph;
- print_endline ("/////");
-;;
+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;*)
 
-let rec iter n l =
- let pkg = classify (normalize l) in
- if n > 0 then
-  iter (n - 1) (step l)
- else
-  analyze pkg
+  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 10 [[]]
+ let cgraph = GL.create () in
+  GL.add_vertex cgraph [[]];
+  iter 9 cgraph (fun w(*(_,_,w)*) -> [w])
 ;;