module Main where data Term Variable String Abstract String Term Appli

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
module Main where
data Term = Variable String
| Abstract String Term
| Application Term Term
eval :: Term -> Term
eval (Variable var) = Variable var
eval (Abstract var body) = Abstract var (eval body) -- can be not evaluated
eval (Application (Variable _) term2) = eval term2
-- may be stack overflow -- (size + sizeOf (body) + 1)
eval (Application (Abstract var body) term2) = eval (replaceVars body var term2)
eval (Application term1 term2) = eval $ Application (eval term1) (eval term2)
replaceVars :: Term -> String -> Term -> Term
replaceVars (Abstract currVar term) var newTerm | currVar == var =
Abstract (var ++ (show 0)) (replaceVars (findAndRename term var) var newTerm)
replaceVars (Abstract currVar term) var newTerm | otherwise =
Abstract (currVar) (replaceVars (findAndRename term var) var newTerm)
replaceVars (Application t1 t2) var newTerm = Application (replaceVars t1 var newTerm) (replaceVars t2 var newTerm)
replaceVars (Variable currVar) var newTerm | currVar == var = newTerm
replaceVars (Variable currVar) _ _ | otherwise = Variable currVar
replaceVars term var newTerm = term
findAndRename :: Term -> String -> Term
findAndRename term name = fAndR' term name 0
where fAndR' :: Term -> String -> Int -> Term
fAndR' (Variable oldName) name ind | oldName == name = Variable (name ++ (show ind))
fAndR' (Variable oldName) _ _ | otherwise = Variable (oldName)
fAndR' (Application t1 t2) name ind = Application (fAndR' t1 name ind) (fAndR' t1 name ind)
fAndR' (Abstract oldName t) name ind | oldName == name = Abstract (name ++ (show (ind+1))) (fAndR' t name (ind+1))
toString :: Term -> String
toString (Variable var) = var
toString (Abstract term1 term2) = "L " ++ (term1) ++ "." ++ (toString term2)
toString (Application term1 term2) = "(" ++ (toString term1) ++ ") (" ++ (toString term2) ++ ")"
main :: IO()
main = print $ toString $ eval $
Application (
(Abstract "b" (Abstract "t" (Abstract "f" (Variable "a"))))
) (
Application (Application (Variable "b") (Variable "t")) (Variable "f")
)
-- Application (
-- Application (
-- Abstract "a" (Abstract "b" (Abstract "t" (Abstract "f" (Variable "a"))))
-- ) (
-- Application (Application (Variable "b") (Variable "t")) (Variable "f")
-- )
-- ) (
-- Abstract "t" (Variable "t")
-- )
--(Application
-- (Application
-- (Application
-- ((Abstract "a" (Abstract "b" (Abstract "t" (Abstract "f" (Variable "a"))))))
-- (Application (Application (Variable "b") (Variable "t")) (Variable "f")))
-- (Application (Variable "t") (Variable "f")))
-- (Abstract "t" (Abstract "f" (Variable "t")))) 0
-- toString (eval(Abstract "a" (Application (Abstract "b" (Variable "b")) (Variable "a"))))
-- Application ((Abstract "x" (Abstract "y" (Variable "x")))) (Variable "y")
-- Application (Abstract "x" (Abstract "y" (Variable "y"))) (Variable "z")
-- eval(Application (Application (Variable "x") (Variable "y")) (Variable "z"))