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

import Control.Monad.State

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

import Agda.Utils.Monad

-- | This is what the lexer manipulates.
data AlexInput = AlexInput
		    { lexPos	    :: !Position    -- ^ current position
		    , lexInput	    :: String	    -- ^ current input
		    , lexPrevChar   :: !Char	    -- ^ previously read character
		    }

-- | 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 = lexPrevChar

-- | Lex a character. No surprises.
alexGetChar :: AlexInput -> Maybe (Char, AlexInput)
alexGetChar (AlexInput { lexInput = []  }) = Nothing
alexGetChar (AlexInput { lexInput = c:s, lexPos = p }) =
    Just (c, AlexInput
		 { lexInput	= s
		 , lexPos	= movePos p c
		 , lexPrevChar	= c
		 }
	 )

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

getLexInput :: Parser AlexInput
getLexInput = getInp <$> get
    where
	getInp s = AlexInput
		    { lexPos	    = parsePos s
		    , lexInput	    = parseInp s
		    , lexPrevChar   = parsePrevChar s
		    }

setLexInput :: AlexInput -> Parser ()
setLexInput inp = modify upd
    where
	upd s = s { parsePos	    = lexPos inp
		  , parseInp	    = lexInput inp
		  , parsePrevChar   = lexPrevChar 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.
type LexAction r    = PreviousInput -> CurrentInput -> TokenLength -> Parser r

-- | 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
p1 .&&. p2 = \x y z u -> p1 x y z u && p2 x y z u

-- | Disjunction of 'LexPredicate's.
(.||.) :: LexPredicate -> LexPredicate -> LexPredicate
p1 .||. p2 = \x y z u -> p1 x y z u || p2 x y z u

-- | Negation of 'LexPredicate's.
not' :: LexPredicate -> LexPredicate
not' p = \x y z u -> not (p x y z u)