résolution des conflits

lam.ml

@@ -8,7 +8,6 @@ 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 *)
@@ -53,6 +52,7 @@ let rec subst (m : lam) (n : lam) (x : id) : lam =
     let e = subst e n x in
     Exf (e, t)
 
+(* INVARIANT : e has already been alpha-converted *)
 let rec betastep (e : lam) : lam option =
   match e with
   Fun ((x, t), e) ->
@@ -60,16 +60,19 @@ let rec betastep (e : lam) : lam option =
     None -> None
     | Some e -> Some (Fun ((x, t), e))
     end
-  | App ((Fun ((x, t), e)), e2) ->
-    begin match betastep e with
-    None -> Some (subst e e2 x)
-    | Some e -> Some (App ((Fun ((x, t), e)), e2))
-    end
   | App (e1, e2) ->
+    (* reduce leftmost redex.
+       e1 e2 -> e1' e2 then
+       e1_nf e2 -> e1_nf e2 then
+       (fun x -> e_nf) e2_nf -> e_nf[e2/x] *) 
     begin match betastep e1 with
     None ->
       begin match betastep e2 with
-      None -> None
+      None ->
+        begin match e1 with
+        Fun ((x, _), e) -> Some (subst e e2 x)
+        | _ -> None
+        end
       | Some e2 -> Some (App (e1, e2))
       end
     | Some e1 -> Some (App (e1, e2))

main.ml

@@ -3,9 +3,33 @@ open Typing
 
 type entry =
   Simple of Lam.lam
+  | Reduce of Lam.lam
   | AlphaEquiv of Lam.lam * Lam.lam
 
 
+let beta_reduce e =
+  let rec aux = function
+    Some e ->
+      print_expr e;
+      print_newline ();
+      aux (Lam.betastep e);
+    | None -> ()
+  in print_expr e;
+  print_newline ();
+  let e = Lam.alpha_convert e in
+  print_expr e;
+  print_newline ();
+  aux (Lam.betastep e)
+
+let alpha_get_lam where_from =
+  let input_str = In_channel.input_all where_from in
+  match Str.split (Str.regexp "&") input_str with
+    [s1; s2] -> AlphaEquiv (
+          Parser.main Lexer.token (Lexing.from_string (s1^"\n")),
+          Parser.main Lexer.token (Lexing.from_string s2)
+        )
+    | _ -> failwith "Alpha-equivalence: nombre de delimiteurs incorrect"
+
 let interpret e =
   begin
     print_expr e;
@@ -15,7 +39,9 @@ let interpret e =
   end
 
 let nom_fichier = ref ""
+let reduce = ref false
 let alpha = ref false
+let equiv_fichier = ref ""
 
 let parse_channel c =
   let lexbuf = Lexing.from_channel c in
@@ -23,7 +49,12 @@ let parse_channel c =
 
 let recupere_entree () =
   let optlist = [
-   ("-alpha", Arg.Set alpha, "Vérifie l'alpha équivalence de deux termes séparés par &");
+   ("-alpha",
+   Arg.Set alpha,
+   "Vérifie l'alpha équivalence de deux termes séparés par &");
+   ("-reduce",
+   Arg.Set reduce,
+   "Affiche les réductions successives du lambda-terme")
   ] in
 
   let usage = "Bienvenue à bord." in  (* message d'accueil, option -help *)
@@ -38,14 +69,10 @@ let recupere_entree () =
     let where_from = match !nom_fichier with
       | "" -> stdin
       | s -> open_in s in
-    if !alpha then
+    if !alpha
-      let input_str = In_channel.input_all where_from in
+    then alpha_get_lam where_from
-      match Str.split (Str.regexp "&") input_str with
+    else if !reduce
-        [s1; s2] -> AlphaEquiv (
+    then Reduce (parse_channel where_from)
-              Parser.main Lexer.token (Lexing.from_string (s1^"\n")),
-              Parser.main Lexer.token (Lexing.from_string s2)
-            )
-        | _ -> failwith "Alpha-equivalence: nombre de delimiteurs incorrect"
     else Simple (parse_channel where_from)
   with e -> (Printf.printf "problème de saisie\n"; raise e)
 
@@ -54,6 +81,7 @@ let run () =
   try
     match recupere_entree () with
      Simple l -> let _ = interpret l in ()
+    | Reduce l -> let _ = beta_reduce l in ()
     | AlphaEquiv (l1, l2) -> begin
         if ((Lam.(=~)) l1 l2) then
           print_string "true\n"

tests/betared1.lam

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

tests/betared2.lam

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

tests/betared_rename.lam

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