    {-| This module defines the things required by Alex and some other
        Alex related things.
    -}
    module Agda.Syntax.Parser.Alex
        ( -- * Alex requirements
          AlexInput(..)
        , lensLexInput
        , alexInputPrevChar
        , alexGetChar, alexGetByte
          -- * Lex actions
        , LexAction(..), LexPredicate
        , (.&&.), (.||.), not'
        , PreviousInput, CurrentInput, TokenLength
          -- * Monad operations
        , getLexInput, setLexInput
        )
        where

    import Control.Monad.State
    import Data.Char
    import Data.Word

    import Agda.Syntax.Position
    import Agda.Syntax.Parser.Monad

    import Agda.Utils.Lens
    import Agda.Utils.Tuple

    -- | This is what the lexer manipulates.
    data AlexInput = AlexInput
      { AlexInput -> SrcFile
    lexSrcFile  :: !SrcFile              -- ^ File.
      , AlexInput -> PositionWithoutFile
    lexPos      :: !PositionWithoutFile  -- ^ Current position.
      , AlexInput -> String
    lexInput    :: String                -- ^ Current input.
      , AlexInput -> Char
    lexPrevChar :: !Char                 -- ^ Previously read character.
      }

    -- | A lens for 'lexInput'.
    lensLexInput :: Lens' String AlexInput
    lensLexInput :: Lens' String AlexInput
    lensLexInput String -> f String
    f AlexInput
    r = String -> f String
    f (AlexInput -> String
    lexInput AlexInput
    r) f String -> (String -> AlexInput) -> f AlexInput
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ String
    s -> AlexInput
    r { lexInput :: String
    lexInput = String
    s }

    -- | Get the previously lexed character. Same as 'lexPrevChar'. Alex needs this
    --   to be defined to handle \"patterns with a left-context\".
    alexInputPrevChar :: AlexInput -> Char
    alexInputPrevChar :: AlexInput -> Char
    alexInputPrevChar = AlexInput -> Char
    lexPrevChar

    -- | Returns the next character, and updates the 'AlexInput' value.
    --
    -- This function is not suitable for use by Alex 2, because it can
    -- return non-ASCII characters.
    alexGetChar :: AlexInput -> Maybe (Char, AlexInput)
    alexGetChar :: AlexInput -> Maybe (Char, AlexInput)
    alexGetChar     (AlexInput { lexInput :: AlexInput -> String
    lexInput = []              }) = Maybe (Char, AlexInput)
    forall a. Maybe a
    Nothing
    alexGetChar inp :: AlexInput
    inp@(AlexInput { lexInput :: AlexInput -> String
    lexInput = Char
    c:String
    s, lexPos :: AlexInput -> PositionWithoutFile
    lexPos = PositionWithoutFile
    p }) =
        (Char, AlexInput) -> Maybe (Char, AlexInput)
    forall a. a -> Maybe a
    Just (Char
    c, AlexInput :: SrcFile -> PositionWithoutFile -> String -> Char -> AlexInput
    AlexInput
                     { lexSrcFile :: SrcFile
    lexSrcFile   = AlexInput -> SrcFile
    lexSrcFile AlexInput
    inp
                     , lexInput :: String
    lexInput     = String
    s
                     , lexPos :: PositionWithoutFile
    lexPos       = PositionWithoutFile -> Char -> PositionWithoutFile
    forall a. Position' a -> Char -> Position' a
    movePos PositionWithoutFile
    p Char
    c
                     , lexPrevChar :: Char
    lexPrevChar  = Char
    c
                     }
             )

    -- | Returns the next byte, and updates the 'AlexInput' value.
    --
    -- A trick is used to handle the fact that there are more than 256
    -- Unicode code points. The function translates characters to bytes in
    -- the following way:
    --
    -- * Whitespace characters other than \'\\t\' and \'\\n\' are
    --   translated to \' \'.
    -- * Non-ASCII alphabetical characters are translated to \'z\'.
    -- * Other non-ASCII printable characters are translated to \'+\'.
    -- * Everything else is translated to \'\\1\'.
    --
    -- Note that it is important that there are no keywords containing
    -- \'z\', \'+\', \' \' or \'\\1\'.
    --
    -- This function is used by Alex (version 3).

    alexGetByte :: AlexInput -> Maybe (Word8, AlexInput)
    alexGetByte :: AlexInput -> Maybe (Word8, AlexInput)
    alexGetByte AlexInput
    ai =
      (Char -> Word8) -> (Char, AlexInput) -> (Word8, AlexInput)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst (Int -> Word8
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Word8) -> (Char -> Int) -> Char -> Word8
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Int
    forall a. Enum a => a -> Int
    fromEnum (Char -> Int) -> (Char -> Char) -> Char -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Char
    toASCII) ((Char, AlexInput) -> (Word8, AlexInput))
    -> Maybe (Char, AlexInput) -> Maybe (Word8, AlexInput)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> AlexInput -> Maybe (Char, AlexInput)
    alexGetChar AlexInput
    ai
      where
      toASCII :: Char -> Char
    toASCII Char
    c
        | Char -> Bool
    isSpace Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '\t' Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '\n' = Char
    ' '
        | Char -> Bool
    isAscii Char
    c                           = Char
    c
        | Char -> Bool
    isPrint Char
    c                           = if Char -> Bool
    isAlpha Char
    c then Char
    'z'
                                                             else Char
    '+'
        | Bool
    otherwise                           = Char
    '\1'

    {--------------------------------------------------------------------------
        Monad operations
     --------------------------------------------------------------------------}

    getLexInput :: Parser AlexInput
    getLexInput :: Parser AlexInput
    getLexInput = (ParseState -> AlexInput) -> Parser AlexInput
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ParseState -> AlexInput
    getInp
        where
            getInp :: ParseState -> AlexInput
    getInp ParseState
    s = AlexInput :: SrcFile -> PositionWithoutFile -> String -> Char -> AlexInput
    AlexInput
                        { lexSrcFile :: SrcFile
    lexSrcFile    = ParseState -> SrcFile
    parseSrcFile ParseState
    s
                        , lexPos :: PositionWithoutFile
    lexPos        = ParseState -> PositionWithoutFile
    parsePos ParseState
    s
                        , lexInput :: String
    lexInput      = ParseState -> String
    parseInp ParseState
    s
                        , lexPrevChar :: Char
    lexPrevChar   = ParseState -> Char
    parsePrevChar ParseState
    s
                        }

    setLexInput :: AlexInput -> Parser ()
    setLexInput :: AlexInput -> Parser ()
    setLexInput AlexInput
    inp = (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ParseState -> ParseState
    upd
        where
            upd :: ParseState -> ParseState
    upd ParseState
    s = ParseState
    s { parseSrcFile :: SrcFile
    parseSrcFile    = AlexInput -> SrcFile
    lexSrcFile AlexInput
    inp
                      , parsePos :: PositionWithoutFile
    parsePos        = AlexInput -> PositionWithoutFile
    lexPos AlexInput
    inp
                      , parseInp :: String
    parseInp        = AlexInput -> String
    lexInput AlexInput
    inp
                      , parsePrevChar :: Char
    parsePrevChar   = AlexInput -> Char
    lexPrevChar AlexInput
    inp
                      }

    {--------------------------------------------------------------------------
        Lex actions
     --------------------------------------------------------------------------}

    type PreviousInput  = AlexInput
    type CurrentInput   = AlexInput
    type TokenLength    = Int

    -- | In the lexer, regular expressions are associated with lex actions who's
    --   task it is to construct the tokens.
    newtype LexAction r
      = LexAction { forall r. LexAction r -> AlexInput -> AlexInput -> Int -> Parser r
    runLexAction :: PreviousInput -> CurrentInput -> TokenLength -> Parser r }
      deriving ((forall a b. (a -> b) -> LexAction a -> LexAction b)
    -> (forall a b. a -> LexAction b -> LexAction a)
    -> Functor LexAction
    forall a b. a -> LexAction b -> LexAction a
    forall a b. (a -> b) -> LexAction a -> LexAction 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 -> LexAction b -> LexAction a
    $c<$ :: forall a b. a -> LexAction b -> LexAction a
    fmap :: forall a b. (a -> b) -> LexAction a -> LexAction b
    $cfmap :: forall a b. (a -> b) -> LexAction a -> LexAction b
    Functor)

    instance Applicative LexAction where
      pure :: forall a. a -> LexAction a
    pure a
    r    = (AlexInput -> AlexInput -> Int -> Parser a) -> LexAction a
    forall r.
    (AlexInput -> AlexInput -> Int -> Parser r) -> LexAction r
    LexAction ((AlexInput -> AlexInput -> Int -> Parser a) -> LexAction a)
    -> (AlexInput -> AlexInput -> Int -> Parser a) -> LexAction a
    forall a b. (a -> b) -> a -> b
    $ \ AlexInput
    _ AlexInput
    _ Int
    _ -> a -> Parser a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    r
      LexAction (a -> b)
    mf <*> :: forall a b. LexAction (a -> b) -> LexAction a -> LexAction b
    <*> LexAction a
    mr = (AlexInput -> AlexInput -> Int -> Parser b) -> LexAction b
    forall r.
    (AlexInput -> AlexInput -> Int -> Parser r) -> LexAction r
    LexAction ((AlexInput -> AlexInput -> Int -> Parser b) -> LexAction b)
    -> (AlexInput -> AlexInput -> Int -> Parser b) -> LexAction b
    forall a b. (a -> b) -> a -> b
    $ \ AlexInput
    a AlexInput
    b Int
    c -> LexAction (a -> b)
    -> AlexInput -> AlexInput -> Int -> Parser (a -> b)
    forall r. LexAction r -> AlexInput -> AlexInput -> Int -> Parser r
    runLexAction LexAction (a -> b)
    mf AlexInput
    a AlexInput
    b Int
    c Parser (a -> b) -> Parser a -> Parser b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> LexAction a -> AlexInput -> AlexInput -> Int -> Parser a
    forall r. LexAction r -> AlexInput -> AlexInput -> Int -> Parser r
    runLexAction LexAction a
    mr AlexInput
    a AlexInput
    b Int
    c

    instance Monad LexAction where
      return :: forall a. a -> LexAction a
    return = a -> LexAction a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      LexAction a
    m >>= :: forall a b. LexAction a -> (a -> LexAction b) -> LexAction b
    >>= a -> LexAction b
    k  = (AlexInput -> AlexInput -> Int -> Parser b) -> LexAction b
    forall r.
    (AlexInput -> AlexInput -> Int -> Parser r) -> LexAction r
    LexAction ((AlexInput -> AlexInput -> Int -> Parser b) -> LexAction b)
    -> (AlexInput -> AlexInput -> Int -> Parser b) -> LexAction b
    forall a b. (a -> b) -> a -> b
    $ \ AlexInput
    a AlexInput
    b Int
    c -> do
        a
    r <- LexAction a -> AlexInput -> AlexInput -> Int -> Parser a
    forall r. LexAction r -> AlexInput -> AlexInput -> Int -> Parser r
    runLexAction LexAction a
    m AlexInput
    a AlexInput
    b Int
    c
        LexAction b -> AlexInput -> AlexInput -> Int -> Parser b
    forall r. LexAction r -> AlexInput -> AlexInput -> Int -> Parser r
    runLexAction (a -> LexAction b
    k a
    r) AlexInput
    a AlexInput
    b Int
    c

    instance MonadState ParseState LexAction where
      get :: LexAction ParseState
    get   = (AlexInput -> AlexInput -> Int -> Parser ParseState)
    -> LexAction ParseState
    forall r.
    (AlexInput -> AlexInput -> Int -> Parser r) -> LexAction r
    LexAction ((AlexInput -> AlexInput -> Int -> Parser ParseState)
     -> LexAction ParseState)
    -> (AlexInput -> AlexInput -> Int -> Parser ParseState)
    -> LexAction ParseState
    forall a b. (a -> b) -> a -> b
    $ \ AlexInput
    _ AlexInput
    _ Int
    _ -> Parser ParseState
    forall s (m :: * -> *). MonadState s m => m s
    get
      put :: ParseState -> LexAction ()
    put ParseState
    s = (AlexInput -> AlexInput -> Int -> Parser ()) -> LexAction ()
    forall r.
    (AlexInput -> AlexInput -> Int -> Parser r) -> LexAction r
    LexAction ((AlexInput -> AlexInput -> Int -> Parser ()) -> LexAction ())
    -> (AlexInput -> AlexInput -> Int -> Parser ()) -> LexAction ()
    forall a b. (a -> b) -> a -> b
    $ \ AlexInput
    _ AlexInput
    _ Int
    _ -> ParseState -> Parser ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put ParseState
    s

    -- | Sometimes regular expressions aren't enough. Alex provides a way to do
    --   arbitrary computations to see if the input matches. This is done with a
    --   lex predicate.
    type LexPredicate   = ([LexState], ParseFlags) -> PreviousInput -> TokenLength -> CurrentInput -> Bool

    -- | Conjunction of 'LexPredicate's.
    (.&&.) :: LexPredicate -> LexPredicate -> LexPredicate
    LexPredicate
    p1 .&&. :: LexPredicate -> LexPredicate -> LexPredicate
    .&&. LexPredicate
    p2 = \([Int], ParseFlags)
    x AlexInput
    y Int
    z AlexInput
    u -> LexPredicate
    p1 ([Int], ParseFlags)
    x AlexInput
    y Int
    z AlexInput
    u Bool -> Bool -> Bool
    && LexPredicate
    p2 ([Int], ParseFlags)
    x AlexInput
    y Int
    z AlexInput
    u

    -- | Disjunction of 'LexPredicate's.
    (.||.) :: LexPredicate -> LexPredicate -> LexPredicate
    LexPredicate
    p1 .||. :: LexPredicate -> LexPredicate -> LexPredicate
    .||. LexPredicate
    p2 = \([Int], ParseFlags)
    x AlexInput
    y Int
    z AlexInput
    u -> LexPredicate
    p1 ([Int], ParseFlags)
    x AlexInput
    y Int
    z AlexInput
    u Bool -> Bool -> Bool
    || LexPredicate
    p2 ([Int], ParseFlags)
    x AlexInput
    y Int
    z AlexInput
    u

    -- | Negation of 'LexPredicate's.
    not' :: LexPredicate -> LexPredicate
    not' :: LexPredicate -> LexPredicate
    not' LexPredicate
    p = \([Int], ParseFlags)
    x AlexInput
    y Int
    z AlexInput
    u -> Bool -> Bool
    not (LexPredicate
    p ([Int], ParseFlags)
    x AlexInput
    y Int
    z AlexInput
    u)