From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 2 Mar 2009 23:36:13 +0000 (+0000)
Subject: New version.
X-Git-Tag: make_still_working~4175
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=943c8baae10afee070468ab54f4bf86563df2418;p=helm.git

New version.
---

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 895273ce8..19874951b 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -1,6 +1,6 @@
 (* 0: 7
-   1: 29
-   2: 120
+   1: 29      6?
+   2: 120    10
    3: > 319
    4: ???
 *)
@@ -35,6 +35,9 @@ let rules =
  ]
 ;;
 
+module V = struct type t = eqclass end;;
+module G = Graph.Imperative.Digraph.Abstract(V);;
+
 let swap = function Le -> Ge | Ge -> Le;;
 
 let rec new_dir dir =
@@ -49,6 +52,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;;
@@ -100,7 +118,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) >= 1 then
+       (if List.length (List.filter (fun w -> w = M) w) >= 2 then
          [[I];[C];[]]
         else
          [[I];[C];[M];[]])
@@ -147,20 +165,20 @@ let normalize (l : w list) =
    (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
+   (function (x,rel,y) -> match rel with Le -> [x],[y] | Ge -> [y],[x]) rels) in
  let res = uniq arcs in
  res
 ;;
 
-let visualize describe graph =
+let visualize graph =
  let module G =
   struct
-   include Graph.Pack.Digraph;;
+   include G;;
    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 (G.V.label v))]
+   let vertex_name v = name_of_eqclass (G.V.label v)
    let default_vertex_attributes _ = []
    let graph_attributes _ = []
   end in
@@ -173,55 +191,34 @@ 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 ->
+let mk_vertex () =
+ let cache1 = Hashtbl.create 5393 in
+ (function w ->
    try
-    Hashtbl.find cache1 n
+    Hashtbl.find cache1 w
    with
     Not_found ->
-     let v = Graph.Pack.Digraph.V.create n in
-      Hashtbl.add cache1 n v;
-      v
+      let v = G.V.create w in
+       Hashtbl.add cache1 w 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 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 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 v ->
     let normalized = norm v in
-    let dsc = dsc_vertex v in
+    let dsc =
+     match G.V.label v with
+        [d] -> d
+      | _ -> assert false
+    in
      if not (List.mem dsc (Hashtbl.find_all cache normalized)) then
       Hashtbl.add cache normalized dsc;
      normalized),
@@ -229,56 +226,49 @@ let normalize_and_describe norm 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
+ let mk_vertex = mk_vertex () in
+ let graph = G.create () in
  let varcs = mapi (fun (x,y) -> mk_vertex x,mk_vertex y) arcs in
- iteri (fun (x,y) -> Graph.Pack.Digraph.add_edge graph x y) varcs;
+ iteri (fun (x,y) -> G.add_edge graph x y) varcs;
  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,dsc_vertex,varcs
+ norm,varcs
 ;;
 
-let analyze (norm,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 dsc_vertex in
+ let normalize,finish,describe = normalize_and_describe norm 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
+ print_endline "finish";
+ finish ();
+ let cgraph = G.create () in
+ let mk_vertex = mk_vertex () 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 ();
+     G.add_edge cgraph (mk_vertex (describe x)) (mk_vertex (describe y))) arcs;
  print_endline "visualize";
- visualize describe cgraph;
+ visualize cgraph;
  print_endline ("/////");
 ;;
 
@@ -289,5 +279,5 @@ let rec iter n l =
  else
   analyze pkg
 in
- iter 6 [[]]
+ iter 10 [[]]
 ;;