module BNFC.Backend.Agda.Template 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.Template (cf2template)
import BNFC.Backend.Haskell.Utilities.Utils

import Control.Monad.State

import qualified Data.Map as Map

import System.FilePath ( takeBaseName )

agdaTemplate :: LBNF -> State AgdaBackendState Result
agdaTemplate :: LBNF -> State AgdaBackendState Result
agdaTemplate 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
    rules :: [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules       = [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
filterRules ([(Type, [(Label, ([Type], (Integer, ARHS)))])]
 -> [(Type, [(Label, ([Type], (Integer, ARHS)))])])
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsAstRules AgdaBackendState
st
    tokensNames :: [CatName]
tokensNames = (CatName, TokenDef) -> CatName
forall a b. (a, b) -> a
fst ((CatName, TokenDef) -> CatName)
-> [(CatName, TokenDef)] -> [CatName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AgdaBackendState -> [(CatName, TokenDef)]
tokens 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
    funct :: Bool
funct       = AgdaBackendOptions -> Bool
functor (AgdaBackendOptions -> Bool) -> AgdaBackendOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
    template :: String
template    = [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [CatName] -> String -> Bool -> Maybe String -> Bool -> String
cf2template [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules [CatName]
tokensNames String
cfName Bool
inDirectory Maybe String
nSpace Bool
funct
  Result -> State AgdaBackendState Result
forall (m :: * -> *) a. Monad m => a -> m a
return [(Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Skel" String
"hs", String
template)]

  where

      filterRules :: [(Type, [(Label, ([Type], (Integer, ARHS)))])]
                  -> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
      filterRules :: [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
filterRules [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules =
        ((Type, [(Label, ([Type], (Integer, ARHS)))]) -> Bool)
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
forall a. (a -> Bool) -> [a] -> [a]
filter
        (\(Type
_,[(Label, ([Type], (Integer, ARHS)))]
l) -> Bool -> Bool
not ([(Label, ([Type], (Integer, ARHS)))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Label, ([Type], (Integer, ARHS)))]
l))
        ((\(Type
f,[(Label, ([Type], (Integer, ARHS)))]
s) -> (Type
f, [String]
-> [(Label, ([Type], (Integer, ARHS)))]
-> [(Label, ([Type], (Integer, ARHS)))]
filterLabelsAST [String]
fNames [(Label, ([Type], (Integer, ARHS)))]
s)) ((Type, [(Label, ([Type], (Integer, ARHS)))])
 -> (Type, [(Label, ([Type], (Integer, ARHS)))]))
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules)

      -- Functions names.
      fNames :: [String]
      fNames :: [String]
fNames = CatName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (CatName -> String) -> [CatName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map CatName (WithPosition Function) -> [CatName]
forall k a. Map k a -> [k]
Map.keys (LBNF -> Map CatName (WithPosition Function)
_lbnfFunctions LBNF
lbnf)