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

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!