typage du exfalso, etc

Makefile

@@ -1,4 +1,4 @@
-pieuvre: main.ml expr.ml affichage.ml lexer.mll parser.mly
+pieuvre: main.ml lam.ml affichage.ml lexer.mll parser.mly
 	dune build
 	cp _build/default/main.exe pieuvre
 	chmod +w pieuvre

affichage.ml

@@ -1,4 +1,4 @@
-open Expr
+open Lam
 open Types
 
 (* fonction d'affichage *)
@@ -7,8 +7,8 @@ let rec string_of_ty = function
   | Arr(t1, t2) ->
     let s1 = string_of_ty t1 in
     let s2 = string_of_ty t2 in
-    s1 ^ " => (" ^ s2 ^ ")"
+    "(" ^ s1 ^ " -> " ^ s2 ^ ")"
-  | Bot -> "#"
+  | Bot -> "False"
 
 let rec string_of_expr = function
   Fun ((s, t), e) ->
@@ -16,12 +16,19 @@ let rec string_of_expr = function
     let s_e = string_of_expr e in
     "fun (" ^ s ^ " : " ^ s_ty ^ ") => (" ^ s_e ^ ")"
   | App (e1, e2) ->
-    "("^(string_of_expr e1)^") "^(string_of_expr e2)
+    "("^(string_of_expr e1)^" "^(string_of_expr e2)^")"
   | Var (s) -> s
-  | Exf (e, s) -> "exf("^(string_of_expr e)^":"^s^")"
+  | Exf (e, t) ->
+    let s_e = string_of_expr e in
+    let s_ty = string_of_ty t in
+    "exf (" ^ s_e ^ " : " ^ s_ty ^ ")"
 
 
+let print_ty t =
+  print_string (string_of_ty t)
+
 let print_expr e =
   print_string (string_of_expr e)
 
-let affiche_val v = print_string "TODO"
+
+let affiche_val _ = print_string "TODO"

expr.ml

@@ -1,9 +0,0 @@
-type id = string
-
-type ty_annot = id * Types.ty
-
-type expr =
-  Fun of ty_annot * expr
-  | App of expr * expr
-  | Var of id
-  | Exf of expr * string

lam.ml

@@ -0,0 +1,9 @@
+type id = string
+
+type ty_annot = id * Types.ty
+
+type lam =
+  Fun of ty_annot * lam
+  | App of lam * lam
+  | Var of id
+  | Exf of lam * Types.ty

lexer.mll

@@ -9,20 +9,22 @@ let digit = ['0'-'9']
 let word = (lowercase | uppercase)*
 
 let var_id = lowercase lowercase* digit*
-let ty_id = uppercase word digit*
+let ty_id = uppercase uppercase* digit*
 
 rule token = parse
   | [' ' '\t']     { token lexbuf }
   | '\n'            { EOL }
   | '+'             { PLUS }
   | '*'             { TIMES }
-  | '1'             { TOP }
+  | "True"          { TOP }
-  | '0'             { BOTTOM }
+  | "False"         { BOT }
   | '('             { LPAREN }
   | ')'             { RPAREN }
   | "fun"           { FUN }
   | ':'             { COLON }
   | "=>"            { ARR }
+  | "->"            { TARR }
+  | '~'             { TILDE }
   | "exf"           { EXFALSO }
   | var_id as s     { VARID(s) }
   | ty_id as s      { TYID(s) }

main.ml

@@ -1,11 +1,11 @@
-open Expr
 open Affichage
+open Typing
 
 let interpret e =
   begin
     print_expr e;
     print_newline();
-    (*print_int (eval e);*)
+    print_ty (typeinfer [] e);
     print_newline()
   end
 

parser.mly

@@ -1,21 +1,22 @@
 %{
-open Expr
+open Lam
 open Types
 %}
 
 %token PLUS TIMES
-%token TOP BOTTOM EXFALSO
+%token TOP BOT EXFALSO TILDE
 %token LPAREN RPAREN
-%token FUN ARR COLON
+%token FUN ARR COLON TARR
 %token <string> VARID
 %token <string> TYID
 
 %token EOL
 
-%right ARR
+%right TARR
+%right TILDE
 
 %start main
-%type <Expr.expr> main
+%type <Lam.lam> main
                                                          
 %%
 main:
@@ -26,12 +27,16 @@ ty_annot:
 
 ty:
   | id=TYID                 { TVar(id) }
+  | BOT                     { Bot }
   | LPAREN t=ty RPAREN      { t }
-  | t1=ty ARR t2=ty         { Arr(t1, t2) }
+  | TILDE t=ty              { Arr(t, Bot) }
+  | t1=ty TARR t2=ty        { Arr(t1, t2) }
 
 expression:
   | FUN LPAREN annot=ty_annot RPAREN ARR e=expression 
                             { Fun (annot, e) }
+  | EXFALSO LPAREN e=expression COLON t=ty RPAREN
+                            { Exf (e, t) }
   | e=app_expr              { e }
 
 app_expr:

tests/arrow_types.lam

@@ -1 +1 @@
-fun (f : A => B) => f
+fun (f : A -> B) => f

tests/exfalso1.lam

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

tests/exfalso2.lam

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

tests/exfalso3.lam

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

tests/neg.lam

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

tests/nested_arrow.lam

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

tests/nested_function.lam

@@ -1 +1 @@
-fun (f : A => B) => fun (x : A) => f x
+fun (f : A -> B) => fun (x : A) => f x

tests/one.lam

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

tests/three.lam

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

tests/zero.lam

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

types.ml

@@ -5,4 +5,4 @@ type ty =
   | Arr of ty * ty
   | Bot
 
-type gam = ty_id * ty list
+type gam = (ty_id * ty) list

typing.ml

@@ -0,0 +1,41 @@
+open Types
+open Lam
+
+let rec typecheck (g : gam) (e : lam) (expected_t : ty) =
+  match e with
+  Var x -> (List.assoc x g) = expected_t
+  | Fun ((x, actual_t1), e) ->
+    begin match expected_t with
+    Arr (expected_t1, expected_t2) ->
+      let g' = (x, expected_t1)::g in
+      (actual_t1 = expected_t1) && (typecheck g' e expected_t2)
+    | _ -> false
+    end
+  | App (e1, e2) ->
+    begin match typeinfer g e1 with
+    Arr (expected_t2, actual_t) ->
+        (actual_t = expected_t) && (typecheck g e2 expected_t2)
+    | _ -> false
+    end
+  | Exf (e, t) ->
+    (expected_t = Bot) && (typecheck g e t)
+
+and typeinfer (g : gam) (e : lam) : ty =
+  match e with
+  Var x -> List.assoc x g
+  | Fun ((x, t1), e) ->
+    let g' = (x, t1)::g in
+    let t2 = typeinfer g' e in
+    Arr (t1, t2)
+  | App (e1, e2) ->
+    begin match typeinfer g e1 with
+    Arr (t1, t2) ->
+      if typecheck g e2 t1
+      then t2
+      else failwith "couldn't infer"
+    | _ -> failwith "couldn't infer"
+    end
+  | Exf (e, t) ->
+    if typecheck g e t
+    then Bot
+    else failwith "couldn't infer"