    {-| 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 { forall a.
    LookAhead a -> ReaderT ErrorFunction (StateT AlexInput Parser) a
    _unLookAhead :: ReaderT ErrorFunction
                                           (StateT AlexInput Parser) a
                  }
        deriving ((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
    <$ :: 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
    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
    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
    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
    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 }

    -- | 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 :: forall a. 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 :: forall a. 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 :: forall a. [(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' :: forall a.
    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.
    (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