Typecheck

lexer.mll

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

main.ml

@@ -77,28 +77,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
@@ -137,7 +136,6 @@ while !subgoals <> [] do
         explore hyps
     in
 
-
     if is_interactive then (
         (* Nettoyage du terminal *)
         let _ = Sys.command("clear -x") in
@@ -267,7 +265,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:
@@ -81,7 +87,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) }

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