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)