(* Абстрактный синтаксис для λ-исчисления:

   e ::= x
       | λx.e
       | e e

   В нашем конкретном синтаксисе,

   1. λx.e заменено на fun x -> e
   2. Допускается (е). Парсер превращает это в e
   3. Допускается let x = e in e'. Парсер преврящает в (λx.e') e *)
type e =
  | Variable of string
  | Lambda of string * e
  | Apply of e * e

(* От абстрактного синтаксиса обратно в конкретный. *)
let rec show e =
  match e with
  | Variable x -> x
  | Lambda (x, e) -> Printf.sprintf "(fun %s -> %s)" x (show e)
  | Apply (e1, e2) -> Printf.sprintf "(%s %s)" (show e1) (show e2)



(* Считывает весь стандартный вход. *)
let rec read () =
  match Stdlib.read_line () with
  | exception End_of_file -> ""
  | s -> s ^ " " ^ (read ())

(* Очень плохой токенизатор. На самом деле надо использовать ocamllex или
   sedlex. *)
let tokenize s =
  let rec insert token strings =
    match strings with
    | s::s'::strings -> s::token::(insert token (s'::strings))
    | _ -> strings
  in
  String.split_on_char '(' s
  |> insert "("
  |> List.map (String.split_on_char ')')
  |> List.map (insert ")")
  |> List.flatten
  |> List.map (String.split_on_char ' ')
  |> List.flatten
  |> List.map String.trim
  |> List.filter ((<>) "")

(* Сам парсер. Первые две функции находят последовательность приложений
   функций, то есть e1 e2 e3 e4... Третья разбирает каждую e1, e2, ...,
   определяя, это переменная, лямбда или скобка, содержащая общее выражение. *)
let rec parse_general input =
  let (e, input) = parse_non_apply input in
  match input with
  | ")"::_ | "in"::_ | [] -> (e, input)
  | _ -> parse_apply ~e1:e input

and parse_apply ~e1 input =
  let (e2, input) = parse_non_apply input in
  let e = Apply (e1, e2) in
  match input with
  | ")"::_ | "in"::_ | [] -> (e, input)
  | _ -> parse_apply ~e1:e input

and parse_non_apply input =
  match input with
  | "("::input ->
    let (e, input) = parse_general input in
    begin match input with
    | ")"::input -> (e, input)
    | _ -> failwith "unmatched '('"
    end
  | "fun"::x::"->"::input ->
    let (e, input) = parse_general input in
    (Lambda (x, e), input)
  | "let"::x::"="::input ->
    let (e1, input) = parse_general input in
    begin match input with
    | "in"::input ->
      let (e2, input) = parse_general input in
      (Apply (Lambda (x, e2), e1), input)
    | _ ->
      failwith "expected 'in'"
    end
  | x::input ->
    (Variable x, input)
  | [] ->
    failwith "expected an expression"

let parse s =
  s
  |> tokenize
  |> parse_general
  |> fst



(* Интерпретатор. *)

(* Под λx.e, в e заменяет x на y. Если е содержит λ как подвыражение, и эта
   λ затеняет x, там замена не происходит. *)
let rec alpha_vary x y e =
  match e with
  | Variable z when z = x -> Variable y
  | Variable z -> Variable z
  | Lambda (z, e) when z = x -> Lambda (z, e)
  | Lambda (z, e) -> Lambda (z, alpha_vary x y e)
  | Apply (e1, e2) -> Apply (alpha_vary x y e1, alpha_vary x y e2)

(* Свободные переменные выражения e. То есть те, которые не происходит от
   окружающей λ. Например, в λx.x y, у свободная переменная, потому что не
   происходит от окружающей её λ. Свободные переменные могут быть захвачены
   внешней λ если в λ их не переименовать, то есть если наивно вычислить
   (λx.λy.x у) у, результат будет λу.у у, но внешняя у не должна ссылаться на
   внутреннюю y в λy. Для этого во время замены в λy.x у, внутреннюю y надо
   α-переименовать используя alpha_vary в, например _у1, и результат вычисления
   будет λ_у1.у _у1. *)
let rec free_variables e =
  match e with
  | Variable x -> [x]
  | Lambda (x, e) -> List.filter ((<>) x) (free_variables e)
  | Apply (e1, e2) -> (free_variables e1) @ (free_variables e2)

(* Добавляет приблизительно уникальный суффикс к переменной. Парсер не
   проверяет, что такие суффиксы не могут быть введены вручную. *)
let unique =
  let last_suffix = ref 0 in
  fun x ->
    incr last_suffix;
    Printf.sprintf "_%s%i" x !last_suffix

(* Заменяет в e все случаи x на e'. Избегает захвата свободных переменных.
   Смотрите комметарий выше у free_variables. *)
let rec substitute e e' x =
  match e with
  | Variable y when y = x -> e'
  | Variable y -> Variable y
  | Lambda (y, e'') ->
    if y = x then
      Lambda (y, e'')
    else
      let (y, e'') =
        if List.mem y (free_variables e') then
          let y' = unique y in
          let e'' = alpha_vary y y' e'' in
          (y', e'')
        else
          (y, e'')
      in
      Lambda (y, substitute e'' e' x)
  | Apply (e1, e2) -> Apply (substitute e1 e' x, substitute e2 e' x)

(* Вычисляет следующий шаг e' вычисления e. Если таковой имеется, результат
   Some e'. Если вычисление невозможно, результат None. *)
let rec step e =
  match e with
  | Apply (Apply (Variable "print", Variable x), e) ->
    print_endline x;
    Some e
  | Apply (Lambda (x, e1), e2) ->
    begin match step e2 with
    | Some e2' -> Some (Apply (Lambda (x, e1), e2'))
    | None -> Some (substitute e1 e2 x)
    end
  | Apply (e1, e2) ->
    begin match step e1 with
    | Some e1' -> Some (Apply (e1', e2))
    | None ->
      match step e2 with
      | Some e2' -> Some (Apply (e1, e2'))
      | None -> None
    end
  | _ -> None

(* Многократно применяет step пока вычисление не становится невозможным. *)
let rec eval e =
  match step e with
  | Some e' -> eval e'
  | None -> e

(* Аналогичен eval, но выводит шаги *)
let rec trace e =
        show e |> print_endline;
        match step e with
            | Some e' ->  trace e'
            | None -> e

let _ =
  read ()
  |> parse
  |> eval
  |> show
  |> print_endline