module Agda.Syntax.Parser.Monad
(
Parser
, ParseResult(..)
, ParseState(..)
, ParseError(..)
, LexState
, LayoutContext(..)
, ParseFlags (..)
, initState
, defaultParseFlags
, parse
, parsePosString
, parseFile
, setParsePos, setLastPos, getParseInterval
, setPrevToken
, getParseFlags
, getLexState, pushLexState, popLexState
, topContext, popContext, pushContext
, pushCurrentContext
, parseError, parseErrorAt, parseError'
, lexError
)
where
import Control.Exception
import Data.Int
import Data.Typeable ( Typeable )
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 Agda.Utils.Pretty
newtype Parser a = P { unP :: ParseState -> ParseResult a }
data ParseState = PState
{ parsePos :: !Position
, parseLastPos :: !Position
, 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
{ errPos :: Position
, errInput :: String
, errPrevToken :: String
, errMsg :: String
}
deriving (Typeable)
instance Exception ParseError
data ParseResult a = ParseOk ParseState a
| ParseFailed ParseError
instance Monad Parser where
return x = P $ \s -> ParseOk s x
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 { errPos = parseLastPos s
, errInput = parseInp s
, errPrevToken = parsePrevToken s
, errMsg = msg
}
instance Functor Parser where
fmap = liftM
instance Applicative Parser where
pure = return
(<*>) = 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 err = vcat
[ pretty (errPos err) <> colon <+> text (errMsg err)
, text $ errPrevToken err ++ "<ERROR>"
, text $ take 30 (errInput err) ++ "..."
]
instance HasRange ParseError where
getRange err = posToRange (errPos err) (errPos err)
initStatePos :: Position -> ParseFlags -> String -> [LexState] -> ParseState
initStatePos pos flags inp st =
PState { parsePos = pos
, parseLastPos = pos
, parseInp = inp
, parsePrevChar = '\n'
, parsePrevToken = ""
, parseLexState = st
, parseLayout = [NoLayout]
, parseFlags = flags
}
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 = unP p (initState Nothing flags input st)
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 input <- liftIO $ UTF8.readTextFile $ filePath file
return $ unP p (initState (Just file) flags input st)
setParsePos :: Position -> Parser ()
setParsePos p = modify $ \s -> s { parsePos = p }
setLastPos :: Position -> Parser ()
setLastPos p = modify $ \s -> s { parseLastPos = p }
setPrevToken :: String -> Parser ()
setPrevToken t = modify $ \s -> s { parsePrevToken = t }
getLastPos :: Parser Position
getLastPos = get >>= return . parseLastPos
getParseInterval :: Parser Interval
getParseInterval =
do s <- get
return $ Interval (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 :: Position -> String -> Parser a
parseErrorAt p msg =
do setLastPos p
parseError msg
parseError' :: Maybe Position -> 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))