From b25a764943902608d4884b2bc4340cedff5e2f0b Mon Sep 17 00:00:00 2001
From: Michael Zhang <failed.down@gmail.com>
Date: Tue, 20 Feb 2018 14:46:39 -0600
Subject: [PATCH] this is Wrong

---
 lambda.ml | 41 +++++++++++++++++++++++++++++++----------
 1 file changed, 31 insertions(+), 10 deletions(-)

diff --git a/lambda.ml b/lambda.ml
index 307dcd7..57377fe 100644
--- a/lambda.ml
+++ b/lambda.ml
@@ -7,10 +7,17 @@ exception UnboundVariable of string
 exception EvaluationComplete
 
 (*
-((\a.(\b.((a a) b))) (\a.(\b.a))) (\a.(\b.a))
-((\a.(\b.((a b) a))) (\a.(\b.a))) (\a.(\b.b))
+((\a.(\b.((a a) b))) (\a.(\b.a))) (\a.(\b.a)) = (\a.(\b.a))
+((\a.(\b.((a b) a))) (\a.(\b.a))) (\a.(\b.b)) = (\a.(\b.b))
+
+(\n.\f.\x.f ((n f) x)) (\f.\x.x)
  *)
 
+let debug = true
+
+let print_debug str =
+  if debug then print_endline str else ()
+
 let rec string_of_term (t: Types.term) =
   match t with
   | TmAbs(x, t1) ->
@@ -49,14 +56,26 @@ let rec subst name tm repl =
 
 let rec try_subst name tm repl =
   match tm with
-  | TmVar(x) -> if x = name then (true, repl) else (false, TmVar(x))
-  | TmAbs(n, t) -> if n = name then (false, TmAbs(n, t)) else (let (s, t') = try_subst name t repl in (s, TmAbs(n, t')))
-  | TmApp(a, b) -> (let ((sa, a'), (sb, b')) = (try_subst name a repl, try_subst name b repl) in (sa || sb, TmApp(a', b')))
+  | TmVar(x) ->
+      if x = name then
+        (true, repl)
+      else
+        (false, TmVar(x))
+  | TmAbs(n, t) ->
+      if n = name then
+        let (s, t') = try_subst n t (TmVar n) in
+        (false, TmAbs(n, t'))
+      else
+        let (s, t') = try_subst name t repl in
+        (s, TmAbs(n, t'))
+  | TmApp(a, b) ->
+      let ((sa, a'), (sb, b')) = (try_subst name a repl, try_subst name b repl) in
+      (sa || sb, TmApp(a', b'))
 
 let rec eval (ctx, t) =
   let rec helper (ctx, t) d =
-    (*print_endline ((String.init (d * 2) (fun _ -> ' ')) ^ "helper" ^ (string_of_term t));
-    print_endline (string_of_ctx ctx);*)
+    print_debug ((String.init (d * 2) (fun _ -> ' ')) ^ "helper" ^ (string_of_term t));
+    print_debug (string_of_ctx ctx);
     match t with
     | TmApp(TmApp(_, _) as a, b) ->
         let (_, a') = helper (ctx, a) (d + 1) in
@@ -65,7 +84,7 @@ let rec eval (ctx, t) =
         (* let ctx' = assign ctx (n, r) in
         helper (ctx', t) (d + 1) *)
         let (s, t') = try_subst n t r in
-        (*print_endline ("try_subst('" ^ n ^ "', " ^ (string_of_term t) ^ ", " ^ (string_of_term r) ^ ") = " ^ (if s then "true" else "false"));*)
+        print_debug ("try_subst('" ^ n ^ "', " ^ (string_of_term t) ^ ", " ^ (string_of_term r) ^ ") = " ^ (if s then "true" else "false"));
         if s then helper (ctx, t') (d + 1) else (ctx, t')
     | TmApp(TmVar(n), b) ->
         let (_, a) = helper (ctx, lookup ctx n) (d + 1) in
@@ -75,7 +94,7 @@ let rec eval (ctx, t) =
     | TmAbs(n, _) as t ->
         let r = TmVar(n) in
         let (s, t') = try_subst n t r in
-        (*print_endline ("try_subst('" ^ n ^ "', " ^ (string_of_term t) ^ ", " ^ (string_of_term r) ^ ") = " ^ (if s then "true" else "false"));*)
+        print_debug ("try_subst('" ^ n ^ "', " ^ (string_of_term t) ^ ", " ^ (string_of_term r) ^ ") = " ^ (if s then "true" else "false"));
         if s then helper (ctx, t') (d + 1) else (ctx, t')
   in try
     let (ctx', t') = helper (ctx, t) 0 in
@@ -83,7 +102,9 @@ let rec eval (ctx, t) =
     eval (ctx', t')
   with
   | UnboundVariable v -> raise (Failure ("unbound variable '" ^ v ^ "'"))
-  | EvaluationComplete -> (ctx, t)
+  | EvaluationComplete ->
+      print_debug "evaluation complete";
+      (ctx, t)
 
 let _ =
   let rec loop ctx =