From f1ff0628c41e9ef88f56d759b7eb9a0aa050e603 Mon Sep 17 00:00:00 2001
From: Marwan <marwan.azizi@ens-lyon.fr>
Date: Tue, 16 Apr 2024 12:05:13 +0200
Subject: [PATCH] je sais pas ce que je fais

---
 lam.ml | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/lam.ml b/lam.ml
index 3b2f51a..7c76a38 100644
--- a/lam.ml
+++ b/lam.ml
@@ -36,3 +36,47 @@ let (=~) (e1 : lam) (e2 : lam) : bool =
   alpha_convert e1 = alpha_convert e2
 
 (** beta-reduction *)
+(* subst m n x substitutes x for n in m *)
+let rec subst (m : lam) (n : lam) (x : id) : lam =
+  match m with
+  Fun ((y, t), e) ->
+    if x = y
+    then m
+    else Fun ((y, t), subst e n x)
+  | App (e1, e2) ->
+    let e1 = subst e1 n x in
+    let e2 = subst e2 n x in
+    App (e1, e2)
+  | Var y ->
+    if x = y then n else m
+  | Exf (e, t) ->
+    let e = subst e n x in
+    Exf (e, t)
+
+let rec betastep (e : lam) : lam option =
+  match e with
+  Fun ((x, t), e) ->
+    begin match betastep e with
+    None -> None
+    | Some e -> Some (Fun ((x, t), e))
+    end
+  | App ((Fun ((x, t), e)), e2) ->
+    begin match betastep e with
+    None -> Some (subst e e2 x)
+    | Some e -> Some (App ((Fun ((x, t), e)), e2))
+    end
+  | App (e1, e2) ->
+    begin match betastep e1 with
+    None ->
+      begin match betastep e2 with
+      None -> None
+      | Some e2 -> Some (App (e1, e2))
+      end
+    | Some e1 -> Some (App (e1, e2))
+    end
+  | Var _ -> None
+  | Exf (e, t) ->
+    begin match betastep e with
+    None -> None
+    | Some e -> Some (Exf (e, t))
+    end