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];
 ]
;;

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_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 print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));;

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
 in
  aux [] 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 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.mem M w then
         [[I];[C];[]]
        else
         [[I];[C](*;[M]*);[]])
     ) l))
;;

let leq rels x y =
 let rec aux avoid x y =
  x = y ||
   List.exists
    (fun (x',z) -> x=x' && not (List.mem z avoid) && aux (z::avoid) z y) rels
 in
  aux [x] x y
;;

let in_class rels eqc he =
 match eqc with
    [] -> assert false
  | k::_ -> leq rels k he && leq rels he k
;;

let add_class rels classes he =
prerr_endline "Add";
 let rec aux visited =
  function
     [] -> [he]::visited
   | eqc::tl ->
      if in_class rels eqc he then
       (he::eqc)::tl@visited
      else
       aux (eqc::visited) tl
 in
  aux [] classes
;;

let classify (l : w list) =
prerr_endline ("Classify: " ^ string_of_int (List.length l));
 let rels =
  List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
 in
  uniq
   (List.map
    (function (x,rel,y) -> match rel with Le -> x,y | Ge -> y,x) rels)
;;

let visualize graph =
  let dot = "" in
  (*Graph.Pack.Digraph.dot_output graph dot;*)
  Graph.Pack.Digraph.display_with_gv graph;
exit 1;
(*
  let ch = open_out "/tmp/comb.dot" in
   output_string ch dot;
   close_out ch;
   Unix.system ("tred /tmp/comb.dot > /tmp/red.dot");
   Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps");
   Unix.system ("ggv /tmp/red.ps");
*) ()
;;

let analyze arcs =
 let mk_vertex =
  let cache = ref [] in
  function w ->
   try
    List.assoc w !cache
   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
prerr_endline (string_of_w w ^ " => " ^ string_of_int n);
      let v = Graph.Pack.Digraph.V.create n in
       cache := (w,v)::!cache;
       v in
 let graph = Graph.Pack.Digraph.create () in
 List.iter
  (function (x,y) ->
    Graph.Pack.Digraph.add_edge graph (mk_vertex x) (mk_vertex y)) arcs;
prerr_endline ("<CLASSI>");
 let classes =  Graph.Pack.Digraph.Components.scc_list graph in
List.iter (function l -> prerr_endline (String.concat "=" (List.map string_of_int (List.map Graph.Pack.Digraph.V.label l)))) classes;
prerr_endline ("</CLASSI>");
 let classes,normalize =  Graph.Pack.Digraph.Components.scc graph in
prerr_endline (string_of_int classes ^ " CLASSI");
 let arcs = uniq (List.map (fun (x,y) -> normalize (mk_vertex x),normalize (mk_vertex y)) arcs) in
 let cgraph = Graph.Pack.Digraph.create () in
 List.iter
  (function (x,y) ->
    Graph.Pack.Digraph.add_edge cgraph (Graph.Pack.Digraph.V.create x) (Graph.Pack.Digraph.V.create y)) arcs;
 visualize cgraph
;;

let rec iter n l =
 let arcs = analyze (classify l) in
 (*print_graph' (analyze arcs);*)
 if n > 0 then
  iter (n - 1) (step l)
in
 iter 4 [[]]
;;