From 241a44528e76770b7a205437a2bb9b5b5847c58a Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Tue, 10 May 2022 15:24:42 +0200
Subject: [PATCH] =?UTF-8?q?Ajout=20de=20la=20=CE=B2-r=C3=A9duction=20du=20?=
 =?UTF-8?q?=CE=BB-terme=20final.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 main.ml             |  6 ++++--
 pieuvre.ml          |  4 ++--
 tests/cut-impl.8pus | 10 ++++++++++
 3 files changed, 16 insertions(+), 4 deletions(-)
 create mode 100644 tests/cut-impl.8pus

diff --git a/main.ml b/main.ml
index 31bc94e..ef7c7ef 100644
--- a/main.ml
+++ b/main.ml
@@ -157,8 +157,10 @@ while !subgoals <> [] do
 done;
 
 let finalLam = !fill_holes [] in
-    if (typecheck [] finalLam ty) then
-        Printf.printf "Final proof :\n%s\n" (string_of_lam finalLam)
+    if (typecheck [] finalLam ty) then (
+        Printf.printf "Final proof :\n";
+        reduce finalLam
+    )
     else (
         Printf.printf "Invalid proof constructed!\n";
         Printf.printf "%s can't be typed with %s.\n" (string_of_lam finalLam) (string_of_ty ty);
diff --git a/pieuvre.ml b/pieuvre.ml
index 2cc64ba..f26cea5 100644
--- a/pieuvre.ml
+++ b/pieuvre.ml
@@ -90,7 +90,7 @@ let rec alpha (l1: lam) (l2: lam) : bool =
 
 (* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
 let rec betastep (l: lam) : lam option = match l with
-    | LFun(v,t,l') -> betastep l'
+    | LFun(v,t,l') -> Option.bind (betastep l') (fun l' -> Some (LFun(v,t,l')))
     | LApp(lf,lx) ->
         begin
         match (betastep lf) with
@@ -104,7 +104,7 @@ let rec betastep (l: lam) : lam option = match l with
                 | _ -> None (* On ne peut pas β-réduire *)
         end
     | LVar(x) -> None
-    | LExf(l',_) -> betastep l'
+    | LExf(l',t) -> Option.bind (betastep l') (fun l' -> Some (LExf(l',t)))
 ;;
 
 (* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
diff --git a/tests/cut-impl.8pus b/tests/cut-impl.8pus
new file mode 100644
index 0000000..b0ede74
--- /dev/null
+++ b/tests/cut-impl.8pus
@@ -0,0 +1,10 @@
+(A -> B -> C) -> (B -> A -> C)
+intro f.
+intro b.
+intro a.
+cut (B -> C).
+intro bc.
+apply bc.
+assumption.
+apply f.
+assumption.