Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 51b15eedd7
Fetching contributors…

Octocat-spinner-32-eaf2f5

Cannot retrieve contributors at this time

file 129 lines (99 sloc) 3.944 kb
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 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
import Text.ParserCombinators.Parsec hiding (many, optional, (<|>))
import Control.Applicative
import Data.Char (isAlpha)
import Data.Maybe (fromMaybe)
import qualified Data.Set as Set
import Control.Monad (forever)
import System.IO

type Name = String

data Term = Var Name
          | Abs Name Term
          | App Term Term
            deriving (Show, Eq)

-- Lexer

type Token = (SourcePos, String)

scan :: String -> Either ParseError [Token]
scan = parse toks "(stdin)"

tok = liftA2 (,) getPosition $ choice [ many1 letter
                                       , string "("
                                       , string ")"
                                       , string "."
                                       , string "\\"
                                       ]

toks = spaces *> many (tok <* spaces) <* eof

-- Parser

sat :: (String -> Bool) -> GenParser Token () String
sat p = token showToken posToken testToken
    where
      showToken (pos, tok) = show tok
      posToken (pos, tok) = pos
      testToken (pos, tok) = if p tok then Just tok else Nothing

symb :: String -> GenParser Token () String
symb sym = sat (== sym) <?> show sym

name :: GenParser Token () String
name = sat (all isAlpha) <?> "variable"

paren = between (symb "(") (symb ")")

p_var = Var <$> name
p_abs = liftA2 Abs (symb "\\" *> name <* symb ".") p_term

p_term = p_abs <|> (foldl1 App <$> many1 (p_var <|> paren p_term))

p_program = p_term <* eof

-- Evaluator

freeVars :: Term -> Set.Set Name
freeVars (Var v) = Set.singleton v
freeVars (Abs v e) = Set.delete v (freeVars e)
freeVars (App e1 e2) = (freeVars e1) `Set.union` (freeVars e2)

type Substitution = Name -> Term

extend :: Substitution -> Name -> Term -> Substitution
extend s v t u = if u == v then t else s u

-- Return the successor of a given name (in lexicographical order).
successor :: Name -> Name
successor = reverse . successor' . reverse
    where successor' [] = "A"
          successor' (c:cs) | c < 'z' = succ c : cs
                            | otherwise = 'A' : successor cs

-- An infinite lexicographically ordered list of names.
names :: [Name]
names = iterate successor "A"

freshName :: Name -> Set.Set Name -> Name
freshName n s | n `Set.member` s = head $ dropWhile (`Set.member` s) names
              | otherwise = n

substitute :: Term -> Substitution -> Term
substitute (Var v) s = s v
substitute (Abs v e) s = Abs v' (substitute e s')
    where vs = Set.unions [ freeVars (s w) |
                            w <- Set.toList . Set.delete v . freeVars $ e]
          v' = freshName v vs
          s' = extend s v (Var v')
substitute (App e1 e2) s = App (substitute e1 s) (substitute e2 s)

evalOne :: Term -> Maybe Term
evalOne (App (Abs v e) e') = Just $ substitute e (extend Var v e')
evalOne (App e e') = (`App` e') <$> evalOne e
evalOne _ = Nothing

eval :: Term -> Term
eval t = fromMaybe t (eval <$> evalOne t)

ppTerm :: Term -> String
ppTerm (Var v) = v
ppTerm (Abs v e) = "\\" ++ v ++ " . " ++ ppTerm e
ppTerm (App e e') = (pp e) ++ " " ++ (pp e')
    where pp t@(Var v) = ppTerm t
          pp t@(Abs v e) = parens $ ppTerm t
          pp t@(App e e') = parens $ ppTerm t
          parens text = "(" ++ text ++ ")"

-- Interpreter

prompt :: String
prompt = "> "

main = do
  hSetBuffering stdin NoBuffering
  hSetBuffering stdout NoBuffering
  forever repl
    where
      repl = do
        putStr prompt
        input <- getLine
        case scan input of
          Left err -> putStrLn "Parse error:" >> print err
          Right toks -> case toks of
                          [] -> return ()
                          (tok:_) -> case parse ((setPosition . fst $ tok) >> p_program) "" toks of
                                       Left err -> putStrLn "Parse error:" >> print err
                                       Right term -> putStrLn . ppTerm $ eval term
Something went wrong with that request. Please try again.