+(* 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
[M;M], Ge, [];
[M], Le, [M];
[M], Ge, [M];
+ (* classical
+ [M;M], Le, [];
+ [C;M], Ge, [M;I];
+ *)
]
;;
+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 =
| (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 string_of_w' w =
+ String.concat ""
+ (List.map (function I -> "i" | C -> "c" | M -> "m") w)
;;
-let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));;
+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;;
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) =
uniq
(List.flatten
(List.map
- (function w -> List.map (fun x -> x@w) [[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
- in
- aux [x] x y
+ (function w ->
+ List.map (fun x -> x@w)
+ (if List.length (List.filter (fun w -> w = M) w) >= 3 then
+ [[I];[C];[]]
+ else
+ [[I];[C];[M];[]])
+ ) l))
;;
-let in_class rels eqc he =
- match eqc with
- [] -> assert false
- | k::_ -> leq rels k he && leq rels he k
+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
+ 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 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)
+ List.flatten
+ (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in
+ let arcs =
+ 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
- let rec aux classes =
- function
- [] -> classes
- | he::tl -> aux (add_class rels classes he) tl
- in
- aux [] l
+ uniq arcs
;;
-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 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 = G.V.label 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 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 graph = G.create () in
+ iteri (fun (x,y) -> G.add_edge graph x y) arcs;
+ print_endline ("<scc>");
+ 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,arcs
+;;
+
+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 ();
+ 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 cgraph;
+ print_endline ("/////");
;;
let rec iter n l =
- print_graph' (classify 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 4 [[]]
+ iter 15 [[]]
;;
projects / helm.git / blobdiff