fork download
  1. module Main where
  2.  
  3. import Control.Monad.Identity
  4. import Text.Parsec
  5.  
  6. data Term = Var String
  7. | Idx Int
  8. | Abs Term
  9. | App Term Term
  10.  
  11. avnames = map (\x -> [x]) "abcdexyzuw"
  12. names = avnames ++ map ('\'' :) names
  13.  
  14. nameidx i n (Abs t) = Abs (nameidx (i + 1) n t)
  15. nameidx i n (App x y) = App (nameidx i n x) (nameidx i n y)
  16. nameidx i n (Idx d)
  17. | i == d = Var n
  18. | otherwise = Idx d
  19. nameidx _ _ v = v
  20.  
  21. markfree (Abs t) = Abs (markfree t)
  22. markfree (App x y) = App (markfree x) (markfree y)
  23. markfree (Var s) = Var ('*' : s)
  24. markfree i = i
  25.  
  26. showTerm :: [String] -> Term -> ShowS
  27. showTerm (n:ns) (Abs t) =
  28. ("(\\" ++)
  29. . (". " ++)
  30. . showTerm ns (nameidx 0 n t)
  31. . (")" ++)
  32. showTerm ns (App x y) =
  33. ("(" ++)
  34. . showTerm ns x
  35. . (" " ++)
  36. . showTerm ns y
  37. . (")" ++)
  38. showTerm ns (Idx i) = ('#' :) . (show i ++)
  39. showTerm ns (Var s) = (s ++)
  40.  
  41. instance Show Term where
  42. show t = showTerm names (markfree t) $ []
  43.  
  44. type Eval a = Identity a
  45.  
  46. runEval :: Eval Term -> Term
  47. runEval = runIdentity
  48.  
  49. eval :: Term -> Eval Term
  50. eval (App x y) = do
  51. x' <- eval x
  52. case x' of
  53. (Abs t) -> eval (subst 0 t y)
  54. proc -> return (App proc y)
  55. eval other = return other
  56.  
  57. subst :: Int -> Term -> Term -> Term
  58. subst i (Idx d) s
  59. | d == i = s
  60. | otherwise = Idx d
  61. subst i (App x y) s = App (subst i x s) (subst i y s)
  62. subst i (Var x) s = Var x
  63. subst i (Abs t) s = Abs (subst (i + 1) t s)
  64.  
  65. setidx :: String -> Int -> Term -> Term
  66. setidx name i (App x y) = App (setidx name i x) (setidx name i y)
  67. setidx name i (Abs t) = Abs (setidx name (i + 1) t)
  68. setidx name i (Var n)
  69. | name == n = Idx i
  70. | otherwise = Var n
  71. setidx _ _ t = t
  72.  
  73. setVariable :: String -> Term -> Term -> Term
  74. setVariable name t' (App x y) =
  75. App (setVariable name t' x) (setVariable name t' y)
  76. setVariable name t' (Abs t) = Abs (setVariable name t' t)
  77. setVariable name t' (Var s)
  78. | s == name = t'
  79. | otherwise = Var s
  80. setVariable _ _ other = other
  81.  
  82. identifier :: Parsec String () String
  83. identifier = many1 alphaNum
  84.  
  85. lambda :: Parsec String () Term
  86. lambda = do
  87. char '('
  88. char '\\'
  89. spaces
  90. varname <- identifier
  91. spaces
  92. char '.'
  93. t <- term
  94. char ')'
  95. return $ Abs (setidx varname 0 t)
  96.  
  97. single :: Parsec String () Term
  98. single = (spaces >>) $ try (fmap Var identifier) <|> try lambda <|> application
  99.  
  100. application :: Parsec String () Term
  101. application = do
  102. char '('
  103. f <- term
  104. char ')'
  105. return f
  106.  
  107. substitution :: Parsec String () (String, Term)
  108. substitution = do
  109. char '['
  110. spaces
  111. varname <- identifier
  112. spaces
  113. string "->"
  114. t <- term
  115. char ']'
  116. return (varname, t)
  117.  
  118. term :: Parsec String () Term
  119. term = do
  120. spaces
  121. sub <- try (optionMaybe substitution)
  122. t <- try (fmap (foldl1 App) (many1 single))
  123. case sub of
  124. Nothing -> return t
  125. Just (var, t') -> return (setVariable var t' t)
  126.  
  127. lambdaEval str =
  128. case parse term "lambda" str of
  129. Right t -> Right $ runEval (eval t)
  130. Left e -> Left e
  131.  
  132. loop :: IO ()
  133. loop = do
  134. x <- getLine
  135. case x of
  136. ":end" -> return ()
  137. str -> putStr "> " >> print (lambdaEval x) >> loop
  138.  
  139. main :: IO ()
  140. main = do
  141. putStrLn "Lambda-Expressions Evaluator.\n> "
  142. loop
Not running #stdin #stdout 0s 0KB
stdin
Standard input is empty
stdout
Standard output is empty