(* State properties with explanation *)

type 'state similarity_explanation = Similar_wrt of 'state * 'state * string

type 'state similarity_criterion = 'state -> bool

type 'state property = bool * 'state similarity_criterion * 'state similarity_explanation


(* Logical connectors on state properties *)

let ( (|&|) : 'state property -> 'state property -> 'state property) = 
  fun (b1,sc1,e1) (b2,sc2,e2) -> if b1 then (b2,sc2,e2) else (b1,sc1,e1)

let ( (|||) : 'state property -> 'state property -> 'state property) = 
  fun  (b1,sc1,e1) (b2,sc2,e2) -> if b1 then (b1,sc1,e1) else (b2,sc2,e2)

let rec (justified_forall_in: 't list -> ('t -> 'state property) -> 'state property) = 
  fun l pred ->
	match l with
	| [] -> (true, (fun _ -> true), Similar_wrt(0,0,"forall {}") )
	| x::xs -> (pred x) |&| (justified_forall_in xs pred)


(* Explanation of the construction of equivalence classes *)

let (explain: ('state -> string) -> 'state similarity_criterion -> 'state similarity_explanation -> string) = 
  fun pretty like_q1 -> 
	function Similar_wrt(q1,q2,criterion_description) ->
	      String.concat " "
		[ "states" ; pretty q1 ; "~/~" ; pretty q2 
		; if like_q1 q2 then ":" else ": NOT" 
	        ; criterion_description
		] 


(* Equivalence classes *)

type 'state eq_class = 'state set 

type 'state partition = ('state eq_class) set

let (pretty_eq_class: ('state -> string) -> 'state eq_class -> string) = 
  fun pretty_state -> prettys "{" "," "}" pretty_state ;;

let (pretty_partition: ('state -> string) -> 'state partition -> string) = 
  fun pretty_state -> prettys "{ " " , " " }" (pretty_eq_class pretty_state) ;;
	

(* Do two states belong to the same equivalence class in a given partition ? *)

let (together_in: 'state partition -> 'state -> 'state -> bool) = 
  fun partition q1 q2 ->
	List.mem q2 (List.find (fun eqc -> List.mem q1 eqc) partition)

(* Does state q1 behaves like state q2 on symbol s ? *)

let (behave_like_on_symbol: 'state automaton -> 'state partition -> 'state -> 'state -> symbol -> bool) = 
  fun aut partition q1 q2 symbol ->
	let targets1 = targets_of (get_transitions (On[symbol]) (get_transitions (From [q1]) aut.transitions))
	and targets2 = targets_of (get_transitions (On[symbol]) (get_transitions (From [q2]) aut.transitions))
	in forall_in targets1 (fun tgt1 -> 
	      exists_in targets2 (fun tgt2 -> 
		    together_in partition tgt1 tgt2 ))

let rec (equiv_wrt: 'state automaton -> 'state partition -> 'state -> 'state -> 'state property) = 
  fun aut partition q1 q2 ->
	(q1 = q2, (=) q1, Similar_wrt(q1,q2,"identical") )
  	 |||
        (let acc_like = fun q1 q2 -> (List.mem q1 aut.accepting) = (List.mem q2 aut.accepting)
	 in (* result      , criterion  , explanation *)
	    (acc_like q1 q2, acc_like q1, Similar_wrt(q1,q2,"same accepting status") )
	     |&|
	    (justified_forall_in aut.alphabet (fun symbol ->
		let simulate = fun q1 q2 -> behave_like_on_symbol aut partition q1 q2 symbol 
		in (* result      , criterion  , explanation *)
		   (simulate q1 q2, simulate q1, Similar_wrt(q1,q2,"same behavior on symbol '" ^ symbol ^ "'"))
                    |&|
                   (simulate q2 q1, simulate q2, Similar_wrt(q2,q1,"same behavior on symbol '" ^ symbol ^ "'")) )
	    )
	)

(* Refinement of a equivalent classes with respect to a separation criterion *)

let (refine_eq_class_wrt: 'state automaton -> 'state partition -> 'state eq_class -> ('state eq_class) list) = 
  fun aut partition eqc ->
	let (all_equivalent,criterion,explanation) = 
	  justified_forall_in eqc (fun q1 ->
		justified_forall_in eqc (fun q2 ->
		      equiv_wrt aut partition q1 q2))
	in
	  if all_equivalent 
	  then [ eqc ] 
	  else 
            let (eqc1,eqc2) = List.partition criterion eqc in
            begin
              print_string 
		(String.concat " "
	      	 [ "\n"
                 ; explain pretty_state criterion explanation 
                 ; "\n"
                 ; "So," 
                 ; pretty_eq_class pretty_state eqc 
                 ; " is splitted into " 
                 ; pretty_eq_class pretty_state eqc1 ; "|_|" ; pretty_eq_class pretty_state eqc2 
		 ; "\n" 
                 ]) ; 
	      [eqc1 ; eqc2]
            end

(* One round of refinement *)

type 'state refineable_partition = (* processed *) ('state eq_class) list * ('state eq_class) list (* to process *)

let (refine_wrt: 'state automaton -> 'state partition -> 'state partition) = 
  fun aut partition -> 
	let rec (one_round_of_refinment: 'state refineable_partition -> 'state partition) = 
	  function
	    | (processed_eqcs, []) -> processed_eqcs
	    | (processed_eqcs, eqc::other_eqcs) -> 
		    let partition = processed_eqcs @ (eqc::other_eqcs)
		    in let refined_eqcs = refine_eq_class_wrt aut partition eqc
		    in one_round_of_refinment (processed_eqcs @ refined_eqcs, other_eqcs)
	in
	  one_round_of_refinment ([],partition) 


(* Fixpoint of a function f computed by iteration of f on an inital approximation x *)

let rec (fixpoint: ('t ->'t) -> 't -> 't) = 
  fun f x -> let x' = f x in if x'=x then x else fixpoint f x'


(* Computing the equivalence classes on states *)

let (eq_classes: 'state automaton -> 'state partition) = 
  fun aut ->
	let initial_partition = [ (states_of aut.transitions) ]
	in
	  begin
	    print_string (String.concat " " 
               [ "\nMinimisation:" 
               ; "\n\n" 
               ; "* initial partition =" ; pretty_partition pretty_state initial_partition 
               ; "\n"
	       ]) ;
	    let final_partition = List.sort Pervasives.compare (fixpoint (refine_wrt aut) initial_partition)
	    in 
	      begin
		print_string (String.concat " " 
		   [ "\n"
                   ; "* final partition =" ; pretty_partition pretty_state final_partition  
                   ; "\n\n"
                   ]) ;
		final_partition
	      end
	  end
	    
let (* USER *) (automaton_induced_by: 'state partition -> 'state automaton -> ('state eq_class) automaton) = 
  fun partition aut ->
	let (covering_classes_of: 'state set -> ('state eq_class) set) = fun states -> 
	      List.filter (fun eqc -> Set.intersect eqc states) partition
	in 
	    { aut with
              name = "Induced(" ^ aut.name ^ ")" ;
	      initial   = covering_classes_of aut.initial ;
	      accepting = covering_classes_of aut.accepting ;
              transitions = 
                 foreach_in partition (fun eqc ->
		    foreach_in aut.alphabet (fun symbol ->
                       foreach_in (covering_classes_of (targets aut eqc symbol)) (fun tgt_eqc -> 
				[ (eqc,symbol,tgt_eqc) ] )))
	    }  

(* Minimization of (deterministic/non-deterministic) automata *)

let (* USER *) (minimization: 'state automaton -> std automaton) =
  fun aut ->
	let partition = eq_classes aut
	in let min_aut = automaton_induced_by partition aut
	in let (indexed_partition,std_min_aut) = rename min_aut
	in std_min_aut



let (* USER *) (explained_minimization: 'state automaton -> std automaton) =
  fun aut ->
	let partition = eq_classes aut
	in let min_aut = automaton_induced_by partition aut
	in let (indexed_partition,std_min_aut) = rename min_aut
	in
	  begin
	    print_string (String.concat " "
              [ "Renaming of eq. classes:" 
	      ; Set.pretty_indexed_set (pretty_eq_class pretty_std_state) indexed_partition 
              ; "\n\n"
              ]) ;
	    std_min_aut
	  end