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=601baed778a190b580982b588ebe49ba3f762b30;hp=895273ce81cb4ba07a5e9f192012f62fcfd7ab2b;hpb=88333aeb79f693c73e880e433fa6bcb33d715193;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 895273ce8..f998b88a9 100755 --- a/helm/software/matita/contribs/formal_topology/bin/comb.ml +++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml @@ -1,8 +1,31 @@ -(* 0: 7 - 1: 29 - 2: 120 - 3: > 319 - 4: ??? +(* 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 @@ -35,6 +58,33 @@ let rules = ] ;; +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 = @@ -45,10 +95,25 @@ let rec new_dir dir = ;; 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_w' w = + let s = + String.concat "" + (List.map (function I -> "i" | C -> "c" | M -> "m") w) + in + if s = "" then "E" else s +;; + +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;; @@ -71,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 @@ -100,10 +166,10 @@ 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 - [[I];[C];[]] + (if List.length (List.filter (fun w -> w = M) w) >= 5 then + [[I];[C]] else - [[I];[C];[M];[]]) + [[I];[C];[M]]) ) l)) ;; @@ -140,31 +206,43 @@ let iteri f l = print_newline (); ;; -let normalize (l : w list) = +let normalize canonical (l : w list) = print_endline (string_of_int (List.length l) ^ " nodes to be normalized"); - let rels = - 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 + 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 + aux l l ;; -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; @@ -173,121 +251,68 @@ 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 -> - 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 dsc_vertex = - 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 - if not (List.mem dsc (Hashtbl.find_all cache normalized)) then - Hashtbl.add cache normalized dsc; - normalized), - (function () -> - 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 - 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 - 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.find descriptions +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 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 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; - print_endline (""); - let classes,norm = Graph.Pack.Digraph.Components.scc graph in - print_endline (string_of_int classes ^ " classes"); - print_endline ("-----"); - norm,dsc_vertex,varcs -;; +exception Found of GL.V.t;; -let analyze (norm,dsc_vertex,arcs) = - print_endline ("building class graph (" ^ string_of_int (List.length arcs) ^ ")"); - let normalize,finish,describe = - normalize_and_describe norm 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; - print_endline "finish"; - finish (); - print_endline "visualize"; - visualize describe cgraph; - print_endline ("/////"); -;; +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;*) -let rec iter n l = - let pkg = classify (normalize l) in - if n > 0 then - iter (n - 1) (step l) - else - analyze pkg + 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 6 [[]] + let cgraph = GL.create () in + GL.add_vertex cgraph [[]]; + iter 9 cgraph (fun w(*(_,_,w)*) -> [w]) ;;