    module Agda.Syntax.Parser
        ( -- * Types
          Parser
          -- * Parse functions
        , Agda.Syntax.Parser.parse
        , Agda.Syntax.Parser.parsePosString
        , parseFile
          -- * Parsers
        , moduleParser
        , moduleNameParser
        , agdaFileExtensions
        , exprParser
        , exprWhereParser
        , holeContentParser
        , tokensParser
          -- * Reading files.
        , readFilePM
          -- * Parse errors
        , ParseError(..)
        , ParseWarning(..)
        , PM(..)
        , runPMIO
        ) where

    import Control.Exception
    import Control.Monad          ( forM_ )
    import Control.Monad.Except
    import Control.Monad.State
    import Control.Monad.IO.Class ( MonadIO(..) )

    import Data.Bifunctor
    import qualified Data.List as List
    import Data.Text.Lazy (Text)

    import Agda.Syntax.Common
    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.Attribute
    import Agda.Syntax.Parser.Tokens

    import Agda.Utils.FileName
    import Agda.Utils.IO.UTF8 (readTextFile)
    import Agda.Utils.Maybe   (forMaybe)
    import qualified Agda.Utils.Maybe.Strict as Strict

    ------------------------------------------------------------------------
    -- Wrapping parse results

    -- | A monad for handling parse errors and warnings.

    newtype PM a = PM { forall a. PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a
    unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a }
      deriving ( (forall a b. (a -> b) -> PM a -> PM b)
    -> (forall a b. a -> PM b -> PM a) -> Functor PM
    forall a b. a -> PM b -> PM a
    forall a b. (a -> b) -> PM a -> PM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> PM a -> PM b
    fmap :: forall a b. (a -> b) -> PM a -> PM b
    $c<$ :: forall a b. a -> PM b -> PM a
    <$ :: forall a b. a -> PM b -> PM a
    Functor, Functor PM
    Functor PM =>
    (forall a. a -> PM a)
    -> (forall a b. PM (a -> b) -> PM a -> PM b)
    -> (forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c)
    -> (forall a b. PM a -> PM b -> PM b)
    -> (forall a b. PM a -> PM b -> PM a)
    -> Applicative PM
    forall a. a -> PM a
    forall a b. PM a -> PM b -> PM a
    forall a b. PM a -> PM b -> PM b
    forall a b. PM (a -> b) -> PM a -> PM b
    forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall a. a -> PM a
    pure :: forall a. a -> PM a
    $c<*> :: forall a b. PM (a -> b) -> PM a -> PM b
    <*> :: forall a b. PM (a -> b) -> PM a -> PM b
    $cliftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
    liftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
    $c*> :: forall a b. PM a -> PM b -> PM b
    *> :: forall a b. PM a -> PM b -> PM b
    $c<* :: forall a b. PM a -> PM b -> PM a
    <* :: forall a b. PM a -> PM b -> PM a
    Applicative, Applicative PM
    Applicative PM =>
    (forall a b. PM a -> (a -> PM b) -> PM b)
    -> (forall a b. PM a -> PM b -> PM b)
    -> (forall a. a -> PM a)
    -> Monad PM
    forall a. a -> PM a
    forall a b. PM a -> PM b -> PM b
    forall a b. PM a -> (a -> PM b) -> PM b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall a b. PM a -> (a -> PM b) -> PM b
    >>= :: forall a b. PM a -> (a -> PM b) -> PM b
    $c>> :: forall a b. PM a -> PM b -> PM b
    >> :: forall a b. PM a -> PM b -> PM b
    $creturn :: forall a. a -> PM a
    return :: forall a. a -> PM a
    Monad, Monad PM
    Monad PM => (forall a. IO a -> PM a) -> MonadIO PM
    forall a. IO a -> PM a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    $cliftIO :: forall a. IO a -> PM a
    liftIO :: forall a. IO a -> PM a
    MonadIO
               , MonadError ParseError, MonadState [ParseWarning]
               )

    -- | Run a 'PM' computation, returning a list of warnings in first-to-last order
    --   and either a parse error or the parsed thing.

    runPMIO :: (MonadIO m) => PM a -> m (Either ParseError a, [ParseWarning])
    runPMIO :: forall (m :: * -> *) a.
    MonadIO m =>
    PM a -> m (Either ParseError a, [ParseWarning])
    runPMIO = IO (Either ParseError a, [ParseWarning])
    -> m (Either ParseError a, [ParseWarning])
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either ParseError a, [ParseWarning])
     -> m (Either ParseError a, [ParseWarning]))
    -> (PM a -> IO (Either ParseError a, [ParseWarning]))
    -> PM a
    -> m (Either ParseError a, [ParseWarning])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Either ParseError a, [ParseWarning])
     -> (Either ParseError a, [ParseWarning]))
    -> IO (Either ParseError a, [ParseWarning])
    -> IO (Either ParseError a, [ParseWarning])
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (([ParseWarning] -> [ParseWarning])
    -> (Either ParseError a, [ParseWarning])
    -> (Either ParseError a, [ParseWarning])
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second [ParseWarning] -> [ParseWarning]
    forall a. [a] -> [a]
    reverse) (IO (Either ParseError a, [ParseWarning])
     -> IO (Either ParseError a, [ParseWarning]))
    -> (PM a -> IO (Either ParseError a, [ParseWarning]))
    -> PM a
    -> IO (Either ParseError a, [ParseWarning])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (StateT [ParseWarning] IO (Either ParseError a)
     -> [ParseWarning] -> IO (Either ParseError a, [ParseWarning]))
    -> [ParseWarning]
    -> StateT [ParseWarning] IO (Either ParseError a)
    -> IO (Either ParseError a, [ParseWarning])
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StateT [ParseWarning] IO (Either ParseError a)
    -> [ParseWarning] -> IO (Either ParseError a, [ParseWarning])
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT [] (StateT [ParseWarning] IO (Either ParseError a)
     -> IO (Either ParseError a, [ParseWarning]))
    -> (PM a -> StateT [ParseWarning] IO (Either ParseError a))
    -> PM a
    -> IO (Either ParseError a, [ParseWarning])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExceptT ParseError (StateT [ParseWarning] IO) a
    -> StateT [ParseWarning] IO (Either ParseError a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT ParseError (StateT [ParseWarning] IO) a
     -> StateT [ParseWarning] IO (Either ParseError a))
    -> (PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a)
    -> PM a
    -> StateT [ParseWarning] IO (Either ParseError a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a
    forall a. PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a
    unPM

    -- | Add a 'ParseWarning'.

    warning :: ParseWarning -> PM ()
    warning :: ParseWarning -> PM ()
    warning ParseWarning
    w = ExceptT ParseError (StateT [ParseWarning] IO) () -> PM ()
    forall a. ExceptT ParseError (StateT [ParseWarning] IO) a -> PM a
    PM (([ParseWarning] -> [ParseWarning])
    -> ExceptT ParseError (StateT [ParseWarning] IO) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (ParseWarning
    wParseWarning -> [ParseWarning] -> [ParseWarning]
    forall a. a -> [a] -> [a]
    :))

    -- | Embed a 'ParseResult' as 'PM' computation.

    wrap :: ParseResult a -> PM (a, Attributes)
    wrap :: forall a. ParseResult a -> PM (a, Attributes)
    wrap (ParseFailed ParseError
    err)  = ParseError -> PM (a, Attributes)
    forall a. ParseError -> PM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ParseError
    err
    wrap (ParseOk ParseState
    s a
    x)      = do
      ([ParseWarning] -> [ParseWarning]) -> PM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (ParseState -> [ParseWarning]
    parseWarnings ParseState
    s [ParseWarning] -> [ParseWarning] -> [ParseWarning]
    forall a. [a] -> [a] -> [a]
    ++)
      (a, Attributes) -> PM (a, Attributes)
    forall a. a -> PM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    x, ParseState -> Attributes
    parseAttributes ParseState
    s)

    wrapM :: IO (ParseResult a) -> PM (a, Attributes)
    wrapM :: forall a. IO (ParseResult a) -> PM (a, Attributes)
    wrapM IO (ParseResult a)
    m = IO (ParseResult a) -> PM (ParseResult a)
    forall a. IO a -> PM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO (ParseResult a)
    m PM (ParseResult a)
    -> (ParseResult a -> PM (a, Attributes)) -> PM (a, Attributes)
    forall a b. PM a -> (a -> PM b) -> PM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= ParseResult a -> PM (a, Attributes)
    forall a. ParseResult a -> PM (a, Attributes)
    wrap

    -- | Returns the contents of the given file.

    readFilePM :: RangeFile -> PM Text
    readFilePM :: RangeFile -> PM Text
    readFilePM RangeFile
    file =
      (IOError -> ParseError) -> IO Text -> PM Text
    forall e (m :: * -> *) a.
    (MonadError e m, MonadIO m) =>
    (IOError -> e) -> IO a -> m a
    wrapIOM (RangeFile -> IOError -> ParseError
    ReadFileError RangeFile
    file) (IO Text -> PM Text) -> IO Text -> PM Text
    forall a b. (a -> b) -> a -> b
    $
      String -> IO Text
    readTextFile (AbsolutePath -> String
    filePath (AbsolutePath -> String) -> AbsolutePath -> String
    forall a b. (a -> b) -> a -> b
    $ RangeFile -> AbsolutePath
    rangeFilePath RangeFile
    file)

    wrapIOM :: (MonadError e m, MonadIO m) => (IOError -> e) -> IO a -> m a
    wrapIOM :: forall e (m :: * -> *) a.
    (MonadError e m, MonadIO m) =>
    (IOError -> e) -> IO a -> m a
    wrapIOM IOError -> e
    f IO a
    m = do
      a <- IO (Either IOError a) -> m (Either IOError a)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either IOError a) -> m (Either IOError a))
    -> IO (Either IOError a) -> m (Either IOError a)
    forall a b. (a -> b) -> a -> b
    $ (a -> Either IOError a
    forall a b. b -> Either a b
    Right (a -> Either IOError a) -> IO a -> IO (Either IOError a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO a
    m) IO (Either IOError a)
    -> (IOError -> IO (Either IOError a)) -> IO (Either IOError a)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `catch` (\ IOError
    err -> Either IOError a -> IO (Either IOError a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either IOError a -> IO (Either IOError a))
    -> Either IOError a -> IO (Either IOError a)
    forall a b. (a -> b) -> a -> b
    $ IOError -> Either IOError a
    forall a b. a -> Either a b
    Left (IOError
    err :: IOError))
      case a of
        Right a
    x  -> a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x
        Left IOError
    err -> e -> m a
    forall a. e -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (IOError -> e
    f IOError
    err)

    ------------------------------------------------------------------------
    -- Parse functions

    -- | Wrapped Parser type.

    data Parser a = Parser
      { forall a. Parser a -> Parser a
    parser         :: M.Parser a
      , forall a. Parser a -> ParseFlags
    parseFlags     :: ParseFlags
      , forall a. Parser a -> LiterateParser a
    parseLiterate  :: LiterateParser a
      }

    type LiterateParser a =
      Parser a -> SrcFile -> [Layer] -> PM (a, Attributes)

    -- | Initial state for lexing.

    normalLexState :: [LexState]
    normalLexState :: [LexState]
    normalLexState = [LexState
    normal]

    -- | Initial state for lexing with top-level layout.

    layoutLexState :: [LexState]
    layoutLexState :: [LexState]
    layoutLexState = [LexState
    layout, LexState
    normal]

    -- | Parse without top-level layout.

    parse :: Parser a -> String -> PM (a, Attributes)
    parse :: forall a. Parser a -> String -> PM (a, Attributes)
    parse Parser a
    p = IO (ParseResult a) -> PM (a, Attributes)
    forall a. IO (ParseResult a) -> PM (a, Attributes)
    wrapM (IO (ParseResult a) -> PM (a, Attributes))
    -> (String -> IO (ParseResult a)) -> String -> PM (a, Attributes)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseResult a -> IO (ParseResult a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ParseResult a -> IO (ParseResult a))
    -> (String -> ParseResult a) -> String -> IO (ParseResult a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
    forall a.
    ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
    M.parse (Parser a -> ParseFlags
    forall a. Parser a -> ParseFlags
    parseFlags Parser a
    p) [LexState]
    normalLexState (Parser a -> Parser a
    forall a. Parser a -> Parser a
    parser Parser a
    p)

    -- | Parse with top-level layout.

    parseFileFromString
      :: SrcFile   -- ^ Name of source file.
      -> Parser a  -- ^ Parser to use.
      -> String    -- ^ Contents of source file.
      -> PM (a, Attributes)
    parseFileFromString :: forall a. SrcFile -> Parser a -> String -> PM (a, Attributes)
    parseFileFromString SrcFile
    src Parser a
    p = IO (ParseResult a) -> PM (a, Attributes)
    forall a. IO (ParseResult a) -> PM (a, Attributes)
    wrapM (IO (ParseResult a) -> PM (a, Attributes))
    -> (String -> IO (ParseResult a)) -> String -> PM (a, Attributes)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseResult a -> IO (ParseResult a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ParseResult a -> IO (ParseResult a))
    -> (String -> ParseResult a) -> String -> IO (ParseResult a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseFlags
    -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
    forall a.
    ParseFlags
    -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
    M.parseFromSrc (Parser a -> ParseFlags
    forall a. Parser a -> ParseFlags
    parseFlags Parser a
    p) [LexState]
    layoutLexState (Parser a -> Parser a
    forall a. Parser a -> Parser a
    parser Parser a
    p) SrcFile
    src

    -- | Parse with top-level layout.

    parseLiterateWithoutComments :: LiterateParser a
    parseLiterateWithoutComments :: forall a. LiterateParser a
    parseLiterateWithoutComments Parser a
    p SrcFile
    f [Layer]
    layers = SrcFile -> Parser a -> String -> PM (a, Attributes)
    forall a. SrcFile -> Parser a -> String -> PM (a, Attributes)
    parseFileFromString SrcFile
    f Parser a
    p (String -> PM (a, Attributes)) -> String -> PM (a, Attributes)
    forall a b. (a -> b) -> a -> b
    $ [Layer] -> String
    illiterate [Layer]
    layers

    -- | Parse with top-level layout.

    parseLiterateWithComments :: LiterateParser [Token]
    parseLiterateWithComments :: LiterateParser [Token]
    parseLiterateWithComments Parser [Token]
    p SrcFile
    f [Layer]
    layers = do
      (code, coh) <- LiterateParser [Token]
    forall a. LiterateParser a
    parseLiterateWithoutComments Parser [Token]
    p SrcFile
    f [Layer]
    layers
      let literate = (Layer -> Bool) -> [Layer] -> [Layer]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Layer -> Bool) -> Layer -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Layer -> Bool
    isCodeLayer) [Layer]
    layers
      let (terms, overlaps) = interleaveRanges (map Left code) (map Right literate)

      forM_ (map fst overlaps) $ \Either Token Layer
    c ->
        ParseWarning -> PM ()
    warning (ParseWarning -> PM ()) -> ParseWarning -> PM ()
    forall a b. (a -> b) -> a -> b
    $ OverlappingTokensWarning { warnRange :: Range' SrcFile
    warnRange = SrcFile
    f SrcFile -> Range' () -> Range' SrcFile
    forall a b. a -> Range' b -> Range' a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Either Token Layer -> Range' ()
    forall a. HasRangeWithoutFile a => a -> Range' ()
    getRangeWithoutFile Either Token Layer
    c }

      return . (,coh) . forMaybe terms $ \case
          Left Token
    t                           -> Token -> Maybe Token
    forall a. a -> Maybe a
    Just Token
    t
          Right (Layer LayerRole
    Comment IntervalWithoutFile
    interval String
    s) -> Token -> Maybe Token
    forall a. a -> Maybe a
    Just (Token -> Maybe Token) -> Token -> Maybe Token
    forall a b. (a -> b) -> a -> b
    $ (Interval, String) -> Token
    TokTeX    (SrcFile
    f SrcFile -> IntervalWithoutFile -> Interval
    forall a b. a -> Interval' b -> Interval' a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ IntervalWithoutFile
    interval, String
    s)
          Right (Layer LayerRole
    Markup  IntervalWithoutFile
    interval String
    s) -> Token -> Maybe Token
    forall a. a -> Maybe a
    Just (Token -> Maybe Token) -> Token -> Maybe Token
    forall a b. (a -> b) -> a -> b
    $ (Interval, String) -> Token
    TokMarkup (SrcFile
    f SrcFile -> IntervalWithoutFile -> Interval
    forall a b. a -> Interval' b -> Interval' a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ IntervalWithoutFile
    interval, String
    s)
          Right (Layer LayerRole
    Code IntervalWithoutFile
    _ String
    _)           -> Maybe Token
    forall a. Maybe a
    Nothing

    parseLiterateFile
      :: Processor
      -> Parser a
      -> RangeFile
         -- ^ The file.
      -> String
         -- ^ The file contents. Note that the file is /not/ read from
         -- disk.
      -> PM (a, Attributes)
    parseLiterateFile :: forall a.
    Processor -> Parser a -> RangeFile -> String -> PM (a, Attributes)
    parseLiterateFile Processor
    po Parser a
    p RangeFile
    path = Parser a -> LiterateParser a
    forall a. Parser a -> LiterateParser a
    parseLiterate Parser a
    p Parser a
    p (RangeFile -> SrcFile
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RangeFile
    path) ([Layer] -> PM (a, Attributes))
    -> (String -> [Layer]) -> String -> PM (a, Attributes)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Processor
    po (() -> Position' ()
    forall a. a -> Position' a
    startPos' ())

    parsePosString :: Parser a -> Position -> String -> PM (a, Attributes)
    parsePosString :: forall a. Parser a -> Position -> String -> PM (a, Attributes)
    parsePosString Parser a
    p Position
    pos = IO (ParseResult a) -> PM (a, Attributes)
    forall a. IO (ParseResult a) -> PM (a, Attributes)
    wrapM (IO (ParseResult a) -> PM (a, Attributes))
    -> (String -> IO (ParseResult a)) -> String -> PM (a, Attributes)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseResult a -> IO (ParseResult a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ParseResult a -> IO (ParseResult a))
    -> (String -> ParseResult a) -> String -> IO (ParseResult a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Position
    -> ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
    forall a.
    Position
    -> ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
    M.parsePosString Position
    pos (Parser a -> ParseFlags
    forall a. Parser a -> ParseFlags
    parseFlags Parser a
    p) [LexState]
    normalLexState (Parser a -> Parser a
    forall a. Parser a -> Parser a
    parser Parser a
    p)

    -- | Extensions supported by `parseFile`.

    agdaFileExtensions :: [String]
    agdaFileExtensions :: [String]
    agdaFileExtensions = String
    ".agda" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : ((String, (Processor, FileType)) -> String
    forall a b. (a, b) -> a
    fst ((String, (Processor, FileType)) -> String)
    -> [(String, (Processor, FileType))] -> [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(String, (Processor, FileType))]
    literateProcessors)

    parseFile
      :: Show a
      => Parser a
      -> RangeFile
         -- ^ The file.
      -> String
         -- ^ The file contents. Note that the file is /not/ read from
         -- disk.
      -> PM ((a, Attributes), FileType)
    parseFile :: forall a.
    Show a =>
    Parser a -> RangeFile -> String -> PM ((a, Attributes), FileType)
    parseFile Parser a
    p RangeFile
    file String
    input =
      if String
    ".agda" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isSuffixOf` String
    path then
        (, FileType
    AgdaFileType) ((a, Attributes) -> ((a, Attributes), FileType))
    -> PM (a, Attributes) -> PM ((a, Attributes), FileType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SrcFile -> Parser a -> String -> PM (a, Attributes)
    forall a. SrcFile -> Parser a -> String -> PM (a, Attributes)
    parseFileFromString (RangeFile -> SrcFile
    forall a. a -> Maybe a
    Strict.Just RangeFile
    file) Parser a
    p String
    input
      else
        [(String, (Processor, FileType))] -> PM ((a, Attributes), FileType)
    go [(String, (Processor, FileType))]
    literateProcessors
      where
        path :: String
    path = AbsolutePath -> String
    filePath (RangeFile -> AbsolutePath
    rangeFilePath RangeFile
    file)

        go :: [(String, (Processor, FileType))] -> PM ((a, Attributes), FileType)
    go [] = ParseError -> PM ((a, Attributes), FileType)
    forall a. ParseError -> PM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError InvalidExtensionError
                       { errPath :: RangeFile
    errPath = RangeFile
    file
                       , errValidExts :: [String]
    errValidExts = [String]
    agdaFileExtensions
                       }
        go ((String
    ext, (Processor
    po, FileType
    ft)) : [(String, (Processor, FileType))]
    pos)
          | String
    ext String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isSuffixOf` String
    path =
              (, FileType
    ft) ((a, Attributes) -> ((a, Attributes), FileType))
    -> PM (a, Attributes) -> PM ((a, Attributes), FileType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Processor -> Parser a -> RangeFile -> String -> PM (a, Attributes)
    forall a.
    Processor -> Parser a -> RangeFile -> String -> PM (a, Attributes)
    parseLiterateFile Processor
    po Parser a
    p RangeFile
    file String
    input
          | Bool
    otherwise = [(String, (Processor, FileType))] -> PM ((a, Attributes), FileType)
    go [(String, (Processor, FileType))]
    pos

    ------------------------------------------------------------------------
    -- Specific parsers

    -- | Parses a module.

    moduleParser :: Parser Module
    moduleParser :: Parser Module
    moduleParser = Parser
      { parser :: Parser Module
    parser        = Parser Module
    P.moduleParser
      , parseFlags :: ParseFlags
    parseFlags    = ParseFlags
    withoutComments
      , parseLiterate :: LiterateParser Module
    parseLiterate = LiterateParser Module
    forall a. LiterateParser a
    parseLiterateWithoutComments
      }

    -- | Parses a module name.

    moduleNameParser :: Parser QName
    moduleNameParser :: Parser QName
    moduleNameParser = Parser
      { parser :: Parser QName
    parser        = Parser QName
    P.moduleNameParser
      , parseFlags :: ParseFlags
    parseFlags    = ParseFlags
    withoutComments
      , parseLiterate :: LiterateParser QName
    parseLiterate = LiterateParser QName
    forall a. LiterateParser a
    parseLiterateWithoutComments
      }

    -- | Parses an expression.

    exprParser :: Parser Expr
    exprParser :: Parser Expr
    exprParser = Parser
      { parser :: Parser Expr
    parser        = Parser Expr
    P.exprParser
      , parseFlags :: ParseFlags
    parseFlags    = ParseFlags
    withoutComments
      , parseLiterate :: LiterateParser Expr
    parseLiterate = LiterateParser Expr
    forall a. LiterateParser a
    parseLiterateWithoutComments
      }

    -- | Parses an expression followed by a where clause.

    exprWhereParser :: Parser ExprWhere
    exprWhereParser :: Parser ExprWhere
    exprWhereParser = Parser
      { parser :: Parser ExprWhere
    parser        = Parser ExprWhere
    P.exprWhereParser
      , parseFlags :: ParseFlags
    parseFlags    = ParseFlags
    withoutComments
      , parseLiterate :: LiterateParser ExprWhere
    parseLiterate = LiterateParser ExprWhere
    forall a. LiterateParser a
    parseLiterateWithoutComments
      }

    -- | Parses an expression or some other content of an interaction hole.

    holeContentParser :: Parser HoleContent
    holeContentParser :: Parser HoleContent
    holeContentParser = Parser
      { parser :: Parser HoleContent
    parser        = Parser HoleContent
    P.holeContentParser
      , parseFlags :: ParseFlags
    parseFlags    = ParseFlags
    withoutComments
      , parseLiterate :: LiterateParser HoleContent
    parseLiterate = LiterateParser HoleContent
    forall a. LiterateParser a
    parseLiterateWithoutComments
      }

    -- | Gives the parsed token stream (including comments).

    tokensParser :: Parser [Token]
    tokensParser :: Parser [Token]
    tokensParser = Parser
      { parser :: Parser [Token]
    parser        = Parser [Token]
    P.tokensParser
      , parseFlags :: ParseFlags
    parseFlags    = ParseFlags
    withComments
      , parseLiterate :: LiterateParser [Token]
    parseLiterate = LiterateParser [Token]
    parseLiterateWithComments
      }

    -- | Keep comments in the token stream generated by the lexer.

    withComments :: ParseFlags
    withComments :: ParseFlags
    withComments = ParseFlags
    defaultParseFlags { parseKeepComments = True }

    -- | Do not keep comments in the token stream generated by the lexer.

    withoutComments :: ParseFlags
    withoutComments :: ParseFlags
    withoutComments = ParseFlags
    defaultParseFlags { parseKeepComments = False }