{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Syntax.Parser
(
Parser
, Agda.Syntax.Parser.parse
, Agda.Syntax.Parser.parsePosString
, parseFile'
, moduleParser
, moduleNameParser
, exprParser
, exprWhereParser
, holeContentParser
, tokensParser
, ParseError(..)
, ParseWarning(..)
, PM(..)
, runPMIO
) where
import Control.Arrow (second)
import Control.Exception
import Control.Monad ((>=>), forM_)
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer hiding ((<>))
import qualified Data.List as 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.Parser.Literate
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Definitions
import Agda.Syntax.Parser.Tokens
import Agda.Utils.Except
( ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.FileName
import Agda.Utils.IO.UTF8 (readTextFile)
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
wrap :: ParseResult a -> PM a
wrap (ParseOk _ x) = return x
wrap (ParseFailed err) = throwError err
wrapIOM :: (MonadError e m, MonadIO m) => (IOError -> e) -> IO a -> m a
wrapIOM f m = do
a <- liftIO$ (Right <$> m) `catch` (\err -> return$ Left (err :: IOError))
case a of
Right x -> return x
Left err -> throwError (f err)
wrapM :: IO (ParseResult a) -> PM a
wrapM m = liftIO m >>= wrap
newtype PM a = PM { unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a }
deriving (Functor, Applicative, Monad,
MonadError ParseError, MonadIO)
warning :: ParseWarning -> PM ()
warning w = PM (modify (w:))
runPMIO :: (MonadIO m) => PM a -> m (Either ParseError a, [ParseWarning])
runPMIO = liftIO . fmap (second reverse) . flip runStateT [] . runExceptT . unPM
data Parser a = Parser
{ parser :: M.Parser a
, parseFlags :: ParseFlags
, parseLiterate :: LiterateParser a
}
type LiterateParser a = Parser a -> [Layer] -> PM a
parse :: Parser a -> String -> PM a
parse p = wrapM . return . M.parse (parseFlags p) [normal] (parser p)
parseFile :: Parser a -> AbsolutePath -> PM a
parseFile p = wrapM . M.parseFile (parseFlags p) [layout, normal] (parser p)
parseString :: Parser a -> String -> PM a
parseString = parseStringFromFile Strict.Nothing
parseStringFromFile :: SrcFile -> Parser a -> String -> PM a
parseStringFromFile src p = wrapM . return . M.parseFromSrc (parseFlags p) [layout, normal] (parser p) src
parseLiterateWithoutComments :: LiterateParser a
parseLiterateWithoutComments p layers = parseStringFromFile (literateSrcFile layers) p $ illiterate layers
parseLiterateWithComments :: LiterateParser [Token]
parseLiterateWithComments p layers = do
code <- map Left <$> parseLiterateWithoutComments p layers
let literate = Right <$> filter (not . isCodeLayer) layers
let (terms, overlaps) = interleaveRanges code literate
forM_ (map fst overlaps) $ \c ->
warning$ OverlappingTokensWarning { warnRange = getRange c }
return$ concat [ case m of
Left t -> [t]
Right (Layer Comment interval s) -> [TokTeX (interval, s)]
Right (Layer Markup _ _) -> []
Right (Layer Code _ _) -> []
| m <- terms ]
readFilePM :: AbsolutePath -> PM String
readFilePM path = wrapIOM (ReadFileError path) (readTextFile (filePath path))
parseLiterateFile :: Processor -> Parser a -> AbsolutePath -> PM a
parseLiterateFile po p path = readFilePM path >>= parseLiterate p p . po (startPos (Just path))
parsePosString :: Parser a -> Position -> String -> PM a
parsePosString p pos = wrapM . return . M.parsePosString pos (parseFlags p) [normal] (parser p)
parseFileExts :: [String]
parseFileExts = ".agda":literateExts
parseFile' :: (Show a) => Parser a -> AbsolutePath -> PM a
parseFile' p file =
if ".agda" `List.isSuffixOf` filePath file then
Agda.Syntax.Parser.parseFile p file
else
go literateProcessors
where
go [] = throwError InvalidExtensionError {
errPath = file
, errValidExts = parseFileExts
}
go ((ext, po):pos) | ext `List.isSuffixOf` filePath file = parseLiterateFile po p file
go (_:pos) = go pos
moduleParser :: Parser Module
moduleParser = Parser { parser = P.moduleParser
, parseFlags = withoutComments
, parseLiterate = parseLiterateWithoutComments
}
moduleNameParser :: Parser QName
moduleNameParser = Parser { parser = P.moduleNameParser
, parseFlags = withoutComments
, parseLiterate = parseLiterateWithoutComments
}
exprParser :: Parser Expr
exprParser = Parser { parser = P.exprParser
, parseFlags = withoutComments
, parseLiterate = parseLiterateWithoutComments
}
exprWhereParser :: Parser ExprWhere
exprWhereParser = Parser
{ parser = P.exprWhereParser
, parseFlags = withoutComments
, parseLiterate = parseLiterateWithoutComments
}
holeContentParser :: Parser HoleContent
holeContentParser = Parser
{ parser = P.holeContentParser
, parseFlags = withoutComments
, parseLiterate = parseLiterateWithoutComments
}
tokensParser :: Parser [Token]
tokensParser = Parser { parser = P.tokensParser
, parseFlags = withComments
, parseLiterate = parseLiterateWithComments
}
withComments :: ParseFlags
withComments = defaultParseFlags { parseKeepComments = True }
withoutComments :: ParseFlags
withoutComments = defaultParseFlags { parseKeepComments = False }