{-| 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 :: (String -> f String) -> AlexInput -> f 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 { LexAction r -> AlexInput -> AlexInput -> Int -> Parser r
runLexAction :: PreviousInput -> CurrentInput -> TokenLength -> Parser r }
  deriving (a -> LexAction b -> LexAction a
(a -> b) -> LexAction a -> LexAction b
(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
<$ :: a -> LexAction b -> LexAction a
$c<$ :: forall a b. a -> LexAction b -> LexAction a
fmap :: (a -> b) -> LexAction a -> LexAction b
$cfmap :: forall a b. (a -> b) -> LexAction a -> LexAction b
Functor)

instance Applicative LexAction where
  pure :: 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 <*> :: 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 :: a -> LexAction a
return = a -> LexAction a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  LexAction a
m >>= :: 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)