From 943c8baae10afee070468ab54f4bf86563df2418 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Mar 2009 23:36:13 +0000 Subject: [PATCH] New version. --- .../contribs/formal_topology/bin/comb.ml | 136 ++++++++---------- 1 file changed, 63 insertions(+), 73 deletions(-) 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 (""); - 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 [[]] ;; -- 2.39.2