Correction des erreurs d'Adrien.

.gitignore

@@ -1,5 +1,6 @@
 _build
 pieuvre
 main.native
+log.8pus
 
 *.kate-swp

Makefile

@@ -10,8 +10,11 @@ main.byte:
 
 byte: main.byte
 
-.PHONY: clean test
+test: all
+	  for f in tests/*.8pus; do echo "### Testing $$f:"; ./pieuvre $$f; echo ""; done
 
 clean:
 	ocamlbuild -clean
 	rm -f pieuvre
+
+.PHONY: clean test

README.md

@@ -1,14 +1,67 @@
-The Pieuvre Proof Prover
+The Pieuvre™ Proof Assistant
-=
+============================
 
-# Presentation
+Ne vous êtes jamais vous dit que votre quotidien était morose ? Que tout ce que vous pourriez prouver dans votre vie ne serait que vain ? C'est que vous avez besoin du réconfort de Pieuvre™ !
 
-# Note d'implementation
+Pieuvre™ est un assistant de preuve à votre service. Lorsque vous doutez, que vous êtes effrayés par l'incurable finitude de votre esprit, l'ineffable efficacité de Pieuvre™ saura vous réconforter en vous assurant des preuves complètes et sans accroc.
 
-# Répartition du travail
+Bien plus efficace que d'autres gallinacés, l'interface CLI de Pieuvre™ saura convenir à petits et grands. Son design entre post-modernisme et romantisme baroque néo-mérovingien rappellera aux utilisateur·ices les plus avertis les plus grandes heures de l'humanité.
+
+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. Attention, le fichier `log.8pus` ne doit jamais être donné en entrée de Pieuvre™ !
+
+## Option `typecheck`
+L'option `typecheck` vérifie si un lambda-terme est bien typé. Elle s'utilise de la manière suivante :
+```
+./pieuvre -typecheck tests/typecheck/right-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
+```
+
+## 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
+
+- Les λ-termes à trous sont représentés par leurs fonctions de remplissage. À la liste des λ-termes à mettre dans les trous, on associe le λ-terme complété.
+
+### Découpage des fichiers
+
+- `lexer.mll` et `parser.mly` sont les fichiers pour le parser `ocamlyacc`
+- `main.ml` contient le code gérant la ligne de commande, la construction du lambda-terme en appelant les fonctions de `pieuvre.ml`
+- `pieuvre.ml` contient toutes les fonctions de manipulation de λ-termes.
+- `structs.ml` contient l'ensemble des structures de données : λ-terme, environnements, types
+- `tactic.ml` contient la structure de définition des tactiques.
+
+## Répartition du travail
 
 ### Adrien
+- Interface interactive (avec le parsage des formules, des tactiques, ...), lecture des fichiers
+- Construction d'un lambda-terme à partir de la preuve (sans et / ou )
+- Tactiques élémentaires (`intro`, `intros`, `assumption`, `apply`, `elim`)
+- Options `alpha`, `reduce`, `typecheck`, ... : partie interactive appelant les fonctions écrites par Samy
+- Écriture de tests (irréfutabilité du tiers exclus, de la formule de Peirce, ...)
 
 ### Samy
-Fonctions de manipulation des λ-termes (pieuvre.ml)
+- Introduction du README
-Typecheck
+- Fonctions de manipulation des λ-termes (`pieuvre.ml`)
+- Typecheck
+- Erreurs lors des tactiques.
+- `\/` et `/\`
+- Parsing des λ-termes
+- `True` et `exact`
+- Option `-computetype`
+- Écriture de tests

lexer.mll

@@ -10,13 +10,37 @@ rule token = parse
   | ')'                         { RPAREN }
   | "->"                        { RARROW }
   | '~'                         { TILDE }
+  | "/\\"                       { LAND } (* logical and *)
+  | "\\/"                       { LOR } (* logical or *)
+  | ','                         { COMMA }
 
   | "intro"                     { INTRO }
+  | "intros"                    { INTROS }
   | "assumption"                { ASSUMPTION }
   | "apply"                     { APPLY }
+  | "elim"                      { ELIM }
   | "cut"                       { CUT }
+  | "split"                     { SPLIT }
+  | "left"                      { LEFT }
+  | "right"                     { RIGHT }
+  | "exact"                     { EXACT }
+
   | "False"                     { FALSE }
-  
+  | "True"                      { TRUE }
+
+  | "fun"                       { FUN }
+  | "=>"                        { MAPS_TO }
+  | ':'                         { COLON }
+  | "exf"                       { EXF }
+  | "fst"                       { FST }
+  | "snd"                       { SND }
+  | "ig"                        { IG }
+  | "id"                        { ID }
+  | "case"                      { CASE }
+  | 'I'                         { I }
+
+  | '&'                         { AMPERSAND }
+
   | ['A'-'Z']+['0'-'9']* as s   { TYPE_NAME s }
   | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
   | '.'                         { DOT }

main.ml

@@ -1,20 +1,28 @@
 open Structs;;
 open Pieuvre;;
+open Tactic;;
 
-let fail () =
+(* Lorsqu'une tactique ne peut se lancer. Contient la tactique ainsi qu'un message contenant l'erreur.*)
-    failwith "Unknown error";;
+exception TacticException of tactic*string;;
+(* Lorsqu'une tactique est mal écrite*)
+exception TacticParseException;;
+(* Exception renvoyée lorsque la fonction de trou est appelée sur une liste trop grande. *)
+(* Ne devrait jamais être lancée *)
+exception TrouException;;
 
 (* Parsage des arguments*)
 let filename = ref "" in
 
-let reduce = ref false in
+let reduce_option = ref false in
-let alpha = ref false in
+let alpha_option = ref false in
 let typecheck_option = ref false in
+let computetype_option = ref false in
 
 Arg.parse
-    [("-reduce", Arg.Set reduce, "Show the step-by-step reduction of a lambda-term");
+    [("-reduce", Arg.Set reduce_option, "Show the step-by-step reduction of a lambda-term");
-     ("-alpha", Arg.Set alpha, "Check is two lambda-terms separated by '&' are alpha-convertible");
+     ("-alpha", Arg.Set alpha_option, "Check is two lambda-terms separated by '&' are alpha-convertible");
-     ("-typecheck", Arg.Set typecheck_option, "Check if a lambda term has a given type")]
+     ("-typecheck", Arg.Set typecheck_option, "Check if a lambda term has a given type");
+     ("-computetype", Arg.Set computetype_option, "Computes the type of the input λ-term")]
     (fun s -> filename := s)
     "The available options are:";
 
@@ -28,21 +36,117 @@ let is_interactive = match file with
   | _ -> false
 in
 
-let readline () = match file with
+if !reduce_option then (
-  | None -> (
+    let lexbuf = Lexing.from_channel (match file with
-        Printf.printf ">>> ";
+      | None -> stdin
-        flush stdout;
+      | Some file -> file
-        read_line ()
     )
-  | Some f -> input_line f
+    in
-in
+    let lambda_term =
+        try
+            Parser.main_lambda Lexer.token lexbuf
+        with e -> (
+            Printf.printf "Can't read lambda term\n";
+            raise e
+       )
+    in
+    reduce lambda_term;
+    exit 0
+);
 
-(* Show a message only if the input is read from stdin *)
+if !alpha_option then (
+    let lexbuf = Lexing.from_channel (match file with
+      | None -> stdin
+      | Some file -> file
+    )
+    in
+    let lam1, lam2 =
+        try
+            Parser.main_two_lambda Lexer.token lexbuf
+        with e -> (
+            Printf.printf "Can't read lambda terms\n";
+            raise e
+       )
+    in
+    if alpha lam1 lam2 then (
+        Printf.printf "%s and %s are α-equivalent\n" (string_of_lam lam1) (string_of_lam lam2)
+    ) else (
+        Printf.printf "%s and %s are not α-equivalent\n" (string_of_lam lam1) (string_of_lam lam2)
+    );
+    exit 0
+);
+
+if !typecheck_option then (
+    let lexbuf = Lexing.from_channel (match file with
+      | None -> stdin
+      | Some file -> file
+    )
+    in
+    let lambda_term, ty =
+        try
+            Parser.main_typed_lambda Lexer.token lexbuf
+        with e -> (
+            Printf.printf "Can't read typed lambda term\n";
+            raise e
+       )
+    in
+    Printf.printf "The type of %s is " (string_of_lam lambda_term);
+    if not (typecheck [] lambda_term ty) then (
+        Printf.printf "not "
+    );
+    Printf.printf "%s.\n" (string_of_ty ty);
+    exit 0
+);
+
+if !computetype_option then (
+    let lexbuf = Lexing.from_channel (match file with
+      | None -> stdin
+      | Some file -> file
+    )
+    in
+    let lambda_term =
+        try
+            Parser.main_lambda Lexer.token lexbuf
+        with e -> (
+            Printf.printf "Can't read lambda term\n";
+            raise e
+        )
+    in
+    begin match (computeType [] lambda_term) with
+      | Some t ->
+            Printf.printf "The type of %s is %s\n" (string_of_lam lambda_term) (string_of_ty t)
+      | None -> (
+            Printf.printf
+                "λ-term %s can't be typed! (it is not closed or not typable)\n"
+                (string_of_lam lambda_term)
+        )
+    end;
+    exit 0
+);
+
+(* 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 =
@@ -62,95 +166,215 @@ let subgoals: (ty * (var_lambda * ty) list) list ref = ref [(ty, [])] in
 let fill_holes = ref (fun holes -> List.hd holes) in
 
 while !subgoals <> [] do
-    let (ty, hyps) = List.hd !subgoals in
-    subgoals := List.tl !subgoals;
-
     if is_interactive then (
         (* Nettoyage du terminal *)
         let _ = Sys.command("clear -x") in
 
         (* Affichage des hypothèses *)
-        List.iter (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) hyps;
+        List.iter
+            (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h))
+            (snd (List.hd !subgoals));
 
         (* Affichage des sous-buts *)
         Printf.printf "================\n";
-        Printf.printf "%s\n" (string_of_ty ty);
+        List.iter (fun (ty, _) ->
+            Printf.printf "%s\n" (string_of_ty ty)
+        ) !subgoals;
 
         (* Lecture d'une tactique *)
         Printf.printf "What do you want to do?\n"
     );
 
-    let tactic =
+    let rec read_tactic () =
-        let rec read_tactic () =
+        try
-            try
+            let lexbuf = Lexing.from_string (readline ()) in
-                let lexbuf = Lexing.from_string (readline ()) in
+            Parser.main_tactic Lexer.token lexbuf
-                Parser.main_tactic Lexer.token lexbuf
+        with e -> raise TacticParseException
-            with e -> (
-                  Printf.printf "Can't parse tactic\n";
-                  if is_interactive then
-                      read_tactic ()
-                  else
-                      raise e
-            )
-        in
-        read_tactic ()
     in
 
-    let f = !fill_holes in
+    let rec applyTactic tactic = (
+        let (ty, hyps) = List.hd !subgoals in
 
-    match tactic with
+        let find_hyp (var: var_lambda) : ty option =
-      | Intro var -> (
-            match ty with
-              | TImpl (ty1, ty2) -> (
-                    subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
-                    fill_holes := fun holes -> match holes with
-                      | h :: hs -> f (LFun (var, ty1, h) :: hs)
-                      | _ -> fail ()
-                )
-              | _ -> failwith "Can't intro"
-        )
-      | Assumption -> (
             let rec explore = function
-              | (var, hyp) :: _ when hyp = ty -> (
+              | [] -> None
-                    fill_holes := fun holes -> f ((LVar var) :: holes)
+              | (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp
-                )
-              | [] -> failwith "No such hypothesis"
               | _ :: hyps -> explore hyps
             in
             explore hyps
-        )
+        in
-      | Apply var -> (
+
-            let rec explore = function
+        let f = !fill_holes in
-              | (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> (
+        match tactic with
-                    subgoals := (t1, hyps) :: !subgoals;
+          | Intro var -> (
-                    fill_holes := function
+                match ty with
-                      | hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes)
+                  | TImpl (ty1, ty2) -> (
-                      | [] -> fail ()
+                        subgoals := List.tl !subgoals;
+                        subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                          | h :: hs -> f (LFun (var, ty1, h) :: hs)
+                          | _ -> raise TrouException
+                    )
+                  | _ -> raise (TacticException(tactic, "Cannot intro when the goal is not an implication."))
+            )
+          | Intros [] -> ()
+          | Intros (t :: ts) -> (
+                applyTactic (Intro t);
+                applyTactic (Intros ts)
+            )
+          | Assumption -> (
+                let rec explore = function
+                  | (var, hyp) :: _ when hyp = ty -> (
+                        subgoals := List.tl !subgoals;
+                        fill_holes := fun holes -> f ((LVar var) :: holes)
+                    )
+                  | [] -> raise (TacticException (tactic, "Cannot find such an assumption."))
+                  | _ :: hyps -> explore hyps
+                in
+                explore hyps
+            )
+          | Apply var -> (
+                match find_hyp var with
+                  | Some (TImpl (t1, t2)) when t2 = ty -> (
+                        subgoals := List.tl !subgoals;
+                        subgoals := (t1, hyps) :: !subgoals;
+                        fill_holes := function
+                          | hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
+                          | [] -> raise TrouException
+                    )
+                  | None -> raise (TacticException (
+                        tactic,
+                        "Cannot apply hypotesis " ^ var ^ " as it does not exist."
+                    ))
+                  | _ -> raise (TacticException (
+                        tactic,
+                        "Cannot apply hypotesis " ^ var ^ " as it is not an implication."
+                    ))
+            )
+          | Elim var -> (
+                match find_hyp var with
+                  | Some TFalse -> (
+                        subgoals := List.tl !subgoals;
+                        fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
+                    )
+                  | Some TAnd(tl,tr) -> (
+                        subgoals := List.tl !subgoals;
+                        subgoals := (TImpl (tl, TImpl (tr, ty)), hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                          | h::r -> f ((LApp (LApp (h, LFst (LVar var)), LSnd (LVar var))) :: r)
+                          | _ -> raise TrouException
+                    )
+                  | Some TOr(tl,tr) -> (
+                        subgoals := List.tl !subgoals;
+                        subgoals := (TImpl (tl, ty), hyps) :: (TImpl (tr, ty), hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                          | hl::hr::r -> f (LCase (LVar var, hl, hr) :: r)
+                          | _ -> raise TrouException
+                      )
+                  | None -> raise (TacticException (
+                        tactic,
+                        "Cannot apply hypotesis " ^ var ^ " as it does not exist."
+                    ))
+                  | _ -> raise (TacticException (
+                        tactic,
+                        "Cannot apply hypotesis " ^ var ^ " as it is neither an implication, a /\\ nor a \\/"
+                    ))
+            )
+          (* Pour montrer A, on montre B -> A et B *)
+          | Cut tint -> (
+                subgoals := List.tl !subgoals;
+                subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
+                fill_holes := function
+                  | pf :: px :: s -> f ((LApp (pf, px)) :: s)
+                  | _ -> raise TrouException
+            )
+
+          | Split -> (
+                match ty with
+                  | TAnd(t1,t2) -> (
+                        subgoals := List.tl !subgoals;
+                        subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                          | h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs)
+                          | _ -> raise TrouException
+                    )
+                  | _ -> raise (TacticException (tactic, "Cannot split as the goal is not a /\\"))
+            )
+          | Left -> (
+                match ty with
+                  | TOr(tl,tr) -> (
+                        subgoals := List.tl !subgoals;
+                        subgoals := (tl, hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                          | hl :: hs -> f (LIg(hl,tr) :: hs)
+                          | _ -> raise TrouException
+                    )
+                  | _ -> raise (TacticException (tactic, "Cannot apply left as the goal is not a \\/"))
+            )
+          | Right -> (
+                match ty with
+                  | TOr(tl,tr) -> (
+                        subgoals := List.tl !subgoals;
+                        subgoals := (tr, hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                          | hr :: hs -> f (LId(hr,tl) :: hs)
+                          | _ -> raise TrouException
+                    )
+                  | _ -> raise (TacticException (tactic, "Cannot apply right as the goal is not a \\/"))
+            )
+          | Exact l -> (
+                if not (typecheck hyps l ty) then
+                    let ty_str = match computeType [] l with
+                      | None -> "None"
+                      | Some t -> string_of_ty t
+                    in
+                    raise (TacticException (
+                        tactic,
+                        "λ-term " ^ (string_of_lam l) ^
+                        " can't be typed with " ^ (string_of_ty ty) ^
+                        " as its type is " ^ ty_str
+                    ))
+                else (
+                    subgoals := List.tl !subgoals;
+                    fill_holes := fun holes -> f (l::holes)
                 )
-              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
+            )
-              | _ :: hyps -> explore hyps
+    )
-            in
+    in
-            explore hyps;
+
-        )
+    let rec applyUntilWorking () =
-        | Cut tint -> (
+        try (
-            subgoals := (TImpl(tint, ty), hyps)::(tint, hyps)::!subgoals;
+            let readTactic = read_tactic () in
-            fill_holes := function 
+            applyTactic readTactic
-                | (pf::px::s) -> f ((LApp(pf, px))::s)
-                | _ -> fail ()
         )
+        with
+          | 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 ->
+                Printf.printf "\027[31mCannot parse the tactic, please refer to pieuvre documentation.\027[0m\n";
+                if is_interactive then
+                    applyUntilWorking ()
+                else
+                    raise TacticParseException
+          | e ->
+                Printf.printf "\027[31mPieuvre Failed Unexpectedly !\027[0m\n";
+                raise e
+    in
+    applyUntilWorking ()
 done;
 
 let finalLam = !fill_holes [] in
-    if (typecheck [] finalLam ty)
+if (typecheck [] finalLam ty) then (
-    then 
+    Printf.printf "Final proof :\n";
-        Printf.printf "Final proof :\n%s\n" (string_of_lam finalLam)
+    reduce finalLam;
-    else
+) else (
-    (
+    Printf.printf "Invalid proof constructed!\n";
-        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 "%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"
-        Printf.printf "The whole development team of pieuvre is sorry for the damage eventually done by this error.\n"
+);
-    )
-;;
-    
-
 
+close_out log_file;;

parser.mly

@@ -4,17 +4,22 @@
 %}
 
 /* Description des lexèmes définis dans lexer.mll */
