(* 0: 7       4
   1: 29      6
   2: 120    10
   3: > 327  >9
   4: > 657  >9
   5: > 526  >8
   6: > 529  >8
   7: > 529  >8
   8: > 529  >8
*)

type t = M | I | C
type w = t list
type eqclass = w list

type dir = Le | Ge

let rules =
 [ [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 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 =
 function
    [] -> dir
  | M::tl -> new_dir (swap dir) tl
  | (C|I)::tl -> new_dir dir tl
;;

let string_of_w 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;;

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
  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
  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
  let rec aux =
   function
      [] -> []
    | rule::tl ->
       (try apply_rule_at_beginning rule w_and_dir
        with NoMatch -> [])
       @
       aux tl
  in
   aux rules
;;

let apply_rules (w,dir as w_and_dir) =
 List.map (fun w' -> w,dir,w')
  (uniq (apply_rules w_and_dir))
;;

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) >= 1 then
         [[I];[C]]
        else
         [[I];[C];[M]])
     ) l))
;;

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 iteri f l =
 let rec aux i =
  function
     [] -> ()
   | 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 1 l;
  print_newline ();
;;

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 =
  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
  uniq arcs
;;

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 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 nodes old_arcs =
 print_endline ("STEP " ^ string_of_int n);
 let arcs = old_arcs @ normalize nodes in
 let pkg = classify arcs in
 if n > 0 then
  iter (n - 1) (step nodes) arcs
 else
  analyze pkg
in
 iter 7 [[]] []
;;