+(* 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 ("<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,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 [[]]
;;
projects / helm.git / blobdiff