# HG changeset patch
# User atton
# Date 1477975998 0
# Node ID 4bfeb679ef15c4af58f738501132890d44df4b47
# Parent  5fa32bb75df68f8342f6462cccbfa039a8013c3a
Add eval1 in Untyped

diff -r 5fa32bb75df6 -r 4bfeb679ef15 untyped/Untyped.hs
--- a/untyped/Untyped.hs	Sun Oct 30 13:17:46 2016 +0000
+++ b/untyped/Untyped.hs	Tue Nov 01 04:53:18 2016 +0000
@@ -1,5 +1,8 @@
 module Untyped where
 
+import Data.Either
+import Data.Functor
+
 type Index       = Int
 type ContextSize = Int
 type Name        = String
@@ -15,7 +18,6 @@
 index2name :: Context -> Index -> String
 index2name ctx i = fst $ ctx !! i
 
--- my implementation
 pickFreshName :: Context -> Name -> (Context, Name)
 pickFreshName ctx n = (((freshName, NameBind) : ctx), freshName)
         where
@@ -31,7 +33,6 @@
   | length ctx == n = index2name ctx i
   | otherwise     = "[bad index]"
 
--- from book
 termShift :: Int -> Term -> Term
 termShift d t = walk 0 t
   where
@@ -41,3 +42,44 @@
     walk c (TmAbs x t1)  = TmAbs x (walk (c+1) t1)
     walk c (TmApp t1 t2) = TmApp (walk c t1) (walk c t2)
 
+termSubst :: Index -> Term -> Term -> Term
+termSubst j s t = walk 0 t
+  where
+    walk c (TmVar x n)
+      | x == (j+c) = termShift c s
+      | otherwise  = TmVar x n
+    walk c (TmAbs x t1)  = TmAbs x (walk (c+1) t1)
+    walk c (TmApp t1 t2) = TmApp (walk c t1) (walk c t2)
+
+termSubstTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t)
+
+isVal :: Context -> Term -> Bool
+isVal ctx (TmAbs _ _) = True
+isval _    _          = False
+
+eval1 :: Context -> Term -> Either String Term
+eval1 ctx (TmApp (TmAbs x t12) v2)
+  | isVal ctx v2 = return $ termSubstTop v2 t12
+  | otherwise    = Left $ show v2 ++ " is not variable."
+eval1 ctx (TmApp t1 t2)
+  | isVal ctx t1 = eval1 ctx t2 >>= (\t -> return $ TmApp t1 t)
+  | otherwise    = eval1 ctx t1 >>= (\t -> return $ TmApp t t2)
+eval1 _ _ = Left "No Rule Applies"
+
+
+-- x
+sampleContext1 = [("x", NameBind)]
+sampleTerm1    = TmVar 0 1
+
+-- \y -> y
+sampleContext2  = []
+sampleTerm2     = TmAbs "y" (TmVar 0 1)
+
+-- (\x -> x) (\x -> x x) == \x' -> x' x'
+sampleContext3 = []
+sampleTerm3    = (TmApp (TmAbs "x" (TmVar 0 1)) (TmAbs "x" (TmApp (TmVar 0 1) (TmVar 0 1))))
+
+-- (\y -> (\x -> y)) (\x -> x x)
+sampleContext4 = []
+sampleTerm3    = (TmApp (TmAbs "x" (TmVar 0 1)) (TmAbs "x" (TmApp (TmVar 0 1) (TmVar 0 1))))
+sampleTerm4    = TmApp (TmAbs "y" (TmAbs "x" (TmVar 1 2))) (TmAbs "x" (TmApp (TmVar 0 1) (TmVar 0 1)))