X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Fcomb.ml;h=19874951b67f6d108da5d6b84c04313d38bfecb2;hb=943c8baae10afee070468ab54f4bf86563df2418;hp=d388acd89f9a209568fb2398f8a75b43c31e467c;hpb=eb0dee396c1a88059cae089aed3184b5d4cf9a72;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 d388acd89..19874951b 100755 --- a/helm/software/matita/contribs/formal_topology/bin/comb.ml +++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml @@ -1,142 +1,283 @@ +(* 0: 7 + 1: 29 6? + 2: 120 10 + 3: > 319 + 4: ??? +*) + type t = M | I | C type w = t list type eqclass = w list +type dir = Le | Ge + let rules = - [ [I;I], [I]; - [C;C], [C]; - [M;M], []; - [M;C], [I;M]; - [C;M], [M;I]; -(* -axiom leq_refl: ∀A. A ⊆ A. -axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B. -axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C. - -axiom i_contrattivita: ∀A. i A ⊆ A. -axiom i_idempotenza: ∀A. i (i A) = i A. -axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B. -axiom c_espansivita: ∀A. A ⊆ c A. -axiom c_idempotenza: ∀A. c (c A) = c A. -axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B. -axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A. -axiom m_saturazione: ∀A. A ⊆ m (m A). -axiom m_puntofisso: ∀A. m A = m (m (m A)). -axiom th1: ∀A. c (m A) ⊆ m (i A). -axiom th2: ∀A. i (m A) ⊆ m (c A). -lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B. -lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B. -*) + [ [I], Le, []; + [C], Ge, []; + [I;I], Ge, [I]; + [C;C], Le, [C]; + [I], Le, [I]; + [I], Ge, [I]; + [C], Le, [C]; + [C], Ge, [C]; + [C;M], Le, [M;I]; + [C;M;I], Le, [M;I]; (* ??? *) + [I;M], Le, [M;C]; + [I;M;C], Ge, [I;M]; (* ??? *) + [M;M;M], Ge, [M]; + [M;M], Ge, []; + [M], Le, [M]; + [M], Ge, [M]; + (* classical + [M;M], Le, []; + [C;M], Ge, [M;I]; + *) ] ;; -let print_w w = +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 = + function + [] -> dir + | M::tl -> new_dir (swap dir) tl + | (C|I)::tl -> new_dir dir tl +;; + +let string_of_w w = String.concat "" (List.map (function I -> "i" | C -> "c" | M -> "-") w) ;; -let print_eqclass eqc = - let eqc = List.sort compare eqc in - prerr_endline (String.concat "=" (List.map print_w eqc)) +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 print = List.iter print_eqclass;; +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 apply_rule_at_beginning (lhs,rhs) l = - let rec aux = - function - [],l -> l - | x::lhs,x'::l when x = x' -> aux (lhs,l) - | _,_ -> raise NoMatch +let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2;; + +let uniq l = + 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 - rhs @ aux (lhs,l) + List.rev (aux [] (List.sort compare l)) +;; + +let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) = + if dir <> dir' then + raise NoMatch + else + let rec aux = + 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) +and apply_rules (w,_ as w_and_dir) = + if w = [] then [[]] + else + let rec aux = + function + [] -> [] + | rule::tl -> + (try apply_rule_at_beginning rule w_and_dir + with NoMatch -> []) + @ + aux tl + in + aux rules ;; -let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2 +let apply_rules (w,dir as w_and_dir) = + List.map (fun w' -> w,dir,w') + (uniq (apply_rules w_and_dir)) ;; -let rec apply_rule rule w = - (try - [apply_rule_at_beginning rule w] - with - NoMatch -> []) @ - match w with - [] -> [] - | he::tl -> [he] @@ apply_rule rule tl +let step (l : w list) = + uniq + (List.flatten + (List.map + (function w -> + List.map (fun x -> x@w) + (if List.length (List.filter (fun w -> w = M) w) >= 2 then + [[I];[C];[]] + else + [[I];[C];[M];[]]) + ) l)) ;; -let uniq = - let rec aux l = +let mapi f l = + let rec aux acc i = function - [] -> l - | he::tl -> aux (if List.mem he l then l else he::l) tl + [] -> 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 [] + let res = List.rev (aux [] 1 l) in + print_newline (); + res ;; -let apply_rules w = - let rec aux = +let iteri f l = + let rec aux i = function - [] -> [w] - | rule::rules -> apply_rule rule w @ aux rules + [] -> () + | 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 - uniq (aux rules) + aux 1 l; + print_newline (); ;; -let subseteq l1 l2 = - List.for_all (fun x -> List.mem x l2) l1 +let normalize (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 (===) l1 l2 = subseteq l1 l2 && subseteq l2 l1;; +let visualize graph = + let module G = + struct + include G;; + let edge_attributes _ = [] + let default_edge_attributes _ = [] + let get_subgraph _ = None + 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 + let module D = Graph.Graphviz.Dot(G) 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 simplify eqc = - let rec aux l = - let l' = uniq (List.flatten (List.map apply_rules l)) in - if l === l' then l else aux l' - in - aux eqc +let mk_vertex () = + let cache1 = Hashtbl.create 5393 in + (function w -> + try + Hashtbl.find cache1 w + with + Not_found -> + let v = G.V.create w in + Hashtbl.add cache1 w v; + v) ;; -let combine_class_with_classes l1 = - let rec aux = - function - [] -> [l1] - | l2::tl -> - if List.exists (fun x -> List.mem x l2) l1 then - uniq (l1 @ l2) :: tl - else - l2:: aux tl - in - aux +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 combine_classes l = - let rec aux acc = - function - [] -> acc - | he::tl -> aux (combine_class_with_classes he acc) tl - in - aux [] l -;; - -let step (s : eqclass list) = - let ns = ref [] in - List.iter (function eqc -> ns := eqc::!ns) s; - List.iter - (function eqc -> - List.iter - (function x -> - let eqc = simplify ([x] @@ eqc) in - if not (List.exists (fun eqc' -> eqc === eqc') !ns) then - ns := eqc::!ns - ) [I;C;M] - ) s; - combine_classes !ns -;; - -let classes = step (step (step (step [[[]]]))) in - prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes)); - print classes +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 = + 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), + (function () -> + let vertexes = uniq (Hashtbl.fold (fun k _ l -> k::l) cache []) in + let xx = + mapi + (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 = + function + [] | [_] -> true + | _::w -> + try Hashtbl.find canonicals w; true with Not_found -> false + in + iteri + (function (v,x) -> + 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 = 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) -> G.add_edge graph x y) varcs; + print_endline (""); + 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,varcs +;; + +let analyze (norm,arcs) = + print_endline ("building class graph (" ^ string_of_int (List.length 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 (); + let cgraph = G.create () in + let mk_vertex = mk_vertex () in + List.iter + (function (x,y) -> + if x <> y then + G.add_edge cgraph (mk_vertex (describe x)) (mk_vertex (describe y))) arcs; + print_endline "visualize"; + visualize cgraph; + print_endline ("/////"); +;; + +let rec iter n l = + let pkg = classify (normalize l) in + if n > 0 then + iter (n - 1) (step l) + else + analyze pkg +in + iter 10 [[]] ;;