(*Terme du Lambda-Calcul*)
type term = 
  | Var of string
  | Lambda of string * term
  | App of term * term


let to_var x = Var x

let rec to_lambda l t = 
  match l with 
  | h::tail -> Lambda (h, to_lambda tail t)
  | [] -> t

let to_app t u = App (t, u)

(*Applique une substitution de x par sub à un terme t*)
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)
    
(*Applique une liste de substition à un terme*)
let rec subst t sub_list =
  List.fold_left (fun t (x, sub) -> apply x sub t) t sub_list
  
(* Applique la beta réduction, qui transforme (lambda x. t)u en t[x:=u] *)
let rec beta = function
  | App (Lambda (x, t), u) -> subst t [(x, u)]
  | _ -> failwith  "This term is not a redex"

(* return i where i is the smallest suffix needed so that "x ^ i"  isn't in l *)
let rec var_counter i x l = 
  if List.mem (x ^ (string_of_int i)) l then var_counter (i+1) x l 
  else i

(* Alpha Conversion : renames lambda variables duplicates by adding a number to them*)
let alpha_conv t =
  let rec aux l = function
  | Var x when List.mem x l -> 
      let i = string_of_int ( (var_counter 0 x l) - 1) in 
      if i = "-1" then Var x
      else Var (x^i)
  | Var x -> Var x
  | Lambda(x, t) when List.mem x l -> 
      let i = string_of_int (var_counter 0 x l) in 
      Lambda (x^i, aux ((x^i)::l) t)
  | Lambda(x, t) -> Lambda (x, aux (x::l) t)
  | App (t, u) -> App (aux l t, aux l u)
  in aux [] t
(* ---------------------------------------
   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
(* Vérifie si un terme est une valeur, c'est à dire qu'on ne peut plus le réduire *)
let is_value = function
  | Lambda (_, _) -> true
  | Var _ -> true
  | _ -> false 
  
(* Vérifie si un lambda est linéaire, i.e. qu'il n'y a qu'une seule occurence de son paramètre *)

let rec count_freevars x = function
  | Lambda (y, t) -> count_freevars x t
  | App (t, u) -> (count_freevars x t) + (count_freevars x u)
  | Var y -> if x = y then 1 else 0

  let rec is_linear = function 
  | Lambda (x, t) -> (count_freevars x t) = 1 && is_linear t
  | App(t, u) -> is_linear t && is_linear u
  | Var x -> true

(* Réduit d'un pas les termes par l
'extérieur puis l'intérieur *)
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 (App (_,_) as t, (_ as u)) -> App (lo_reduction t, u)
  (*| App (t, u) -> (App (lo_reduction t, lo_reduction u))*)
  | Lambda (x, t) -> Lambda (x, lo_reduction t)
  | _ -> raise Irreductible

(* Boucle sur la lo_reduction pour appliquer cette stratégie de réduction jusqu'à la fin *)
let rec lo_eval t = 
  try let t' = lo_reduction t in
    lo_eval t' with Irreductible -> t 
      
(* Réduit d'un pas les termes en commençant par l'argument puis réduit les fonctions *)
let rec cbv = function
  | App ( Lambda (x, t), v) as redex when is_value v -> (*cbv*) (beta redex)
  | App (t, u) when is_value u -> (App (cbv t, u))
  | App (t, u) -> (App (t, cbv u))
  | Lambda (x, t) -> raise Irreductible
  | Var x -> raise Irreductible

(* Boucle sur call_by_value pour appliquer cette stratégie de réduction jusqu'à la fin *)
let rec cbv_eval t = 
  try let t' = cbv t in
    cbv_eval t' with Irreductible -> t 

(* Réduit d'un pas les termes en commençant par la fonction puis passe à l'argument*)
let rec cbn = function
  | App ( Lambda (x, t), v) as redex -> beta redex
  | App (t, u) -> (App (cbn t, u))
  | Lambda (x, t) -> raise Irreductible
  | Var x -> raise Irreductible

(* Boucle sur call_by_name pour appliquer cette stratégie de réduction jusqu'à la fin *)
let rec cbn_eval t = 
  try let t' = cbv t in
    cbn_eval t' with Irreductible -> t