type 'a prop =
  | Top 
  | Bot 
  | V of 'a 
  | Et of 'a prop * 'a prop 
  | Ou of 'a prop * 'a prop 
  | Non of 'a prop
  | Implique of 'a prop * 'a prop 
;;

let e  = Non (Ou (Et (V "a", V "b"), Et (V "a", V "c"))) ;;

let f1 = Implique (Et (V "c", Non (V "a")), Ou (V "b", Implique (V "c", V "a"))) ;;

let f2 = Ou (Implique (V "b", Implique (V "c", V "a")), Ou (Non (V "c"), V "a")) ;;

let f3 =
  Ou (Et (V "a", V "b"),
      Ou (V "c",
          Ou (Non (Et (V "b", Non (V "c"))), Ou (Non (V "a"), Non (V "c")))))
;;

let f4=
  Ou (Et (V "a", V "b"),
      Ou (V "c",
          Ou (Et (Non (V "b"), Non (V "c")), Ou (Non (V "a"), Non (V "c"))))) ;;

let f5 =
  Ou (V "a",
      Ou (Et (Non (V "b"), Non (V "c")),
          Ou (Et (Non (V "a"), V "c"), Et (V "b", Non (V "c")))))
;;

(* Q1 *)

let rec hauteur f = match f with
  | Top | Bot | V _ -> 0
  | Non(f') -> 1 + hauteur f'
  | Et(g,d) | Ou(g,d) | Implique(g,d) -> 1 + max (hauteur g) (hauteur d)
;;

hauteur e ;;

(* Q2*)

let rec longueur f = match f with
  | Top | Bot | V _ -> 1
  | Non(f') -> 1 + longueur f'
  | Et(g,d) | Ou(g,d) | Implique(g,d) -> 1 + longueur g + longueur d
;;

longueur e ;;

(* Q3 *)

let rec concat l1 l2 = match l1 with
  | [] -> l2
  | x::q when List.mem x l2 -> concat q l2
  | x::q -> x::concat q l2
;;

let rec variables f = match f with
  | Bot | Top -> []
  | V x -> [x]
  | Non(f') -> variables f'
  | Et(g,d) | Ou(g,d) | Implique(g,d) -> concat (variables g) (variables d)
;;

variables e ;;

(* Q4 *)

let rec association x l = match l with
  | [] -> failwith "aucune association"
  | (x',y)::q when x = x' -> y
  | _::q -> association x q
;;

(* Q5 *)

let rec evalue f v = match f with
  | Bot -> false
  | Top -> true
  | V x -> association x v
  | Non(f') -> not (evalue f' v)
  | Et(g,d) -> evalue g v && evalue d v
  | Ou(g,d) -> evalue g v || evalue d v
  | Implique(g,d) -> (not (evalue g v)) || evalue d v
;;

evalue e [("a", true); ("b", false); ("c", true)] ;;

(* Q6 *)

let rec valuations v = match v with
  | [] -> [[]]
  | x::q -> let l = valuations q in
    let l1 = List.map (fun l' -> (x,true)::l') l in
    let l2 = List.map (fun l' -> (x,false)::l') l in
    l1@l2
;;

valuations ["a"; "b"] ;;

(* Q7 *)

let est_tautologie f =
  let rec aux l = match l with
    | [] -> true
    | v::q -> evalue f v && aux q
  in aux (valuations (variables f))
;;

est_tautologie f1 ;;

est_tautologie f2 ;;

est_tautologie f3 ;;

(* Q8 *)

let p = V "p" in
let q = V "q" in
let pierce1 = Implique(Implique(Implique(p,q),p),p) in
let pierce2 = Implique(Implique(Implique(p,q),p),q) in
est_tautologie pierce1, est_tautologie pierce2
;;

(* Q9 *)

let rec affiche v = match v with
  | [] -> print_newline ()
  | (x,b)::q ->
    print_string x ;
    print_string " --> " ;
    print_int (if b then 1 else 0);
    print_string "    " ;
    affiche q
;;

affiche ["a", true; "b", false; "c", true] ;;

(* Q10 *)

exception Contre_ex of (string * bool) list ;;

(* pour la fin *)

let est_tautologie' f =
  let rec aux l = match l with
    | [] -> true
    | v::q when evalue f v = false -> raise (Contre_ex v)
    | _::q -> aux q
  in
  try
    aux (valuations (variables f))
  with Contre_ex v ->
    print_string "Ca ne marche pas avec la valuation :\n" ;
    affiche v ;
    false
;;

est_tautologie' f2 ;;

(* Q11 *)

exception Certificat of (string * bool) list ;;

let est_satisfiable f =
  let rec aux l = match l with
    | [] -> false
    | v::q when evalue f v -> raise (Certificat v)
    | _::q -> aux q
  in
  try
    aux (valuations (variables f))
  with Certificat v ->
    print_string "La valuation suivante satisfait la formule :\n" ;
    affiche v ;
    true
;;


(* Q12 *)

let rec subs f v b = match f with
  | V x when x = v -> b
  | Non(f') -> Non(subs f' v b)
  | Et(g,d) -> Et(subs g v b, subs d v b)
  | Ou(g,d) -> Ou(subs g v b, subs d v b)
  | Implique(g,d) -> Implique(subs g v b, subs d v b)
  | _ -> f
;;

(* Q13 *)

let rec simpl f = match f with
  | Et(f1, f2) -> begin match simpl f1, simpl f2 with
      | Top, f -> f
      | f, Top -> f
      | Bot, _ -> Bot
      | _, Bot -> Bot
      | f1', f2' -> Et(f1', f2')
    end
  | Ou(f1, f2) -> begin match simpl f1, simpl f2 with
      | Top, _ -> Top
      | _, Top -> Top
      | Bot, f -> f
      | f, Bot -> f
      | f1', f2' -> Ou(f1', f2')
    end
  | Implique(f1, f2) -> begin match simpl f1, simpl f2 with
      | Top, f -> f
      | _, Top -> Top
      | Bot, _ -> Top
      | f, Bot -> Non(f)
      | f1', f2' -> Implique(f1', f2')
    end
  | Non f -> begin match simpl f with
      | Top -> Bot
      | Bot -> Top
      | f' -> Non f'
    end
  | _ -> f
;;

(* Q14 *)

type 'a arbre_quine =
  | Valide
  | Invalide
  | Branchement of 'a * 'a arbre_quine * 'a arbre_quine
;;

let rec quine f = match simpl f with
  | Top -> Valide
  | Bot -> Invalide
  | f' -> let x = List.hd (variables f') in
    Branchement(x, quine (subs f' x Top), quine (subs f' x Bot))
;;

quine f2 ;;

quine f3 ;;