diff --git a/Makefile b/Makefile index 25cc62d..e2b6871 100644 --- a/Makefile +++ b/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 diff --git a/affichage.ml b/affichage.ml index c659de2..b4f79eb 100644 --- a/affichage.ml +++ b/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 ^ ")" - | Bot -> "#" + "(" ^ s1 ^ " -> " ^ s2 ^ ")" + | 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" diff --git a/expr.ml b/expr.ml deleted file mode 100644 index 0601ea1..0000000 --- a/expr.ml +++ /dev/null @@ -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 diff --git a/lam.ml b/lam.ml new file mode 100644 index 0000000..80bb36b --- /dev/null +++ b/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 diff --git a/lexer.mll b/lexer.mll index 8d05184..6d5c765 100644 --- a/lexer.mll +++ b/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 } - | '0' { BOTTOM } + | "True" { TOP } + | "False" { BOT } | '(' { LPAREN } | ')' { RPAREN } | "fun" { FUN } | ':' { COLON } | "=>" { ARR } + | "->" { TARR } + | '~' { TILDE } | "exf" { EXFALSO } | var_id as s { VARID(s) } | ty_id as s { TYID(s) } diff --git a/main.ml b/main.ml index f2d1bc5..733b2dc 100644 --- a/main.ml +++ b/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 diff --git a/parser.mly b/parser.mly index 97b74b7..51ee756 100644 --- a/parser.mly +++ b/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 VARID %token TYID %token EOL -%right ARR +%right TARR +%right TILDE %start main -%type main +%type 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: diff --git a/tests/arrow_types.lam b/tests/arrow_types.lam index 932ed93..d6c6d20 100644 --- a/tests/arrow_types.lam +++ b/tests/arrow_types.lam @@ -1 +1 @@ -fun (f : A => B) => f +fun (f : A -> B) => f diff --git a/tests/exfalso1.lam b/tests/exfalso1.lam new file mode 100644 index 0000000..44844de --- /dev/null +++ b/tests/exfalso1.lam @@ -0,0 +1 @@ +fun (x : A) => exf (x : A) diff --git a/tests/exfalso2.lam b/tests/exfalso2.lam new file mode 100644 index 0000000..8b9336f --- /dev/null +++ b/tests/exfalso2.lam @@ -0,0 +1 @@ +exf(fun (f : ~A) => fun (x : A) => f x : (A -> False) -> A -> False) diff --git a/tests/exfalso3.lam b/tests/exfalso3.lam new file mode 100644 index 0000000..81c3674 --- /dev/null +++ b/tests/exfalso3.lam @@ -0,0 +1 @@ +fun (f : ~A) => fun (x : A) => exf (x : A) diff --git a/tests/neg.lam b/tests/neg.lam new file mode 100644 index 0000000..d23211f --- /dev/null +++ b/tests/neg.lam @@ -0,0 +1 @@ +fun (x : ~A -> B) => x diff --git a/tests/nested_arrow.lam b/tests/nested_arrow.lam new file mode 100644 index 0000000..c340aed --- /dev/null +++ b/tests/nested_arrow.lam @@ -0,0 +1 @@ +fun (x : A -> B -> C -> ~A) => x diff --git a/tests/nested_function.lam b/tests/nested_function.lam index b021a6e..8d679c4 100644 --- a/tests/nested_function.lam +++ b/tests/nested_function.lam @@ -1 +1 @@ -fun (f : A => B) => fun (x : A) => f x +fun (f : A -> B) => fun (x : A) => f x diff --git a/tests/one.lam b/tests/one.lam new file mode 100644 index 0000000..6aa0147 --- /dev/null +++ b/tests/one.lam @@ -0,0 +1 @@ +fun (z : A) => fun (f : A -> A) => f z diff --git a/tests/three.lam b/tests/three.lam new file mode 100644 index 0000000..4344001 --- /dev/null +++ b/tests/three.lam @@ -0,0 +1 @@ +fun (z : A) => fun (f : A -> A) => f (f (f z)) diff --git a/tests/zero.lam b/tests/zero.lam new file mode 100644 index 0000000..7bb3a58 --- /dev/null +++ b/tests/zero.lam @@ -0,0 +1 @@ +fun (z : A) => fun (f : A -> A) => z diff --git a/types.ml b/types.ml index e5ad378..810e3d0 100644 --- a/types.ml +++ b/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 diff --git a/typing.ml b/typing.ml new file mode 100644 index 0000000..86c1d25 --- /dev/null +++ b/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"