From 0b67d9a5eb86ab4dcc5f990e07ad2f68e40d2e60 Mon Sep 17 00:00:00 2001 From: Marwan Date: Mon, 15 Apr 2024 12:07:49 +0200 Subject: [PATCH] =?UTF-8?q?types=20fl=C3=A8ches=20et=20affichage=20des=20t?= =?UTF-8?q?ypes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- : | 44 +++++++++++++++++++++++++++++++++++++++ affichage.ml | 19 ++++++++++++++--- expr.ml | 2 +- parser.mly | 14 ++++++++----- tests/arrow_types.lam | 1 + tests/id_function.lam | 1 + tests/nested_function.lam | 1 + types.ml | 8 +++++++ 8 files changed, 81 insertions(+), 9 deletions(-) create mode 100644 : create mode 100644 tests/arrow_types.lam create mode 100644 tests/id_function.lam create mode 100644 tests/nested_function.lam create mode 100644 types.ml diff --git a/: b/: new file mode 100644 index 0000000..b86e16f --- /dev/null +++ b/: @@ -0,0 +1,44 @@ +%{ +open Expr +%} + +%token PLUS TIMES +%token TOP BOTTOM EXFALSO +%token LPAREN RPAREN +%token FUN ARR COLON +%token VARID +%token TYID + +%token EOL + + +%left ARR + +%start main +%type main + +%% +main: +e=expression EOL { e } + +ty_annot: + | id=VARID COLON t=ty { (id, t) } + +ty: + | id=TYID { id } + | LPAREN t=ty RPAREN { ty } + | t1=ty ARR t2=ty { + +expression: + | FUN LPAREN annot=ty_annot RPAREN ARR e=expression + { Fun (annot, e) } + | e=app_expr { e } + +app_expr: + | e=app_expr a=atomic { App (e, a) } + | a=atomic { a } + +atomic: + | id=VARID { Var id } + | LPAREN e=expression RPAREN + { e } diff --git a/affichage.ml b/affichage.ml index 493f5d3..c659de2 100644 --- a/affichage.ml +++ b/affichage.ml @@ -1,14 +1,27 @@ open Expr +open Types (* fonction d'affichage *) +let rec string_of_ty = function + TVar s -> s + | Arr(t1, t2) -> + let s1 = string_of_ty t1 in + let s2 = string_of_ty t2 in + s1 ^ " => (" ^ s2 ^ ")" + | Bot -> "#" + let rec string_of_expr = function - Fun ((s, t), e) -> "fun ("^s^":"^t^") => "^(string_of_expr e) - | App (e1, e2) -> "("^(string_of_expr e1)^") "^(string_of_expr e2) + Fun ((s, t), e) -> + let s_ty = string_of_ty t in + 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) | Var (s) -> s | Exf (e, s) -> "exf("^(string_of_expr e)^":"^s^")" + let print_expr e = print_string (string_of_expr e) let affiche_val v = print_string "TODO" - diff --git a/expr.ml b/expr.ml index 72e7192..0601ea1 100644 --- a/expr.ml +++ b/expr.ml @@ -1,6 +1,6 @@ type id = string -type ty_annot = id * string +type ty_annot = id * Types.ty type expr = Fun of ty_annot * expr diff --git a/parser.mly b/parser.mly index 68f5a10..97b74b7 100644 --- a/parser.mly +++ b/parser.mly @@ -1,5 +1,6 @@ %{ open Expr +open Types %} %token PLUS TIMES @@ -10,7 +11,9 @@ open Expr %token TYID %token EOL - + +%right ARR + %start main %type main @@ -18,13 +21,14 @@ open Expr main: e=expression EOL { e } - -ty: - | id=TYID { id } - ty_annot: | id=VARID COLON t=ty { (id, t) } +ty: + | id=TYID { TVar(id) } + | LPAREN t=ty RPAREN { t } + | t1=ty ARR t2=ty { Arr(t1, t2) } + expression: | FUN LPAREN annot=ty_annot RPAREN ARR e=expression { Fun (annot, e) } diff --git a/tests/arrow_types.lam b/tests/arrow_types.lam new file mode 100644 index 0000000..932ed93 --- /dev/null +++ b/tests/arrow_types.lam @@ -0,0 +1 @@ +fun (f : A => B) => f diff --git a/tests/id_function.lam b/tests/id_function.lam new file mode 100644 index 0000000..8e72633 --- /dev/null +++ b/tests/id_function.lam @@ -0,0 +1 @@ +fun (x : A) => x diff --git a/tests/nested_function.lam b/tests/nested_function.lam new file mode 100644 index 0000000..b021a6e --- /dev/null +++ b/tests/nested_function.lam @@ -0,0 +1 @@ +fun (f : A => B) => fun (x : A) => f x diff --git a/types.ml b/types.ml new file mode 100644 index 0000000..e5ad378 --- /dev/null +++ b/types.ml @@ -0,0 +1,8 @@ +type ty_id = string + +type ty = + TVar of ty_id + | Arr of ty * ty + | Bot + +type gam = ty_id * ty list