{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Agda.Syntax.Parser.Monad
    ( -- * The parser monad
      Parser
    , ParseResult(..)
    , ParseState(..)
    , ParseError(..), ParseWarning(..)
    , LexState
    , LayoutContext(..)
    , ParseFlags (..)
      -- * Running the parser
    , initState
    , defaultParseFlags
    , parse
    , parsePosString
    , parseFromSrc
      -- * Manipulating the state
    , setParsePos, setLastPos, getParseInterval
    , setPrevToken
    , getParseFlags
    , getLexState, pushLexState, popLexState
      -- ** Layout
    , topContext, popContext, pushContext
    , pushCurrentContext
      -- ** Errors
    , parseWarningName
    , parseError, parseErrorAt, parseError', parseErrorRange
    , lexError
    )
    where

import Control.Exception (displayException)
import Data.Int

import Data.Data (Data)

import Control.Monad.State

import Agda.Interaction.Options.Warnings

import Agda.Syntax.Position

import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.FileName
import Agda.Utils.List ( tailWithDefault )
import qualified Agda.Utils.Maybe.Strict as Strict

import Agda.Utils.Pretty

import Agda.Utils.Impossible

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

-- | The parse monad.
newtype Parser a = P { Parser a -> StateT ParseState (Either ParseError) a
_runP :: StateT ParseState (Either ParseError) a }
  deriving (a -> Parser b -> Parser a
(a -> b) -> Parser a -> Parser b
(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
<$ :: a -> Parser b -> Parser a
$c<$ :: forall a b. a -> Parser b -> Parser a
fmap :: (a -> b) -> Parser a -> Parser b
$cfmap :: forall a b. (a -> b) -> Parser a -> Parser b
Functor, Functor Parser
a -> Parser a
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
Parser a -> Parser b -> Parser b
Parser a -> Parser b -> Parser a
Parser (a -> b) -> Parser a -> Parser b
(a -> b -> c) -> Parser a -> Parser b -> Parser c
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
<* :: Parser a -> Parser b -> Parser a
$c<* :: forall a b. Parser a -> Parser b -> Parser a
*> :: Parser a -> Parser b -> Parser b
$c*> :: forall a b. Parser a -> Parser b -> Parser b
liftA2 :: (a -> b -> c) -> Parser a -> Parser b -> Parser c
$cliftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
<*> :: Parser (a -> b) -> Parser a -> Parser b
$c<*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
pure :: a -> Parser a
$cpure :: forall a. a -> Parser a
$cp1Applicative :: Functor Parser
Applicative, Applicative Parser
a -> Parser a
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
Parser a -> (a -> Parser b) -> Parser b
Parser a -> Parser b -> Parser b
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
return :: a -> Parser a
$creturn :: forall a. a -> Parser a
>> :: Parser a -> Parser b -> Parser b
$c>> :: forall a b. Parser a -> Parser b -> Parser b
>>= :: Parser a -> (a -> Parser b) -> Parser b
$c>>= :: forall a b. Parser a -> (a -> Parser b) -> Parser b
$cp1Monad :: Applicative Parser
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 contexts
    , 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
    }
    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
showList :: [ParseState] -> ShowS
$cshowList :: [ParseState] -> ShowS
show :: ParseState -> String
$cshow :: ParseState -> String
showsPrec :: LexState -> ParseState -> ShowS
$cshowsPrec :: LexState -> 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

-- | We need to keep track of the context to do layout. The context
--   specifies the indentation (if any) of a layout block. See
--   "Agda.Syntax.Parser.Layout" for more informaton.
data LayoutContext  = NoLayout        -- ^ no layout
                    | Layout Int32    -- ^ layout at specified column
    deriving LexState -> LayoutContext -> ShowS
[LayoutContext] -> ShowS
LayoutContext -> String
(LexState -> LayoutContext -> ShowS)
-> (LayoutContext -> String)
-> ([LayoutContext] -> ShowS)
-> Show LayoutContext
forall a.
(LexState -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LayoutContext] -> ShowS
$cshowList :: [LayoutContext] -> ShowS
show :: LayoutContext -> String
$cshow :: LayoutContext -> String
showsPrec :: LexState -> LayoutContext -> ShowS
$cshowsPrec :: LexState -> LayoutContext -> 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
showList :: [ParseFlags] -> ShowS
$cshowList :: [ParseFlags] -> ShowS
show :: ParseFlags -> String
$cshow :: ParseFlags -> String
showsPrec :: LexState -> ParseFlags -> ShowS
$cshowsPrec :: LexState -> 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 -> AbsolutePath
errPath      :: !AbsolutePath
                      -- ^ The file which the error concerns.
    , ParseError -> [String]
errValidExts :: [String]
    }
  | ReadFileError
    { errPath      :: !AbsolutePath
    , ParseError -> IOError
errIOError   :: IOError
    }

-- | 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
    }
  deriving Typeable ParseWarning
