    module Agda.Syntax.Parser
        ( -- * Types
          Parser
          -- * Parse functions
        , Agda.Syntax.Parser.parse
        , Agda.Syntax.Parser.parsePosString
        , parseFile
          -- * Parsers
        , moduleParser
        , moduleNameParser
        , acceptableFileExts
        , 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.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
    <$ :: forall a b. a -> PM b -> PM a
    $c<$ :: forall a b. a -> PM b -> PM a
    fmap :: forall a b. (a -> b) -> PM a -> PM b
    $cfmap :: forall a b. (a -> b) -> PM a -> PM b
    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
    <* :: forall a b. PM a -> PM b -> PM a
    $c<* :: forall a b. PM a -> PM b -> PM a
    *> :: forall a b. PM a -> PM b -> PM b
    $c*> :: forall a b. PM a -> PM b -> PM b
    liftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
    $cliftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
    <*> :: forall a b. PM (a -> b) -> PM a -> PM b
    $c<*> :: forall a b. PM (a -> b) -> PM a -> PM b
    pure :: forall a. a -> PM a
    $cpure :: forall a. a -> 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
    return :: forall a. a -> PM a
    $creturn :: forall a. a -> PM a
    >> :: forall a b. PM a -> PM b -> PM b
    $c>> :: forall a b. PM a -> PM b -> PM b
    >>= :: forall a b. PM a -> (a -> PM b) -> PM b
    $c>>= :: forall a b. PM a -> (a -> PM b) -> PM b
    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
    liftIO :: forall a. IO a -> PM a
    $cliftIO :: 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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (([ParseWarning] -> [ParseWarning])
    -> (Either ParseError a, [ParseWarning])
    -> (Either ParseError a, [ParseWarning])
    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
    wrap :: forall a. ParseResult a -> PM a
    wrap (ParseFailed ParseError
    err)  = 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 -> PM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

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

    -- | Returns the contents of the given file.

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

    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
      Either IOError a
    a <- IO (Either IOError a) -> m (Either IOError 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 (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 Either IOError a
    a of
        Right a
    x  -> a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x
        Left IOError
    err -> 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 -> [Layer] -> PM a

    -- | 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
    parse :: forall a. Parser a -> String -> PM a
    parse Parser a
    p = IO (ParseResult a) -> PM a
    forall a. IO (ParseResult a) -> PM a
    wrapM (IO (ParseResult a) -> PM a)
    -> (String -> IO (ParseResult a)) -> String -> PM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseResult a -> IO (ParseResult 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
    parseFileFromString :: forall a. SrcFile -> Parser a -> String -> PM a
    parseFileFromString SrcFile
    src Parser a
    p = IO (ParseResult a) -> PM a
    forall a. IO (ParseResult a) -> PM a
    wrapM (IO (ParseResult a) -> PM a)
    -> (String -> IO (ParseResult a)) -> String -> PM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseResult a -> IO (ParseResult 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 [Layer]
    layers = SrcFile -> Parser a -> String -> PM a
    forall a. SrcFile -> Parser a -> String -> PM a
    parseFileFromString ([Layer] -> SrcFile
    literateSrcFile [Layer]
    layers) Parser a
    p (String -> PM a) -> String -> PM a
    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 [Layer]
    layers = do
      [Token]
    code <- LiterateParser [Token]
    forall a. LiterateParser a
    parseLiterateWithoutComments Parser [Token]
    p [Layer]
    layers
      let literate :: [Layer]
    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 ([Either Token Layer]
    terms, [(Either Token Layer, Either Token Layer)]
    overlaps) = [Either Token Layer]
    -> [Either Token Layer]
    -> ([Either Token Layer],
        [(Either Token Layer, Either Token Layer)])
    forall a. HasRange a => [a] -> [a] -> ([a], [(a, a)])
    interleaveRanges ((Token -> Either Token Layer) -> [Token] -> [Either Token Layer]
    forall a b. (a -> b) -> [a] -> [b]
    map Token -> Either Token Layer
    forall a b. a -> Either a b
    Left [Token]
    code) ((Layer -> Either Token Layer) -> [Layer] -> [Either Token Layer]
    forall a b. (a -> b) -> [a] -> [b]
    map Layer -> Either Token Layer
    forall a b. b -> Either a b
    Right [Layer]
    literate)

      [Either Token Layer] -> (Either Token Layer -> PM ()) -> PM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ (((Either Token Layer, Either Token Layer) -> Either Token Layer)
    -> [(Either Token Layer, Either Token Layer)]
    -> [Either Token Layer]
    forall a b. (a -> b) -> [a] -> [b]
    map (Either Token Layer, Either Token Layer) -> Either Token Layer
    forall a b. (a, b) -> a
    fst [(Either Token Layer, Either Token Layer)]
    overlaps) ((Either Token Layer -> PM ()) -> PM ())
    -> (Either Token Layer -> PM ()) -> PM ()
    forall a b. (a -> b) -> a -> b
    $ \Either Token Layer
    c ->
        ParseWarning -> PM ()
    warning (ParseWarning -> PM ()) -> ParseWarning -> PM ()
    forall a b. (a -> b) -> a -> b
    $ OverlappingTokensWarning :: Range' SrcFile -> ParseWarning
    OverlappingTokensWarning { warnRange :: Range' SrcFile
    warnRange = Either Token Layer -> Range' SrcFile
    forall a. HasRange a => a -> Range' SrcFile
    getRange Either Token Layer
    c }

      [Token] -> PM [Token]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Token] -> PM [Token]) -> [Token] -> PM [Token]
    forall a b. (a -> b) -> a -> b
    $ [Either Token Layer]
    -> (Either Token Layer -> Maybe Token) -> [Token]
    forall a b. [a] -> (a -> Maybe b) -> [b]
    forMaybe [Either Token Layer]
    terms ((Either Token Layer -> Maybe Token) -> [Token])
    -> (Either Token Layer -> Maybe Token) -> [Token]
    forall a b. (a -> b) -> a -> b
    $ \case
        Left Token
    t                           -> Token -> Maybe Token
    forall a. a -> Maybe a
    Just Token
    t
        Right (Layer LayerRole
    Comment Interval
    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    (Interval
    interval, String
    s)
        Right (Layer LayerRole
    Markup  Interval
    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 (Interval
    interval, String
    s)
        Right (Layer LayerRole
    Code Interval
    _ String
    _)           -> Maybe Token
    forall a. Maybe a
    Nothing

    parseLiterateFile
      :: Processor
      -> Parser a
      -> AbsolutePath
         -- ^ The path to the file.
      -> String
         -- ^ The file contents. Note that the file is /not/ read from
         -- disk.
      -> PM a
    parseLiterateFile :: forall a. Processor -> Parser a -> AbsolutePath -> String -> PM a
    parseLiterateFile Processor
    po Parser a
    p AbsolutePath
    path = Parser a -> LiterateParser a
    forall a. Parser a -> LiterateParser a
    parseLiterate Parser a
    p Parser a
    p ([Layer] -> PM a) -> (String -> [Layer]) -> String -> PM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Processor
    po (Maybe AbsolutePath -> Position
    startPos (AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Just AbsolutePath
    path))

    parsePosString :: Parser a -> Position -> String -> PM a
    parsePosString :: forall a. Parser a -> Position -> String -> PM a
    parsePosString Parser a
    p Position
    pos = IO (ParseResult a) -> PM a
    forall a. IO (ParseResult a) -> PM a
    wrapM (IO (ParseResult a) -> PM a)
    -> (String -> IO (ParseResult a)) -> String -> PM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseResult a -> IO (ParseResult 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`.

    acceptableFileExts :: [String]
    acceptableFileExts :: [String]
    acceptableFileExts = 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
      -> AbsolutePath
         -- ^ The path to the file.
      -> String
         -- ^ The file contents. Note that the file is /not/ read from
         -- disk.
      -> PM (a, FileType)
    parseFile :: forall a.
    Show a =>
    Parser a -> AbsolutePath -> String -> PM (a, FileType)
    parseFile Parser a
    p AbsolutePath
    file String
    input =
      if String
    ".agda" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isSuffixOf` AbsolutePath -> String
    filePath AbsolutePath
    file then
        (, FileType
    AgdaFileType) (a -> (a, FileType)) -> PM a -> PM (a, FileType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SrcFile -> Parser a -> String -> PM a
    forall a. SrcFile -> Parser a -> String -> PM a
    parseFileFromString (AbsolutePath -> SrcFile
    forall a. a -> Maybe a
    Strict.Just AbsolutePath
    file) Parser a
    p String
    input
      else
        [(String, (Processor, FileType))] -> PM (a, FileType)
    go [(String, (Processor, FileType))]
    literateProcessors
      where
        go :: [(String, (Processor, FileType))] -> PM (a, FileType)
    go [] = ParseError -> PM (a, FileType)
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError InvalidExtensionError :: AbsolutePath -> [String] -> ParseError
    InvalidExtensionError
                       { errPath :: AbsolutePath
    errPath = AbsolutePath
    file
                       , errValidExts :: [String]
    errValidExts = [String]
    acceptableFileExts
                       }
        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` AbsolutePath -> String
    filePath AbsolutePath
    file =
              (, FileType
    ft) (a -> (a, FileType)) -> PM a -> PM (a, FileType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Processor -> Parser a -> AbsolutePath -> String -> PM a
    forall a. Processor -> Parser a -> AbsolutePath -> String -> PM a
    parseLiterateFile Processor
    po Parser a
    p AbsolutePath
    file String
    input
          | Bool
    otherwise = [(String, (Processor, FileType))] -> PM (a, FileType)
    go [(String, (Processor, FileType))]
    pos

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

    -- | Parses a module.

    moduleParser :: Parser Module
    moduleParser :: Parser Module
    moduleParser = Parser :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
    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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
    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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
    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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
    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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
    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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
    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 :: Bool
    parseKeepComments = Bool
    True }

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

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