je sais pas ce que je fais

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