module Type where
import qualified TermParser as Parser
import qualified Term
import qualified SourceText as Source
import Term ( Term(Node), Identifier(Identifier), liftMonadFail )
import SourceText ( ParserRange )
import InOut ( input )
import qualified Text.ParserCombinators.Parsec.Token as T
import qualified Text.ParserCombinators.Parsec.Language as L
import qualified Text.ParserCombinators.Parsec.Expr as Expr
import qualified Text.ParserCombinators.Parsec as Parsec
import Text.ParserCombinators.Parsec
( CharParser, Parser, (<|>), (<?>), )
import Text.ParserCombinators.Parsec.Expr
( Assoc(AssocRight) )
import Control.Monad ( liftM2 )
lexer :: T.TokenParser st
lexer =
T.makeTokenParser $ L.emptyDef {
L.commentStart = "{-",
L.commentEnd = "-}",
L.commentLine = "--",
L.nestedComments = True,
L.identStart = Parser.identifierStart,
L.identLetter = Parser.identifierLetter,
L.opStart = operatorStart,
L.opLetter = operatorLetter,
L.caseSensitive = True,
L.reservedNames = [ "forall" ],
L.reservedOpNames = [ "=", "::", "|" ]
}
operators :: [[(String, Assoc)]]
operators =
[ [ ( "->", AssocRight ) ]
-- , [ ( ",", AssocRight) ]
]
parseBracket :: (ParserRange range) => Parser (Term range)
parseBracket = T.lexeme lexer $ do
(rng,term) <-
Source.ranged $
Parsec.between (T.symbol lexer "[") (Parsec.char ']') parseExpression
return (Node (Identifier { Term.name = "[]", Term.range = rng }) [term])
parseAtom :: (ParserRange range) => Parser (Term range)
parseAtom =
T.parens lexer parseExpression
<|> parseBracket
<|> fmap (flip Node []) input
parseApply :: (ParserRange range) => Parser (Term range)
parseApply =
liftMonadFail =<<
liftM2 Term.appendArguments parseAtom (Parsec.many parseAtom)
operatorStart, operatorLetter :: CharParser st Char
operatorStart = Parsec.oneOf operatorSymbols
operatorLetter = Parsec.oneOf operatorSymbols
operatorSymbols :: [Char]
operatorSymbols = ":->"
table :: (ParserRange range) => Expr.OperatorTable Char st (Term range)
table = map ( map binary ) operators
-- duplicate to Term.binary, however, lexer and operatorLetter are different
binary ::
(ParserRange range) =>
(String, Assoc) -> Expr.Operator Char st (Term range)
binary (s, assoc) = flip Expr.Infix assoc $ do
rng <- Parsec.try $ T.lexeme lexer $ do
(rng,_) <- Source.ranged $ Parsec.string s
Parsec.notFollowedBy operatorLetter <?> ("end of " ++ show s)
return rng
return $ \ l r -> Node ( Identifier { Term.name = s, Term.range = rng } ) [ l, r ]
parseContext :: (ParserRange range) => Parsec.Parser [Term range]
parseContext = do
constraints <- T.parens lexer $ T.commaSep lexer input
T.reservedOp lexer "=>"
return constraints
parseExpression :: (ParserRange range) => Parsec.Parser (Term range)
parseExpression =
Expr.buildExpressionParser table parseApply