DataType
Constr
Typeable ParseWarning
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ParseWarning -> c ParseWarning)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ParseWarning)
-> (ParseWarning -> Constr)
-> (ParseWarning -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ParseWarning))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ParseWarning))
-> ((forall b. Data b => b -> b) -> ParseWarning -> ParseWarning)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r)
-> (forall u. (forall d. Data d => d -> u) -> ParseWarning -> [u])
-> (forall u.
    LexState -> (forall d. Data d => d -> u) -> ParseWarning -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning)
-> Data ParseWarning
ParseWarning -> DataType
ParseWarning -> Constr
(forall b. Data b => b -> b) -> ParseWarning -> ParseWarning
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ParseWarning -> c ParseWarning
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ParseWarning
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. LexState -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
LexState -> (forall d. Data d => d -> u) -> ParseWarning -> u
forall u. (forall d. Data d => d -> u) -> ParseWarning -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ParseWarning -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ParseWarning -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ParseWarning
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ParseWarning -> c ParseWarning
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ParseWarning)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ParseWarning)
$cOverlappingTokensWarning :: Constr
$tParseWarning :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning
gmapMp :: (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning
gmapM :: (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning
gmapQi :: LexState -> (forall d. Data d => d -> u) -> ParseWarning -> u
$cgmapQi :: forall u.
LexState -> (forall d. Data d => d -> u) -> ParseWarning -> u
gmapQ :: (forall d. Data d => d -> u) -> ParseWarning -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ParseWarning -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ParseWarning -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ParseWarning -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ParseWarning -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ParseWarning -> r
gmapT :: (forall b. Data b => b -> b) -> ParseWarning -> ParseWarning
$cgmapT :: (forall b. Data b => b -> b) -> ParseWarning -> ParseWarning
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ParseWarning)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ParseWarning)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ParseWarning)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ParseWarning)
dataTypeOf :: ParseWarning -> DataType
$cdataTypeOf :: ParseWarning -> DataType
toConstr :: ParseWarning -> Constr
$ctoConstr :: ParseWarning -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ParseWarning
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ParseWarning
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ParseWarning -> c ParseWarning
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ParseWarning -> c ParseWarning
$cp1Data :: Typeable ParseWarning
Data

parseWarningName :: ParseWarning -> WarningName
parseWarningName :: ParseWarning -> WarningName
parseWarningName = \case
  OverlappingTokensWarning{} -> WarningName
OverlappingTokensWarning_

-- | 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
showList :: [ParseResult a] -> ShowS
$cshowList :: forall a. Show a => [ParseResult a] -> ShowS
show :: ParseResult a -> String
$cshow :: forall a. Show a => ParseResult a -> String
showsPrec :: LexState -> ParseResult a -> ShowS
$cshowsPrec :: forall a. Show a => LexState -> ParseResult a -> ShowS
Show

-- | Old interface to parser.
unP :: Parser a -> ParseState -> ParseResult a
unP :: 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 :: String -> Parser a
parseError String
msg = do
  ParseState
s <- Parser ParseState
forall s (m :: * -> *). MonadState s m => m s
get
  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 :: SrcFile
-> PositionWithoutFile -> String -> String -> String -> ParseError
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
    }

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

instance Show ParseError where
  show :: ParseError -> String
show = ParseError -> String
forall a. Pretty a => a -> String
prettyShow

