X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Fcomb.ml;h=2f4d46fcac930ad2456db3c522c2d12f8bbeddee;hb=c9a4185ac1fef28e5741b8671abf02e33d04ac0d;hp=e0c58dec07e245d3b23add9a6076a4eda758731a;hpb=6006ddfa14ae1caa5adf92119fc38a3a7c4919b3;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 e0c58dec0..2f4d46fca 100755 --- a/helm/software/matita/contribs/formal_topology/bin/comb.ml +++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml @@ -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 (""); - 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 [[]] ;;