.gitignore

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

Makefile

@@ -10,11 +10,8 @@ main.byte:
 
 byte: main.byte
 
-test: all
+.PHONY: clean test
-	  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,67 +1,14 @@
-The Pieuvre™ Proof Assistant
+The Pieuvre Proof Prover
-============================
+=
 
-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™ !
+# Presentation
 
-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.
+# Note d'implementation
 
-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é.
+# Répartition du travail
-
-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
-- Introduction du README
+Fonctions de manipulation des λ-termes (pieuvre.ml)
-- Fonctions de manipulation des λ-termes (`pieuvre.ml`)
+Typecheck
-- Typecheck
-- Erreurs lors des tactiques.
-- `\/` et `/\`
-- Parsing des λ-termes
-- `True` et `exact`
-- Option `-computetype`
-- Écriture de tests

lexer.mll

@@ -10,36 +10,12 @@ 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 }

main.ml

@@ -1,28 +1,20 @@
 open Structs;;
 open Pieuvre;;
-open Tactic;;
 
-(* Lorsqu'une tactique ne peut se lancer. Contient la tactique ainsi qu'un message contenant l'erreur.*)
+let fail () =
-exception TacticException of tactic*string;;
+    failwith "Unknown error";;
-(* 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_option = ref false in
+let reduce = ref false in
-let alpha_option = ref false in
+let alpha = ref false in
 let typecheck_option = ref false in
-let computetype_option = ref false in
 
 Arg.parse
-    [("-reduce", Arg.Set reduce_option, "Show the step-by-step reduction of a lambda-term");
+    [("-reduce", Arg.Set reduce, "Show the step-by-step reduction of a lambda-term");
-     ("-alpha", Arg.Set alpha_option, "Check is two lambda-terms separated by '&' are alpha-convertible");
+     ("-alpha", Arg.Set alpha, "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:";
 
@@ -36,105 +28,7 @@ let is_interactive = match file with
   | _ -> false
 in
 
-if !reduce_option then (
+let readline () = match file with
-    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
-    reduce lambda_term;
-    exit 0
-);
-
-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;
@@ -142,9 +36,11 @@ let readline () =
     )
   | Some f -> input_line f
 in
-    Printf.fprintf log_file "%s\n" line;
+
-    flush log_file;
+(* Show a message only if the input is read from stdin *)
-    line
+let show s = match file with
+  | None -> Printf.printf "%s" s
+  | _ -> ()
 in
 
 show "Please type the formula to prove\n";
@@ -166,215 +62,95 @@ 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
+        List.iter (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) hyps;
-            (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h))
-            (snd (List.hd !subgoals));
 
         (* Affichage des sous-buts *)
         Printf.printf "================\n";
-        List.iter (fun (ty, _) ->
+        Printf.printf "%s\n" (string_of_ty 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 () =
             try
                 let lexbuf = Lexing.from_string (readline ()) in
                 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 ()
-    let rec applyTactic tactic = (
-        let (ty, hyps) = List.hd !subgoals in
-
-        let find_hyp (var: var_lambda) : ty option =
-            let rec explore = function
-              | [] -> None
-              | (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp
-              | _ :: hyps -> explore hyps
-            in
-            explore hyps
     in
 
     let f = !fill_holes in
+
     match tactic with
       | Intro var -> (
             match ty with
               | TImpl (ty1, ty2) -> (
-                        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
+                      | _ -> fail ()
                 )
-                  | _ -> raise (TacticException(tactic, "Cannot intro when the goal is not an implication."))
+              | _ -> failwith "Can't intro"
-            )
-          | 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."))
+              | [] -> failwith "No such hypothesis"
               | _ :: hyps -> explore hyps
             in
             explore hyps
         )
       | Apply var -> (
-                match find_hyp var with
+            let rec explore = function
-                  | Some (TImpl (t1, t2)) when t2 = ty -> (
+              | (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> (
-                        subgoals := List.tl !subgoals;
                     subgoals := (t1, hyps) :: !subgoals;
                     fill_holes := function
-                          | hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
+                      | hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes)
-                          | [] -> raise TrouException
+                      | [] -> fail ()
                 )
-                  | None -> raise (TacticException (
+              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
-                        tactic,
+              | _ :: hyps -> explore hyps
-                        "Cannot apply hypotesis " ^ var ^ " as it does not exist."
+            in
-                    ))
+            explore hyps;
-                  | _ -> 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)
+                | (pf::px::s) -> f ((LApp(pf, px))::s)
-                  | _ -> raise TrouException
+                | _ -> fail ()
         )
-
-          | 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)
-                )
-            )
-    )
-    in
-
-    let rec applyUntilWorking () =
-        try (
-            let readTactic = read_tactic () in
-            applyTactic readTactic
-        )
-        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) then (
+    if (typecheck [] finalLam ty)
-    Printf.printf "Final proof :\n";
+    then 
-    reduce finalLam;
+        Printf.printf "Final proof :\n%s\n" (string_of_lam finalLam)
-) else (
+    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;;

parser.mly

@@ -4,22 +4,17 @@
 %}
 
 /* Description des lexèmes définis dans lexer.mll */
-%token LPAREN RPAREN RARROW TILDE LAND LOR COMMA FALSE TRUE
+%token LPAREN RPAREN RARROW TILDE FALSE
 %token EOF
 
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
 
-%token DOT INTRO INTROS ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT EXACT FST SND IG ID CASE I
+%token DOT INTRO ASSUMPTION APPLY CUT
-%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
@@ -27,80 +22,22 @@
 %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 }
 
-var_list:
+main_tactic:
-  | VAR_NAME                              { [$1] }
+  | tactic EOF                            { $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,46 +5,29 @@ 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) ^ ")"
-        | TAnd(t1,t2) -> "(" ^ (string_of_ty t1) ^ " /\\ " ^ (string_of_ty t2) ^ ")"
+        | TFalse -> "⊥"
-        | 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') -> "(fun "^v^":"^(string_of_ty t)^" => "^(string_of_lam l')^")"
+    | LFun(v,t,l') -> "λ"^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, if xInt="" then 0 else (int_of_string xInt))
+            (xStr, int_of_string xInt)
 
     else raise (IllegalVarNameException(x))
     in (splitter varRegex, splitter tvarRegex);;
@@ -59,36 +42,11 @@ 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
@@ -97,9 +55,6 @@ 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;
@@ -117,14 +72,6 @@ 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 *)
@@ -134,23 +81,16 @@ 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') -> Option.bind (betastep l') (fun l' -> Some (LFun(v,t,l')))
+    | LFun(v,t,l') -> betastep l'
     | LApp(lf,lx) ->
         begin
         match (betastep lf) with
@@ -164,31 +104,7 @@ let rec betastep (l: lam) : lam option = match l with
                 | _ -> None (* On ne peut pas β-réduire *)
         end
     | LVar(x) -> None
-    | LExf(l',t) -> Option.bind (betastep l') (fun l' -> Some (LExf(l',t)))
+    | LExf(l',_) -> betastep l'
-    | 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 *)
@@ -200,7 +116,7 @@ let rec reduce (l:lam) : unit =
     | None -> ()
 ;;
 
-(* Calcule le type du λ-terme l sous l'environnement env.
+(* Calcule le type du λ-terme l sous l'environnement env. 7
 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
@@ -220,24 +136,11 @@ let rec computeType (env: gam) (l: lam) : ty option =
             else computeType env' l
         | [] -> None
         end
-    | LExf(l',t) -> begin
+    | LExf(l',t) ->
-        match (computeType env l') with
+        if (computeType env l')=Some t
-        | Some TFalse -> Some t (* On applique le ExFalso *)
+        then Some t
-        | _ -> None (* Le ex falso a le mauvais type *)
+        else 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 =
+let typecheck (env: gam) (l: lam) (t: ty) : bool = (computeType env l = Some t);
-    computeType env l = Some t;;

structs.ml

@@ -1,36 +1,26 @@
 (* 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
-  | TAnd of ty * ty
+  | TFalse;;
-  | 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,12 +2,6 @@ open Structs;;
 
 type tactic =
   | Intro of var_lambda
-  | Intros of var_lambda list
   | Assumption
   | Apply of var_lambda
-  | Elim of var_lambda
+  | Cut of ty;;
-  | Cut of ty
-  | Split
-  | Left
-  | Right
-  | Exact of lam;;

tests/cut-impl.8pus

@@ -1,10 +0,0 @@
-(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

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

tests/elim-faux.8pus

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

tests/elim-or.8pus

@@ -1,12 +0,0 @@
-(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

@@ -1,26 +0,0 @@
-( (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

@@ -1,15 +0,0 @@
-(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

@@ -1,13 +0,0 @@
-(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

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

tests/irrefutabilite-peirce.8pus

@@ -1,38 +0,0 @@
-~~(((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

@@ -1,13 +0,0 @@
-~~(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

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

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

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

tests/lambda-terms/lambda.lam

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

tests/ou.8pus

@@ -1,32 +0,0 @@
-(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

@@ -1,10 +0,0 @@
-(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

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

tests/test03.8pus

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

tests/test04.8pus

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

tests/test05.8pus

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

tests/test06.8pus

@@ -1,11 +0,0 @@
-(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

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

tests/test08.8pus

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

tests/typecheck/right-type

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

tests/typecheck/wrong-type

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

tests/vrai-pas-faux.8pus

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