instance Pretty ParseError where
  pretty :: ParseError -> Doc
pretty ParseError{PositionWithoutFile
errPos :: PositionWithoutFile
errPos :: ParseError -> PositionWithoutFile
errPos,SrcFile
errSrcFile :: SrcFile
errSrcFile :: ParseError -> SrcFile
errSrcFile,String
errMsg :: String
errMsg :: ParseError -> String
errMsg,String
errPrevToken :: String
errPrevToken :: ParseError -> String
errPrevToken,String
errInput :: String
errInput :: ParseError -> String
errInput} = [Doc] -> Doc
vcat
      [ (Position' SrcFile -> Doc
forall a. Pretty a => a -> Doc
pretty (PositionWithoutFile
errPos { srcFile :: SrcFile
srcFile = SrcFile
errSrcFile }) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon) Doc -> Doc -> Doc
<+>
        String -> Doc
text String
errMsg
      , String -> Doc
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
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 :: Range' SrcFile
errRange :: ParseError -> Range' SrcFile
errRange} = [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
<+>
        Doc
"Multi-line comment spans one or more literate text blocks."
      ]
  pretty InvalidExtensionError{AbsolutePath
errPath :: AbsolutePath
errPath :: ParseError -> AbsolutePath
errPath,[String]
errValidExts :: [String]
errValidExts :: ParseError -> [String]
errValidExts} = [Doc] -> Doc
vcat
      [ (AbsolutePath -> Doc
forall a. Pretty a => a -> Doc
pretty AbsolutePath
errPath Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon) Doc -> Doc -> Doc
<+>
        Doc
"Unsupported extension."
      , Doc
"Supported extensions are:" Doc -> Doc -> Doc
<+> [String] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList_ [String]
errValidExts
      ]
  pretty ReadFileError{AbsolutePath
errPath :: AbsolutePath
errPath :: ParseError -> AbsolutePath
errPath,IOError
errIOError :: IOError
errIOError :: ParseError -> IOError
errIOError} = [Doc] -> Doc
vcat
      [ Doc
"Cannot read file" Doc -> Doc -> Doc
<+> AbsolutePath -> Doc
forall a. Pretty a => a -> Doc
pretty AbsolutePath
errPath
      , Doc
"Error:" Doc -> Doc -> Doc
<+> String -> Doc
text (IOError -> String
forall e. Exception e => e -> String
displayException IOError
errIOError)
      ]

instance HasRange ParseError where
  getRange :: ParseError -> Range' SrcFile
