From: Tomáš Musil <tomik.musil@gmail.com>
Date: Thu, 30 Oct 2014 01:57:46 +0000 (+0100)
Subject: substitution
X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/ae04c2201bf076af502c479c2fd93546b453e5fb

substitution
---

diff --git a/Lambda.hs b/Lambda.hs
index d9bdaee..dbb2fcf 100644
--- a/Lambda.hs
+++ b/Lambda.hs
@@ -37,8 +37,22 @@ parseApp = do
   t <- parseTerm
   char ' '
   r <- parseTerm
-  char '('
+  char ')'
   return $! App t r
 
 parseTerm :: Parser Term
 parseTerm = parseVar <|> parseLambda <|> parseApp
+
+-------------------------------------------------
+
+rename :: Term -> Term
+rename (Lambda x t) = Lambda n (substitute x n t)
+  where n = x ++ "r"
+
+substitute :: VarName -> VarName -> Term -> Term
+substitute a b (Var x) = if x == a then Var b else Var x
+substitute a b (Lambda x t) 
+  | x == a = Lambda x t
+  | x == b = substitute a b $ rename (Lambda x t)
+  | otherwise = Lambda x (substitute a b t)
+substitute a b (App t u) = App (substitute a b t) (substitute a b u)