type term = 
  | Var of string
  | Lambda of string * term
  | App of term * term


let rec apply x sub = function
  | Var (y) -> if y = x then sub else Var (y)
  | Lambda (y,t) -> Lambda (y, apply x sub t)
  | App (t1, t2) -> App (apply x sub t1, apply x sub t2)
    
let rec subst t sub_list =
  List.fold_left (fun t (x, sub) -> apply x sub t) t sub_list
  
let rec beta = function
  | App (Lambda (x, t), u) -> subst t [(x, u)]
  | _ -> failwith  "This term is not a redex"

(* ---------------------------------------
   Exemples
   --------------------------------------- *)

let x = Var "x";;
let y = Var "y";;
let a = Var "a" ;;
let b = Var "b" ;;
let i = Lambda ("x", x);;

(*(λx. x x) a — duplication*)
let n1 = App (Lambda ("x", App (x, x)), a);;
(*(λx. x x) (λa. a) — passage de fonction / ordre supérieur*)
let n2 = App (Lambda ("x", App (x, x)), Lambda (("a"), a));;
(*(λx. x (λx.x)) y — variable libres/liées*)
let n3 = App (Lambda ("x", App (x, Lambda ("x", x) ) ), y) ;;
(*(λx. x (λy. x y)) y — capture de variable*)
let n4 = App (Lambda ("x", App(x, Lambda ("y", App (x, y)))), y);;
(*(λxy. x) a b — fonction à deux entrées et effacement*)
let n5 = App ( App ( Lambda ("x", ( Lambda ("y", x))), a), b);;
(*(λxy. x) a — application partielle pour deux entrées*)
let n6 = App ( Lambda ("x", ( Lambda ("y", x))), a);;
(*(λxy. x) I a b — sur application pour deux entrées*)
let n7 = App (App ( App (Lambda ("x", ( Lambda ("y", x))), i), a), b);;
(*(λx. x x) (I I) — duplication inutile dans une stratégie*)
let n8 = App ( Lambda ("x", App (x, x)), App ( i, i));;
(*(λxy. y) (I I) I — différence de complexité selon la stratégie*)
let n9 = App ( App (Lambda ("x", ( Lambda ("y", y))), App (i, i)), i);;

(* ---------------------------------------
   Display
   --------------------------------------- *)

let rec string_of_list printer sep = function
  | [] -> ""
  | [x] -> printer x
  | h::t ->
      (printer h) ^ sep ^ (string_of_list printer sep t)
 

let rec string_of_term = function
  | Var x -> x
  | Lambda (x, Lambda (y, t)) -> "λ" ^ x ^ y ^ ". " ^ string_of_term t ^ ""
  | Lambda (x, t) -> "λ" ^ x ^ ". " ^ string_of_term t ^ ""
  | App (Var x, Var y) -> x ^ " " ^ y
  | App (t, Var x) -> "(" ^ string_of_term t ^ ") " ^ x
  | App ( App  ( t, u), v) -> "(" ^ string_of_term (App (t, u)) ^ ") " ^ string_of_term v 
  | App ( u, App  ( t, v)) -> string_of_term u ^ " (" ^ string_of_term (App (t, v)) ^ ")"
  | App ( Lambda (x, App (t, y)), v) -> "(" ^ string_of_term (Lambda (x, App (t, y))) ^ ") " ^ string_of_term v
  | App ( Lambda (x, t), u) -> string_of_term (Lambda (x,t)) ^ " (" ^ string_of_term u ^")" 
  | App (t, u) -> string_of_term t ^ " (" ^ string_of_term u ^ ")"


(* ---------------------------------------
  Réduction
  --------------------------------------- *)

exception Irreductible

let is_value = function
  | Lambda (_, _) -> true
  | Var _ -> true
  | _ -> false 

let rec lo_reduction = function 
  | App ( Lambda (x, t), u) as redex -> (beta redex)
  | App (Var x, (_ as t)) -> App (Var x, lo_reduction t)
  | App (App (_,_) as t, Var x) -> App (lo_reduction t, Var x)
  | App (t, u) -> (App (lo_reduction t, lo_reduction u))
  | Lambda (x, t) -> Lambda (x, lo_reduction t)
  | _ -> raise Irreductible


let rec lo_eval t = 
  try let t' = lo_reduction t in
    lo_eval t' with Irreductible -> t 
      

let (*cbv*) cbv = function
  | App ( Lambda (x, t), v) as redex when is_value v -> (*cbv*) (beta redex)
  | App (t, u) -> (App (t, (*cbv*) u))
  | Lambda (x, t) as l -> l 
  | Var x -> Var x

let rec cbv_loop t = 
  let t' = cbv t in 
  if t' = t then t'
  else cbv_loop t'

let rec cbn = function
  | App ( Lambda (x, t), v) as redex -> cbn (beta redex)
  | App (t, u) -> cbn (App (cbn t, u))
  | Lambda (x, t) -> Lambda (x, t)
  | Var x -> Var x