(**************************MODE D'EMPLOI**************************************Romain Sahut 2A1**********

 Analyser:                 pro EXPRESSION     EXPRESSION: l'expression a évaluer entre parentheses.
 Developper et lineariser: red EXPRESSION \
 Apparition des consensus: css EXPRESSION  }-  rea, csa et asa pour une sortie formatée
 Absorber les redondances: asp EXPRESSION /

Les symboles permis sont :
	* : le "et" logique
	+ : le "ou" logique
	! : le "non" logique
	(): les parentheses

Les variables sont composees d'une ou plusieurs lettres (Attention : a n'est pas la meme variable que A).
Les blancs ne sont pas significatifs.
Vous pouvez appeler cette aide par la fonction help().                                                *)




type lexeme = Plus
	      |Fois
	      |Non
	      |ParG
	      |ParD
	      |Nom of string
	      |Cste of int
;;

let rec nbl = function
  [< '` `|`\n`|`\r`|`\t` ; nbl _ >] -> ()
  |[<>] -> ()
;;

let rec lire_nom = function
  [< '`A`..`Z`|`a`..`z` as c ; lire_nom n >] -> string_of_char c^n
  |[< nbl _ >] -> ""
and lire_cste = function
  [< '`0`|`1` as c ; lire_cste n >] -> string_of_char c^n
  |[< nbl _ >] -> ""
;;

let rec lexemiser = function
  [< '`+` ; nbl _ ; f >] -> [< 'Plus ; lexemiser f >]
  |[< '`!` ; nbl _ ; f >]-> [< 'Non ; lexemiser f >]
  |[< '`*` ; nbl _ ; f >] -> [< 'Fois ; lexemiser f >]
  |[< '`(` ; nbl _ ; f >] -> [< 'ParG ; lexemiser f >]
  |[< '`)` ; nbl _ ; f >] -> [< 'ParD ; lexemiser f >]
  |[< '`A`..`Z`|`a`..`z` as c ; lire_nom n ; f >] -> [< 'Nom (string_of_char c^n); lexemiser f >]
  |[< '`0`|`1` as c ; lire_cste n ; f >] -> [< 'Cste (int_of_string (string_of_char c^n)); lexemiser f >]
  |[< 'c >] -> failwith "Vous avez tapé un caractére inconnu... Corrigez!"
  |[<>] ->[<>]
;;

let lexe = function
  [< nbl _ ; f >] -> lexemiser f;;

let lex s = lexe (stream_of_string s);;

type arbre = ET of arbre * arbre
      	       |OU of arbre * arbre
	       |NON of arbre
	       |Var of string
	       |Val of int
      	       |Err;;

let rec somme = function
  [< 'Plus ; terme t  ; (fin_somme t) s >] -> s
  |[< terme t  ; (fin_somme t) s >] -> s
and fin_somme t  = function
  [< 'Plus ; terme e ; (fin_somme (OU(t,e))) s >] -> s 
  |[<>] -> t
and terme = function 
  [< facteur f ; (fin_produit f) t >] -> t 
and fin_produit f = function	
  |[< 'Fois ; facteur r ; (fin_produit (ET(f,r))) t >] -> t
  |[<>] -> f
and facteur = function
  [< 'Nom n >] -> Var n 
  |[< 'Cste c >] -> Val c
  |[< 'Non ; facteur f >] -> NON f
  |[< 'ParG ; somme s ; parenr _ >] -> s
  |[<>] -> failwith "Caractere inconnu ou mal placé... Corrigez!"
and parenr = function
  [< 'ParD >] -> ()
  |[<>] -> failwith "Manque parenthese fermante... Corrigez!"
and vide = function
  [< 'c >] -> failwith "L'expression n'est pas correcte... Recommencez!"
  |[<>] -> ()
and analyse = function
  [< somme s ; vide _ >] -> s
and pro s =
  analyse (lex s)
;;

 (*repousse les NON devant les vriables et valeurs *)
let rec repousser_NON = function 
       ET(a,b) -> ET(repousser_NON a , repousser_NON b )
     | OU(a,b) -> OU(repousser_NON a , repousser_NON b )
     | NON(ET(a,b)) -> OU(repousser_NON (NON a) , repousser_NON (NON b))
     | NON(OU(a,b)) -> ET(repousser_NON (NON a) , repousser_NON (NON b))
     | NON(NON(a)) -> repousser_NON a
     | NON(Val 1) -> Val 0
     | NON(Val 0) -> Val 1
     | a -> a
 ;;
 let repp s = repousser_NON(pro s);;
 
  (* developpe afin d'obtenir une somme de produits *)
 let rec developpe = function 
      OU(a,b) -> OU(developpe a , developpe b) 	     	 
    | ET(OU(a,b),c) -> 
          OU( developpe (ET(a ,c)) , developpe (ET(b ,c)))
    | ET(c,OU(a,b)) -> 
 	 OU( developpe (ET(c,a)) , developpe (ET(c,b)))
    | ET(a,b) ->( match (developpe a,developpe b) with
 	 (x,y) when (x=a && y=b) -> ET(x,y)
 	 | (x,y) -> developpe (ET(x,y))
 	 )
    | a -> a
;;
 

(* Simplifie l'arbre tant que cela est possible en enlevant les valeurs parasites ( ET(Val 0,Var a) -> Val 0 ) *)
 let rec simplifie = function 
      OU(a,Val 0) -> simplifie a	 
      |OU(Val 0,a) -> simplifie a	
      |OU(a,b) -> OU (simplifie a,simplifie b)
      |ET(Val 1,a) -> simplifie a
      |ET(a,Val 1) -> simplifie a 
      |ET(Val 0,a) -> Val 0
      |ET(a,Val 0) -> Val 0 
      |ET(a,b) -> ET (simplifie a,simplifie b) 
      |a -> a
;;
let dev s = simplifie(developpe (repp s));;


 
let rec lineariser_o = function
   OU(a,b) -> conjonction (lineariser_o a) (lineariser_o b)
   | Err -> failwith " Erreur "	
   | a -> [lineariser_e a]
   and conjonction = fun
       lg [] -> lg
       | [] ld -> ld
       | (tg::lg) (td::ld) when tg=td -> tg::conjonction lg ld
       | (tg::lg) (td::ld) -> tg::td::conjonction lg ld
   and lineariser_e = function
       ET(a,b)-> disjonction (lineariser_e a) (lineariser_e b)
       | NON(Var a) ->  ["!"^a] 
       | Var a -> [a]
       | Val a -> [string_of_int(a)]
       | _ -> failwith "Erreur de linearisation -> type non reconnu"
   and disjonction = fun
       lg [] -> lg
       | [] ld -> ld
       | (tg::lg) (td::ld) when tg=td -> tg::disjonction lg ld
       | (tg::lg) (td::ld) -> tg::td::disjonction lg ld
;;
let red s = lineariser_o (dev s);;



let negation = function	(*Retourne l'inverse d'un monome*)
	"0" -> "1"
	|"1" -> "0"
      	|a when (eq_string (sub_string a 0 1) "!") -> sub_string a 1 ((string_length a)-1) 
      	|a -> "!"^a
;;
let rec appartient x = function (*VRAI si l'element x appartient a la liste passee en argument *)
	[] -> false
	|t::q when x=t -> true
	|t::q -> appartient x q
;;
let rec appartient_tous l = function (*VRAI si la 2eme liste d'elements est incluse dans la premiere *) 
	[] -> true
	|t::q when appartient t l -> appartient_tous l q
	|t::q -> false
;;
let rec retirer x = function (*Permet de retirer tous les elements x d'une liste l*)
	[] -> []
	|t::q when x=t -> retirer x q
	|t::q -> t::retirer x q
;;
let rec identique lg ld =  (*Verifie que 2 listes sont identiques*)
	(appartient_tous lg ld)&&(appartient_tous ld lg)	
;;
let rec contradiction = function (* Si dans la liste d'elements il y a 2 termes contradictoires, c'est que le terme vaut 0 *)
	[] -> []
	|t::q when appartient (negation t) (contradiction q) -> ["0"] 
	|t::q when (appartient t q) -> contradiction q 
	|t::q -> t::(contradiction q)
;;
let rec appartient_liste l = function (*VRAI si la liste l est incluse dans la liste de listes passee en 2eme parametre *)
	[] -> false
	|t::q when identique l t -> true  
	|t::q -> appartient_liste l q
;;
let rec appartient_tous_liste l = function (*VRAI si la liste de listes d'elements passee en second parametre est incluse dans la premiere *) 
	[] -> true
	|t::q when appartient_liste t l -> appartient_tous_liste l q
	|t::q -> false
;;	



let rec aspiration = function   (* Parcours et debut de l'absorption des termes redondants *)
	[] -> []
	|t::q -> aspiration2 t (aspiration q) 
and aspiration2 = fun           (* Absorption des termes redondants *)
	t [] -> [t]
	|t (i::q) when appartient_tous t i -> i::q
	|t (i::q) when appartient_tous i t -> aspiration2 t q
	|t (i::q) when appartient "0" i -> aspiration2 t q
	|t (i::q) -> i::(aspiration2 t q)
;;



(*demarrage prend la liste de linearise et fait un parcours
    prend le 1er element et le 2eme element et fait cherchecss
      si trouve -> on continue
      si pas trouve -> on continue
    prend le 1er element de la liste et le 3eme et fait cherchecss
    qd queue vide, on passe au 2eme element et jusqu'a la fin *)
let rec appliquecss = function  (*   Parcours et debut recherche consensus *)
	[] -> []
	|t::[] -> [contradiction t]   (* t est une liste *)
	|t::q -> (contradiction  t)::(cherchecss (contradiction t) (appliquecss q)) (*q est 1 liste de liste*)
and cherchecss = fun   (* parcours, recherche et inclusion des consensus *)
	[] [] -> []
      	|lg [] -> [lg]
	|lg (t::q) when (verif_cons (lg@(contradiction t)))=1 -> (contradiction t)::(contradiction (ret_cons (lg@t)))::(cherchecss lg q) 
	|lg (t::q) -> (contradiction t)::(cherchecss lg q)
and verif_cons = function(* prend en param une concatenation de 2 listes et combien il y a de termes contratictoires *)
	[] -> 0
	|(t::q) when (appartient (negation t) q) -> (verif_cons q)+1
	|(t::q) -> verif_cons q
and ret_cons = function  (* prend en param une concatenation de 2 listes avec 2 termes contratictoires et renvoie la liste sans les termes *)
	[] -> []
	|t::[] -> [t]
	|t::q when (appartient (negation t) q) -> simpli (retirer (negation t) (retirer t q))
	|t::q -> t::(ret_cons q)
and simpli = function    (* prend en parametre une liste d'elements et retire les doublons *)
	t::q when (appartient t q) -> simpli q
	|t::q -> t::(simpli q)
	|a -> a
;;

		
(* Fonction qui verifie qu'il n'y a plus de consensus à trouver en comparant la liste passee en parametre
	et la liste obtenue apres methode des consensus *)
let rec verification = function
	[] -> []
	|l when (appartient_tous_liste l (aspiration (appliquecss l)))&&(appartient_tous_liste (aspiration (appliquecss l)) l) -> l
	|l -> verification (aspiration (appliquecss l))
;;
		


let css s =verification (red s);; (*la liste et tous les consensus sans redondances*)
let asp s = aspiration (css s);;




(* Fonction qui affiche la liste *)
let rec affiche = function
  [] -> ()
  |t::[] -> print_string("   ");
	affichel t;
      	    print_string("\n")
  |t::q -> print_string("   ");
	   (affichel t);
      	   print_string("   +");
      	   (affiche q)
and affichel = function
  [] -> ()
  |t::[] -> print_string(t)
  |t::q -> print_string(t);
      	   print_string(" * ");
      	   affichel q  
;;
(* Fonctions qui permettent d'afficher les resultats intermediaires a differentes etapes *)
let rea s = affiche (red s);;
let csa s = affiche (css s);;
let asa s = affiche (asp s);;


(*Fonction non indispensable mais tres pratique!*)
let help = function
  a -> print_string ("\n
  Analyser:                 pro EXPRESSION     EXPRESSION: l'expression a évaluer entre parentheses.
  Developper et lineariser: red EXPRESSION \\
  Apparition des consensus: css EXPRESSION  }-  rea, csa et asa pour une sortie formatée
  Absorber les redondances: asp EXPRESSION /
\nLes symboles permis sont :\n\t* : le \"et\" logique\n\t+ : le \"ou\" logique\n\t! : le \"non\" logique\n\t():"); 
print_string(" les parentheses\n\nLes variables sont composees d'une ou plusieurs lettres (Attention : a n'est pas la meme variable que A)
Les blancs ne sont pas significatifs.\n\nVous pouvez rappeler cette aide par la fonction help().\n")
;;
help();;


(*Des tests pour faire mouliner l'ordinateur*)
rea "g*d*!f*!e*(a+!a*b)*!(d*(r*f+!g*f*s))*!r";;
csa "g*d*!f*!e*(a+!a*b)*!(d*(r*f+!g*f*s))*!r";;
asa "g*d*!f*!e*(a+!a*b)*!(d*(r*f+!g*f*s))*!r";;
asa "!(a*!(b*c+d+!c)+b*!a)";;
asa "a+!a*b+b*f*d*g*t*e+d*f*e*s*!g";;
asa "!(a*b*c+a*b*d)*!(!a+!b+!(c+d))+a*b*(c+d)*(!a+!b+!(c+d))";;
asa "!a*!b+a*!b";;
asa "!(a*b*c+a*b*d)*!(!a+!b+!(c+d))+a*b*(c+d)*(!a+!b+!(c+d))+b";;
asa "!a*!c+!a*b*c+a*!b*!c+a*b*d+!b*c*!d+!a*!b*!c";;