X-Git-Url: http://git.tomasm.cz/fp.git/blobdiff_plain/cde0eee2a072f74e1f3578dc1c45955a0425d183..c291e22383673d73f8e17e4de85bc68ad2f2c454:/Lambda.hs?ds=sidebyside

diff --git a/Lambda.hs b/Lambda.hs
index d9bdaee..578c00f 100644
--- a/Lambda.hs
+++ b/Lambda.hs
@@ -37,8 +37,35 @@ parseApp = do
   t <- parseTerm
   char ' '
   r <- parseTerm
-  char '('
+  char ')'
   return $! App t r
 
 parseTerm :: Parser Term
 parseTerm = parseVar <|> parseLambda <|> parseApp
+
+-------------------------------------------------
+
+isFreeIn :: VarName -> Term -> Bool
+isFreeIn x (Var v) = x == v
+isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
+isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
+
+rename :: Term -> Term
+rename (Lambda x t) = Lambda n (substitute x (Var n) t)
+  where n = rnm x 
+        rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
+
+substitute :: VarName -> Term -> Term -> Term
+substitute a b (Var x) = if x == a then b else Var x
+substitute a b (Lambda x t) 
+  | x == a = Lambda x t
+  | x `isFreeIn` 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)
+
+reduce :: Term -> Term
+reduce (Var x) = Var x
+reduce (Lambda x t) = Lambda x (reduce t)
+reduce (App t u) = app (reduce t) u
+  where app (Lambda x v) w = reduce $ substitute x w v
+        app a b = App a (reduce b)