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

let classify (l : w list) =
 List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
;;

let print_graph =
 List.iter
  (function (w,dir,w') ->
    prerr_endline (string_of_w w ^ string_of_dir dir ^ string_of_w w'))
;;

print_graph (classify (step (step (step [[]]))));;

(*
 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 subseteq l1 l2 =
 List.for_all (fun x -> List.mem x l2) l1
;;

let (===) l1 l2 = subseteq l1 l2 && subseteq l2 l1;;

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 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 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
;;
*)