From 97971a1d0c754345a0de439f6c50d659d0ec0b64 Mon Sep 17 00:00:00 2001
From: Michael Zhang <failed.down@gmail.com>
Date: Fri, 16 Feb 2018 05:22:07 -0600
Subject: [PATCH] test

---
 README.md  |  3 +++
 lambda.ml  | 64 +++++++++++++++++++++++++++++++++++++++++++++++-------
 lexer.mll  |  5 ++++-
 parser.mly | 13 ++++++++---
 types.ml   | 11 +++++-----
 5 files changed, 79 insertions(+), 17 deletions(-)

diff --git a/README.md b/README.md
index 5d414e5..41354d6 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,4 @@
 # λ
+
+Based on Benjamin Pierce's _Types and Programming Languages_
+
diff --git a/lambda.ml b/lambda.ml
index e2870d9..3390806 100644
--- a/lambda.ml
+++ b/lambda.ml
@@ -3,24 +3,72 @@ open Lexing
 open Parser
 open Types
 
+exception EvaluationComplete
+
 let rec string_of_term (t:term) =
   match t with
   | TmAbs(x, t1) ->
-      "(\\" ^ (String.make 1 x) ^ "." ^ (string_of_term t1) ^ ")"
+      "(\\" ^ x ^ "." ^ (string_of_term t1) ^ ")"
   | TmApp(t1, t2) ->
-      "(" ^ (string_of_term t1) ^ (string_of_term t2) ^ ")"
-  | TmVar(x) ->
-      String.make 1 x
+      "(" ^ (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 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 =
+  (name, t)::ctx
+
+let rec lookup ctx name : term =
+  match ctx with
+  | [] -> raise (Failure ("unbound variable " ^ name))
+  | (n, t)::tail ->
+      if n = name then t else lookup tail name
+
+let rec eval (ctx, t) =
+  let rec helper (ctx, t) =
+    match t with
+    | Assign(name, t') ->
+        let (ctx', r) = helper(ctx, t') in
+          (assign ctx (name, r), r)
+    | TmAbs(name, t') ->
+        let (ctx', v) = helper (ctx, t') in
+        (assign ctx (name, v), v)
+    | TmVar(name) ->
+        (ctx, lookup ctx name)
+    | _ -> raise EvaluationComplete
+  in try
+    let (ctx', t') = helper (ctx, t) in
+    eval (ctx', t')
+  with EvaluationComplete -> (ctx, t)
 
 let _ =
   try
     let rec loop ctx =
       print_string "> "; flush stdout;
       let lexbuf = Lexing.from_channel stdin in
-      let result = Parser.main Lexer.token lexbuf in
-        print_endline (string_of_term result); flush stdout;
-        loop ctx in
+      let t = Parser.main Lexer.token lexbuf in
+      let (ctx', r) = eval (ctx, t) in
+        print_endline (string_of_term r); flush stdout;
+        loop ctx' in
     loop []
   with Lexer.Eof ->
-    print_endline "error";
+    print_endline "^D";
     exit 0
diff --git a/lexer.mll b/lexer.mll
index f6ac937..04412b6 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -6,7 +6,10 @@
 rule token = parse
   | ' ' | '\t' { token lexbuf }
   | '\n' { EOL }
+  | '=' { Equal }
   | '\\' { Lambda }
+  | '(' { LParen }
+  | ')' { RParen }
   | '.' { Dot }
-  | ['a'-'z'] as c | ['A'-'Z'] as c { Ident(c) }
+  | ['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* as s { Ident(s) }
   | eof { raise Eof }
diff --git a/parser.mly b/parser.mly
index c2959bd..f6e9def 100644
--- a/parser.mly
+++ b/parser.mly
@@ -4,7 +4,10 @@
 
 %token EOL
 %token Dot
-%token <char> Ident
+%token Equal
+%token LParen
+%token RParen
+%token <string> Ident
 %token Lambda
 
 %start main
@@ -12,12 +15,16 @@
 %%
 
 main:
-  expr EOL { $1 }
+  | assign EOL { $1 }
+  | expr EOL { $1 }
+;
+assign:
+  | Ident Equal expr { Types.Assign($1, $3) }
 ;
 expr:
   | var { Types.TmVar($1) }
   | Lambda var Dot expr { Types.TmAbs($2, $4) }
-  | expr expr { Types.TmApp ($1, $2) }
+  | LParen expr expr RParen { Types.TmApp ($2, $3) }
 ;
 var:
   Ident { $1 }
diff --git a/types.ml b/types.ml
index 83286fa..60ca23d 100644
--- a/types.ml
+++ b/types.ml
@@ -1,9 +1,10 @@
+type var = string
+
 type term =
-  | TmVar of char
-  | TmAbs of char * term
+  | Assign of string * term
+  | TmVar of var
+  | TmAbs of var * term
   | TmApp of term * term
 
-type binding = NameBind
-
-type context = (char * binding) list
+type context = (string * term) list