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)

let _ = 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

let _ = 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)

let _ = 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

let _ = 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

let _ = 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))

let _ = est_tautologie f1

let _ = est_tautologie f2

let _ = est_tautologie f3

(* Q8 *)

let _ =
  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

let _ = 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

let _ = 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))

let _ = quine f2

let _ = quine f3