Parsec Lambda Calculus

module Parse where

import Text.Parsec
import Text.Parsec.Combinator
import Syntax
import Data.List

----------------------
-- Main entry point --
----------------------
type BoundContext = [String]
type LCParser = Parsec String BoundContext Term

----------------------
-- Helper functions --
----------------------

infoFrom :: SourcePos -> Info
infoFrom pos = Info (sourceLine pos) (sourceColumn pos)

---------------
-- Variables --
---------------

findVar :: String -> BoundContext -> LCParser
findVar v list = case elemIndex v list of
  Nothing -> fail $ "Variable " ++ v ++ " is unbound"
  Just n -> do pos <- getPosition
               return $ TmVar (infoFrom pos) n (length list)


parseVarname :: Parsec String u String
parseVarname = many1 $ letter <|> char '\''


parseVar :: LCParser
parseVar = do v    <- parseVarname
              list <- getState
              findVar v list

-------------
-- Numbers --
-------------

parseNum :: LCParser
parseNum = do v   <- many1 digit
              pos <- getPosition
              return $ TmNum (infoFrom pos) (read v :: Int)


--------------
-- Booleans --
--------------

parseTrue :: LCParser
parseTrue = do v   <- string "#t"
               pos <- getPosition
               return $ TmBool (infoFrom pos) Truthy


parseFalse :: LCParser
parseFalse = do v   <- string "#f"
                pos <- getPosition
                return $ TmBool (infoFrom pos) Falsy

parseBool :: LCParser
parseBool = parseTrue <|> parseFalse
               
-----------------
-- Abstraction --
-----------------

parseAbst :: LCParser
parseAbst = do char '\\'
               v <- parseVarname
               -- Push the variable on the env as bound.
               modifyState (v :)
               char '.'
               -- Get the position from within the source code.
               pos <- getPosition            
               term <- parseTerm
               -- Leaving body, pop from env.
               modifyState tail
               return $ TmAbs (infoFrom pos) v term


parens :: Parsec String u a -> Parsec String u a
parens = between (char '(') (char ')')

parseNonApp :: LCParser
parseNonApp = parens parseTerm
              <|> parseAbst
              <|> parseVar
              <|> parseNum
              <|> parseBool


parseTerm :: LCParser
parseTerm = chainl1 parseNonApp $
            do space
               pos <- getPosition
               return $ TmApp (infoFrom pos)


parseProg :: String -> Either ParseError Term
parseProg = parseWith parseTerm

parseWith :: LCParser -> String -> Either ParseError Term
parseWith p = runParser p [] "(source)"