module Agda.Syntax.Parser
(
Parser
, Agda.Syntax.Parser.parse
, Agda.Syntax.Parser.parseLiterate
, Agda.Syntax.Parser.parsePosString
, parseFile'
, moduleParser
, exprParser
, tokensParser
, ParseError(..)
) where
import Control.Exception
import Data.List
import Agda.Syntax.Position
import Agda.Syntax.Parser.Monad as M hiding (Parser, parseFlags)
import qualified Agda.Syntax.Parser.Monad as M
import qualified Agda.Syntax.Parser.Parser as P
import Agda.Syntax.Parser.Lexer
import Agda.Syntax.Concrete
import Agda.Syntax.Parser.Tokens
import Agda.Utils.FileName
wrap :: ParseResult a -> a
wrap (ParseOk _ x) = x
wrap (ParseFailed err) = throw err
wrapM:: Monad m => m (ParseResult a) -> m a
wrapM m =
do r <- m
case r of
ParseOk _ x -> return x
ParseFailed err -> throw err
data Parser a = Parser
{ parser :: M.Parser a
, parseFlags :: ParseFlags
}
parse :: Parser a -> String -> IO a
parse p = wrapM . return . M.parse (parseFlags p) [normal] (parser p)
parseFile :: Parser a -> AbsolutePath -> IO a
parseFile p = wrapM . M.parseFile (parseFlags p) [layout, normal] (parser p)
parseLiterate :: Parser a -> String -> IO a
parseLiterate p =
wrapM . return . M.parse (parseFlags p) [literate, layout, code] (parser p)
parseLiterateFile :: Parser a -> AbsolutePath -> IO a
parseLiterateFile p =
wrapM . M.parseFile (parseFlags p) [literate, layout, code] (parser p)
parsePosString :: Parser a -> Position -> String -> IO a
parsePosString p pos =
wrapM . return . M.parsePosString pos (parseFlags p) [normal] (parser p)
parseFile' :: Parser a -> AbsolutePath -> IO a
parseFile' p file =
if "lagda" `isSuffixOf` filePath file then
Agda.Syntax.Parser.parseLiterateFile p file
else
Agda.Syntax.Parser.parseFile p file
moduleParser :: Parser Module
moduleParser = Parser { parser = P.moduleParser
, parseFlags = withoutComments }
exprParser :: Parser Expr
exprParser = Parser { parser = P.exprParser
, parseFlags = withoutComments }
tokensParser :: Parser [Token]
tokensParser = Parser { parser = P.tokensParser
, parseFlags = withComments }
withComments :: ParseFlags
withComments = defaultParseFlags { parseKeepComments = True }
withoutComments :: ParseFlags
withoutComments = defaultParseFlags { parseKeepComments = False }