Merge remote-tracking branch 'origin/master'

README.md

@@ -1,11 +1,18 @@
-The Pieuvre Proof Prover
-=
+The Pieuvre Proof Assistant
+===========================
 
-# Presentation
+# Utilisation
 
-# Note d'implementation
+## Option `typecheck`
+L'option `typecheck` peut être testée avec les fichiers tests dans `tests/typecheck`. Pour cela, utiliser les commandes :
+```
+./pieuvre -typecheck tests/typecheck/right-type
+./pieuvre -typecheck tests/typecheck/wrong-type
+```
 
-# Répartition du travail
+## Note d'implémentation
+
+## Répartition du travail
 
 ### Adrien
 

lexer.mll

@@ -27,7 +27,7 @@ rule token = parse
 
   | "fun"                       { FUN }
   | "=>"                        { MAPS_TO }
-  | ':'                         { VDOTS }
+  | ':'                         { COLON }
   | "exf"                       { EXF }
   | "fst"                       { FST }
   | "snd"                       { SND }

main.ml

@@ -83,28 +83,27 @@ if !alpha_option then (
     exit 0
 );
 
-(*if !typecheck_option then (
+if !typecheck_option then (
     let lexbuf = Lexing.from_channel (match file with
       | None -> stdin
       | Some file -> file
     )
     in
-    let lambda_term =
+    let lambda_term, ty =
         try
-            Parser.main_lambda Lexer.token lexbuf
+            Parser.main_typed_lambda Lexer.token lexbuf
         with e -> (
-            Printf.printf "Can't read lambda term\n";
+            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 typecheck [] lambda_term then (
-        Printf.printf "correct\n"
-    ) else (
-        Printf.printf "incorrect\n"
+    if not (typecheck [] lambda_term ty) then (
+        Printf.printf "not "
     );
+    Printf.printf "%s.\n" (string_of_ty ty);
     exit 0
-);*)
+);
 
 (* Show a message only if the input is read from stdin *)
 let show s = match file with
@@ -143,7 +142,6 @@ while !subgoals <> [] do
         explore hyps
     in
 
-
     if is_interactive then (
         (* Nettoyage du terminal *)
         let _ = Sys.command("clear -x") in
@@ -286,7 +284,7 @@ done;
 let finalLam = !fill_holes [] in
     if (typecheck [] finalLam ty) then (
         Printf.printf "Final proof :\n";
-        reduce finalLam
+        reduce finalLam;
     )
     else (
         Printf.printf "Invalid proof constructed!\n";

parser.mly

@@ -11,7 +11,7 @@
 %token <string> TYPE_NAME
 
 %token DOT INTRO ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT FST SND IG ID CASE
-%token FUN MAPS_TO VDOTS EXF
+%token FUN MAPS_TO COLON EXF
 
 %token AMPERSAND
 
@@ -33,6 +33,9 @@
 %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 }
@@ -44,7 +47,10 @@ main_lambda:
   | lambda EOF                            { $1 }
 
 main_two_lambda:
-  | lambda AMPERSAND lambda               { $1, $3 }
+  | lambda AMPERSAND lambda EOF           { $1, $3 }
+
+main_typed_lambda:
+  | lambda COLON ty EOF                   { $1, $3 }
 
 /* Types */
 ty:
@@ -67,7 +73,7 @@ tactic:
   | SPLIT DOT                             { Split }
   | LEFT DOT                              { Left }
   | RIGHT DOT                             { Right }
-  
+
 /* Lambda-termes */
 lambda_arg: /* Expression pouvant être en argument d'une fonction */
   | VAR_NAME                              { LVar $1 }
@@ -80,7 +86,7 @@ lambda_app:
 
 lambda:
   | lambda_app                            { $1 }
-  | FUN VAR_NAME VDOTS ty MAPS_TO lambda  { LFun ($2, $4, $6) }
-  | FUN LPAREN VAR_NAME VDOTS ty RPAREN MAPS_TO lambda
+  | 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) }
-  | EXF LPAREN VAR_NAME VDOTS ty RPAREN   { LExf (LVar $3, $5) }
+  | EXF LPAREN VAR_NAME COLON ty RPAREN   { LExf (LVar $3, $5) }

pieuvre.ml

@@ -18,7 +18,7 @@ let rec string_of_ty (t: ty) : string =
         | 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) ^ ")"
-        | TOr(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"
 ;;
@@ -234,4 +234,5 @@ let rec computeType (env: gam) (l: lam) : ty option =
 ;;
 
 (* 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;;

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