-%token LPAREN RPAREN RARROW TILDE FALSE
+%token LPAREN RPAREN RARROW TILDE LAND LOR COMMA FALSE TRUE
 %token EOF
 
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
 
-%token DOT INTRO ASSUMPTION APPLY CUT
+%token DOT INTRO INTROS ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT EXACT FST SND IG ID CASE I
+%token FUN MAPS_TO COLON EXF
+
+%token AMPERSAND
 
 /* L'ordre de définition définit la priorité */
 %right RARROW
 %nonassoc TILDE
+%left LAND
+%left LOR
 
 %start main_type
 %type <Structs.ty> main_type
@@ -22,22 +27,80 @@
 %start main_tactic
 %type <Tactic.tactic> main_tactic
 
+%start main_lambda
+%type <Structs.lam> main_lambda
+
+%start main_two_lambda
+%type <Structs.lam * Structs.lam> main_two_lambda
+
+%start main_typed_lambda
+%type <Structs.lam * Structs.ty> main_typed_lambda
+
 %%
 main_type:
   | ty EOF                                { $1 }
 
+main_tactic:
+  | tactic EOF                            { $1 }
+
+main_lambda:
+  | lambda EOF                            { $1 }
+
+main_two_lambda:
+  | lambda AMPERSAND lambda EOF           { $1, $3 }
+
+main_typed_lambda:
+  | lambda COLON ty EOF                   { $1, $3 }
+
+/* Types */
 ty:
   | LPAREN ty RPAREN                      { $2 }
   | ty RARROW ty                          { TImpl ($1, $3) }
   | TYPE_NAME                             { TSimple $1 }
   | TILDE ty                              { TImpl ($2, TFalse) }
