From d071fa74c51da381145f7a6f3943e1df9ccfe5c0 Mon Sep 17 00:00:00 2001
From: Michael Zhang <failed.down@gmail.com>
Date: Tue, 20 Feb 2018 05:04:09 -0600
Subject: [PATCH] holy shit it works

---
 lambda.ml  | 80 ++++++++++++++++++++++++++++++++++++------------------
 parser.mly | 13 +++++----
 2 files changed, 61 insertions(+), 32 deletions(-)

diff --git a/lambda.ml b/lambda.ml
index 943c29a..39c5cc7 100644
--- a/lambda.ml
+++ b/lambda.ml
@@ -5,7 +5,12 @@ open Types
 
 exception EvaluationComplete
 
-let rec string_of_term (t:term) =
+(*
+((\a.(\b.((a a) b))) (\a.(\b.a))) (\a.(\b.a))
+((\a.(\b.((a b) a))) (\a.(\b.a))) (\a.(\b.b))
+ *)
+
+let rec string_of_term (t: Types.term) =
   match t with
   | TmAbs(x, t1) ->
       "(\\" ^ x ^ "." ^ (string_of_term t1) ^ ")"
@@ -13,40 +18,63 @@ let rec string_of_term (t:term) =
       "(" ^ (string_of_term t1) ^ " " ^ (string_of_term t2) ^ ")"
   | TmVar(x) -> x
 
-(*
-let termshift d t =
-  let rec walk c t =
-    match t with
-    | TmVar(x) -> if 
+let rec string_of_ctx (c: Types.context) =
+  match c with
+  | [] -> ""
+  | (n, t)::r -> (n ^ ": " ^ (string_of_term t) ^ "\n" ^ (string_of_ctx r))
 
-let termsubsttop (s:term) (t:term) =
-  termshift (-1) (termsubst 0 (termshift 1 s) t)
-
-let rec isval ctx t =
-  match t with
-  | TmAbs(_, _, _) -> true
-  | _ -> false
-
-let rec helper ctx t =
-  match t with
-  | TmApp(TmAbs(x, t1), v2) when isval ctx v2 -> termsubsttop v2 t1
-  | _ -> EvaluationComplete
-*)
-
-let assign ctx (name, t) : context =
+let assign ctx (name, t) : Types.context =
   (name, t)::ctx
 
-let rec lookup ctx name : term =
+let remove ctx name =
+  List.filter (fun (a, b) -> a != name) ctx
+
+let rec lookup ctx name : Types.term =
   match ctx with
-  | [] -> raise (Failure ("unbound variable " ^ name))
+  | [] -> print_endline ("unbound variable " ^ name); raise (Failure ("unbound variable " ^ name))
   | (n, t)::tail ->
       if n = name then t else lookup tail name
 
+let rec subst name tm repl =
+  match tm with
+  | TmVar(x) -> if x = name then repl else TmVar(x)
+  | TmAbs(n, t) -> if n = name then TmAbs(n, t) else TmAbs(n, subst name t repl)
+  | TmApp(a, b) -> TmApp(subst name a repl, subst name b 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')))
+
 let rec eval (ctx, t) =
-  let rec helper (ctx, t) =
-    raise EvaluationComplete
+  let rec helper (ctx, t) d =
+    (*print_endline ((String.init (d * 2) (fun _ -> ' ')) ^ "helper" ^ (string_of_term t));
+    print_endline (string_of_ctx ctx);*)
+    match t with
+    | TmApp(TmApp(_, _) as a, b) ->
+        let (_, a') = helper (ctx, a) (d + 1) in
+        helper (ctx, TmApp(a', b)) (d + 1)
+    | TmApp(TmAbs(n, t), r) ->
+        (* 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"));*)
+        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
+        helper (ctx, TmApp(a, b)) (d + 1)
+    | TmVar(n) -> (ctx, lookup ctx n)
+    | TmAbs(_, TmVar(_)) as t -> (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"));*)
+        if s then helper (ctx, t') (d + 1) else (ctx, t')
+    | _ -> (*print_endline "called EvaluationComplete"; *)raise EvaluationComplete
   in try
-    let (ctx', t') = helper (ctx, t) in
+    let (ctx', t') = helper (ctx, t) 0 in
+    if t = t' then raise EvaluationComplete else
     eval (ctx', t')
   with EvaluationComplete -> (ctx, t)
 
diff --git a/parser.mly b/parser.mly
index 4c3299b..e816dcf 100644
--- a/parser.mly
+++ b/parser.mly
@@ -10,8 +10,12 @@
 %token <string> Ident
 %token Lambda
 
+%right prec_Abs
+%left prec_App
+
 %start main
 %type <Types.input> main
+
 %%
 
 main:
@@ -22,12 +26,9 @@ assign:
   | Ident Equal expr { Types.Assign($1, $3) }
 ;
 expr:
-  | var { Types.TmVar($1) }
+  | Ident { Types.TmVar($1) }
   | LParen expr RParen { $2 }
-  | Lambda var Dot expr { Types.TmAbs($2, $4) }
-  | expr expr { Types.TmApp($1, $2) }
-;
-var:
-  Ident { $1 }
+  | Lambda Ident Dot expr %prec prec_Abs { Types.TmAbs($2, $4) }
+  | expr expr %prec prec_App { Types.TmApp($1, $2) }
 ;