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.Int
import Data.Maybe ( listToMaybe )

import Agda.Interaction.Options.Warnings

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

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 = Int32

-- | 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
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

-- | Warnings for parsing.
data ParseWarning
  -- | Parse errors that concern a range in a file.
  = OverlappingTokensWarning
    { ParseWarning -> Range
warnRange    :: !(Range' SrcFile)
                      -- ^ The range of the bigger overlapping token
    }
  | 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
_) = ()
  rnf (UnsupportedAttribute Range
_ Maybe String
s)   = Maybe String -> ()
forall a. NFData a => a -> ()
rnf Maybe String
s
  rnf (MultipleAttributes Range
_ 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_
  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
  ParseState
s <- Parser ParseState
forall s (m :: * -> *). MonadState s m => m s
get
  ParseError -> Parser a
forall a. ParseError -> Parser a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ParseError -> Parser a) -> ParseError -> Parser a
forall a b. (a -> b) -> a -> b
$ ParseError
    { errSrcFile :: SrcFile
errSrcFile   = ParseState -> SrcFile
parseSrcFile ParseState
s
    , errPos :: PositionWithoutFile
errPos       = ParseState -> PositionWithoutFile
parseLastPos ParseState
s
    , errInput :: String
errInput     = ParseState -> String
parseInp ParseState
s
    , errPrevToken :: String
errPrevToken = ParseState -> String
parsePrevToken ParseState
s
    , errMsg :: String
errMsg       = String
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
<+>
        String -> Doc
forall a. String -> Doc a
text String
errMsg
      , 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
errRange :: ParseError -> Range
errRange :: Range
errRange} = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ (Range -> Doc
forall a. Pretty a => a -> Doc
pretty Range
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
"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
"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
displayException IOError
errIOError)
      ]

instance HasRange ParseError where
  getRange :: ParseError -> Range
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
forall a.
a -> PositionWithoutFile -> PositionWithoutFile -> Range' a
posToRange' SrcFile
errSrcFile PositionWithoutFile
p PositionWithoutFile
p
      OverlappingTokensError{ Range
errRange :: ParseError -> Range
errRange :: Range
errRange }   -> Range
errRange
      InvalidExtensionError{}              -> Range
errPathRange
      ReadFileError{}                      -> Range
errPathRange
    where
    errPathRange :: Range
errPathRange = Position' SrcFile -> Position' SrcFile -> Range
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

instance Pretty ParseWarning where
  pretty :: ParseWarning -> Doc
pretty OverlappingTokensWarning{Range
warnRange :: ParseWarning -> Range
warnRange :: Range
warnRange} = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ (Range -> Doc
forall a. Pretty a => a -> Doc
pretty Range
warnRange Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>
        Doc
"Multi-line comment spans one or more literate text blocks."
      ]
  pretty (UnsupportedAttribute Range
r Maybe String
s) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ (Range -> Doc
forall a. Pretty a => a -> Doc
pretty Range
r Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>
      (case Maybe String
s 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 -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>
      Doc
"are not supported here."
    ]
  pretty (MultipleAttributes Range
r Maybe String
s) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ (Range -> Doc
forall a. Pretty a => a -> Doc
pretty Range
r Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>
      Doc
"Multiple" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>
      (Doc -> Doc)
-> (String -> Doc -> Doc) -> Maybe String -> Doc -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc -> Doc
forall a. a -> a
id (\String
s -> (String -> Doc
forall a. String -> Doc a
text String
s Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>)) Maybe String
s Doc
"attributes (ignored)."
    ]

instance HasRange ParseWarning where
  getRange :: ParseWarning -> Range
getRange OverlappingTokensWarning{Range
warnRange :: ParseWarning -> Range
warnRange :: Range
warnRange} = Range
warnRange
  getRange (UnsupportedAttribute Range
r Maybe String
_)          = Range
r
  getRange (MultipleAttributes Range
r Maybe String
_)            = Range
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
  ParseState
s <- Parser ParseState
forall s (m :: * -> *). MonadState s m => m s
get
  Interval -> Parser Interval
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Interval -> Parser Interval) -> Interval -> Parser Interval
forall a b. (a -> b) -> a -> b
$ SrcFile -> PositionWithoutFile -> PositionWithoutFile -> Interval
forall a.
a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
posToInterval (ParseState -> SrcFile
parseSrcFile ParseState
s) (ParseState -> PositionWithoutFile
parseLastPos ParseState
s) (ParseState -> PositionWithoutFile
parsePos ParseState
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 -> Maybe PositionWithoutFile
forall a. Range' a -> Maybe PositionWithoutFile
rStart' (Range -> Maybe PositionWithoutFile)
-> (r -> Range) -> r -> Maybe PositionWithoutFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> Range
forall a. HasRange a => a -> Range
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  PositionWithoutFile
p <- (ParseState -> PositionWithoutFile) -> Parser PositionWithoutFile
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ParseState -> PositionWithoutFile
parsePos
        PositionWithoutFile -> String -> Parser a
forall a. PositionWithoutFile -> String -> Parser a
parseErrorAt PositionWithoutFile
p String
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  LayoutContext
ctx <- Parser LayoutContext
forall (m :: * -> *). MonadState ParseState m => m LayoutContext
getContext
        case LayoutContext
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 }