Add arguments to main.ml

lam.ml

@@ -8,6 +8,7 @@ type lam =
   | Var of id
   | Exf of lam * Types.ty
 
+
 (** alpha renaming in a deterministic way *)
 let alpha_convert (e : lam) : lam =
   let cpt_var = ref 0 in (* id cpt for variables *)
@@ -15,26 +16,23 @@ let alpha_convert (e : lam) : lam =
     let v = "__"^(string_of_int !cpt)
     in incr cpt; v
 
-  in let renamed = ref []
+    in let get_ren_var (var : id) (g : (id * id) list): id = (* returns var if not found *)
-  in let new_ren_var (cpt : int ref) (var : id) : id = (* checks if a variable already has a new id, or generates one *)
+    match List.assoc_opt var g with
-    let var' = generator cpt in (
-      renamed := (var, var')::!renamed;
-      var'
-    )
-
-  in let get_ren_var (var : id) : id = (* returns var if not found *)
-    match List.assoc_opt var !renamed with
       | Some var' -> var'
       | None -> var
 
-  in let rec alpha_aux (e : lam) : lam = match e with (* actual renaming *)
+  in let rec alpha_aux (e : lam) (g : (id * id) list): lam = match e with (* actual renaming *)
-    Fun ((v, t), e) -> Fun ((new_ren_var cpt_var v, t), alpha_aux e)
+    Fun ((v, t), e) ->
-    | App (e1, e2) -> App (alpha_aux e1, alpha_aux e2)
+      let v' = generator cpt_var in
-    | Var v -> Var (get_ren_var v)
+      Fun ((v', t), alpha_aux e ((v, v')::g))
-    | Exf (e, t) -> Exf (alpha_aux e, t)
+    | App (e1, e2) -> App (alpha_aux e1 g, alpha_aux e2 g)
-  in alpha_aux e
+    | Var v -> Var (get_ren_var v g)
+    | Exf (e, t) -> Exf (alpha_aux e g, t)
+  in alpha_aux e []
 
 
 (** alpha equivalence *)
 let (=~) (e1 : lam) (e2 : lam) : bool =
   alpha_convert e1 = alpha_convert e2
+
+(** beta-reduction *)

main.ml

@@ -1,6 +1,11 @@
 open Affichage
 open Typing
 
+type entry =
+  Simple of Lam.lam
+  | AlphaEquiv of Lam.lam * Lam.lam
+
+
 let interpret e =
   begin
     print_expr e;
@@ -9,12 +14,52 @@ let interpret e =
     print_newline()
   end
 
-let lexbuf = Lexing.from_channel stdin
+let nom_fichier = ref ""
+let equiv_fichier = ref ""
 
-let parse () = Parser.main Lexer.token lexbuf
+let parse_channel c =
+  let lexbuf = Lexing.from_channel c in
+  Parser.main Lexer.token lexbuf
 
-let calc () =
+let recupere_entree () =
-  let result = parse () in
+  let optlist = [
-  interpret result; flush stdout
+   ("-alphaequiv", Arg.Set_string equiv_fichier, "Vérifie l'alpha équivalence avec un autre fichier");
+  ] in
+
+  let usage = "Bienvenue à bord." in  (* message d'accueil, option -help *)
+
+  Arg.parse (* ci-dessous les 3 arguments de Arg.parse : *)
+    optlist (* la liste des options definie plus haut *)
+
+    (fun s -> nom_fichier := s) (* la fonction a declencher lorsqu'on recupere un string qui n'est pas une option : ici c'est le nom du fichier, et on stocke cette information dans la reference nom_fichier *)
+    usage; (* le message d'accueil *)
+
+  let lam1 = try
+    let where_from = match !nom_fichier with
+      | "" -> stdin
+      | s -> open_in s in
+    parse_channel where_from
+  with e -> (Printf.printf "problème de saisie\n"; raise e)
+  in if !equiv_fichier <> "" then
+    let lam2 = try parse_channel (open_in !equiv_fichier)
+    with e -> (Printf.printf "problème de saisie\n"; raise e)
+    in AlphaEquiv (lam1, lam2)
+  else Simple lam1
+
+
+(* la fonction principale *)
+let run () =
+  try
+    match recupere_entree () with
+     Simple l -> let _ = interpret l in ()
+    | AlphaEquiv (l1, l2) -> begin
+        if ((Lam.(=~)) l1 l2) then
+          print_string "true\n"
+        else
+          print_string "false\n"
+      end;
+    flush stdout
+  with e -> raise e
+
+let _ = run ()
 
-let _ = calc()

tests/alpha_equiv/basic.ml

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

tests/alpha_equiv/basic_alpha.ml

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

tests/alpha_equiv/basic_alpha2.ml

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