Test d'alpha equivalence

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 }

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

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 <Structs.lam> main_lambda
 
+%start main_two_lambda
+%type <Structs.lam * Structs.lam> 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 }

tests/lambda-terms/alpha-eq.lam

@@ -0,0 +1,3 @@
+fun x: A => x x
+&
+fun y: A => y y

tests/lambda-terms/alpha-not-eq.lam

@@ -0,0 +1,3 @@
+fun x: A => x x
+&
+fun y: A => y y y