{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Syntax.Parser.Monad
(
Parser
, ParseResult(..)
, ParseState(..)
, ParseError(..), ParseWarning(..)
, LexState
, LayoutContext(..)
, ParseFlags (..)
, initState
, defaultParseFlags
, parse
, parsePosString
, parseFromSrc
, setParsePos, setLastPos, getParseInterval
, setPrevToken
, getParseFlags
, getLexState, pushLexState, popLexState
, topContext, popContext, pushContext
, pushCurrentContext
, parseWarningName
, parseError, parseErrorAt, parseError', parseErrorRange
, lexError
)
where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ((<>))
#endif
import Control.Exception (catch, displayException)
import Data.Int
import Data.Data (Data)
import qualified Data.Text.Lazy as T
import Control.Monad.State
import Control.Monad.Except
import Agda.Interaction.Options.Warnings
import Agda.Syntax.Position
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import Agda.Utils.List ( tailWithDefault )
import qualified Agda.Utils.IO.UTF8 as UTF8
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
newtype Parser a = P { runP :: StateT ParseState (Either ParseError) a }
deriving (Functor, Applicative, Monad, MonadState ParseState, MonadError ParseError)
data ParseState = PState
{ parseSrcFile :: !SrcFile
, parsePos :: !PositionWithoutFile
, parseLastPos :: !PositionWithoutFile
, parseInp :: String
, parsePrevChar :: !Char
, parsePrevToken:: String
, parseLayout :: [LayoutContext]
, parseLexState :: [LexState]
, parseFlags :: ParseFlags
}
deriving Show
type LexState = Int
data LayoutContext = NoLayout
| Layout Int32
deriving Show
data ParseFlags = ParseFlags
{ parseKeepComments :: Bool
}
deriving Show
data ParseError
= ParseError
{ errSrcFile :: !SrcFile
, errPos :: !PositionWithoutFile
, errInput :: String
, errPrevToken :: String
, errMsg :: String
}
| OverlappingTokensError
{ errRange :: !(Range' SrcFile)
}
| InvalidExtensionError
{ errPath :: !AbsolutePath
, errValidExts :: [String]
}
| ReadFileError
{ errPath :: !AbsolutePath
, errIOError :: IOError
}
data ParseWarning
= OverlappingTokensWarning
{ warnRange :: !(Range' SrcFile)
}
deriving Data
parseWarningName :: ParseWarning -> WarningName
parseWarningName = \case
OverlappingTokensWarning{} -> OverlappingTokensWarning_
data ParseResult a
= ParseOk ParseState a
| ParseFailed ParseError
deriving Show
unP :: Parser a -> ParseState -> ParseResult a
unP (P m) s = case runStateT m s of
Left err -> ParseFailed err
Right (a, s) -> ParseOk s a
parseError :: String -> Parser a
parseError msg = do
s <- get
throwError $ ParseError
{ errSrcFile = parseSrcFile s
, errPos = parseLastPos s
, errInput = parseInp s
, errPrevToken = parsePrevToken s
, errMsg = msg
}
instance Show ParseError where
show = prettyShow
instance Pretty ParseError where
pretty ParseError{errPos,errSrcFile,errMsg,errPrevToken,errInput} = vcat
[ pretty (errPos { srcFile = errSrcFile }) <> colon <+>
text errMsg
, text $ errPrevToken ++ "<ERROR>"
, text $ take 30 errInput ++ "..."
]
pretty OverlappingTokensError{errRange} = vcat
[ pretty errRange <> colon <+>
"Multi-line comment spans one or more literate text blocks."
]
pretty InvalidExtensionError{errPath,errValidExts} = vcat
[ pretty errPath <> colon <+>
"Unsupported extension."
, "Supported extensions are:" <+> prettyList_ errValidExts
]
pretty ReadFileError{errPath,errIOError} = vcat
[ "Cannot read file" <+> pretty errPath
, "Error:" <+> text (displayException errIOError)
]
instance HasRange ParseError where
getRange err = case err of
ParseError{ errSrcFile, errPos = p } -> posToRange' errSrcFile p p
OverlappingTokensError{ errRange } -> errRange
InvalidExtensionError{} -> errPathRange
ReadFileError{} -> errPathRange
where
errPathRange = posToRange p p
where p = startPos $ Just $ errPath err
instance Show ParseWarning where
show = prettyShow
instance Pretty ParseWarning where
pretty OverlappingTokensWarning{warnRange} = vcat
[ pretty warnRange <> colon <+>
"Multi-line comment spans one or more literate text blocks."
]
instance HasRange ParseWarning where
getRange OverlappingTokensWarning{warnRange} = warnRange
initStatePos :: Position -> ParseFlags -> String -> [LexState] -> ParseState
initStatePos pos flags inp st =
PState { parseSrcFile = srcFile pos
, parsePos = pos'
, parseLastPos = pos'
, parseInp = inp
, parsePrevChar = '\n'
, parsePrevToken = ""
, parseLexState = st
, parseLayout = [NoLayout]
, parseFlags = flags
}
where
pos' = pos { srcFile = () }
initState :: Maybe AbsolutePath -> ParseFlags -> String -> [LexState]
-> ParseState
initState file = initStatePos (startPos file)
defaultParseFlags :: ParseFlags
defaultParseFlags = ParseFlags { parseKeepComments = False }
parse :: ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
parse flags st p input = parseFromSrc flags st p Strict.Nothing input
parsePosString :: Position -> ParseFlags -> [LexState] -> Parser a -> String ->
ParseResult a
parsePosString pos flags st p input = unP p (initStatePos pos flags input st)
parseFromSrc :: ParseFlags -> [LexState] -> Parser a -> SrcFile -> String
-> ParseResult a
parseFromSrc flags st p src input = unP p (initState (Strict.toLazy src) flags input st)
setParsePos :: PositionWithoutFile -> Parser ()
setParsePos p = modify $ \s -> s { parsePos = p }
setLastPos :: PositionWithoutFile -> Parser ()
setLastPos p = modify $ \s -> s { parseLastPos = p }
setPrevToken :: String -> Parser ()
setPrevToken t = modify $ \s -> s { parsePrevToken = t }
getLastPos :: Parser PositionWithoutFile
getLastPos = gets parseLastPos
getParseInterval :: Parser Interval
getParseInterval = do
s <- get
return $ posToInterval (parseSrcFile s) (parseLastPos s) (parsePos s)
getLexState :: Parser [LexState]
getLexState = parseLexState <$> get
setLexState :: [LexState] -> Parser ()
setLexState ls = modify $ \ s -> s { parseLexState = ls }
modifyLexState :: ([LexState] -> [LexState]) -> Parser ()
modifyLexState f = modify $ \ s -> s { parseLexState = f (parseLexState s) }
pushLexState :: LexState -> Parser ()
pushLexState l = modifyLexState (l:)
popLexState :: Parser ()
popLexState = modifyLexState $ tailWithDefault __IMPOSSIBLE__
getParseFlags :: Parser ParseFlags
getParseFlags = gets parseFlags
parseErrorAt :: PositionWithoutFile -> String -> Parser a
parseErrorAt p msg =
do setLastPos p
parseError msg
parseError' :: Maybe PositionWithoutFile -> String -> Parser a
parseError' = maybe parseError parseErrorAt
parseErrorRange :: HasRange r => r -> String -> Parser a
parseErrorRange = parseError' . rStart' . getRange
lexError :: String -> Parser a
lexError msg =
do p <- gets parsePos
parseErrorAt p msg
getContext :: Parser [LayoutContext]
getContext = gets parseLayout
setContext :: [LayoutContext] -> Parser ()
setContext ctx = modify $ \ s -> s { parseLayout = ctx }
topContext :: Parser LayoutContext
topContext =
do ctx <- getContext
case ctx of
[] -> parseError "No layout context in scope"
l:_ -> return l
popContext :: Parser ()
popContext =
do ctx <- getContext
case ctx of
[] -> parseError "There is no layout block to close at this point."
_:ctx -> setContext ctx
pushContext :: LayoutContext -> Parser ()
pushContext l =
do ctx <- getContext
setContext (l : ctx)
pushCurrentContext :: Parser ()
pushCurrentContext =
do p <- getLastPos
pushContext (Layout (posCol p))