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 =
  failwith "A coder"
;;

hauteur e ;;

(* Q2*)

let rec longueur f =
  failwith "A coder"
;;

longueur e ;;

(* Q3 *)

let rec variables f =
  failwith "A coder"
;;

variables e ;;

(* Q4 *)

let rec association x l =
  failwith "A coder"
;;

(* Q5 *)

let rec evalue f v =
  failwith "A coder"
;;

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

(* Q6 *)

let rec valuations v =
  failwith "A coder"
;;

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

(* Q7 *)

let est_tautologie f =
  failwith "A coder"
;;

est_tautologie f1 ;;

est_tautologie f2 ;;

est_tautologie f3 ;;

(* Q8 *)

(* formules à écrire et à tester *)

(* Q9 *)

let rec affiche v =
  failwith "A coder"
;;

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

(* Q10 *)

exception Contre_ex of (string * bool) list ;;

let est_tautologie' f =
  failwith "A coder"
;;

est_tautologie' f2 ;;

(* Q11 *)

exception Certificat of (string * bool) list ;;

let est_satisfiable f =
  failwith "A coder"
;;


(* Q12 *)

let rec subs f v b =
  failwith "A coder"
;;

(* Q13 *)

let rec simpl f =
  failwith "A coder"
;;

(* Q14 *)

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

let rec quine f =
  failwith "A coder"
;;

quine f2 ;;

quine f3 ;;