(***********)
(*  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