getRange ParseError
err = case ParseError
err of
      ParseError{ SrcFile
errSrcFile :: SrcFile
errSrcFile :: ParseError -> 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 :: Range' SrcFile
errRange :: ParseError -> 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 AbsolutePath -> Position' SrcFile
startPos (Maybe AbsolutePath -> Position' SrcFile)
-> Maybe AbsolutePath -> Position' SrcFile
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just (AbsolutePath -> Maybe AbsolutePath)
-> AbsolutePath -> Maybe AbsolutePath
forall a b. (a -> b) -> a -> b
$ ParseError -> AbsolutePath
errPath ParseError
err

instance Show ParseWarning where
  show :: ParseWarning -> String
show = ParseWarning -> String
forall a. Pretty a => a -> String
prettyShow

instance Pretty ParseWarning where
  pretty :: ParseWarning -> Doc
pretty OverlappingTokensWarning{Range' SrcFile
warnRange :: Range' SrcFile
warnRange :: ParseWarning -> Range' SrcFile
warnRange} = [Doc] -> Doc
vcat
      [ (Range' SrcFile -> Doc
forall a. Pretty a => a -> Doc
pretty Range' SrcFile
warnRange Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon) Doc -> Doc -> Doc
<+>
        Doc
"Multi-line comment spans one or more literate text blocks."
      ]
instance HasRange ParseWarning where
  getRange :: ParseWarning -> Range' SrcFile
getRange OverlappingTokensWarning{Range' SrcFile
warnRange :: Range' SrcFile
warnRange :: ParseWarning -> Range' SrcFile
warnRange} = Range' SrcFile
warnRange

{--------------------------------------------------------------------------
    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 :: SrcFile
-> PositionWithoutFile
-> PositionWithoutFile
-> String
-> Char
-> String
-> [LayoutContext]
-> [LexState]
-> ParseFlags
-> ParseState
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       = [LayoutContext
NoLayout]
                , parseFlags :: ParseFlags
parseFlags        = ParseFlags
flags
                }
  where
  pos' :: PositionWithoutFile
pos' = Position' SrcFile
pos { srcFile :: ()
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 AbsolutePath -> ParseFlags -> String -> [LexState]
          -> ParseState
initState :: Maybe AbsolutePath
-> ParseFlags -> String -> [LexState] -> ParseState
initState Maybe AbsolutePath
file = Position' SrcFile
-> ParseFlags -> String -> [LexState] -> ParseState
initStatePos (Maybe AbsolutePath -> Position' SrcFile
startPos Maybe AbsolutePath
file)

-- | The default flags.
defaultParseFlags :: ParseFlags
defaultParseFlags :: ParseFlags
defaultParseFlags = ParseFlags :: Bool -> ParseFlags
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 :: 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 :: 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 :: 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 AbsolutePath
-> ParseFlags -> String -> [LexState] -> ParseState
initState (SrcFile -> Maybe AbsolutePath
forall a. Maybe a -> Maybe a
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 :: PositionWithoutFile
parsePos = PositionWithoutFile
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 :: PositionWithoutFile
parseLastPos = PositionWithoutFile
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 :: String
parsePrevToken = String
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 (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]
parseLexState (ParseState -> [LexState])
-> Parser ParseState -> Parser [LexState]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser ParseState
forall s (m :: * -> *). MonadState s m => m s
get

-- 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 :: [LexState]
parseLexState = [LexState] -> [LexState]
f (ParseState -> [LexState]
parseLexState ParseState
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 :: 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' :: 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 :: 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 t. HasRange t => t -> 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 :: 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 :: Parser [LayoutContext]
getContext :: Parser [LayoutContext]
getContext = (ParseState -> [LayoutContext]) -> Parser [LayoutContext]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ParseState -> [LayoutContext]
parseLayout

setContext :: [LayoutContext] -> Parser ()
setContext :: [LayoutContext] -> Parser ()
setContext [LayoutContext]
ctx = (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 :: [LayoutContext]
parseLayout = [LayoutContext]
ctx }

-- | Return the current layout context.
topContext :: Parser LayoutContext
topContext :: Parser LayoutContext
topContext =
    do  [LayoutContext]
ctx <- Parser [LayoutContext]
getContext
        case [LayoutContext]
ctx of
            []  -> String -> Parser LayoutContext
forall a. String -> Parser a
parseError String
"No layout context in scope"
            LayoutContext
l:[LayoutContext]
_ -> LayoutContext -> Parser LayoutContext
forall (m :: * -> *) a. Monad m => a -> m a
return LayoutContext
l

popContext :: Parser ()
popContext :: Parser ()
popContext =
    do  [LayoutContext]
ctx <- Parser [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."
            LayoutContext
_:[LayoutContext]
ctx   -> [LayoutContext] -> Parser ()
setContext [LayoutContext]
ctx

pushContext :: LayoutContext -> Parser ()
pushContext :: LayoutContext -> Parser ()
pushContext LayoutContext
l =
    do  [LayoutContext]
ctx <- Parser [LayoutContext]
getContext
        [LayoutContext] -> Parser ()
setContext (LayoutContext
l LayoutContext -> [LayoutContext] -> [LayoutContext]
forall a. a -> [a] -> [a]
: [LayoutContext]
ctx)

-- | Should only be used at the beginning of a file. When we start parsing
--   we should be in layout mode. Instead of forcing zero indentation we use
--   the indentation of the first token.
pushCurrentContext :: Parser ()
pushCurrentContext :: Parser ()
pushCurrentContext =
    do  PositionWithoutFile
p <- Parser PositionWithoutFile
getLastPos
        LayoutContext -> Parser ()
pushContext (Int32 -> LayoutContext
Layout (PositionWithoutFile -> Int32
forall a. Position' a -> Int32
posCol PositionWithoutFile
p))