X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Fcomb.ml;h=f998b88a98934ee324b0c7516fe9f55d34ff5d5a;hb=700b170aa9b0377d33f1edd44de8d89129477fb8;hp=922d39a7e4f9b21cb325843982010e37aa8a6bbc;hpb=fc8408a10c29e472ec05e725a36da1f71d850937;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 922d39a7e..f998b88a9 100755 --- a/helm/software/matita/contribs/formal_topology/bin/comb.ml +++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml @@ -1,3 +1,33 @@ +(* 0: 7 4 0.312 3 5 7 + 1: 29 6 0.549 3 8 16 24 29 + 2: 120 10 25.525 3 8 19 39 66 95 113 119 120 + 3: > 327 >9 3 8 19 39 75 134 208 274 + 4: > 657 >9 3 8 19 39 75 139 245 + 5: > 526 >8 3 8 19 39 75 139 245 + 6: > 529 >8 + 7: > 529 >8 + 8: > 529 >8 + +(CMM?)+ | (MM?C)+ + +cCw = Cw +-Cw = MCw +cMw = CMw +-MMw = -w +-MCw = MMCw +iw = w + + + s <= s' s <= s' s <= s' s <= s' +=========== =========== ============ ========== + ws <= Cws' Cs <= Cs' CMs' <= Ms Ms' <= MCs + + s <= s' s <= s' +=========== ============ + s <= MMs' Ms' <= Ms + +*) + type t = M | I | C type w = t list type eqclass = w list @@ -21,9 +51,40 @@ let rules = [M;M], Ge, []; [M], Le, [M]; [M], Ge, [M]; + (* classical + [M;M], Le, []; + [C;M], Ge, [M;I]; + *) ] ;; +let inject = + let cache = Hashtbl.create 5393 in + function w -> + try + Hashtbl.find cache w + with + Not_found -> + let rec aux acc = + function + [] -> acc + | he::tl -> aux (4 * acc + (match he with I -> 1 | C -> 2 | M -> 3)) tl + in + let res = 0, aux 0 w, w in + Hashtbl.add cache w res; + res +;; + +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 = @@ -33,31 +94,38 @@ 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 s = + String.concat "" + (List.map (function I -> "i" | C -> "c" | M -> "-") w) + in + if s = "" then "." else s ;; -let string_of_eqclass eqc = - let eqc = List.sort compare eqc in - String.concat "=" (List.map string_of_w eqc) +let string_of_w' w = + let s = + String.concat "" + (List.map (function I -> "i" | C -> "c" | M -> "m") w) + in + if s = "" then "E" else s ;; -let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));; +let string_of_eqclass l = String.concat "=" (List.map string_of_w l);; + +let name_of_eqclass l = String.concat "_" (List.map string_of_w' l);; 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) = @@ -68,9 +136,10 @@ let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) = function [],w -> w | x::lhs,x'::w when x = x' -> aux (lhs,w) - | _,_ -> raise NoMatch - in - rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs) + | _,_ -> raise NoMatch in + let w' = aux (lhs,w) in + if List.length rhs < List.length lhs then rhs @@ [w'] + else rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs) and apply_rules (w,_ as w_and_dir) = if w = [] then [[]] else @@ -95,71 +164,155 @@ let step (l : w list) = uniq (List.flatten (List.map - (function w -> List.map (fun x -> x@w) [[I];[C];(*[M];*)[]]) - l)) + (function w -> + List.map (fun x -> x@w) + (if List.length (List.filter (fun w -> w = M) w) >= 5 then + [[I];[C]] + else + [[I];[C];[M]]) + ) l)) ;; -let leq rels x y = - let rec aux avoid x y = - x = y - || List.exists - (fun (x',dir,z) -> - x=x' && dir = Le && not (List.mem z avoid) && aux (z::avoid) z y) rels - || List.exists - (fun (z,dir,x') -> - x=x' && dir = Ge && not (List.mem z avoid) && aux (z::avoid) z y) rels +let mapi f l = + let rec aux acc i = + function + [] -> acc + | he::tl -> + if i mod 1000 = 0 then + begin + print_string ("@" ^ string_of_int i ^ " "); + flush stdout; + end; + aux (f he :: acc) (i+1) tl 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 res = List.rev (aux [] 1 l) in + print_newline (); + res ;; -let add_class rels classes he = - let rec aux visited = +let iteri f l = + let rec aux i = function - [] -> [he]::visited - | eqc::tl -> - if in_class rels eqc he then - (he::eqc)::tl@visited - else - aux (eqc::visited) tl + [] -> () + | he::tl -> + if i mod 1000 = 0 then + begin + print_string ("@" ^ string_of_int i ^ " "); + flush stdout; + end; + f he; aux (i+1) tl in - aux [] classes + aux 1 l; + print_newline (); ;; -let classify (l : w list) = -(*prerr_endline ("Classify: " ^ string_of_int (List.length l));*) - let rels = - List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) +let normalize canonical (l : w list) = + print_endline (string_of_int (List.length l) ^ " nodes to be normalized"); + let rec aux all l = + let rels = + List.flatten + (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in + let arcs = + mapi + (function (x,rel,y) -> + let x = canonical x(*(inject x)*) in + let y = canonical y(*(inject y)*) in + match rel with Le -> x,y | Ge -> y,x) rels in + let res = uniq arcs in + let nodes = uniq (l @ List.map (fun (_,_,n) -> n) rels) in + let new_nodes = List.filter (fun n -> not (List.mem n all)) nodes in + let new_nodes = List.filter (function n -> [n] = canonical n) new_nodes in + if new_nodes = [] then + res + else + uniq (res @ aux nodes new_nodes) in - let rec aux classes = - function - [] -> classes - | he::tl -> aux (add_class rels classes he) tl - in - aux [] l + aux l l ;; -let print_graph = - List.iter - (function (w,dir,w') -> - prerr_endline (string_of_w w ^ string_of_dir dir ^ string_of_w w')) +let visualize graph = + let module GL = + struct + include GL;; + let edge_attributes _ = [] + let default_edge_attributes _ = [] + let get_subgraph _ = None + 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(GL) in + let ch = open_out "/tmp/comb.dot" in + D.output_graph ch graph; + close_out ch; + 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 print_graph' classes = - prerr_endline "============================="; - prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes)); - List.iter (function eqc -> prerr_endline (string_of_eqclass eqc)) classes +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 rec iter n l = - print_graph' (classify l); - if n > 0 then - iter (n - 1) (step l) +exception Found of GL.V.t;; + +let rec iter n cgraph (canonical: w -> GL.V.t) = + print_endline ("STEP " ^ string_of_int n); + let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in + let nodes = step (List.map List.hd nodes) in +(*let nodes = [[C;M];[C;M;C;M];[C;M;C;M;C;M];[C;M;C;M;C;M;C;M];[C;M;C;M;C;M;C;M;C;M]] in*) +(*let nodes = [[C;I;C;I;C;I]] in*) + (*let nodes = step (List.concat nodes) in*) +(*List.iter (fun x -> prerr_endline ("#@ " ^ string_of_w x)) nodes;*) + let arcs = normalize canonical nodes in + iteri (fun (x,y) -> if x <> y then GL.add_edge cgraph x y) arcs; +(*List.iter (fun (x,y) -> prerr_endline (string_of_eqclass x ^ " -> " ^ string_of_eqclass y)) arcs;*) + + print_endline (""); + let classes,norm = + let module SCC = Graph.Components.Make(GL) in SCC.scc cgraph in + let xxx = + let module SCC = Graph.Components.Make(GL) in SCC.scc_array cgraph in + print_endline (""); + let get_canonical n = + try List.sort w_compare (List.concat (xxx.(norm n))) + with Not_found -> n + in + let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in + print_endline "get_canonical"; + let nodes = mapi (fun n -> n,get_canonical n) nodes in + print_endline "/get_canonical"; + print_endline ("collapse " ^ string_of_int (List.length nodes)); + iteri + (function (n,n') -> + let succ = GL.succ cgraph n in + let pred = GL.pred cgraph n in + GL.remove_vertex cgraph n; + let add_edge s t = if s <> t then GL.add_edge cgraph s t in + List.iter (fun s -> add_edge n' (get_canonical s)) succ; + List.iter (fun p -> add_edge (get_canonical p) n') pred) + nodes; + print_endline (string_of_int classes ^ " classes"); + print_endline ("-----"); + print_endline "visualize"; + visualize cgraph; + print_endline ("/////"); + GL.iter_vertex (fun l -> print_endline ("?" ^ string_of_eqclass l)) cgraph; + let canonical = + function (*_,_,*)w -> + try + GL.iter_vertex (fun l -> if List.mem w l then raise (Found l)) cgraph; + [w] + with + Found l -> l in + if n > 0 then + iter (n - 1) cgraph canonical + else + () in - iter 4 [[]] + let cgraph = GL.create () in + GL.add_vertex cgraph [[]]; + iter 9 cgraph (fun w(*(_,_,w)*) -> [w]) ;;