From 7b42215aa1f7cf7a765d2447963731156e04151a Mon Sep 17 00:00:00 2001
From: nihonium <nihonium@nekoea.red>
Date: Thu, 2 Nov 2023 02:51:31 +0300
Subject: [PATCH] task5

---
 task5/eval.ml        | 194 +++++++++++++++++++++++++++++++++++++++++++
 task5/numeral.lambda |  31 +++++++
 task5/test.lambda    |   1 +
 3 files changed, 226 insertions(+)
 create mode 100644 task5/eval.ml
 create mode 100644 task5/numeral.lambda
 create mode 100644 task5/test.lambda

diff --git a/task5/eval.ml b/task5/eval.ml
new file mode 100644
index 0000000..de2269e
--- /dev/null
+++ b/task5/eval.ml
@@ -0,0 +1,194 @@
+(* Абстрактный синтаксис для λ-исчисления:
+
+   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
diff --git a/task5/numeral.lambda b/task5/numeral.lambda
new file mode 100644
index 0000000..80880b9
--- /dev/null
+++ b/task5/numeral.lambda
@@ -0,0 +1,31 @@
+let 0 =
+  fun f -> fun init ->
+    init
+in
+
+let +1 =
+  fun n ->
+    fun f -> fun init ->
+      f (n f init)
+in
+
+let 1 = +1 0 in
+let 2 = +1 1 in
+let 3 = +1 2 in
+let 4 = +1 3 in
+let 5 = +1 4 in
+
+let print_n =
+  fun n ->
+    n (fun accumulator -> print foo accumulator) (fun x -> x)
+in
+
+let + =
+  fun n -> fun n' -> n +1 n'
+in
+
+let * =
+  fun n -> fun n' -> n (n' +1) 0
+in
+
+print_n (* 4 3)
diff --git a/task5/test.lambda b/task5/test.lambda
new file mode 100644
index 0000000..cbbb4c8
--- /dev/null
+++ b/task5/test.lambda
@@ -0,0 +1 @@
+(fun x -> fun y -> x) z w