+  | ty LAND ty                            { TAnd($1, $3) }
+  | ty LOR ty                             { TOr($1, $3) }
   | FALSE                                 { TFalse }
+  | TRUE                                  { TTrue }
 
-main_tactic:
+var_list:
-  | tactic EOF                            { $1 }
+  | VAR_NAME                              { [$1] }
+  | VAR_NAME var_list                     { $1 :: $2 }
 
+/* Tactiques */
 tactic:
   | INTRO VAR_NAME DOT                    { Intro $2 }
+  | INTROS var_list DOT                   { Intros $2 }
   | ASSUMPTION DOT                        { Assumption }
   | APPLY VAR_NAME DOT                    { Apply $2 }
+  | ELIM VAR_NAME DOT                     { Elim $2 }
   | CUT ty DOT                            { Cut $2 }
+  | SPLIT DOT                             { Split }
+  | LEFT DOT                              { Left }
+  | RIGHT DOT                             { Right }
+  | EXACT lambda DOT                      { Exact $2 }
+
+/* Lambda-termes */
+lambda_arg: /* Expression pouvant être en argument d'une fonction */
+  | VAR_NAME                              { LVar $1 }
+  | EXF LPAREN lambda COLON ty RPAREN     { LExf ($3, $5) }
+  | FST LPAREN lambda RPAREN              { LFst ($3) }
+  | SND LPAREN lambda RPAREN              { LSnd ($3) }
+  | IG LPAREN lambda COMMA ty RPAREN      { LIg ($3, $5) }
+  | ID LPAREN lambda COMMA ty RPAREN      { LId ($3, $5) }
+  | CASE LPAREN lambda COMMA lambda COMMA lambda RPAREN
+                                          { LCase ($3, $5,$7) }
+  | I                                     { LI }
+  | LPAREN lambda COMMA lambda RPAREN     { LCouple($2, $4) }
+  | LPAREN lambda RPAREN                  { $2 }
+
+/* Application d'une fonction */
+lambda_app:
+  | lambda_app lambda_arg                 { LApp ($1, $2) }
+  | lambda_arg                            { $1 }
+
+lambda:
+  | lambda_app                            { $1 }
+  | FUN VAR_NAME COLON ty MAPS_TO lambda  { LFun ($2, $4, $6) }
+  | FUN LPAREN VAR_NAME COLON ty RPAREN MAPS_TO lambda
+                                          { LFun ($3, $5, $8) }

