lambdabot-4.0: Plugin/Lambda/LMParser.hs
--
-- screw modularity (at least temporarily)
--
module Plugin.Lambda.LMParser (parseTerm,Term(..)) where
import Plugin.Lambda.LangPack
import Plugin.Lambda.ArithTerm (ArithTerm(..))
import Plugin.Lambda.LambdaTerm (LambdaTerm(..))
import Plugin.Lambda.RelTerm (RelTerm(..))
import Plugin.Lambda.ListTerm (ListTerm(..))
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import Text.ParserCombinators.Parsec.Language (emptyDef, reservedNames)
import qualified Text.ParserCombinators.Parsec.Token as P hiding (reservedNames)
tp :: P.TokenParser st
tp = P.makeTokenParser
(emptyDef { reservedNames =
["if","then","else","True","False","head","tail","null"] })
{-# INLINE tp #-}
-- integer :: CharParser st Integer
-- integer = P.integer tp
natural :: CharParser st Integer
natural = P.natural tp
boolean :: GenParser Char st Bool
boolean = (reserved "True" >> return True)
<|> (reserved "False" >> return False)
reserved :: String -> CharParser st ()
reserved = P.reserved tp
symbol :: String -> CharParser st String
symbol = P.symbol tp
parens, brackets :: CharParser st a -> CharParser st a
parens = P.parens tp
brackets = P.brackets tp
identifier, dot, comma :: CharParser st String
identifier = P.identifier tp
dot = P.dot tp
comma = P.comma tp
charLiteral :: CharParser st Char
charLiteral = P.charLiteral tp
stringLiteral :: CharParser st String
stringLiteral = P.stringLiteral tp
identStart, identLetter :: CharParser st Char
identStart = P.identStart emptyDef
identLetter = P.identLetter emptyDef
class Up f x where
up :: f x -> x
data Term x
= ArithT (ArithTerm x)
| LambdaT (LambdaTerm x)
| RelT (RelTerm x)
| ListT (ListTerm x)
type Term' = Fix Term
instance Functor Term where
fmap f (ArithT x) = ArithT (fmap f x)
fmap f (LambdaT x) = LambdaT (fmap f x)
fmap f (RelT x) = RelT (fmap f x)
fmap f (ListT x) = ListT (fmap f x)
instance Up ArithTerm Term' where
up = In . ArithT
instance Up LambdaTerm Term' where
up = In . LambdaT
instance Up RelTerm Term' where
up = In . RelT
instance Up ListTerm Term' where
up = In . ListT
-- up' :: (Up f x) => Parser (f x) -> Parser x
-- up' p = p >>= return . up
up2 :: (Up f x) => (t -> t1 -> f x) -> t -> t1 -> x
up2 f = (\x y -> up $ f x y)
parseTerm :: [Char] -> Either ParseError Term'
parseTerm = parse (do spaces; r <- parser';eof; return r) ""
application :: GenParser Char () Term'
application = do v <- (var <|> listOp)
es <- many (var <|> listOp <|> literal <|> parens parser')
case es of
[] -> return v
es'-> return $ foldl1 (up2 App) (v:es')
parser' :: GenParser Char () Term'
parser' = do e <- expr
es <- many expr'
case es of
[] -> return e
es'-> return $ foldl1 (up2 App) (e:es')
var :: GenParser Char st Term'
var = (identifier >>= return . up . Var) <?> "var"
-- var without stripping trailing spaces
var' :: GenParser Char st Term'
var' = (do c <- identStart; cs <- many identLetter; return $ up $ Var (c:cs)) <?> "var"
num :: GenParser Char st Term'
num = (natural >>= return . up . Num) <?> "num"
bool :: GenParser Char st Term'
bool = (boolean >>= return . up . Boolean) <?> "bool"
character :: GenParser Char st Term'
character = (charLiteral >>= return . up . Character) <?> "character"
stringL :: GenParser Char st Term'
stringL = (stringLiteral >>= return . foldr (up2 Cons . up . Character) (up Nil)) <?> "string"
listOp :: GenParser Char st Term'
listOp = do o <- (reserved "head" >> return Head) <|>
(reserved "tail" >> return Tail) <|>
(reserved "null" >> return Null)
return $ up2 Lam "x" (up $ o $ up $ Var "x")
list :: GenParser Char () Term'
list = do es <- brackets (parser' `sepBy` comma)
return (foldr (up2 Cons) (up Nil) es) <?> "list"
literal :: GenParser Char () Term'
literal = bool <|> num <|> character <|> list <|> stringL
term :: GenParser Char () Term' -> GenParser Char () Term'
term x = x <|> literal <|> ifEx <|> listOp <|>
abstraction <|> parens parser' <?> "simple term"
expr :: GenParser Char () Term'
expr = buildExpressionParser table (term application)
{-# INLINE expr #-}
expr' :: GenParser Char () Term'
expr' = buildExpressionParser table (term var)
table :: OperatorTable Char () Term'
table = [[Infix (op "." (\f g -> Lam "#x#" $ up2 App f $ up2 App g (up $ Var "#x#"))) AssocRight,
Infix (do v <- between (char '`') (symbol "`") var'; return $ up2 App . up2 App v) AssocLeft],
[Infix (op "*" Mul) AssocLeft, Infix (try $ do char '/'; notFollowedBy (char '='); spaces; return $ up2 Div) AssocLeft],
[Infix (op "-" Sub) AssocLeft, Infix (try $ do char '+'; notFollowedBy (char '+'); spaces; return $ up2 Add) AssocLeft],
[Infix (op ":" Cons) AssocRight, Infix (op "++" Append) AssocRight],
[Infix (op "<=" LessThanOrEqual) AssocNone, Infix (op ">=" GreaterThanOrEqual) AssocNone,
Infix (op "<" LessThan) AssocNone, Infix (op ">" GreaterThan) AssocNone,
Infix (op "==" Equal) AssocNone, Infix (op "/=" NotEqual) AssocNone],
[Infix (op "&&" And) AssocRight],
[Infix (op "||" Or) AssocRight],
[Infix (op "$" App) AssocRight]]
--
-- This gets hammered
--
op :: (Up f trm) => String -> (trm -> trm -> f trm) -> Parser (trm -> trm -> trm)
op s o = try $ do symbol s; return (up2 o)
{-# INLINE op #-}
abstraction :: GenParser Char () Term'
abstraction = do symbol "\\"
vs <- many1 identifier
(dot <|> symbol "->") -- yay!
b <- parser'
return $ foldr (up2 Lam) b vs
<?> "abstraction"
ifEx :: GenParser Char () Term'
ifEx = do reserved "if"
c <- parser'
reserved "then"
t <- parser'
reserved "else"
e <- parser'
return $ up $ IfE c t e
<?> "if"