diff --git a/: b/: deleted file mode 100644 index b86e16f..0000000 --- a/: +++ /dev/null @@ -1,44 +0,0 @@ -%{ -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/expr.ml b/expr.ml index 0601ea1..31d611c 100644 --- a/expr.ml +++ b/expr.ml @@ -7,3 +7,37 @@ type expr = | App of expr * expr | Var of id | Exf of expr * string + +(** alpha renaming in a deterministic way *) +let alpha_convert (e : expr) : expr = + 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 *) + let v = string_of_int !cpt + in incr cpt; v + + in let renamed = ref [] + in let rename (cpt : int ref) (var : id) : id = (* checks if a variable already has a new id, or generates one *) + match List.assoc_opt var !renamed with + | Some var' -> var' + | None -> let var' = generator cpt in ( + renamed := (var, var')::!renamed; + var') + + in let rec alpha_ty (t : Types.ty) : Types.ty = match t with + Arr (t1, t2) -> Arr (alpha_ty t1, alpha_ty t2) + | TVar (v) -> TVar (rename cpt_ty v) + | Bot -> Bot + + + in let rec alpha_aux (e : expr) : expr = 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) + | Exf (e, s) -> Exf (alpha_aux e, s) + in alpha_aux e + + +(** alpha equivalence *) +let (=~) (e1 : expr) (e2 : expr) : bool = + alpha_convert e1 = alpha_convert e2 \ No newline at end of file