(* ouverture du module Ast.cmi *)
open Ast


(* transforme un arbre en chaine lisible *)
let rec pretty_print res = match res with
    Atom(s)    -> "`" ^ s
  |Not(e)      -> "NON(" ^ pretty_print(e) ^ ")"
  |And(e1,e2)  -> "(" ^ pretty_print(e1) ^ " ET " ^ pretty_print(e2) ^ ")"
  |Or(e1,e2)   -> "(" ^ pretty_print(e1) ^ " OU " ^ pretty_print(e2) ^ ")"
  |Imp(e1,e2)  -> "(" ^ pretty_print(e1) ^ " IMPLIQUE " ^ pretty_print(e2) ^ ")"
  |Eq(e1,e2)   -> "(" ^ pretty_print(e1) ^ " EQUIVALENT " ^ pretty_print(e2) ^ ")"


(* transforme un arbre en arbre disjonctif *)
let rec disj a = match a with
    Atom(s)          -> Atom(s)
  |Not(Atom(s))      -> Not(Atom(s))
  |Not(Not(e))       -> disj(e)
  |Not(And(e1,e2))   -> Or( disj(Not(disj(e1))) , disj(Not(disj(e2))) )
  |Not(Or(e1,e2))    -> disj(And( disj(Not(disj(e1))) , disj(Not(disj(e2))) ))
  |Not(e1)           -> disj(Not(disj(e1)))

  |And(Atom(s1),Atom(s2)) -> And(Atom(s1),Atom(s2))
  |And(Or(e1,e2),e3)      -> Or( disj(And(disj(e1),disj(e3))) , disj(And(disj(e2),disj(e3))) )
  |And(e3,Or(e1,e2))      -> Or( disj(And(disj(e1),disj(e3))) , disj(And(disj(e2),disj(e3))) )
  |And(e1,e2)             -> And(disj(e1),disj(e2))

  |Imp(e1,e2)             -> Or( disj(Not(disj(e1))) , (disj(e2)) )
  |Eq(e1,e2)              -> Or( disj(And((disj(e1)),(disj(e2)))) , disj(And((disj(Not(disj(e1)))),(disj(Not(disj(e2)))))) )
  |Or(e1,e2)         -> Or(disj(e1),disj(e2))


(* transforme un arbre disjonctif en liste *)
let rec tree_to_list a = match a with
    Atom(s)     -> s::[]
  |Or(e1,e2)    -> (tree_to_list(e1))@(tree_to_list(e2))
  |And(e1,e2)   -> ((tree_to_list(e1))@(tree_to_list(e2)))
  |Not(Atom(s1))      -> ("!" ^ s1) :: []

(* cherche si l'inverse (conjugué) de e est dans l2 *)
let rec inv_in e l2 = match l2 with
    []  -> false
  |h::t when (h = ("!" ^ e)) or (("!" ^ h) = e) -> true
  |h::t -> inv_in e t

(* vérifie si la sous liste est satisfiable *)
let rec sat2 l = match l with
    []  -> false
  |h::t when inv_in h t -> false
  |h::t -> sat2(t)


(* vérifie si la liste de liste est satisfiable *)
let rec satisfiable l = match l with
    []  -> false
  |h::t when sat2(h) = false -> satisfiable(t)
  |h::t when sat2(h) = true  -> true


(* programme principal *)
let _ =
   try
    (* ouverture du channel sur l'entree standard stdin *)
    let lexbuf =
      Lexing.from_channel stdin
    in
      (* boucle sur les expressions *)
      while true do
	(* result contient l'arbre obtenu *)
	let result = Parser.main Lexer.token lexbuf in

	  (* Affichage du résultat *)

	  print_string ("resultat en toutes lettres : " ^ (pretty_print result));
	  print_string "\n";

	  print_string "forme disjonctive : " ;
	  print_string (pretty_print(disj(result))) ;
	  print_string "\n" ; 

	  print_string "expression satisfiable : " ;
	  if satisfiable(tree_to_list(disj(result))) = true then print_string "OUI"
	  else print_string "NON";
	  print_string "\n" ;

      done

	(* le lexer leve l'exception Lexer.Eof lorsque la fin de fichier est
	   atteinte (Ctrl D sur l'entree standard) *)
  with Lexer.Eof -> exit 0