From d78428c831dd8c743b2ea17c6b99fc4571d967c9 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 17 May 2022 11:34:59 +0200 Subject: [PATCH 1/4] README alpha --- README.md | 8 ++++++++ tests/lambda-terms/{alpha-eq.lam => alpha-eq.lams} | 0 .../lambda-terms/{alpha-not-eq.lam => alpha-not-eq.lams} | 0 3 files changed, 8 insertions(+) rename tests/lambda-terms/{alpha-eq.lam => alpha-eq.lams} (100%) rename tests/lambda-terms/{alpha-not-eq.lam => alpha-not-eq.lams} (100%) diff --git a/README.md b/README.md index 64fa4d8..b99cd29 100644 --- a/README.md +++ b/README.md @@ -10,11 +10,19 @@ L'option `typecheck` peut être testée avec les fichiers tests dans `tests/type ./pieuvre -typecheck tests/typecheck/wrong-type ``` +## 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 +``` + ## Note d'implémentation ## Répartition du travail ### Adrien +- Option `typecheck` ### Samy Fonctions de manipulation des λ-termes (pieuvre.ml) diff --git a/tests/lambda-terms/alpha-eq.lam b/tests/lambda-terms/alpha-eq.lams similarity index 100% rename from tests/lambda-terms/alpha-eq.lam rename to tests/lambda-terms/alpha-eq.lams diff --git a/tests/lambda-terms/alpha-not-eq.lam b/tests/lambda-terms/alpha-not-eq.lams similarity index 100% rename from tests/lambda-terms/alpha-not-eq.lam rename to tests/lambda-terms/alpha-not-eq.lams From 41c2b27823415724dfa76cd916ed121e8524fdd0 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 17 May 2022 11:38:40 +0200 Subject: [PATCH 2/4] README reduce --- README.md | 6 ++++++ tests/lambda-terms/lambda.lam | 2 ++ 2 files changed, 8 insertions(+) create mode 100644 tests/lambda-terms/lambda.lam diff --git a/README.md b/README.md index b99cd29..5291ec7 100644 --- a/README.md +++ b/README.md @@ -17,6 +17,12 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s' ./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 +``` + ## Note d'implémentation ## Répartition du travail diff --git a/tests/lambda-terms/lambda.lam b/tests/lambda-terms/lambda.lam new file mode 100644 index 0000000..c61560b --- /dev/null +++ b/tests/lambda-terms/lambda.lam @@ -0,0 +1,2 @@ +fun a: A => fun f: A -> A => + (fun x: A => f (f (f a))) a From 70fa9659be6fbe04129aaf0b09bfe580b50501b6 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 17 May 2022 11:43:45 +0200 Subject: [PATCH 3/4] Orthographe --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 5291ec7..3572bec 100644 --- a/README.md +++ b/README.md @@ -23,7 +23,7 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s' ./pieuvre -reduce tests/lambda-terms/lambda.lam ``` -## Note d'implémentation +## Notes d'implémentation ## Répartition du travail From a03a5f5504da21af09e991995916731c7966f223 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 17 May 2022 12:08:25 +0200 Subject: [PATCH 4/4] 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;;