Merge remote-tracking branch 'origin/master'

README.md

@@ -12,6 +12,7 @@ Allez, tous à vos pieuvres !
 *L'équipe de Pieuvre™ n'est pas responsable des dommages occasionnés par les réalisations philosophiques causées aux utilisateur·ices de par l'utilisation du programme*
 
 # 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 :
@@ -20,11 +21,25 @@ L'option `typecheck` peut être testée avec les fichiers tests dans `tests/type
 ./pieuvre -typecheck tests/typecheck/wrong-type
 ```
 
-## Note d'implémentation
+## Option `alpha`
+L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s'utilise de la manière suivante :
+```
+./pieuvre -alpha tests/lambda-terms/alpha-eq.lams
+./pieuvre -alpha tests/lambda-terms/alpha-not-eq.lams
+```
+
+## Option `reduce`
+L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s'utilise de la manière suivante :
+```
+./pieuvre -reduce tests/lambda-terms/lambda.lam
+```
+
+## Notes d'implémentation
 
 ## Répartition du travail
 
 ### Adrien
+- Option `typecheck`
 
 ### Samy
 Fonctions de manipulation des λ-termes (pieuvre.ml)

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;;

tests/lambda-terms/lambda.lam

@@ -0,0 +1,2 @@
+fun a: A => fun f: A -> A =>
+	(fun x: A => f (f (f a))) a