module BNFC.Backend.Agda.Printer 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.Utilities.Utils
import BNFC.Backend.Haskell.Options (TokenText (..))
import BNFC.Backend.Haskell.Printer (cf2printer)

import Control.Monad.State

import           Data.Bifunctor
import qualified Data.Map as Map

import System.FilePath ( takeBaseName )

agdaPrinter :: LBNF -> State AgdaBackendState Result
agdaPrinter :: LBNF -> State AgdaBackendState Result
agdaPrinter 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
      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
      tks :: [(CatName, TokenDef)]
tks           = AgdaBackendState -> [(CatName, TokenDef)]
tokens AgdaBackendState
st
      funct :: Bool
funct         = AgdaBackendOptions -> Bool
functor (AgdaBackendOptions -> Bool) -> AgdaBackendOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
      prettyPrinter :: String
prettyPrinter = LBNF
-> String
-> Bool
-> Maybe String
-> Bool
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(CatName, TokenDef)]
-> Bool
-> TokenText
-> String
cf2printer LBNF
lbnf String
cfName Bool
inDirectory Maybe String
nSpace Bool
False [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules [(CatName, TokenDef)]
tks Bool
funct TokenText
TextToken
  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
"Print" String
"hs", String
prettyPrinter)]
  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))
      (([(Label, ([Type], (Integer, ARHS)))]
 -> [(Label, ([Type], (Integer, ARHS)))])
-> (Type, [(Label, ([Type], (Integer, ARHS)))])
-> (Type, [(Label, ([Type], (Integer, ARHS)))])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
Data.Bifunctor.second ([String]
-> [(Label, ([Type], (Integer, ARHS)))]
-> [(Label, ([Type], (Integer, ARHS)))]
filterLabelsPrinter [String]
fNames) ((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)