diff --git a/lexer.mll b/lexer.mll index 56e3374..8308435 100644 --- a/lexer.mll +++ b/lexer.mll @@ -23,6 +23,8 @@ rule token = parse | ':' { VDOTS } | "exf" { EXF } + | '&' { AMPERSAND } + | ['A'-'Z']+['0'-'9']* as s { TYPE_NAME s } | ['a'-'z']+['0'-'9']* as s { VAR_NAME s } | '.' { DOT } diff --git a/main.ml b/main.ml index 11e8679..a15359d 100644 --- a/main.ml +++ b/main.ml @@ -55,6 +55,28 @@ if !reduce_option then ( exit 0 ); +if !alpha_option then ( + let lexbuf = Lexing.from_channel (match file with + | None -> stdin + | Some file -> file + ) + in + let lam1, lam2 = + try + Parser.main_two_lambda Lexer.token lexbuf + with e -> ( + Printf.printf "Can't read lambda terms\n"; + raise e + ) + in + if alpha lam1 lam2 then ( + Printf.printf "%s and %s are α-equivalent\n" (string_of_lam lam1) (string_of_lam lam2) + ) else ( + Printf.printf "%s and %s are not α-equivalent\n" (string_of_lam lam1) (string_of_lam lam2) + ); + exit 0 +); + (* Show a message only if the input is read from stdin *) let show s = match file with | None -> Printf.printf "%s" s diff --git a/parser.mly b/parser.mly index b5e1710..34270fa 100644 --- a/parser.mly +++ b/parser.mly @@ -13,6 +13,8 @@ %token DOT INTRO ASSUMPTION APPLY ELIM CUT %token FUN MAPS_TO VDOTS EXF +%token AMPERSAND + /* L'ordre de définition définit la priorité */ %right RARROW %nonassoc TILDE @@ -26,6 +28,9 @@ %start main_lambda %type main_lambda +%start main_two_lambda +%type main_two_lambda + %% main_type: | ty EOF { $1 } @@ -36,6 +41,9 @@ main_tactic: main_lambda: | lambda EOF { $1 } +main_two_lambda: + | lambda AMPERSAND lambda { $1, $3 } + /* Types */ ty: | LPAREN ty RPAREN { $2 } diff --git a/tests/lambda-terms/alpha-eq.lam b/tests/lambda-terms/alpha-eq.lam new file mode 100644 index 0000000..694304a --- /dev/null +++ b/tests/lambda-terms/alpha-eq.lam @@ -0,0 +1,3 @@ +fun x: A => x x +& +fun y: A => y y diff --git a/tests/lambda-terms/alpha-not-eq.lam b/tests/lambda-terms/alpha-not-eq.lam new file mode 100644 index 0000000..aacca0d --- /dev/null +++ b/tests/lambda-terms/alpha-not-eq.lam @@ -0,0 +1,3 @@ +fun x: A => x x +& +fun y: A => y y y