```(***********)
(*  EXO 1  *)
(***********)

type binop = And | Or | Imp
type fmla =
| True
| False
| Var of int
| Not of fmla
| Bin of binop * fmla * fmla

(* Question 1 *)
let rec contains i f = match f with
| True | False   -> false
| Var j          -> i=j
| Not f'         -> contains i f'
| Bin(_, f1, f2) -> contains i f1 || contains i f2

(* Question 2 *)
let rec elim_imp f = match f with
| True | False | Var _ -> f
| Not f'               -> Not (elim_imp f')
| Bin(Imp, f1, f2)     -> Bin(Or, Not (elim_imp f1), elim_imp f2)
| Bin(op, f1, f2)      -> Bin(op, elim_imp f1, elim_imp f2)
(*  | Bin(op, f1, f2) ->
if op = Imp then
Bin(Or, Not (elim_imp f1), elim_imp f2)
else
Bin(op, elim_imp f1, elim_imp f2) *)

(* Question 3 *)
let rec is_nnf f = match f with
| True | False            -> true
| Var _ | Not(Var _)      -> true
| Bin((And | Or), f1, f2) -> is_nnf f1 && is_nnf f2
| _                       -> false

(* Question 4 *)
let rec neg_nnf f = match f with
| True   -> False
| False  -> True
| Var _  -> Not f
| Not f' -> f'
| Bin(And, f1, f2) -> Bin(Or, neg_nnf f1, neg_nnf f2)
| Bin(Or,  f1, f2) -> Bin(And, neg_nnf f1, neg_nnf f2)
| _ -> raise (Invalid_argument "neg_nnf")

(* Question 5 *)
let rec nnf f = match f with
| True | False | Var _ -> f
| Not f'               -> neg_nnf (nnf f')
| Bin(Imp, f1, f2)     -> Bin(Or, neg_nnf (nnf f1), nnf f2)
| Bin(op, f1, f2)      -> Bin(op, nnf f1, nnf f2)

(* Question 6
* Complexité quadratique dans le pire des cas : si plusieurs négations sont présentes l'une
* au-dessus de l'autre, on aura des applications répétées de neg_nnf.
* Exemple : Not (Not (Not (Not ... (Var 0) )))
*)

(* Question 7 *)
let rec nnf = function
| True  -> True
| False -> False
| Var i -> Var i
| Not f -> neg_nnf f
| Bin (Imp, f1, f2) -> Bin (Or, neg_nnf f1, nnf f2)
| Bin (op,  f1, f2) -> Bin (op,     nnf f1, nnf f2)
and neg_nnf = function
| True  -> False
| False -> True
| Var i -> Not (Var i)
| Not f -> nnf f
| Bin (And, f1, f2) -> Bin (Or,  neg_nnf f1, neg_nnf f2)
| Bin (Or,  f1, f2) -> Bin (And, neg_nnf f1, neg_nnf f2)
| Bin (Imp, f1, f2) -> Bin (And,     nnf f1, neg_nnf f2)

(***********)
(*  EXO 2  *)
(***********)

let s_not f = match f with
| True   -> False
| False  -> True
| Not f' -> f'
| _      -> Not f

let s_and f1 f2 = match f1, f2 with
| False, _ | _, False -> False
| True,  f | f, True  -> f
| _, _                -> Bin(And, f1, f2)

let s_or f1 f2 = match f1, f2 with
| True,  _ | _, True  -> True
| False, f | f, False -> f
| _, _                -> Bin(Or, f1, f2)

let s_imp f1 f2 = match f1, f2 with
| False, _ | _, True  -> True
| True, f             -> f
| f,    False         -> s_not f
| _, _                -> Bin(Imp, f1, f2)

let s_iff f1 f2 = s_and (s_imp f1 f2) (s_imp f2 f1)
let s_xor f1 f2 = s_iff f1 (s_not f2)

let  rec simplify f = match f with
| Var _ | True | False -> f
| Not f                -> s_not (simplify f)
| Bin (And, f1, f2)    -> s_and (simplify f1) (simplify f2)
| Bin (Or,  f1, f2)    -> s_or  (simplify f1) (simplify f2)
| Bin (Imp, f1, f2)    -> s_imp (simplify f1) (simplify f2)

(***********)
(*  EXO 3  *)
(***********)

(* Question 1 *)
type expr =
| Cst of int          (* n *)
| Var of int          (* X_i *)
| Opp of expr         (* - e *)
| Add of expr * expr  (* e1 + e2 *)
| Sub of expr * expr  (* e1 - e2 *)
| Mul of expr * expr  (* e1 * e2 *)

(*
Variante : factoriser les opérateurs binaires avec la déclaration
type binop = Add | Sub | Mul
et en remplçant les trois derniers cas de expr par
| Bin of binop * expr * expr  (\* e1 op e2 *\)
*)

(* - (X_0 + 3) * (2 - X_1) *)
let e = Opp(Mul(Add(Var 0, Cst 3), Sub(Cst 2, Var 1)))

(* Question 2 *)
let rec constant e = match e with
| Cst n -> true
| Var i -> false
| Opp e' -> constant e'
| Add(e1, e2) | Sub(e1, e2) | Mul(e1, e2) -> constant e1 && constant e2

(* Question 3 *)
let rec eval e v = match e with
| Cst n       -> n
| Var i       -> v.(i)
| Opp e'      -> - eval e' v
| Add(e1, e2) -> eval e1 v + eval e2 v
| Sub(e1, e2) -> eval e1 v - eval e2 v
| Mul(e1, e2) -> eval e1 v * eval e2 v

(***********)
(*  EXO 4  *)
(***********)

type regexp =
| Epsilon
| Char   of char
| Alt    of regexp * regexp
| Concat of regexp * regexp
| Star   of regexp

(* Question 1 *)
let rec epsilon = function
| Epsilon | Star _ -> true
| Char _           -> false
| Alt (e1, e2)     -> epsilon e1 || epsilon e2
| Concat (e1, e2)  -> epsilon e1 && epsilon e2

(* Question 2 *)
let rec first c = function
| Char d when d = c -> true
| Epsilon | Char _  -> false
| Alt (e1, e2)      -> first c e1 || first c e2
| Concat (e1, e2)   -> first c e1 || (epsilon e1 && first c e2)
| Star e            -> first c e

let rec last c = function
| Char d when d = c -> true
| Epsilon | Char _  -> false
| Alt (e1, e2)      -> last c e1 || last c e2
| Concat (e1, e2)   -> last c e2 || (epsilon e2 && last c e1)
| Star e            -> last c e

(* Question 3 *)
let rec follow c d = function
| Epsilon | Char _ -> false
| Alt (e1, e2)     -> follow c d e1 || follow c d e2
| Concat (e1, e2)  -> follow c d e1 || follow c d e2 || (last c e1 && first d e2)
| Star e           -> follow c d e  || (last c e && first d e)

(* Question 4 *)
type regexp =
| Epsilon
| Char   of char
| Alt    of regexp * regexp
| Concat of regexp * regexp
| Star   of regexp
| Empty

let rec epsilon = function
| Epsilon | Star _ -> true
| Char _           -> false
| Alt (e1, e2)     -> epsilon e1 || epsilon e2
| Concat (e1, e2)  -> epsilon e1 && epsilon e2
| Empty            -> false

(* Question 5 *)
let rec derive c = function
| Char d when d = c        -> Epsilon
| Empty | Epsilon | Char _ -> Empty
| Alt (e1, e2)             -> Alt (derive c e1, derive c e2)
| Concat (e1, e2) ->
if epsilon e1 then
Alt (Concat (derive c e1, e2), derive c e2)
else
Concat (derive c e1, e2)
| Star e ->
Concat (derive c e, Star e)

(* Question 6 *)
let rec recognize e = function
| []   -> epsilon e
| c::l -> recognize (derive c e) l
```