pieuvre.ml

@@ -5,29 +5,46 @@ open Str
 exception TODOException;;
 exception IllegalVarNameException of var
 
+(* Casse un objet option *)
+let optionmatch (nonefun: 'b option) (somefun: 'a -> 'b option) (o: 'a option) : 'b option =
+    match o with
+        | Some x -> somefun x
+        | None -> nonefun
+;;
+
 (* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
 let rec string_of_ty (t: ty) : string =
     match t with
         | TSimple(tn) -> tn
         | TImpl(t1,t2) -> "(" ^ (string_of_ty t1) ^ " -> " ^ (string_of_ty t2) ^ ")"
-        | TFalse -> "⊥"
+        | TAnd(t1,t2) -> "(" ^ (string_of_ty t1) ^ " /\\ " ^ (string_of_ty t2) ^ ")"
+        | TOr(t1,t2) -> "(" ^ (string_of_ty t1) ^  " \\/ " ^ (string_of_ty t2) ^ ")"
+        | TFalse -> "False"
+        | TTrue -> "True"
 ;;
 
 (* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
 let rec string_of_lam (l: lam) : string = match l with
-    | LFun(v,t,l') -> "λ"^v^":"^(string_of_ty t)^" . "^(string_of_lam l')
+    | LFun(v,t,l') -> "(fun "^v^":"^(string_of_ty t)^" => "^(string_of_lam l')^")"
     | LApp(l1, l2) -> "("^(string_of_lam l1)^" "^(string_of_lam l2)^")"
     | LVar(v) -> v
     | LExf(l',t) -> "exf("^(string_of_lam l')^" : "^(string_of_ty t)^")"
+    | LCouple(lg,ld) -> "("^(string_of_lam lg)^","^(string_of_lam ld)^")"
+    | LFst(ll) -> "fst("^(string_of_lam ll)^")"
+    | LSnd(ll) -> "snd("^(string_of_lam ll)^")"
+    | LIg(ll,t) -> "ig("^(string_of_lam ll)^","^(string_of_ty t)^")"
+    | LId(ll,t) -> "id("^(string_of_lam ll)^","^(string_of_ty t)^")"
+    | LCase(ll,lg,ld) -> "case("^(string_of_lam ll)^","^(string_of_lam lg)^","^(string_of_lam ld)^")"
+    | LI -> "I"
 ;;
 
 let split, tsplit =
     let splitter regex x =
-    if string_match regex x 0
+    if (string_match regex x 0)
         then
             let xStr = matched_group 1 x in
             let xInt = matched_group 2 x in
-            (xStr, int_of_string xInt)
+            (xStr, if xInt="" then 0 else (int_of_string xInt))
 
     else raise (IllegalVarNameException(x))
     in (splitter varRegex, splitter tvarRegex);;
@@ -42,11 +59,36 @@ let findFreeName (l: lam) (x: var) =
         | LVar(v) -> let (vS,vI) = split v in
             if xStr=vS then maxi := max !maxi vI
         | LExf(l',t) -> finder l'
+        | LCouple(l1,l2) -> (finder l1;finder l2)
+        | LFst(l') -> finder l'
+        | LSnd(l') -> finder l'
+        | LIg(l',t) -> finder l'
+        | LId(l',t) -> finder l'
+        | LCase(ll,lg,ld) -> (finder ll; finder lg; finder ld)
+        | LI -> ()
+
     in
     finder l;
     xStr ^ (string_of_int (!maxi+1))
 ;;
 
+(* Renvoie un nom non utilisé dans la liste de nom donnée, basée sur le nom x *)
+let findHypName (names: var list) (x: var) =
+    let xStr = fst (split x) in
+    let maxi = ref 0 in
+    let rec finder l = match l with
+        | [] -> ()
+        | v::r ->
+            begin
+                let (vS,vI) = split v in
+                (if xStr=vS then maxi := max !maxi vI);
+                finder r
+            end
+    in
+    finder names;
+    xStr ^ (string_of_int (!maxi+1))
+;;
+
 (* Renvoie un nom de type simple non utilisé dans le type t qui commence par x *)
 let findTFreeName (t: ty) (x: tvar) =
     let xStr = fst (tsplit x) in
@@ -55,6 +97,9 @@ let findTFreeName (t: ty) (x: tvar) =
         | TImpl(t1, t2) -> (finder t1;finder t2)
         | TSimple(y) -> let (yS,yI) = split y in
             if xStr=yS then maxi := max !maxi yI
+        | TAnd(t1, t2) -> (finder t1;finder t2)
+        | TOr(t1, t2) -> (finder t1;finder t2)
+        | TTrue -> ()
         | TFalse -> () (* Le faux ne réserve pas de variables *)
     in
     finder t;
@@ -72,6 +117,14 @@ let rec replace (l: lam) (x: var) (s: lam) = match l with
     | LApp(l1, l2) -> LApp(replace l1 x s, replace l2 x s)
     | LVar(v) -> if v=x then s else LVar(v)
     | LExf(l',t) -> LExf(replace l' x s, t)
+    | LCouple(lg,ld) -> LCouple(replace lg x s, replace ld x s)
+    | LFst(l') -> LFst(replace l' x s)
+    | LSnd(l') -> LSnd(replace l' x s)
+    | LIg(l',t) -> LIg(replace l' x s, t)
+    | LId(l',t) -> LId(replace l' x s, t)
+    | LCase(l',lg,ld) -> LCase(replace l' x s, replace lg x s, replace ld x s)
+    | LI -> LI
+
 ;;
 
 (* Teste si les deux λ-termes l1 et l2 sont α-convertibles *)
@@ -81,16 +134,23 @@ let rec alpha (l1: lam) (l2: lam) : bool =
             (t1 = t2) &&
             (* On trouve un nom libre dans les deux sous-termes *)
             let v' = findFreeName (LApp(l1', l2')) v1 in
-            alpha (replace l1 v1 (LVar(v'))) (replace l2 v2 (LVar(v')))
+            alpha (replace l1' v1 (LVar(v'))) (replace l2' v2 (LVar(v')))
         | (LApp(lf1,lx1),LApp(lf2,lx2)) -> (alpha lf1 lf2) && (alpha lx1 lx2)
         | (LVar(x1),LVar(x2)) -> x1 = x2
         | (LExf(l1', t1),LExf(l2', t2)) -> t1=t2 && (alpha l1' l2')
+        | (LFst(l1),LFst(l2)) -> alpha l1 l2
+        | (LSnd(l1),LSnd(l2)) -> alpha l1 l2
+        | (LIg(l1,t1),LIg(l2,t2)) -> t1=t2 && alpha l1 l2
+        | (LId(l1,t1),LId(l2,t2)) -> t1=t2 && alpha l1 l2
+        | (LCase(l1,lg1,ld1),LCase(l2,lg2,ld2)) -> (alpha l1 l2) && (alpha lg1 lg2) && (alpha ld1 ld2)
+        | (LI,LI) -> true
+
         | _ -> false (* Les deux formules n'ont pas la même structure *)
 ;;
 
 (* 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 +164,31 @@ 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)))
+    | LCouple(lg,ld) -> optionmatch (Option.bind (betastep ld) (fun lg' -> Some (LCouple(ld,lg')))) (fun lg' -> Some (LCouple(lg',ld))) (betastep lg)
+    | LFst(ll) -> begin
+        match (ll,betastep ll) with
+        | (_,Some ll') -> Some (LFst(ll'))
+        | (LCouple(lg,ld),None) -> Some lg
+        | (_,None) -> None
+        end
+    | LSnd(ll) -> begin
+        match (ll,betastep ll) with
+        | (_,Some ll') -> Some (LFst(ll'))
+        | (LCouple(lg,ld),None) -> Some ld
+        | (_,None) -> None
+        end
+    | LIg(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LIg(l',t)))
+    | LId(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LId(l',t)))
+    | LCase(ll,lg,ld) ->  begin
+        match (ll,betastep ll) with
+        | (_,Some ll') -> Some (LFst(ll'))
+        | (LIg(_,_),None) -> Some lg
+        | (LId(_,_),None) -> Some ld
+        | (_,None) -> None
+        end
+    | LI -> None
+
 ;;
 
 (* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
@@ -116,7 +200,7 @@ let rec reduce (l:lam) : unit =
     | None -> ()
 ;;
 
-(* Calcule le type du λ-terme l sous l'environnement env. 7
+(* Calcule le type du λ-terme l sous l'environnement env.
 Renvoie None si la formule n'est pas typable ou si la formule n'est pas close (sous d'environnement)*)
 let rec computeType (env: gam) (l: lam) : ty option =
     match l with
@@ -136,11 +220,24 @@ let rec computeType (env: gam) (l: lam) : ty option =
             else computeType env' l
         | [] -> None
         end
-    | LExf(l',t) ->
+    | LExf(l',t) -> begin
-        if (computeType env l')=Some t
+        match (computeType env l') with
-        then Some t
+        | Some TFalse -> Some t (* On applique le ExFalso *)
-        else None (* Le ex falso a le mauvais type *)
+        | _ -> None (* Le ex falso a le mauvais type *)
+        end
+    | LCouple(lg,ld) -> Option.bind (computeType env lg) (fun tg -> Option.bind (computeType env ld) (fun td -> Some (TAnd(tg,td))))
+    | LFst(l') -> Option.bind (computeType env l') (function TAnd(t1,t2) -> Some t1 | _ -> None)
+    | LSnd(l') -> Option.bind (computeType env l') (function TAnd(t1,t2) -> Some t2 | _ -> None)
+    | LIg(l',td) -> Option.bind (computeType env l') (fun tg -> Some (TOr(tg,td)))
+    | LId(l',tg) -> Option.bind (computeType env l') (fun td -> Some (TOr(tg,td)))
+    | LCase(l',lg,ld) -> begin
+        match (computeType env l',computeType env lg,computeType env ld) with
+        | (Some TOr(t1a,t1b),Some TImpl(t2a,t2c),Some TImpl(t3b,t3c)) when t1a=t2a && t1b=t3b && t2c=t3c -> Some t3c
+        | _ -> None
+        end
+    | LI -> Some TTrue
 ;;
 
 (* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
-let typecheck (env: gam) (l: lam) (t: ty) : bool = (computeType env l = Some t);
+let typecheck (env: gam) (l: lam) (t: ty) : bool =
+    computeType env l = Some t;;

structs.ml

@@ -1,26 +1,36 @@
 (* Variables des λ-termes *)
 type var_lambda = string;;
 type var = var_lambda;; (* TODEL *)
-let varRegex = Str.regexp "^([a-z]+)([0-9]*)$";;
+let varRegex = Str.regexp "^\\([a-z]+\\)\\([0-9]*\\)$";;
 
 (* Variable des types simples *)
 type var_type = string;;
 type tvar = var_type;; (* TODEL *)
 
-let tvarRegex = Str.regexp "^([A-Z]+)([0-9]*)$";;
+let tvarRegex = Str.regexp "^([A-Z]+)([0-9]*)?$";;
 
 (* Type complexe *)
 type ty =
   | TSimple of var_type
   | TImpl of ty * ty
-  | TFalse;;
+  | TAnd of ty * ty
+  | TOr of ty * ty
+  | TFalse
+  | TTrue;;
 
 (* λ-terme *)
 type lam =
   | LFun of var_lambda * ty * lam
   | LApp of lam * lam
   | LVar of var_lambda
-  | LExf of lam * ty;;
+  | LExf of lam * ty
+  | LCouple of lam * lam
+  | LFst of lam
+  | LSnd of lam
+  | LIg of lam * ty
+  | LId of lam * ty
+  | LCase of lam * lam * lam
+  | LI;;
 
 (* Environnement de typage *)
 type gam = (var_type * ty) list;;

tactic.ml

@@ -2,6 +2,12 @@ open Structs;;
 
 type tactic =
   | Intro of var_lambda
+  | Intros of var_lambda list
   | Assumption
   | Apply of var_lambda
-  | Cut of ty;;
+  | Elim of var_lambda
+  | Cut of ty
+  | Split
+  | Left
+  | Right
+  | Exact of lam;;

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.

tests/elim-and.8pus

@@ -0,0 +1,6 @@
+(A /\ B) -> A
+intro et.
+elim et.
+intro a.
+intro b.
+assumption.

tests/elim-faux.8pus

@@ -0,0 +1,3 @@
+False -> A
+intro f.
+elim f.

tests/elim-or.8pus

@@ -0,0 +1,12 @@
+(A \/ B) -> (~A -> B)
+intro ou.
+intro aa.
+elim ou.
+intro a.
+cut False.
+intro ff.
+elim ff.
+apply aa.
+assumption.
+intro b.
+assumption.

tests/et.8pus

@@ -0,0 +1,26 @@
+( (A /\ B) /\ C -> A /\ (B /\ C) ) /\ ( A /\ (B /\ C) -> (A /\ B) /\ C )
+split.
+intro et.
+elim et.
+intro ab.
+intro c.
+elim ab.
+intro a.
+intro b.
+split.
+assumption.
+split.
+assumption.
+assumption.
+intro et.
+elim et.
+intro a.
+intro bc.
+elim bc.
+intro b.
+intro c.
+split.
+split.
+assumption.
+assumption.
+assumption.

tests/intro-and.8pus

@@ -0,0 +1,15 @@
+(A/\B)->(A->C)->(B->D)->(C/\D)
+intro et.
+intro i1.
+intro i2.
+split.
+apply i1.
+elim et.
+intro a.
+intro b.
+assumption.
+apply i2.
+elim et.
+intro a.
+intro b.
+assumption.

tests/intro-or.8pus

@@ -0,0 +1,13 @@
+(A \/ B) -> (A -> C) -> (B -> D) -> (C \/ D)
+intro ou.
+intro i1.
+intro i2.
+elim ou.
+intro a.
+left.
+apply i1.
+assumption.
+intro b.
+right.
+apply i2.
+assumption.

tests/intros.8pus

@@ -0,0 +1,4 @@
+A -> (A -> B) -> B
+intros a f.
+apply f.
+assumption.

tests/irrefutabilite-peirce.8pus

@@ -0,0 +1,38 @@
+~~(((A -> B) -> A) -> A)
+intro peirce.
+cut ~~(A \/ ~A).
+intro te.
+apply te.
+intro te2.
+elim te2.
+intro a.
+cut ~A.
+intro f.
+apply f.
+assumption.
+intro a2.
+apply peirce.
+intro f.
+assumption.
+intro na.
+apply peirce.
+intro f.
+apply f.
+intro a.
+cut False.
+intro false.
+elim false.
+apply na.
+assumption.
+intro f.
+cut ~A.
+intro f2.
+cut A \/ ~A.
+assumption.
+right.
+assumption.
+intro a.
+cut A \/ ~A.
+assumption.
+left.
+assumption.

tests/irrefutabilite-tiers-exclu.8pus

@@ -0,0 +1,13 @@
+~~(F \/ ~F)
+intro f.
+cut ~F.
+intro f2.
+cut F \/ ~F.
+assumption.
+right.
+assumption.
+intro f2.
+cut F \/ ~F.
+assumption.
+left.
+assumption.

tests/lambda-terms/alpha-eq.lams

@@ -0,0 +1,3 @@
+fun x: A => x x
+&
+fun y: A => y y

tests/lambda-terms/alpha-not-eq.lams

@@ -0,0 +1,3 @@
+fun x: A => x x
+&
+fun y: A => y y y

tests/lambda-terms/lambda.lam

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

tests/ou.8pus

@@ -0,0 +1,32 @@
+(A \/ (B \/ C) -> (A \/ B) \/ C) /\ ((A \/ B) \/ C -> A \/ (B \/ C))
+split.
+intro ou.
+elim ou.
+intro a.
+left.
+left.
+assumption.
+intro bc.
+elim bc.
+intro b.
+left.
+right.
+assumption.
+intro c.
+right.
+assumption.
+intro ou.
+elim ou.
+intro ab.
+elim ab.
+intro a.
+left.
+assumption.
+intro b.
+right.
+left.
+assumption.
+intro c.
+right.
+right.
+assumption.

tests/test01.8pus

@@ -0,0 +1,10 @@
+(A -> B -> C) -> (B -> A -> C)
+intro f.
+intro b.
+intro a.
+cut B -> C.
+intro g.
+apply g.
+assumption.
+apply f.
+assumption.

tests/test02.8pus

@@ -0,0 +1,4 @@
+A -> B -> A
+intro a.
+intro b.
+assumption.

tests/test03.8pus

@@ -0,0 +1,5 @@
+A -> (A -> B) -> B
+intro a.
+intro f.
+apply f.
+assumption.

tests/test04.8pus

@@ -0,0 +1,7 @@
+(A -> B) -> (B -> C) -> A -> C
+intro f.
+intro g.
+intro a.
+apply g.
+apply f.
+assumption.

tests/test05.8pus

@@ -0,0 +1,5 @@
+((A -> A) -> B) -> B
+intro f.
+apply f.
+intro x.
+assumption.

tests/test06.8pus

@@ -0,0 +1,11 @@
+(A -> B -> C) -> (A -> B) -> A -> C
+intro f.
+intro g.
+intro a.
+cut B -> C.
+intro h.
+apply h.
+apply g.
+assumption.
+apply f.
+assumption.

tests/test07.8pus

@@ -0,0 +1,5 @@
+A -> ~(~A)
+intro x.
+intro f.
+apply f.
+assumption.

tests/test08.8pus

@@ -0,0 +1,7 @@
+(A -> B) -> ~B -> ~A
+intro f.
+intro b.
+intro a.
+apply b.
+apply f.
+assumption.

tests/typecheck/right-type

@@ -0,0 +1 @@
+fun x: A => fun f: A -> False => f x : A -> ~~A

tests/typecheck/wrong-type

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

tests/vrai-pas-faux.8pus

@@ -0,0 +1,8 @@
+(True \/ False) /\ (~(False /\ True))
+split.
+left.
+exact I.
+intro x.
+elim x.
+intro a.
+elim a.