{-| When lexing by hand (for instance string literals) we need to do some
    looking ahead. The 'LookAhead' monad keeps track of the position we are
    currently looking at, and provides facilities to synchronise the look-ahead
    position with the actual position of the 'Parser' monad (see 'sync' and
    'rollback').
-}
module Agda.Syntax.Parser.LookAhead
    ( -- * The LookAhead monad
      LookAhead
    , runLookAhead
      -- * Operations
    , 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)

{--------------------------------------------------------------------------
    The look-ahead monad
 --------------------------------------------------------------------------}

{-| The LookAhead monad is basically a state monad keeping with an extra
    'AlexInput', wrapped around the 'Parser' monad.
-}
newtype LookAhead a =
    LookAhead { LookAhead a -> ReaderT ErrorFunction (StateT AlexInput Parser) a
_unLookAhead :: ReaderT ErrorFunction
                                       (StateT AlexInput Parser) a
              }
    deriving (a -> LookAhead b -> LookAhead a
(a -> b) -> LookAhead a -> LookAhead b
(forall a b. (a -> b) -> LookAhead a -> LookAhead b)
-> (forall a b. a -> LookAhead b -> LookAhead a)
-> Functor LookAhead
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
<$ :: a -> LookAhead b -> LookAhead a
$c<$ :: forall a b. a -> LookAhead b -> LookAhead a
fmap :: (a -> b) -> LookAhead a -> LookAhead b
$cfmap :: forall a b. (a -> b) -> LookAhead a -> LookAhead b
Functor, Functor LookAhead
a -> LookAhead a
Functor LookAhead
-> (forall a. a -> LookAhead a)
-> (forall a b. LookAhead (a -> b) -> LookAhead a -> LookAhead b)
-> (forall a b c.
    (a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead c)
-> (forall a b. LookAhead a -> LookAhead b -> LookAhead b)
-> (forall a b. LookAhead a -> LookAhead b -> LookAhead a)
-> Applicative LookAhead
LookAhead a -> LookAhead b -> LookAhead b
LookAhead a -> LookAhead b -> LookAhead a
LookAhead (a -> b) -> LookAhead a -> LookAhead b
(a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead c
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
<* :: LookAhead a -> LookAhead b -> LookAhead a
$c<* :: forall a b. LookAhead a -> LookAhead b -> LookAhead a
*> :: LookAhead a -> LookAhead b -> LookAhead b
$c*> :: forall a b. LookAhead a -> LookAhead b -> LookAhead b
liftA2 :: (a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead c
$cliftA2 :: forall a b c.
(a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead c
<*> :: LookAhead (a -> b) -> LookAhead a -> LookAhead b
$c<*> :: forall a b. LookAhead (a -> b) -> LookAhead a -> LookAhead b
pure :: a -> LookAhead a
$cpure :: forall a. a -> LookAhead a
$cp1Applicative :: Functor LookAhead
Applicative, Applicative LookAhead
a -> LookAhead a
Applicative LookAhead
-> (forall a b. LookAhead a -> (a -> LookAhead b) -> LookAhead b)
-> (forall a b. LookAhead a -> LookAhead b -> LookAhead b)
-> (forall a. a -> LookAhead a)
-> Monad LookAhead
LookAhead a -> (a -> LookAhead b) -> LookAhead b
LookAhead a -> LookAhead b -> LookAhead b
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 :: a -> LookAhead a
$creturn :: forall a. a -> LookAhead a
>> :: LookAhead a -> LookAhead b -> LookAhead b
$c>> :: forall a b. LookAhead a -> LookAhead b -> LookAhead b
>>= :: LookAhead a -> (a -> LookAhead b) -> LookAhead b
$c>>= :: forall a b. LookAhead a -> (a -> LookAhead b) -> LookAhead b
$cp1Monad :: Applicative LookAhead
Monad)

newtype ErrorFunction =
    ErrorFun { ErrorFunction -> forall a. String -> LookAhead a
throwError :: forall a. String -> LookAhead a }

-- | Throw an error message according to the supplied method.
lookAheadError :: String -> LookAhead a
-- ASR (2021-02-07). The eta-expansion @\e -> throwError e@ is
-- required GHC >= 9.0.1 ((see Issue #4955).
lookAheadError :: String -> LookAhead a
lookAheadError String
s = ((String -> LookAhead a) -> String -> LookAhead a
forall a b. (a -> b) -> a -> b
$ String
s) ((String -> LookAhead a) -> LookAhead a)
-> LookAhead (String -> LookAhead a) -> LookAhead a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do ReaderT
  ErrorFunction (StateT AlexInput Parser) (String -> LookAhead a)
-> LookAhead (String -> LookAhead a)
forall a.
ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
LookAhead (ReaderT
   ErrorFunction (StateT AlexInput Parser) (String -> LookAhead a)
 -> LookAhead (String -> LookAhead a))
-> ReaderT
     ErrorFunction (StateT AlexInput Parser) (String -> LookAhead a)
-> LookAhead (String -> LookAhead a)
forall a b. (a -> b) -> a -> b
$ (ErrorFunction -> String -> LookAhead a)
-> ReaderT
     ErrorFunction (StateT AlexInput Parser) (String -> LookAhead a)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (\ErrorFunction
e -> ErrorFunction -> forall a. String -> LookAhead a
throwError ErrorFunction
e)

{--------------------------------------------------------------------------
    Operations
 --------------------------------------------------------------------------}

-- | Get the current look-ahead position.
getInput :: LookAhead AlexInput
getInput :: LookAhead AlexInput
getInput = ReaderT ErrorFunction (StateT AlexInput Parser) AlexInput
-> LookAhead AlexInput
forall a.
ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
LookAhead ReaderT ErrorFunction (StateT AlexInput Parser) AlexInput
forall s (m :: * -> *). MonadState s m => m s
get


-- | Set the look-ahead position.
setInput :: AlexInput -> LookAhead ()
setInput :: AlexInput -> LookAhead ()
setInput = ReaderT ErrorFunction (StateT AlexInput Parser) () -> LookAhead ()
forall a.
ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
LookAhead (ReaderT ErrorFunction (StateT AlexInput Parser) ()
 -> LookAhead ())
-> (AlexInput
    -> ReaderT ErrorFunction (StateT AlexInput Parser) ())
-> AlexInput
-> LookAhead ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlexInput -> ReaderT ErrorFunction (StateT AlexInput Parser) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put


-- | Lift a computation in the 'Parser' monad to the 'LookAhead' monad.
liftP :: Parser a -> LookAhead a
liftP :: Parser a -> LookAhead a
liftP = ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
forall a.
ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a
LookAhead (ReaderT ErrorFunction (StateT AlexInput Parser) a -> LookAhead a)
-> (Parser a -> ReaderT ErrorFunction (StateT AlexInput Parser) a)
-> Parser a
-> LookAhead a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT AlexInput Parser a
-> ReaderT ErrorFunction (StateT AlexInput Parser) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT AlexInput Parser a
 -> ReaderT ErrorFunction (StateT AlexInput Parser) a)
-> (Parser a -> StateT AlexInput Parser a)
-> Parser a
-> ReaderT ErrorFunction (StateT AlexInput Parser) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser a -> StateT AlexInput Parser a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift


-- | Look at the next character. Fails if there are no more characters.
nextChar :: LookAhead Char
nextChar :: LookAhead Char
nextChar = LookAhead Char -> LookAhead (Maybe Char) -> LookAhead Char
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (String -> LookAhead Char
forall a. String -> LookAhead a
lookAheadError String
"unexpected end of file") LookAhead (Maybe Char)
nextCharMaybe

-- | Look at the next character. Return 'Nothing' if there are no more characters.
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         -> Maybe Char -> LookAhead (Maybe Char)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Char
forall a. Maybe a
Nothing
            Just (Char
c,AlexInput
inp')   ->
                do  AlexInput -> LookAhead ()
setInput AlexInput
inp'
                    Maybe Char -> LookAhead (Maybe Char)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Char -> LookAhead (Maybe Char))
-> Maybe Char -> LookAhead (Maybe Char)
forall a b. (a -> b) -> a -> b
$ Char -> Maybe Char
forall a. a -> Maybe a
Just Char
c


-- | Consume all the characters up to the current look-ahead position.
sync :: LookAhead ()
sync :: LookAhead ()
sync =
    do  AlexInput
inp <- LookAhead AlexInput
getInput
        Parser () -> LookAhead ()
forall a. Parser a -> LookAhead a
liftP (Parser () -> LookAhead ()) -> Parser () -> LookAhead ()
forall a b. (a -> b) -> a -> b
$ AlexInput -> Parser ()
setLexInput AlexInput
inp


-- | Undo look-ahead. Restores the input from the 'ParseState'.
rollback :: LookAhead ()
rollback :: LookAhead ()
rollback =
    do  AlexInput
inp <- Parser AlexInput -> LookAhead AlexInput
forall a. Parser a -> LookAhead a
liftP Parser AlexInput
getLexInput
        AlexInput -> LookAhead ()
setInput AlexInput
inp


-- | Consume the next character. Does 'nextChar' followed by 'sync'.
eatNextChar :: LookAhead Char
eatNextChar :: LookAhead Char
eatNextChar =
    do  Char
c <- LookAhead Char
nextChar
        LookAhead ()
sync
        Char -> LookAhead Char
forall (m :: * -> *) a. Monad m => a -> m a
return Char
c


{-| Do a case on the current input string. If any of the given strings match we
    move past it and execute the corresponding action. If no string matches, we
    execute a default action, advancing the input one character. This function
    only affects the look-ahead position.
-}
match :: [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match :: [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match [(String, LookAhead a)]
xs LookAhead a
def =
    do  Char
c <- LookAhead Char
nextChar
        Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a
forall a.
Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match' Char
c [(String, LookAhead a)]
xs LookAhead a
def

{-| Same as 'match' but takes the initial character from the first argument
    instead of reading it from the input.  Consequently, in the default case
    the input is not advanced.
-}
match' :: Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match' :: Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match' Char
c [(String, LookAhead a)]
xs LookAhead a
def = do

  -- Set the error continuation to the default @def@, but make sure we reset
  -- the input to where we started speculative matching.
  AlexInput
inp <- LookAhead AlexInput
getInput
  let fallback :: LookAhead a
fallback = AlexInput -> LookAhead ()
setInput AlexInput
inp LookAhead () -> LookAhead a -> LookAhead a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LookAhead a
def

  -- Find the longest match from the table.
  LookAhead a -> [(String, LookAhead a)] -> Char -> LookAhead a
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 =

    -- Match the first character, dropping entries that do not match.
    [(String, LookAhead b)]
-> LookAhead b
-> ([(String, LookAhead b)] -> LookAhead b)
-> LookAhead b
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 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c' ]

      -- If no alternatives are left, fall back to the failure continuation.
      {-then-} LookAhead b
fallback

      -- Otherwise:
      {-else-} (([(String, LookAhead b)] -> LookAhead b) -> LookAhead b)
-> ([(String, LookAhead b)] -> LookAhead b) -> LookAhead b
forall a b. (a -> b) -> a -> b
$ \ [(String, LookAhead b)]
bs' -> do

        -- If we have a successful match, store it in the failure continuation.
        LookAhead b
fallback' <- do
          case String -> [(String, LookAhead b)] -> Maybe (LookAhead b)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"" [(String, LookAhead b)]
bs' of

            -- No match yet.
            Maybe (LookAhead b)
Nothing -> LookAhead b -> LookAhead (LookAhead b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure LookAhead b
fallback

            -- Match found!  Remember it, and the state of the input where we found it.
            Just LookAhead b
p  -> do
              AlexInput
inp <- LookAhead AlexInput
getInput
              LookAhead b -> LookAhead (LookAhead b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LookAhead b -> LookAhead (LookAhead b))
-> LookAhead b -> LookAhead (LookAhead b)
forall a b. (a -> b) -> a -> b
$ AlexInput -> LookAhead ()
setInput AlexInput
inp LookAhead () -> LookAhead b -> LookAhead b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LookAhead b
p

        -- Keep trying to find a (longer) match.
        LookAhead b -> (Char -> LookAhead b) -> Maybe Char -> LookAhead b
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') (Maybe Char -> LookAhead b)
-> LookAhead (Maybe Char) -> LookAhead b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LookAhead (Maybe Char)
nextCharMaybe

-- | Run a 'LookAhead' computation. The first argument is the error function.
runLookAhead :: (forall b. String -> LookAhead b) -> LookAhead a -> Parser a
runLookAhead :: (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
        StateT AlexInput Parser a -> AlexInput -> Parser a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (ReaderT ErrorFunction (StateT AlexInput Parser) a
-> ErrorFunction -> StateT AlexInput Parser a
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