]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/formal_topology/bin/comb.ml
...
[helm.git] / helm / software / matita / contribs / formal_topology / bin / comb.ml
index e0c58dec07e245d3b23add9a6076a4eda758731a..2f4d46fcac930ad2456db3c522c2d12f8bbeddee 100755 (executable)
@@ -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
@@ -28,6 +35,36 @@ let rules =
  ]
 ;;
 
+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 =
@@ -42,6 +79,21 @@ let string_of_w w =
   (List.map (function I -> "i" | C -> "c" | M -> "-") w)
 ;;
 
+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 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;;
@@ -93,7 +145,7 @@ 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
+       (if List.length (List.filter (fun w -> w = M) w) >= 3 then
          [[I];[C];[]]
         else
          [[I];[C];[M];[]])
@@ -139,25 +191,28 @@ let normalize (l : w list) =
   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
+  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 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,56 +221,18 @@ 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 w_compare s1 s2 =
+ let c = compare (List.length s1) (List.length s2) in
+  if c = 0 then compare s1 s2 else c
 ;;
 
-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 normalize_and_describe norm =
  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
+  (function v ->
     let normalized = norm v in
-    let dsc = dsc_vertex 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),
@@ -223,66 +240,55 @@ let normalize_and_describe norm mk_vertex dsc_vertex =
     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
+      (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 s =
-     let len = String.length s in
-      if len <= 1 then true
-      else
-       let w = String.sub s 1 (len - 1) in
+    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
-         (let s = String.concat "=" (List.filter is_not_redundant x) in
-           if s = "" then "." else s)) xx),
+        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 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;
+ let graph = G.create () in
+ iteri (fun (x,y) -> G.add_edge graph x y) arcs;
  print_endline ("<scc>");
- let classes,norm =  Graph.Pack.Digraph.Components.scc graph in
+ 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,mk_vertex,dsc_vertex,arcs
+ norm,arcs
 ;;
 
-let analyze (norm,mk_vertex,dsc_vertex,arcs) =
+let analyze (norm,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;
+ 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 describe cgraph;
+ visualize cgraph;
  print_endline ("/////");
 ;;
 
 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 10 [[]]
+ iter 15 [[]]
 ;;