(* ================================================= *)
(* == DEA Logique et fondements de l'informatique == *)
(* == Programmation                                  *)
(* == ------------------------------------------- == *)
(* == Evaluation d'un lambda-calcul etendu        == *)
(* ================================================= *)

(* == Types *)
(* -- Operateurs predefinis *)
type op_bool2 = Conj | Disj ;;
type op_bool1 = Neg ;; 
type op_ar2 = Add | Sub | Mul | Div ;;
type rel_ar = Eq | Lt | Gt ;;

(* -- Expressions du langage *)
type exp_bool =
  Bcste of bool
| Bvar of string
| Bop1 of op_bool1 * exp 
| Bop2 of op_bool2 * exp * exp
| Irel of rel_ar * exp * exp

and exp_ar =
  Icste of int
| Ivar of string
| Iop2 of op_ar2 * exp * exp 

and exp =
  Evar of string
| Bexp of exp_bool
| Iexp of exp_ar
| Ifexp of exp * exp * exp
| App of exp * exp
| Abs of string * exp
| Fix of string * exp
| Dec of string * exp * exp 

(* -- Valeurs et environnement *)
type value =
  Ival of int 
| Bval of bool 
| Fval of string * exp * env_list
| Rval of string * exp * env_list

and env_list = (string * value) list ;;

(* == Fonctions *)
(* -- Verification dynamique de type *)
let checked_Bval v =
  match v with
    Bval _ -> v
  | _ -> failwith"Type error: Bval expected" ;;

let checked_bool v =
  match v with
    Bval b -> b
  | _ -> failwith"Type error: bool expected" ;;

let checked_Ival v =
  match v with
    Ival _ -> v
  | _ -> failwith"Type error: Ival expected" ;;

let checked_int v =
  match v with
    Ival n -> n
  | _ -> failwith"Type error: int expected" ;;

(* -- Code et application des operateurs predefinis *)
let val_of_Bop1 op =
  match op with
    Neg -> not ;;

let app_Bop1 op b = Bval ((val_of_Bop1 op) b) ;;

let val_of_Bop2 op =
  match op with
    Conj -> (&&)
  | Disj -> (||) ;;

let app_Bop2 op b1 b2 = Bval ((val_of_Bop2 op) b1 b2) ;;

let val_of_Irel r =
  match r with
    Eq -> (=)
  | Lt -> (<)
  | Gt -> (>) ;;

let app_Irel r n1 n2 = Bval ((val_of_Irel r) n1 n2) ;; 

let val_of_Iop2 op =
  match op with
    Add -> (+)
  | Sub -> (-) 
  | Mul -> ( * )
  | Div -> (/) ;;

let app_Iop2 op n1 n2 = Ival ((val_of_Iop2 op) n1 n2) ;;

(* -- Fonction(s) d'evaluation *)
let rec eval_bool exp env =
  match exp with
    Bcste b -> Bval b
  | Bvar x 
   -> checked_Bval (List.assoc x env)
  | Bop1 (op,e)
   -> app_Bop1 op (checked_bool (eval_exp e env))
  | Bop2 (op,e1,e2)
   -> app_Bop2 op (checked_bool (eval_exp e1 env))
                  (checked_bool (eval_exp e2 env))
  | Irel (r,e1,e2)
   -> app_Irel r (checked_int (eval_exp e1 env)) 
                 (checked_int (eval_exp e2 env))

and eval_ar exp env =
  match exp with
    Icste n -> Ival n
  | Ivar x -> checked_Ival (List.assoc x env)
  | Iop2 (op,e1,e2)
   -> app_Iop2 op (checked_int (eval_exp e1 env))
                  (checked_int (eval_exp e2 env))

and eval_exp exp env =
  match exp with
    Evar x -> List.assoc x env
  | Bexp e -> eval_bool e env
  | Iexp e -> eval_ar e env
  | Ifexp(e1,e2,e3) 
   -> if checked_bool (eval_exp e1 env) then
        eval_exp e2 env
      else
        eval_exp e3 env
  | App(e1,e2)
   -> let v1 = eval_exp e1 env in
      let v2 = eval_exp e2 env in
        (match v1 with
           Fval(x,e,env) -> eval_exp e ((x,v2)::env)
         | Rval(f,Abs(x,e),env) -> eval_exp e ((x,v2)::(f,v1)::env)
         | _ -> failwith"Type error: (F|R)val expected") 
  | Abs(x,e) -> Fval(x,e,env)
  | Fix(x,e) -> eval_exp e ((x,Rval(exp,env))::env)
  | Dec(x,e1,e2) -> eval_exp e2 ((x,eval_exp e1 env)::env) ;;

let eval e = eval_exp e [] ;;

(* == Exemples *)
(* -- Quelques utilitaires *)
let bc b = Bexp(Bcste b) ;;
let bv x = Bexp(Bvar x) ;;
let ou e1 e2 = Bexp(Bop2(Disj,e1,e2)) ;;
let et e1 e2 = Bexp(Bop2(Conj,e1,e2)) ;;
let non e = Bexp(Bop1(Neg,e)) ;;
let eq e1 e2 = Bexp(Irel(Eq,e1,e2));;
let lt e1 e2 = Bexp(Irel(Lt,e1,e2));;
let gt e1 e2 = Bexp(Irel(Gt,e1,e2));;

let ic n = Iexp(Icste n) ;;
let iv x = Iexp(Ivar x) ;;
let add e1 e2 = Iexp(Iop2(Add,e1,e2)) ;;
let sub e1 e2 = Iexp(Iop2(Sub,e1,e2)) ;;
let mul e1 e2 = Iexp(Iop2(Mul,e1,e2)) ;;
let div e1 e2 = Iexp(Iop2(Div,e1,e2)) ;;
let succ e = add e (ic 1) ;;
let pred e = sub e (ic 1) ;;

let ev x = Evar x ;;

(* -- Quelques expressions *)
let e1 = sub (ic 0) (add (mul (ic 3) (ic 4)) (div (ic 5) (ic 2))) ;;
let e2 = Ifexp (bc true, ic 1, ic 0) ;;
let e3 = Dec("x", ic 1, add (iv "x") (iv "x")) ;;
let e4 = Abs("x", mul (iv"x") (iv"x")) ;;
let e5 = App(e4, (ic 4)) ;;
let e6 = Dec("x", e5, App(e4, iv "x")) ;;
let e7 = Dec("x", e4, App(ev "x", e5)) ;;
let e8 = Dec("x", (ic 0), lt (iv "x") (succ (iv "x"))) ;;
let e9 = Fix("f", Abs("n", Ifexp (eq (iv "n") (ic 0), 
                                 ic 1, 
                                 mul (iv "n") 
                                     (App(ev "f", (pred (iv "n"))))))) ;;
let e10 = Dec("f",e9,App(ev "f", ic 5));;