l3-ENSL/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge branch

Browse Source
This commit is contained in:
augustin64 2024-04-16 10:30:10 +02:00
commit bc697b30a0
18 changed files with 92 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -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

19
affichage.ml
View File

@ -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"

14
expr.ml → lam.ml
View File

@ -2,14 +2,14 @@ type id = string
type ty_annot = id * Types.ty
type expr =
Fun of ty_annot * expr
| App of expr * expr
type lam =
Fun of ty_annot * lam
| App of lam * lam
| Var of id
| Exf of expr * string
| Exf of lam * Types.ty
(** alpha renaming in a deterministic way *)
let alpha_convert (e : expr) : expr =
let alpha_convert (e : lam) : lam =
let cpt_ty = ref 0 in (* id cpt for type variables *)
let cpt_var = ref 0 in (* id cpt for variables *)
let generator (cpt : int ref) : id = (* id generator *)
@ -30,7 +30,7 @@ let alpha_convert (e : expr) : expr =
| Bot -> Bot
in let rec alpha_aux (e : expr) : expr = match e with (* actual renaming *)
in let rec alpha_aux (e : lam) : lam = match e with (* actual renaming *)
Fun ((v, t), e) -> Fun ((rename cpt_var v, alpha_ty t), alpha_aux e)
| App (e1, e2) -> App (alpha_aux e1, alpha_aux e2)
| Var v -> Var (rename cpt_var v)
@ -39,5 +39,5 @@ let alpha_convert (e : expr) : expr =
(** alpha equivalence *)
let (=~) (e1 : expr) (e2 : expr) : bool =
let (=~) (e1 : lam) (e2 : lam) : bool =
alpha_convert e1 = alpha_convert e2

8
lexer.mll
View File

@ -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) }

4
main.ml
View File

@ -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

17
parser.mly
View File

@ -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:

2
tests/arrow_types.lam
View File

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

1
tests/exfalso1.lam Normal file
View File

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

1
tests/exfalso2.lam Normal file
View File

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

1
tests/exfalso3.lam Normal file
View File

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

1
tests/neg.lam Normal file
View File

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

1
tests/nested_arrow.lam Normal file
View File

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

2
tests/nested_function.lam
View File

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

1
tests/one.lam Normal file
View File

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

1
tests/three.lam Normal file
View File

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

1
tests/zero.lam Normal file
View File

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

2
types.ml
View File

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

41
typing.ml Normal file
View File

@ -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"