module Agda.Syntax.Parser.Monad
(
Parser
, ParseResult(..)
, ParseState(..)
, ParseError(..), ParseWarning(..)
, LexState
, LayoutContext(..)
, ParseFlags (..)
, initState
, defaultParseFlags
, parse
, parseFile
, parsePosString
, parseFromSrc
, setParsePos, setLastPos, getParseInterval
, setPrevToken
, getParseFlags
, getLexState, pushLexState, popLexState
, topContext, popContext, pushContext
, pushCurrentContext
, parseError, parseErrorAt, parseError'
, lexError
)
where
import Control.Exception (catch)
import Data.Int
import Data.Typeable ( Typeable )
import Data.Data (Data)
import Control.Monad.State
import Control.Applicative
import Agda.Syntax.Position
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
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 { unP :: ParseState -> ParseResult a }
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
}
deriving (Typeable)
data ParseWarning =
OverlappingTokensWarning
{ warnRange :: !(Range' SrcFile)
} deriving (Typeable, Data)
data ParseResult a = ParseOk ParseState a
| ParseFailed ParseError
instance Monad Parser where
return = pure
P m >>= f = P $ \s -> case m s of
ParseFailed e -> ParseFailed e
ParseOk s' x -> unP (f x) s'
fail msg = P $ \s -> ParseFailed $
ParseError { errSrcFile = parseSrcFile s
, errPos = parseLastPos s
, errInput = parseInp s
, errPrevToken = parsePrevToken s
, errMsg = msg
}
instance Functor Parser where
fmap = liftM
instance Applicative Parser where
pure x = P $ \s -> ParseOk s x
(<*>) = ap
instance MonadError ParseError Parser where
throwError e = P $ \_ -> ParseFailed e
P m `catchError` h = P $ \s -> case m s of
ParseFailed err -> unP (h err) s
m' -> m'
instance MonadState ParseState Parser where
get = P $ \s -> ParseOk s s
put s = P $ \_ -> ParseOk s ()
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 <+>
text "Multi-line comment spans one or more literate text blocks."
]
pretty InvalidExtensionError{errPath,errValidExts} = vcat
[ pretty errPath <> colon <+>
text "Unsupported extension."
, text "Supported extensions are:" <+> prettyList_ errValidExts
]
pretty ReadFileError{errPath,errIOError} = vcat
[ text "Cannot read file" <+> pretty errPath
, text "Error:" <+> text (show errIOError)
]
instance HasRange ParseError where
getRange ParseError{errSrcFile,errPos=p} = posToRange' errSrcFile p p
getRange OverlappingTokensError{errRange} = errRange
getRange InvalidExtensionError{errPath} = posToRange p p
where p = startPos (Just errPath)
getRange ReadFileError{errPath} = posToRange p p
where p = startPos (Just errPath)
instance Show ParseWarning where
show = prettyShow
instance Pretty ParseWarning where
pretty OverlappingTokensWarning{warnRange} = vcat
[ pretty warnRange <> colon <+>
text "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)
parseFile :: ParseFlags -> [LexState] -> Parser a -> AbsolutePath
-> IO (ParseResult a)
parseFile flags st p file =
do res <- (Right <$> (UTF8.readTextFile (filePath file))) `catch`
(return . Left . ReadFileError file)
case res of
Left error -> return$ ParseFailed error
Right input -> return$ parseFromSrc flags st p (Strict.Just file) input
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 = get >>= return . 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 =
do s <- get
put $ s { parseLexState = ls }
pushLexState :: LexState -> Parser ()
pushLexState l = do s <- getLexState
setLexState (l:s)
popLexState :: Parser ()
popLexState = do _:ls <- getLexState
setLexState ls
getParseFlags :: Parser ParseFlags
getParseFlags = parseFlags <$> get
parseError :: String -> Parser a
parseError = fail
parseErrorAt :: PositionWithoutFile -> String -> Parser a
parseErrorAt p msg =
do setLastPos p
parseError msg
parseError' :: Maybe PositionWithoutFile -> String -> Parser a
parseError' = maybe parseError parseErrorAt
lexError :: String -> Parser a
lexError msg =
do p <- parsePos <$> get
parseErrorAt p msg
getContext :: Parser [LayoutContext]
getContext = parseLayout <$> get
setContext :: [LayoutContext] -> Parser ()
setContext ctx =
do s <- get
put $ 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))