From 79a489c46c77de80979d68a512d1f640f8273f9e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Mar 2009 23:35:31 +0000 Subject: [PATCH] New version. --- .../contribs/formal_topology/bin/comb.ml | 218 ++++++++++-------- 1 file changed, 126 insertions(+), 92 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml index 7c7cd3ecd..59807ed69 100755 --- a/helm/software/matita/contribs/formal_topology/bin/comb.ml +++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml @@ -33,31 +33,23 @@ let rec new_dir dir = | (C|I)::tl -> new_dir dir tl ;; -let string_of_dir = function Le -> "<=" | Ge -> ">=";; - let string_of_w w = String.concat "" (List.map (function I -> "i" | C -> "c" | M -> "-") w) ;; -let string_of_eqclass eqc = - let eqc = List.sort compare eqc in - String.concat "=" (List.map string_of_w eqc) -;; - -let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));; - exception NoMatch;; let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2;; let uniq l = - let rec aux l = - function - [] -> l - | he::tl -> aux (if List.mem he l then l else he::l) tl + let rec aux acc = function + | [] -> acc + | h::[] -> h::acc + | h1::h2::tl when h1=h2 -> aux (h2::acc) tl + | h1::tl (* when h1 <> h2 *) -> aux (h1::acc) tl in - aux [] l + List.rev (aux [] (List.sort compare l)) ;; let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) = @@ -97,110 +89,152 @@ let step (l : w list) = (List.map (function w -> List.map (fun x -> x@w) - (if List.mem M w then + (if List.length (List.filter (fun w -> w = M) w) >= 2 then [[I];[C];[]] else - [[I];[C](*;[M]*);[]]) + [[I];[C];[M];[]]) ) l)) ;; -let leq rels x y = - let rec aux avoid x y = - x = y || - List.exists - (fun (x',z) -> x=x' && not (List.mem z avoid) && aux (z::avoid) z y) rels - in - aux [x] x y -;; - -let in_class rels eqc he = - match eqc with - [] -> assert false - | k::_ -> leq rels k he && leq rels he k -;; - -let add_class rels classes he = -prerr_endline "Add"; - let rec aux visited = +let mapi f l = + let rec aux acc i = function - [] -> [he]::visited - | eqc::tl -> - if in_class rels eqc he then - (he::eqc)::tl@visited - else - aux (eqc::visited) tl + [] -> acc + | he::tl -> aux (f i he :: acc) (i+1) tl in - aux [] classes + List.rev (aux [] 1 l) ;; -let classify (l : w list) = -prerr_endline ("Classify: " ^ string_of_int (List.length l)); +let normalize (l : w list) = + print_endline (string_of_int (List.length l) ^ " nodes to be normalized"); let rels = - List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) - in - uniq - (List.map - (function (x,rel,y) -> match rel with Le -> x,y | Ge -> y,x) rels) + List.flatten + (mapi + (fun i x -> + if i mod 100 = 0 then print_string ("@" ^ string_of_int i ^ " "); + apply_rules (x,Le) @ apply_rules (x,Ge)) l) in + print_newline (); + 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 visualize graph = - let dot = "" in - (*Graph.Pack.Digraph.dot_output graph dot;*) - Graph.Pack.Digraph.display_with_gv graph; -exit 1; -(* +let visualize describe graph = + let module G = + struct + include Graph.Pack.Digraph;; + 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 default_vertex_attributes _ = [] + let graph_attributes _ = [] + end in + let module D = Graph.Graphviz.Dot(G) in let ch = open_out "/tmp/comb.dot" in - output_string ch dot; + D.output_graph ch graph; close_out ch; - Unix.system ("tred /tmp/comb.dot > /tmp/red.dot"); - Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps"); - Unix.system ("ggv /tmp/red.ps"); -*) () -;; - -let analyze arcs = - let mk_vertex = - let cache = ref [] in - function w -> - try - List.assoc w !cache - 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 + ignore (Unix.system ("tred /tmp/comb.dot > /tmp/red.dot")); + ignore (Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps")); + (*Unix.system ("ggv /tmp/red.ps");*) +;; + +let mk_vertex_and_dsc_vertex = + function () -> + let cache1 = Hashtbl.create 37 in + let cache2 = Hashtbl.create 37 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 - aux 0 w - in -prerr_endline (string_of_w w ^ " => " ^ string_of_int n); - let v = Graph.Pack.Digraph.V.create n in - cache := (w,v)::!cache; - v 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 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 37 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 v -> + let vertexes = uniq (Hashtbl.fold (fun k _ l -> k::l) cache []) in + let ll = + List.map + (fun v -> + v, + List.sort string_compare + (List.map string_of_w (Hashtbl.find_all cache v)) + ) vertexes in + 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 + List.exists (function w'::_ -> w=w' | [] -> false) (List.map snd ll) + in + let l = List.filter is_not_redundant (List.assoc v ll) in + let s = String.concat "=" l in + if s = "" then "." else s) +;; + +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 List.iter (function (x,y) -> Graph.Pack.Digraph.add_edge graph (mk_vertex x) (mk_vertex y)) arcs; -prerr_endline (""); - let classes = Graph.Pack.Digraph.Components.scc_list graph in -List.iter (function l -> prerr_endline (String.concat "=" (List.map string_of_int (List.map Graph.Pack.Digraph.V.label l)))) classes; -prerr_endline (""); - let classes,normalize = Graph.Pack.Digraph.Components.scc graph in -prerr_endline (string_of_int classes ^ " CLASSI"); - let arcs = uniq (List.map (fun (x,y) -> normalize (mk_vertex x),normalize (mk_vertex y)) arcs) in + print_endline (""); + let classes,norm = Graph.Pack.Digraph.Components.scc graph in + print_endline (string_of_int classes ^ " classes"); + norm,mk_vertex,dsc_vertex,arcs +;; + +let analyze (norm,mk_vertex,dsc_vertex,arcs) = + print_endline "building class graph"; + let normalize,describe = normalize_and_describe norm mk_vertex dsc_vertex in + let arcs = uniq (List.map (fun (x,y) -> normalize x,normalize y) arcs) in let cgraph = Graph.Pack.Digraph.create () in List.iter (function (x,y) -> - Graph.Pack.Digraph.add_edge cgraph (Graph.Pack.Digraph.V.create x) (Graph.Pack.Digraph.V.create y)) arcs; - visualize cgraph + if x <> y then + Graph.Pack.Digraph.add_edge cgraph (Graph.Pack.Digraph.V.create x + ) (Graph.Pack.Digraph.V.create y)) arcs; + print_endline "visualize"; + visualize describe cgraph; + print_endline ("-----"); ;; let rec iter n l = - let arcs = analyze (classify l) in - (*print_graph' (analyze arcs);*) + let pkg = classify (normalize l) in if n > 0 then iter (n - 1) (step l) + else + analyze pkg in - iter 4 [[]] + iter 10 [[]] ;; -- 2.39.2