    module Agda.Syntax.Parser.Monad
        ( -- * The parser monad
          Parser
        , ParseResult(..)
        , ParseState(..)
        , ParseError(..), ParseWarning(..)
        , LexState
        , LayoutBlock(..), LayoutContext, LayoutStatus(..)
        , Column
        , ParseFlags (..)
          -- * Running the parser
        , initState
        , defaultParseFlags
        , parse
        , parsePosString
        , parseFromSrc
          -- * Manipulating the state
        , setParsePos, setLastPos, getParseInterval
        , setPrevToken
        , getParseFlags
        , getLexState, pushLexState, popLexState
          -- ** Layout
        , topBlock, popBlock, pushBlock
        , getContext, setContext, modifyContext
        , resetLayoutStatus
          -- ** Errors
        , parseWarning, parseWarningName
        , parseError, parseErrorAt, parseError', parseErrorRange
        , lexError
        )
        where

    import Control.DeepSeq
    import Control.Exception ( displayException )
    import Control.Monad.Except
    import Control.Monad.State

    import Data.Maybe ( listToMaybe )
    import Data.Word  ( Word32)

    import Agda.Interaction.Options.Warnings

    import Agda.Syntax.Concrete.Attribute
    import Agda.Syntax.Position
    import Agda.Syntax.Parser.Tokens ( Keyword( KwMutual ) )

    import Agda.TypeChecking.Positivity.Occurrence ( pattern Mixed )

    import Agda.Utils.IO   ( showIOException )
    import Agda.Utils.List ( tailWithDefault )
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Syntax.Common.Pretty

    import Agda.Utils.Impossible

    {--------------------------------------------------------------------------
        The parse monad
     --------------------------------------------------------------------------}

    -- | The parse monad.
    newtype Parser a = P { forall a. Parser a -> StateT ParseState (Either ParseError) a
    _runP :: StateT ParseState (Either ParseError) a }
      deriving ((forall a b. (a -> b) -> Parser a -> Parser b)
    -> (forall a b. a -> Parser b -> Parser a) -> Functor Parser
    forall a b. a -> Parser b -> Parser a
    forall a b. (a -> b) -> Parser a -> Parser 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) -> Parser a -> Parser b
    fmap :: forall a b. (a -> b) -> Parser a -> Parser b
    $c<$ :: forall a b. a -> Parser b -> Parser a
    <$ :: forall a b. a -> Parser b -> Parser a
    Functor, Functor Parser
    Functor Parser =>
    (forall a. a -> Parser a)
    -> (forall a b. Parser (a -> b) -> Parser a -> Parser b)
    -> (forall a b c.
        (a -> b -> c) -> Parser a -> Parser b -> Parser c)
    -> (forall a b. Parser a -> Parser b -> Parser b)
    -> (forall a b. Parser a -> Parser b -> Parser a)
    -> Applicative Parser
    forall a. a -> Parser a
    forall a b. Parser a -> Parser b -> Parser a
    forall a b. Parser a -> Parser b -> Parser b
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser 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 -> Parser a
    pure :: forall a. a -> Parser a
    $c<*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
    <*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
    $cliftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
    liftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
    $c*> :: forall a b. Parser a -> Parser b -> Parser b
    *> :: forall a b. Parser a -> Parser b -> Parser b
    $c<* :: forall a b. Parser a -> Parser b -> Parser a
    <* :: forall a b. Parser a -> Parser b -> Parser a
    Applicative, Applicative Parser
    Applicative Parser =>
    (forall a b. Parser a -> (a -> Parser b) -> Parser b)
    -> (forall a b. Parser a -> Parser b -> Parser b)
    -> (forall a. a -> Parser a)
    -> Monad Parser
    forall a. a -> Parser a
    forall a b. Parser a -> Parser b -> Parser b
    forall a b. Parser a -> (a -> Parser b) -> Parser 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. Parser a -> (a -> Parser b) -> Parser b
    >>= :: forall a b. Parser a -> (a -> Parser b) -> Parser b
    $c>> :: forall a b. Parser a -> Parser b -> Parser b
    >> :: forall a b. Parser a -> Parser b -> Parser b
    $creturn :: forall a. a -> Parser a
    return :: forall a. a -> Parser a
    Monad, MonadState ParseState, MonadError ParseError)

    -- | The parser state. Contains everything the parser and the lexer could ever
    --   need.
    data ParseState = PState
        { ParseState -> SrcFile
    parseSrcFile  :: !SrcFile
        , ParseState -> PositionWithoutFile
    parsePos      :: !PositionWithoutFile  -- ^ position at current input location
        , ParseState -> PositionWithoutFile
    parseLastPos  :: !PositionWithoutFile  -- ^ position of last token
        , ParseState -> String
    parseInp      :: String                -- ^ the current input
        , ParseState -> Char
    parsePrevChar :: !Char                 -- ^ the character before the input
        , ParseState -> String
    parsePrevToken:: String                -- ^ the previous token
        , ParseState -> LayoutContext
    parseLayout   :: LayoutContext         -- ^ the stack of layout blocks
        , ParseState -> LayoutStatus
    parseLayStatus:: LayoutStatus          -- ^ the status of the coming layout block
        , ParseState -> Keyword
    parseLayKw    :: Keyword               -- ^ the keyword for the coming layout block
        , ParseState -> [LexState]
    parseLexState :: [LexState]            -- ^ the state of the lexer
                                                 --   (states can be nested so we need a stack)
        , ParseState -> ParseFlags
    parseFlags    :: ParseFlags            -- ^ parametrization of the parser
        , ParseState -> [ParseWarning]
    parseWarnings :: ![ParseWarning]       -- ^ In reverse order.
        , ParseState -> Attributes
    parseAttributes
                        :: !Attributes
          -- ^ Every encountered attribute.
        }
        deriving LexState -> ParseState -> ShowS
    [ParseState] -> ShowS
    ParseState -> String
    (LexState -> ParseState -> ShowS)
    -> (ParseState -> String)
    -> ([ParseState] -> ShowS)
    -> Show ParseState
    forall a.
    (LexState -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LexState -> ParseState -> ShowS
    showsPrec :: LexState -> ParseState -> ShowS
    $cshow :: ParseState -> String
    show :: ParseState -> String
    $cshowList :: [ParseState] -> ShowS
    showList :: [ParseState] -> ShowS
    Show

    {-| For context sensitive lexing alex provides what is called /start codes/
        in the Alex documentation.  It is really an integer representing the state
        of the lexer, so we call it @LexState@ instead.
    -}
    type LexState = Int

    -- | The stack of layout blocks.
    --
    --   When we encounter a layout keyword, we push a 'Tentative' block
    --   with 'noColumn'.  This is replaced by aproper column once we
    --   reach the next token.
    type LayoutContext = [LayoutBlock]

    -- | We need to keep track of the context to do layout. The context
    --   specifies the indentation columns of the open layout blocks. See
    --   "Agda.Syntax.Parser.Layout" for more informaton.
    data LayoutBlock
      = Layout Keyword LayoutStatus Column
          -- ^ Layout at specified 'Column', introduced by 'Keyword'.
        deriving LexState -> LayoutBlock -> ShowS
    LayoutContext -> ShowS
    LayoutBlock -> String
    (LexState -> LayoutBlock -> ShowS)
    -> (LayoutBlock -> String)
    -> (LayoutContext -> ShowS)
    -> Show LayoutBlock
    forall a.
    (LexState -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LexState -> LayoutBlock -> ShowS
    showsPrec :: LexState -> LayoutBlock -> ShowS
    $cshow :: LayoutBlock -> String
    show :: LayoutBlock -> String
    $cshowList :: LayoutContext -> ShowS
    showList :: LayoutContext -> ShowS
    Show

    -- | A (layout) column.
    type Column = Word32

    -- | Status of a layout column (see #1145).
    --   A layout column is 'Tentative' until we encounter a new line.
    --   This allows stacking of layout keywords.
    --
    --   Inside a @LayoutContext@ the sequence of 'Confirmed' columns
    --   needs to be strictly increasing.
    --   'Tentative columns between 'Confirmed' columns need to be
    --   strictly increasing as well.
    data LayoutStatus
      = Tentative  -- ^ The token defining the layout column was on the same line
                   --   as the layout keyword and we have not seen a new line yet.
      | Confirmed  -- ^ We have seen a new line since the layout keyword
                   --   and the layout column has not been superseded by
                   --   a smaller column.
        deriving (LayoutStatus -> LayoutStatus -> Bool
    (LayoutStatus -> LayoutStatus -> Bool)
    -> (LayoutStatus -> LayoutStatus -> Bool) -> Eq LayoutStatus
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LayoutStatus -> LayoutStatus -> Bool
    == :: LayoutStatus -> LayoutStatus -> Bool
    $c/= :: LayoutStatus -> LayoutStatus -> Bool
    /= :: LayoutStatus -> LayoutStatus -> Bool
    Eq, LexState -> LayoutStatus -> ShowS
    [LayoutStatus] -> ShowS
    LayoutStatus -> String
    (LexState -> LayoutStatus -> ShowS)
    -> (LayoutStatus -> String)
    -> ([LayoutStatus] -> ShowS)
    -> Show LayoutStatus
    forall a.
    (LexState -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LexState -> LayoutStatus -> ShowS
    showsPrec :: LexState -> LayoutStatus -> ShowS
    $cshow :: LayoutStatus -> String
    show :: LayoutStatus -> String
    $cshowList :: [LayoutStatus] -> ShowS
    showList :: [LayoutStatus] -> ShowS
    Show)

    -- | Parser flags.
    data ParseFlags = ParseFlags
      { ParseFlags -> Bool
    parseKeepComments :: Bool
        -- ^ Should comment tokens be returned by the lexer?
      }
      deriving LexState -> ParseFlags -> ShowS
    [ParseFlags] -> ShowS
    ParseFlags -> String
    (LexState -> ParseFlags -> ShowS)
    -> (ParseFlags -> String)
    -> ([ParseFlags] -> ShowS)
    -> Show ParseFlags
    forall a.
    (LexState -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LexState -> ParseFlags -> ShowS
    showsPrec :: LexState -> ParseFlags -> ShowS
    $cshow :: ParseFlags -> String
    show :: ParseFlags -> String
    $cshowList :: [ParseFlags] -> ShowS
    showList :: [ParseFlags] -> ShowS
    Show

    -- | Parse errors: what you get if parsing fails.
    data ParseError

      -- | Errors that arise at a specific position in the file
      = ParseError
        { ParseError -> SrcFile
    errSrcFile   :: !SrcFile
                          -- ^ The file in which the error occurred.
        , ParseError -> PositionWithoutFile
    errPos       :: !PositionWithoutFile
                          -- ^ Where the error occurred.
        , ParseError -> String
    errInput     :: String
                          -- ^ The remaining input.
        , ParseError -> String
    errPrevToken :: String
                          -- ^ The previous token.
        , ParseError -> String
    errMsg       :: String
                          -- ^ Hopefully an explanation of what happened.
        }

      -- | Parse errors that concern a range in a file.
      | OverlappingTokensError
        { ParseError -> Range' SrcFile
    errRange     :: !(Range' SrcFile)
                          -- ^ The range of the bigger overlapping token
        }

      -- | Parse errors that concern a whole file.
      | InvalidExtensionError
        { ParseError -> RangeFile
    errPath      :: !RangeFile
                          -- ^ The file which the error concerns.
        , ParseError -> [String]
    errValidExts :: [String]
        }
      | ReadFileError
        { errPath      :: !RangeFile
        , ParseError -> IOError
    errIOError   :: IOError
        }
      deriving LexState -> ParseError -> ShowS
    [ParseError] -> ShowS
    ParseError -> String
    (LexState -> ParseError -> ShowS)
    -> (ParseError -> String)
    -> ([ParseError] -> ShowS)
    -> Show ParseError
    forall a.
    (LexState -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LexState -> ParseError -> ShowS
    showsPrec :: LexState -> ParseError -> ShowS
    $cshow :: ParseError -> String
    show :: ParseError -> String
    $cshowList :: [ParseError] -> ShowS
    showList :: [ParseError] -> ShowS
    Show

    instance NFData ParseError where
      rnf :: ParseError -> ()
    rnf = \case
        ParseError SrcFile
    _f PositionWithoutFile
    _r String
    inp String
    tok String
    msg  -> String -> ()
    forall a. NFData a => a -> ()
    rnf String
    inp () -> () -> ()
    forall a b. a -> b -> b
    `seq` String -> ()
    forall a. NFData a => a -> ()
    rnf String
    tok () -> () -> ()
    forall a b. a -> b -> b
    `seq` String -> ()
    forall a. NFData a => a -> ()
    rnf String
    msg
        OverlappingTokensError Range' SrcFile
    _r     -> ()
        InvalidExtensionError RangeFile
    _r [String]
    exts -> [String] -> ()
    forall a. NFData a => a -> ()
    rnf [String]
    exts
        ReadFileError RangeFile
    _r IOError
    _err         -> ()

    -- | Warnings for parsing.
    data ParseWarning
      -- | Parse errors that concern a range in a file.
      = OverlappingTokensWarning
        { ParseWarning -> Range' SrcFile
    warnRange :: !(Range' SrcFile)
            -- ^ The range of the bigger overlapping token.
        }
      | MisplacedAttributes Range String
          -- ^ The 'String' is the error message.
      | UnknownPolarity Range String
          -- ^ Unknown polarity, ignored.
      | UnknownAttribute Range String
          -- ^ Unknown attribute, ignored.
          --   The 'Range' includes the "@", the 'String' not.
      | UnsupportedAttribute Range !(Maybe String)
          -- ^ Unsupported attribute.
      | MultipleAttributes Range !(Maybe String)
          -- ^ Multiple attributes.
      deriving LexState -> ParseWarning -> ShowS
    [ParseWarning] -> ShowS
    ParseWarning -> String
    (LexState -> ParseWarning -> ShowS)
    -> (ParseWarning -> String)
    -> ([ParseWarning] -> ShowS)
    -> Show ParseWarning
    forall a.
    (LexState -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LexState -> ParseWarning -> ShowS
    showsPrec :: LexState -> ParseWarning -> ShowS
    $cshow :: ParseWarning -> String
    show :: ParseWarning -> String
    $cshowList :: [ParseWarning] -> ShowS
    showList :: [ParseWarning] -> ShowS
    Show

    instance NFData ParseWarning where
      rnf :: ParseWarning -> ()
    rnf (OverlappingTokensWarning Range' SrcFile
    _) = ()
      rnf (MisplacedAttributes Range' SrcFile
    _ String
    s)    = String -> ()
    forall a. NFData a => a -> ()
    rnf String
    s
      rnf (UnknownPolarity Range' SrcFile
    _ String
    s)        = String -> ()
    forall a. NFData a => a -> ()
    rnf String
    s
      rnf (UnknownAttribute Range' SrcFile
    _ String
    s)       = String -> ()
    forall a. NFData a => a -> ()
    rnf String
    s
      rnf (UnsupportedAttribute Range' SrcFile
    _ Maybe String
    s)   = Maybe String -> ()
    forall a. NFData a => a -> ()
    rnf Maybe String
    s
      rnf (MultipleAttributes Range' SrcFile
    _ Maybe String
    s)     = Maybe String -> ()
    forall a. NFData a => a -> ()
    rnf Maybe String
    s

    parseWarningName :: ParseWarning -> WarningName
    parseWarningName :: ParseWarning -> WarningName
    parseWarningName = \case
      OverlappingTokensWarning{} -> WarningName
    OverlappingTokensWarning_
      MisplacedAttributes{}      -> WarningName
    MisplacedAttributes_
      UnknownPolarity{}          -> WarningName
    UnknownPolarity_
      UnknownAttribute{}         -> WarningName
    UnknownAttribute_
      UnsupportedAttribute{}     -> WarningName
    UnsupportedAttribute_
      MultipleAttributes{}       -> WarningName
    MultipleAttributes_

    -- | The result of parsing something.
    data ParseResult a
      = ParseOk ParseState a
      | ParseFailed ParseError
      deriving LexState -> ParseResult a -> ShowS
    [ParseResult a] -> ShowS
    ParseResult a -> String
    (LexState -> ParseResult a -> ShowS)
    -> (ParseResult a -> String)
    -> ([ParseResult a] -> ShowS)
    -> Show (ParseResult a)
    forall a. Show a => LexState -> ParseResult a -> ShowS
    forall a. Show a => [ParseResult a] -> ShowS
    forall a. Show a => ParseResult a -> String
    forall a.
    (LexState -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => LexState -> ParseResult a -> ShowS
    showsPrec :: LexState -> ParseResult a -> ShowS
    $cshow :: forall a. Show a => ParseResult a -> String
    show :: ParseResult a -> String
    $cshowList :: forall a. Show a => [ParseResult a] -> ShowS
    showList :: [ParseResult a] -> ShowS
    Show

    -- | Old interface to parser.
    unP :: Parser a -> ParseState -> ParseResult a
    unP :: forall a. Parser a -> ParseState -> ParseResult a
    unP (P StateT ParseState (Either ParseError) a
    m) ParseState
    s = case StateT ParseState (Either ParseError) a
    -> ParseState -> Either ParseError (a, ParseState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT StateT ParseState (Either ParseError) a
    m ParseState
    s of
      Left ParseError
    err     -> ParseError -> ParseResult a
    forall a. ParseError -> ParseResult a
    ParseFailed ParseError
    err
      Right (a
    a, ParseState
    s) -> ParseState -> a -> ParseResult a
    forall a. ParseState -> a -> ParseResult a
    ParseOk ParseState
    s a
    a

    -- | Throw a parse error at the current position.
    parseError :: String -> Parser a
    parseError :: forall a. String -> Parser a
    parseError String
    msg = do
      s <- Parser ParseState
    forall s (m :: * -> *). MonadState s m => m s
    get
      throwError $ ParseError
        { errSrcFile   = parseSrcFile s
        , errPos       = parseLastPos s
        , errInput     = parseInp s
        , errPrevToken = parsePrevToken s
        , errMsg       = msg
        }

    -- | Records a warning.

    parseWarning :: ParseWarning -> Parser ()
    parseWarning :: ParseWarning -> Parser ()
    parseWarning ParseWarning
    w =
      (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' ((ParseState -> ParseState) -> Parser ())
    -> (ParseState -> ParseState) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ \ParseState
    s -> ParseState
    s { parseWarnings = w : parseWarnings s }

    {--------------------------------------------------------------------------
        Instances
     --------------------------------------------------------------------------}

    instance Pretty ParseError where
      pretty :: ParseError -> Doc
    pretty ParseError{PositionWithoutFile
    errPos :: ParseError -> PositionWithoutFile
    errPos :: PositionWithoutFile
    errPos,SrcFile
    errSrcFile :: ParseError -> SrcFile
    errSrcFile :: SrcFile
    errSrcFile,String
    errMsg :: ParseError -> String
    errMsg :: String
    errMsg,String
    errPrevToken :: ParseError -> String
    errPrevToken :: String
    errPrevToken,String
    errInput :: ParseError -> String
    errInput :: String
    errInput} = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ (Position' SrcFile -> Doc
    forall a. Pretty a => a -> Doc
    pretty PositionWithoutFile
    errPos{ srcFile = errSrcFile } Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    colon) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "error: [ParseError]"
          , if Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    errMsg then String -> Doc
    forall a. String -> Doc a
    text String
    errMsg else [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep
              -- Happy errors have no message, so we print the context instead
              [ String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    errPrevToken String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "<ERROR>"
              , String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ LexState -> ShowS
    forall a. LexState -> [a] -> [a]
    take LexState
    30 String
    errInput String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "..."
              ]
          ]
      pretty OverlappingTokensError{Range' SrcFile
    errRange :: ParseError -> Range' SrcFile
    errRange :: Range' SrcFile
    errRange} = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ (Range' SrcFile -> Doc
    forall a. Pretty a => a -> Doc
    pretty Range' SrcFile
    errRange Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    colon) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "error: [OverlappingTokensError]"
          , Doc
    "Multi-line comment spans one or more literate text blocks."
          ]
      pretty InvalidExtensionError{RangeFile
    errPath :: ParseError -> RangeFile
    errPath :: RangeFile
    errPath,[String]
    errValidExts :: ParseError -> [String]
    errValidExts :: [String]
    errValidExts} = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ (RangeFile -> Doc
    forall a. Pretty a => a -> Doc
    pretty RangeFile
    errPath Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    colon) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "error: [InvalidExtensionError]"
          , Doc
    "Unsupported extension."
          , Doc
    "Supported extensions are:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [String] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList_ [String]
    errValidExts
          ]
      pretty ReadFileError{RangeFile
    errPath :: ParseError -> RangeFile
    errPath :: RangeFile
    errPath,IOError
    errIOError :: ParseError -> IOError
    errIOError :: IOError
    errIOError} = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ Doc
    "Cannot read file" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> RangeFile -> Doc
    forall a. Pretty a => a -> Doc
    pretty RangeFile
    errPath
          , Doc
    "Error:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text (IOError -> String
    forall e. Exception e => e -> String
    showIOException IOError
    errIOError)
          ]

    instance HasRange ParseError where
      getRange :: ParseError -> Range' SrcFile
    getRange ParseError
    err = case ParseError
    err of
          ParseError{ SrcFile
    errSrcFile :: ParseError -> SrcFile
    errSrcFile :: SrcFile
    errSrcFile, errPos :: ParseError -> PositionWithoutFile
    errPos = PositionWithoutFile
    p } -> SrcFile
    -> PositionWithoutFile -> PositionWithoutFile -> Range' SrcFile
    forall a.
    a -> PositionWithoutFile -> PositionWithoutFile -> Range' a
    posToRange' SrcFile
    errSrcFile PositionWithoutFile
    p PositionWithoutFile
    p
          OverlappingTokensError{ Range' SrcFile
    errRange :: ParseError -> Range' SrcFile
    errRange :: Range' SrcFile
    errRange }   -> Range' SrcFile
    errRange
          InvalidExtensionError{}              -> Range' SrcFile
    errPathRange
          ReadFileError{}                      -> Range' SrcFile
    errPathRange
        where
        errPathRange :: Range' SrcFile
    errPathRange = Position' SrcFile -> Position' SrcFile -> Range' SrcFile
    forall a. Position' a -> Position' a -> Range' a
    posToRange Position' SrcFile
    p Position' SrcFile
    p
          where p :: Position' SrcFile
    p = Maybe RangeFile -> Position' SrcFile
    startPos (Maybe RangeFile -> Position' SrcFile)
    -> Maybe RangeFile -> Position' SrcFile
    forall a b. (a -> b) -> a -> b
    $ RangeFile -> Maybe RangeFile
    forall a. a -> Maybe a
    Just (RangeFile -> Maybe RangeFile) -> RangeFile -> Maybe RangeFile
    forall a b. (a -> b) -> a -> b
    $ ParseError -> RangeFile
    errPath ParseError
    err

    -- | Does not include printing of the range.
    --
    instance Pretty ParseWarning where
      pretty :: ParseWarning -> Doc
    pretty = \case

        OverlappingTokensWarning Range' SrcFile
    _r ->
          Doc
    "Multi-line comment spans one or more literate text blocks."

        MisplacedAttributes Range' SrcFile
    _r String
    s -> String -> Doc
    forall a. String -> Doc a
    text String
    s

        UnknownPolarity Range' SrcFile
    _r String
    s ->
          Doc
    "Replacing unknown polarity" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text String
    s Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "by" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Occurrence -> Doc
    forall a. Pretty a => a -> Doc
    pretty Occurrence
    Mixed

        UnknownAttribute Range' SrcFile
    _r String
    s ->
          Doc
    "Ignoring unknown attribute:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> (Doc
    "@" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> String -> Doc
    forall a. String -> Doc a
    text String
    s)

        UnsupportedAttribute Range' SrcFile
    _r Maybe String
    ms -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
          [ case Maybe String
    ms of
              Maybe String
    Nothing -> Doc
    "Attributes"
              Just String
    s  -> String -> Doc
    forall a. String -> Doc a
    text String
    s Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "attributes"
          , Doc
    "are not supported here."
          ]

        MultipleAttributes Range' SrcFile
    _r Maybe String
    ms -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
          [ Doc
    "Multiple", Maybe String -> Doc
    forall a. Pretty a => a -> Doc
    pretty Maybe String
    ms, Doc
    "attributes (ignored)." ]

    instance HasRange ParseWarning where
      getRange :: ParseWarning -> Range' SrcFile
    getRange OverlappingTokensWarning{Range' SrcFile
    warnRange :: ParseWarning -> Range' SrcFile
    warnRange :: Range' SrcFile
    warnRange} = Range' SrcFile
    warnRange
      getRange (MisplacedAttributes Range' SrcFile
    r String
    _)           = Range' SrcFile
    r
      getRange (UnknownPolarity Range' SrcFile
    r String
    _)               = Range' SrcFile
    r
      getRange (UnknownAttribute Range' SrcFile
    r String
    _)              = Range' SrcFile
    r
      getRange (UnsupportedAttribute Range' SrcFile
    r Maybe String
    _)          = Range' SrcFile
    r
      getRange (MultipleAttributes Range' SrcFile
    r Maybe String
    _)            = Range' SrcFile
    r

    {--------------------------------------------------------------------------
        Running the parser
     --------------------------------------------------------------------------}

    initStatePos :: Position -> ParseFlags -> String -> [LexState] -> ParseState
    initStatePos :: Position' SrcFile
    -> ParseFlags -> String -> [LexState] -> ParseState
    initStatePos Position' SrcFile
    pos ParseFlags
    flags String
    inp [LexState]
    st =
            PState  { parseSrcFile :: SrcFile
    parseSrcFile      = Position' SrcFile -> SrcFile
    forall a. Position' a -> a
    srcFile Position' SrcFile
    pos
                    , parsePos :: PositionWithoutFile
    parsePos          = PositionWithoutFile
    pos'
                    , parseLastPos :: PositionWithoutFile
    parseLastPos      = PositionWithoutFile
    pos'
                    , parseInp :: String
    parseInp          = String
    inp
                    , parsePrevChar :: Char
    parsePrevChar     = Char
    '\n'
                    , parsePrevToken :: String
    parsePrevToken    = String
    ""
                    , parseLexState :: [LexState]
    parseLexState     = [LexState]
    st
                    , parseLayout :: LayoutContext
    parseLayout       = []        -- the first block will be from the top-level layout
                    , parseLayStatus :: LayoutStatus
    parseLayStatus    = LayoutStatus
    Confirmed -- for the to-be-determined column of the top-level layout
                    , parseLayKw :: Keyword
    parseLayKw        = Keyword
    KwMutual  -- Layout keyword for the top-level layout.
                                                    -- Does not mean that the top-level block is a mutual block.
                                                    -- Just for better errors on stray @constructor@ decls.
                    , parseFlags :: ParseFlags
    parseFlags        = ParseFlags
    flags
                    , parseWarnings :: [ParseWarning]
    parseWarnings     = []
                    , parseAttributes :: Attributes
    parseAttributes   = []
                    }
      where
      pos' :: PositionWithoutFile
    pos' = Position' SrcFile
    pos { srcFile = () }

    -- | Constructs the initial state of the parser. The string argument
    --   is the input string, the file path is only there because it's part
    --   of a position.
    initState ::
      Maybe RangeFile -> ParseFlags -> String -> [LexState] -> ParseState
    initState :: Maybe RangeFile -> ParseFlags -> String -> [LexState] -> ParseState
    initState Maybe RangeFile
    file = Position' SrcFile
    -> ParseFlags -> String -> [LexState] -> ParseState
    initStatePos (Maybe RangeFile -> Position' SrcFile
    startPos Maybe RangeFile
    file)

    -- | The default flags.
    defaultParseFlags :: ParseFlags
    defaultParseFlags :: ParseFlags
    defaultParseFlags = ParseFlags { parseKeepComments :: Bool
    parseKeepComments = Bool
    False }

    -- | The most general way of parsing a string. The "Agda.Syntax.Parser" will define
    --   more specialised functions that supply the 'ParseFlags' and the
    --   'LexState'.
    parse :: ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
    parse :: forall a.
    ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
    parse ParseFlags
    flags [LexState]
    st Parser a
    p String
    input = ParseFlags
    -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
    forall a.
    ParseFlags
    -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
    parseFromSrc ParseFlags
    flags [LexState]
    st Parser a
    p SrcFile
    forall a. Maybe a
    Strict.Nothing String
    input

    -- | The even more general way of parsing a string.
    parsePosString :: Position -> ParseFlags -> [LexState] -> Parser a -> String ->
                      ParseResult a
    parsePosString :: forall a.
    Position' SrcFile
    -> ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
    parsePosString Position' SrcFile
    pos ParseFlags
    flags [LexState]
    st Parser a
    p String
    input = Parser a -> ParseState -> ParseResult a
    forall a. Parser a -> ParseState -> ParseResult a
    unP Parser a
    p (Position' SrcFile
    -> ParseFlags -> String -> [LexState] -> ParseState
    initStatePos Position' SrcFile
    pos ParseFlags
    flags String
    input [LexState]
    st)

    -- | Parses a string as if it were the contents of the given file
    --   Useful for integrating preprocessors.
    parseFromSrc :: ParseFlags -> [LexState] -> Parser a -> SrcFile -> String
                  -> ParseResult a
    parseFromSrc :: forall a.
    ParseFlags
    -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
    parseFromSrc ParseFlags
    flags [LexState]
    st Parser a
    p SrcFile
    src String
    input = Parser a -> ParseState -> ParseResult a
    forall a. Parser a -> ParseState -> ParseResult a
    unP Parser a
    p (Maybe RangeFile -> ParseFlags -> String -> [LexState] -> ParseState
    initState (SrcFile -> Maybe RangeFile
    forall lazy strict. Strict lazy strict => strict -> lazy
    Strict.toLazy SrcFile
    src) ParseFlags
    flags String
    input [LexState]
    st)

    {--------------------------------------------------------------------------
        Manipulating the state
     --------------------------------------------------------------------------}

    setParsePos :: PositionWithoutFile -> Parser ()
    setParsePos :: PositionWithoutFile -> Parser ()
    setParsePos PositionWithoutFile
    p = (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ParseState -> ParseState) -> Parser ())
    -> (ParseState -> ParseState) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ \ParseState
    s -> ParseState
    s { parsePos = p }

    setLastPos :: PositionWithoutFile -> Parser ()
    setLastPos :: PositionWithoutFile -> Parser ()
    setLastPos PositionWithoutFile
    p = (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ParseState -> ParseState) -> Parser ())
    -> (ParseState -> ParseState) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ \ParseState
    s -> ParseState
    s { parseLastPos = p }

    setPrevToken :: String -> Parser ()
    setPrevToken :: String -> Parser ()
    setPrevToken String
    t = (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ParseState -> ParseState) -> Parser ())
    -> (ParseState -> ParseState) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ \ParseState
    s -> ParseState
    s { parsePrevToken = t }

    getLastPos :: Parser PositionWithoutFile
    getLastPos :: Parser PositionWithoutFile
    getLastPos = (ParseState -> PositionWithoutFile) -> Parser PositionWithoutFile
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ParseState -> PositionWithoutFile
    parseLastPos

    -- | The parse interval is between the last position and the current position.
    getParseInterval :: Parser Interval
    getParseInterval :: Parser Interval
    getParseInterval = do
      s <- Parser ParseState
    forall s (m :: * -> *). MonadState s m => m s
    get
      return $ posToInterval (parseSrcFile s) (parseLastPos s) (parsePos s)

    getLexState :: Parser [LexState]
    getLexState :: Parser [LexState]
    getLexState = (ParseState -> [LexState]) -> Parser [LexState]
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ParseState -> [LexState]
    parseLexState

    -- UNUSED Liang-Ting Chen 2019-07-16
    --setLexState :: [LexState] -> Parser ()
    --setLexState ls = modify $ \ s -> s { parseLexState = ls }

    modifyLexState :: ([LexState] -> [LexState]) -> Parser ()
    modifyLexState :: ([LexState] -> [LexState]) -> Parser ()
    modifyLexState [LexState] -> [LexState]
    f = (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ParseState -> ParseState) -> Parser ())
    -> (ParseState -> ParseState) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ \ ParseState
    s -> ParseState
    s { parseLexState = f (parseLexState s) }

    pushLexState :: LexState -> Parser ()
    pushLexState :: LexState -> Parser ()
    pushLexState LexState
    l = ([LexState] -> [LexState]) -> Parser ()
    modifyLexState (LexState
    lLexState -> [LexState] -> [LexState]
    forall a. a -> [a] -> [a]
    :)

    popLexState :: Parser ()
    popLexState :: Parser ()
    popLexState = ([LexState] -> [LexState]) -> Parser ()
    modifyLexState (([LexState] -> [LexState]) -> Parser ())
    -> ([LexState] -> [LexState]) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ [LexState] -> [LexState] -> [LexState]
    forall a. [a] -> [a] -> [a]
    tailWithDefault [LexState]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    getParseFlags :: Parser ParseFlags
    getParseFlags :: Parser ParseFlags
    getParseFlags = (ParseState -> ParseFlags) -> Parser ParseFlags
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ParseState -> ParseFlags
    parseFlags

    -- | Fake a parse error at the specified position. Used, for instance, when
    --   lexing nested comments, which when failing will always fail at the end
    --   of the file. A more informative position is the beginning of the failing
    --   comment.
    parseErrorAt :: PositionWithoutFile -> String -> Parser a
    parseErrorAt :: forall a. PositionWithoutFile -> String -> Parser a
    parseErrorAt PositionWithoutFile
    p String
    msg =
        do  PositionWithoutFile -> Parser ()
    setLastPos PositionWithoutFile
    p
            String -> Parser a
    forall a. String -> Parser a
    parseError String
    msg

    -- | Use 'parseErrorAt' or 'parseError' as appropriate.
    parseError' :: Maybe PositionWithoutFile -> String -> Parser a
    parseError' :: forall a. Maybe PositionWithoutFile -> String -> Parser a
    parseError' = (String -> Parser a)
    -> (PositionWithoutFile -> String -> Parser a)
    -> Maybe PositionWithoutFile
    -> String
    -> Parser a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe String -> Parser a
    forall a. String -> Parser a
    parseError PositionWithoutFile -> String -> Parser a
    forall a. PositionWithoutFile -> String -> Parser a
    parseErrorAt

    -- | Report a parse error at the beginning of the given 'Range'.
    parseErrorRange :: HasRange r => r -> String -> Parser a
    parseErrorRange :: forall r a. HasRange r => r -> String -> Parser a
    parseErrorRange = Maybe PositionWithoutFile -> String -> Parser a
    forall a. Maybe PositionWithoutFile -> String -> Parser a
    parseError' (Maybe PositionWithoutFile -> String -> Parser a)
    -> (r -> Maybe PositionWithoutFile) -> r -> String -> Parser a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range' SrcFile -> Maybe PositionWithoutFile
    forall a. Range' a -> Maybe PositionWithoutFile
    rStart' (Range' SrcFile -> Maybe PositionWithoutFile)
    -> (r -> Range' SrcFile) -> r -> Maybe PositionWithoutFile
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . r -> Range' SrcFile
    forall a. HasRange a => a -> Range' SrcFile
    getRange

    -- | For lexical errors we want to report the current position as the site of
    --   the error, whereas for parse errors the previous position is the one
    --   we're interested in (since this will be the position of the token we just
    --   lexed). This function does 'parseErrorAt' the current position.
    lexError :: String -> Parser a
    lexError :: forall a. String -> Parser a
    lexError String
    msg =
        do  p <- (ParseState -> PositionWithoutFile) -> Parser PositionWithoutFile
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ParseState -> PositionWithoutFile
    parsePos
            parseErrorAt p msg

    {--------------------------------------------------------------------------
        Layout
     --------------------------------------------------------------------------}

    getContext :: MonadState ParseState m => m LayoutContext
    getContext :: forall (m :: * -> *). MonadState ParseState m => m LayoutContext
    getContext = (ParseState -> LayoutContext) -> m LayoutContext
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ParseState -> LayoutContext
    parseLayout

    setContext :: LayoutContext -> Parser ()
    setContext :: LayoutContext -> Parser ()
    setContext = (LayoutContext -> LayoutContext) -> Parser ()
    modifyContext ((LayoutContext -> LayoutContext) -> Parser ())
    -> (LayoutContext -> LayoutContext -> LayoutContext)
    -> LayoutContext
    -> Parser ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LayoutContext -> LayoutContext -> LayoutContext
    forall a b. a -> b -> a
    const

    modifyContext :: (LayoutContext -> LayoutContext) -> Parser ()
    modifyContext :: (LayoutContext -> LayoutContext) -> Parser ()
    modifyContext LayoutContext -> LayoutContext
    f = (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ParseState -> ParseState) -> Parser ())
    -> (ParseState -> ParseState) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ \ ParseState
    s -> ParseState
    s { parseLayout = f (parseLayout s) }

    -- | Return the current layout block.
    topBlock :: Parser (Maybe LayoutBlock)
    topBlock :: Parser (Maybe LayoutBlock)
    topBlock = LayoutContext -> Maybe LayoutBlock
    forall a. [a] -> Maybe a
    listToMaybe (LayoutContext -> Maybe LayoutBlock)
    -> Parser LayoutContext -> Parser (Maybe LayoutBlock)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser LayoutContext
    forall (m :: * -> *). MonadState ParseState m => m LayoutContext
    getContext

    popBlock :: Parser ()
    popBlock :: Parser ()
    popBlock =
        do  ctx <- Parser LayoutContext
    forall (m :: * -> *). MonadState ParseState m => m LayoutContext
    getContext
            case ctx of
                []      -> String -> Parser ()
    forall a. String -> Parser a
    parseError String
    "There is no layout block to close at this point."
                LayoutBlock
    _:LayoutContext
    ctx   -> LayoutContext -> Parser ()
    setContext LayoutContext
    ctx

    pushBlock :: LayoutBlock -> Parser ()
    pushBlock :: LayoutBlock -> Parser ()
    pushBlock LayoutBlock
    l = (LayoutContext -> LayoutContext) -> Parser ()
    modifyContext (LayoutBlock
    l LayoutBlock -> LayoutContext -> LayoutContext
    forall a. a -> [a] -> [a]
    :)

    -- | When we see a layout keyword, by default we expect a 'Tentative' block.
    resetLayoutStatus :: Parser ()
    resetLayoutStatus :: Parser ()
    resetLayoutStatus = (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ParseState -> ParseState) -> Parser ())
    -> (ParseState -> ParseState) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ \ ParseState
    s -> ParseState
    s { parseLayStatus = Tentative }