log.8pus

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 :

main.ml

@@ -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 =
@@ -262,19 +270,18 @@ while !subgoals <> [] do
     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;;