module Agda.Syntax.Parser.LookAhead
(
LookAhead
, runLookAhead
, lookAheadError
, getInput, setInput, liftP
, nextChar, eatNextChar
, sync, rollback
, match, match'
)
where
import Control.Monad.Reader
import Control.Monad.State
import Agda.Syntax.Parser.Alex
import Agda.Syntax.Parser.Monad
import Agda.Utils.Null (ifNull)
import Agda.Utils.Maybe (caseMaybeM, fromMaybeM)
newtype LookAhead a =
LookAhead { forall a.
LookAhead a -> ReaderT ErrorFunction (StateT AlexInput Parser) a
_unLookAhead :: ReaderT ErrorFunction
(StateT AlexInput Parser) a
}
deriving (forall a b. a -> LookAhead b -> LookAhead a
forall a b. (a -> b) -> LookAhead a -> LookAhead b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> LookAhead b -> LookAhead a
$c<$ :: forall a b. a -> LookAhead b -> LookAhead a
fmap :: forall a b. (a -> b) -> LookAhead a -> LookAhead b
$cfmap :: forall a b. (a -> b) -> LookAhead a -> LookAhead b
Functor, Functor LookAhead
forall a. a -> LookAhead a
forall a b. LookAhead a -> LookAhead b -> LookAhead a
forall a b. LookAhead a -> LookAhead b -> LookAhead b
forall a b. LookAhead (a -> b) -> LookAhead a -> LookAhead b
forall a b c.
(a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead 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
<* :: forall a b. LookAhead a -> LookAhead b -> LookAhead a
$c<* :: forall a b. LookAhead a -> LookAhead b -> LookAhead a
*> :: forall a b. LookAhead a -> LookAhead b -> LookAhead b
$c*> :: forall a b. LookAhead a -> LookAhead b -> LookAhead b
liftA2 :: forall a b c.
(a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead c
$cliftA2 :: forall a b c.
(a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead c
<*> :: forall a b. LookAhead (a -> b) -> LookAhead a -> LookAhead b
$c<*> :: forall a b. LookAhead (a -> b) -> LookAhead a -> LookAhead b
pure :: forall a. a -> LookAhead a
$cpure :: forall a. a -> LookAhead a
Applicative, Applicative LookAhead
forall a. a -> LookAhead a
forall a b. LookAhead a -> LookAhead b -> LookAhead b
forall a b. LookAhead a -> (a -> LookAhead b) -> LookAhead 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 :: forall a. a -> LookAhead a
$creturn :: forall a. a -> LookAhead a
>> :: forall a b. LookAhead a -> LookAhead b -> LookAhead b
$c>> :: forall a b. LookAhead a -> LookAhead b -> LookAhead b
>>= :: forall a b. LookAhead a -> (a -> LookAhead b) -> LookAhead b
$c>>= :: forall a b. LookAhead a -> (a -> LookAhead b) -> LookAhead b
Monad)
newtype ErrorFunction =
ErrorFun { ErrorFunction -> forall a. String -> LookAhead a
throwError :: forall a. String -> LookAhead a }
lookAheadError :: String -> LookAhead a
String
s = (forall a b. (a -> b) -> a -> b
$ String
s) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall a.
ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
LookAhead forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (\ErrorFunction
e -> ErrorFunction -> forall a. String -> LookAhead a
throwError ErrorFunction
e)
getInput :: LookAhead AlexInput
getInput :: LookAhead AlexInput
getInput = forall a.
ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
LookAhead forall s (m :: * -> *). MonadState s m => m s
get
setInput :: AlexInput -> LookAhead ()
setInput :: AlexInput -> LookAhead ()
setInput = forall a.
ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
LookAhead forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *). MonadState s m => s -> m ()
put
liftP :: Parser a -> LookAhead a
liftP :: forall a. Parser a -> LookAhead a
liftP = forall a.
ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
LookAhead forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
nextChar :: LookAhead Char
nextChar :: LookAhead Char
nextChar = forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall a. String -> LookAhead a
lookAheadError String
"unexpected end of file") LookAhead (Maybe Char)
nextCharMaybe
nextCharMaybe :: LookAhead (Maybe Char)
nextCharMaybe :: LookAhead (Maybe Char)
nextCharMaybe =
do AlexInput
inp <- LookAhead AlexInput
getInput
case AlexInput -> Maybe (Char, AlexInput)
alexGetChar AlexInput
inp of
Maybe (Char, AlexInput)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Just (Char
c,AlexInput
inp') ->
do AlexInput -> LookAhead ()
setInput AlexInput
inp'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Char
c
sync :: LookAhead ()
sync :: LookAhead ()
sync =
do AlexInput
inp <- LookAhead AlexInput
getInput
forall a. Parser a -> LookAhead a
liftP forall a b. (a -> b) -> a -> b
$ AlexInput -> Parser ()
setLexInput AlexInput
inp
rollback :: LookAhead ()
rollback :: LookAhead ()
rollback =
do AlexInput
inp <- forall a. Parser a -> LookAhead a
liftP Parser AlexInput
getLexInput
AlexInput -> LookAhead ()
setInput AlexInput
inp
eatNextChar :: LookAhead Char
eatNextChar :: LookAhead Char
eatNextChar =
do Char
c <- LookAhead Char
nextChar
LookAhead ()
sync
forall (m :: * -> *) a. Monad m => a -> m a
return Char
c
match :: [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match :: forall a. [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match [(String, LookAhead a)]
xs LookAhead a
def =
do Char
c <- LookAhead Char
nextChar
forall a.
Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match' Char
c [(String, LookAhead a)]
xs LookAhead a
def
match' :: Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match' :: forall a.
Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match' Char
c [(String, LookAhead a)]
xs LookAhead a
def = do
AlexInput
inp <- LookAhead AlexInput
getInput
let fallback :: LookAhead a
fallback = AlexInput -> LookAhead ()
setInput AlexInput
inp forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LookAhead a
def
forall {b}.
LookAhead b -> [(String, LookAhead b)] -> Char -> LookAhead b
match'' LookAhead a
fallback [(String, LookAhead a)]
xs Char
c
where
match'' :: LookAhead b -> [(String, LookAhead b)] -> Char -> LookAhead b
match'' LookAhead b
fallback [(String, LookAhead b)]
bs Char
c =
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull [ (String
s, LookAhead b
p) | (Char
c':String
s, LookAhead b
p) <- [(String, LookAhead b)]
bs, Char
c forall a. Eq a => a -> a -> Bool
== Char
c' ]
LookAhead b
fallback
forall a b. (a -> b) -> a -> b
$ \ [(String, LookAhead b)]
bs' -> do
LookAhead b
fallback' <- do
case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"" [(String, LookAhead b)]
bs' of
Maybe (LookAhead b)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure LookAhead b
fallback
Just LookAhead b
p -> do
AlexInput
inp <- LookAhead AlexInput
getInput
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ AlexInput -> LookAhead ()
setInput AlexInput
inp forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LookAhead b
p
forall b a. b -> (a -> b) -> Maybe a -> b
maybe LookAhead b
fallback' (LookAhead b -> [(String, LookAhead b)] -> Char -> LookAhead b
match'' LookAhead b
fallback' [(String, LookAhead b)]
bs') forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LookAhead (Maybe Char)
nextCharMaybe
runLookAhead :: (forall b. String -> LookAhead b) -> LookAhead a -> Parser a
runLookAhead :: forall a.
(forall a. String -> LookAhead a) -> LookAhead a -> Parser a
runLookAhead forall a. String -> LookAhead a
err (LookAhead ReaderT ErrorFunction (StateT AlexInput Parser) a
m) =
do AlexInput
inp <- Parser AlexInput
getLexInput
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT ErrorFunction (StateT AlexInput Parser) a
m ((forall a. String -> LookAhead a) -> ErrorFunction
ErrorFun forall a. String -> LookAhead a
err)) AlexInput
inp