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

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

let print_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 print = List.iter print_eqclass;;

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
 in
  rhs @ aux (lhs,l)
;;

let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2
;;

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 uniq =
 let rec aux l =
  function
     [] -> l
   | he::tl -> aux (if List.mem he l then l else he::l) tl
 in
  aux []
;;

let apply_rules w =
 let rec aux =
  function
     [] -> [w]
   | rule::rules -> apply_rule rule w @ aux rules
 in
  uniq (aux rules)
;;

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