From a03a5f5504da21af09e991995916731c7966f223 Mon Sep 17 00:00:00 2001
From: Adrien Vannson <adrien.vannson@protonmail.com>
Date: Tue, 17 May 2022 12:08:25 +0200
Subject: [PATCH] log.8pus

---
 README.md |  1 +
 main.ml   | 69 ++++++++++++++++++++++++++++++-------------------------
 2 files changed, 39 insertions(+), 31 deletions(-)

diff --git a/README.md b/README.md
index 3572bec..976ad86 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,7 @@ The Pieuvre Proof Assistant
 ===========================
 
 # Utilisation
+`Pieuvre` génère automatiquement un fichier `log.8pus` contenant la preuve venant d'être faite.
 
 ## Option `typecheck`
 L'option `typecheck` peut être testée avec les fichiers tests dans `tests/typecheck`. Pour cela, utiliser les commandes :
diff --git a/main.ml b/main.ml
index 9eb1289..2819cb1 100644
--- a/main.ml
+++ b/main.ml
@@ -1,7 +1,7 @@
 open Structs;;
 open Pieuvre;;
 open Tactic;;
-    
+
 (* Lorsqu'une tactique ne peut se lancer. Contient la tactique ainsi qu'un message contenant l'erreur.*)
 exception TacticException of tactic*string;;
 (* Lorsqu'une tactique est mal écrite*)
@@ -34,15 +34,6 @@ let is_interactive = match file with
   | _ -> false
 in
 
-let readline () = match file with
-  | None -> (
-        Printf.printf ">>> ";
-        flush stdout;
-        read_line ()
-    )
-  | Some f -> input_line f
-in
-
 if !reduce_option then (
     let lexbuf = Lexing.from_channel (match file with
       | None -> stdin
@@ -105,12 +96,29 @@ if !typecheck_option then (
     exit 0
 );
 
-(* Show a message only if the input is read from stdin *)
+(* Affiche un message si l'entrée est lue sur stdin *)
 let show s = match file with
   | None -> Printf.printf "%s" s
   | _ -> ()
 in
 
+(* Ouvre un fichier contenant la preuve écrite *)
+let log_file = open_out "log.8pus" in
+
+let readline () =
+    let line = match file with
+      | None -> (
+            Printf.printf ">>> ";
+            flush stdout;
+            read_line ()
+        )
+      | Some f -> input_line f
+    in
+    Printf.fprintf log_file "%s\n" line;
+    flush log_file;
+    line
+in
+
 show "Please type the formula to prove\n";
 
 let ty =
@@ -166,7 +174,7 @@ while !subgoals <> [] do
             Parser.main_tactic Lexer.token lexbuf
         with e -> raise TacticParseException
     in
-    
+
     let applyTactic tactic =
         begin
         let f = !fill_holes in
@@ -260,21 +268,20 @@ while !subgoals <> [] do
             )
         end
     in
-    
+
     let rec applyUntilWorking () =
-        try
-            (
-                let readTactic = read_tactic () in
-                    applyTactic readTactic
-            )
+        try (
+            let readTactic = read_tactic () in
+            applyTactic readTactic
+        )
         with
-            | TacticException(t,s) -> 
+          | TacticException(t,s) ->
                 Printf.printf "\027[31mCannot apply the tactic: %s\027[0m\n" s;
                 if(is_interactive) then applyUntilWorking () else raise (TacticException(t,s))
-            | TacticParseException -> 
+          | TacticParseException ->
                 Printf.printf "\027[31mCannot parse the tactic, please refer to pieuvre documentation.\027[0m\n";
                 if(is_interactive) then applyUntilWorking () else raise TacticParseException
-            | e -> 
+          | e ->
                 Printf.printf "\027[31mPieuvre Failed Unexpectedly !\027[0m\n";
                 raise e
     in
@@ -282,13 +289,13 @@ while !subgoals <> [] do
 done;
 
 let finalLam = !fill_holes [] in
-    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);
-        Printf.printf "The whole development team of pieuvre is sorry for the damage eventually done by this error.\n"
-    )
-;;
+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);
+    Printf.printf "The whole development team of pieuvre is sorry for the damage eventually done by this error.\n"
+);
+
+close_out log_file;;