module BNFC.Backend.Agda.Lexer where

import BNFC.CF
import BNFC.Options.GlobalOptions
import BNFC.Prelude

import BNFC.Backend.Agda.Options
import BNFC.Backend.Agda.State
import BNFC.Backend.CommonInterface.Backend
import BNFC.Backend.Haskell.Options (TokenText (..))
import BNFC.Backend.Haskell.Utilities.Utils
import BNFC.Backend.Haskell.Layout (cf2layout)
import BNFC.Backend.Haskell.Lexer (cf2lexer)

import Control.Monad.State

import System.FilePath ( takeBaseName )

agdaLexer :: LBNF -> State AgdaBackendState Result
agdaLexer :: LBNF -> State AgdaBackendState Result
agdaLexer LBNF
lbnf = do
  AgdaBackendState
st <- StateT AgdaBackendState Identity AgdaBackendState
forall s (m :: * -> *). MonadState s m => m s
get
  let cfName :: String
cfName      = String -> String
takeBaseName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ GlobalOptions -> String
optInput (GlobalOptions -> String) -> GlobalOptions -> String
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> GlobalOptions
globalOpt AgdaBackendState
st
      inDirectory :: Bool
inDirectory = AgdaBackendOptions -> Bool
inDir (AgdaBackendOptions -> Bool) -> AgdaBackendOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
      nSpace :: Maybe String
nSpace      = AgdaBackendOptions -> Maybe String
nameSpace (AgdaBackendOptions -> Maybe String)
-> AgdaBackendOptions -> Maybe String
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
      toks :: [Token]
toks        = AgdaBackendState -> [Token]
lexerParserTokens AgdaBackendState
st
      lexerSpecification :: String
lexerSpecification = LBNF
-> String -> Bool -> Maybe String -> TokenText -> [Token] -> String
cf2lexer LBNF
lbnf String
cfName Bool
inDirectory Maybe String
nSpace TokenText
TextToken [Token]
toks
      layout :: String
layout      = LBNF -> String -> Bool -> Maybe String -> String
cf2layout LBNF
lbnf String
cfName Bool
inDirectory Maybe String
nSpace
  Result -> State AgdaBackendState Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> State AgdaBackendState Result)
-> Result -> State AgdaBackendState Result
forall a b. (a -> b) -> a -> b
$
    if LBNF -> Bool
layoutsAreUsed LBNF
lbnf
    then (Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Lex" String
"x", String
lexerSpecification)
         (String, String) -> Result -> Result
forall a. a -> [a] -> [a]
:
         [(Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Layout" String
"hs", String
layout)]
    else [(Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Lex" String
"x", String
lexerSpecification)]