module BNFC.Backend.Agda.InitState where

import BNFC.Prelude

import Control.Monad.Except

import BNFC.CF

import BNFC.Backend.Agda.Options
import BNFC.Backend.Agda.State
import BNFC.Backend.Agda.Utilities.ReservedWords
import BNFC.Backend.Haskell.InitState
import BNFC.Backend.Haskell.Utilities.InitState

import BNFC.Options.GlobalOptions

import           Data.Bifunctor (second)
import qualified Data.Map as Map

agdaInitState :: LBNF -> GlobalOptions -> AgdaBackendOptions -> Except String AgdaBackendState
agdaInitState :: LBNF
-> GlobalOptions
-> AgdaBackendOptions
-> Except String AgdaBackendState
agdaInitState LBNF
lbnf GlobalOptions
globalOpts AgdaBackendOptions
agdaOpts = do
  let hsAstRules :: [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsAstRules    = ASTRulesAP -> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
processRules (ASTRulesAP -> [(Type, [(Label, ([Type], (Integer, ARHS)))])])
-> ASTRulesAP -> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
forall a b. (a -> b) -> a -> b
$ LBNF -> ASTRulesAP
_lbnfASTRulesAP LBNF
lbnf
      agdaAstRules :: [(Type, [(Label, [Type])])]
agdaAstRules  = [String]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, [Type])])]
processASTRulesAgda [String]
fNames [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsAstRules
      fNames :: [String]
fNames        = NonEmpty Char -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (NonEmpty Char -> String) -> [NonEmpty Char] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (NonEmpty Char) (WithPosition Function) -> [NonEmpty Char]
forall k a. Map k a -> [k]
Map.keys (LBNF -> Map (NonEmpty Char) (WithPosition Function)
_lbnfFunctions LBNF
lbnf)
      hsFunctions :: [(NonEmpty Char, Function)]
hsFunctions   = Map (NonEmpty Char) (WithPosition Function)
-> [(NonEmpty Char, Function)]
processFunctions (Map (NonEmpty Char) (WithPosition Function)
 -> [(NonEmpty Char, Function)])
-> Map (NonEmpty Char) (WithPosition Function)
-> [(NonEmpty Char, Function)]
forall a b. (a -> b) -> a -> b
$ LBNF -> Map (NonEmpty Char) (WithPosition Function)
_lbnfFunctions  LBNF
lbnf
      agdaFunctions :: [(NonEmpty Char, Function)]
agdaFunctions = [(NonEmpty Char, Function)] -> [(NonEmpty Char, Function)]
processFunctionsAgda [(NonEmpty Char, Function)]
hsFunctions
      tokens :: [(NonEmpty Char, TokenDef)]
tokens        = TokenDefs -> [(NonEmpty Char, TokenDef)]
sortTokens (TokenDefs -> [(NonEmpty Char, TokenDef)])
-> TokenDefs -> [(NonEmpty Char, TokenDef)]
forall a b. (a -> b) -> a -> b
$ LBNF -> TokenDefs
_lbnfTokenDefs LBNF
lbnf
  LBNF -> Except String ()
hsChecks LBNF
lbnf
  AgdaBackendState -> Except String AgdaBackendState
forall (m :: * -> *) a. Monad m => a -> m a
return (AgdaBackendState -> Except String AgdaBackendState)
-> AgdaBackendState -> Except String AgdaBackendState
forall a b. (a -> b) -> a -> b
$
    GlobalOptions
-> AgdaBackendOptions
-> [Token]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, [Type])])]
-> [(Cat, Map RHS RuleLabel)]
-> [(NonEmpty Char, Function)]
-> [(NonEmpty Char, Function)]
-> [(NonEmpty Char, TokenDef)]
-> AgdaBackendState
AgdaSt
      GlobalOptions
globalOpts
      AgdaBackendOptions
agdaOpts
      (LBNF -> [Token]
getTokens LBNF
lbnf)
      [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsAstRules
      [(Type, [(Label, [Type])])]
agdaAstRules
      (ParserRules -> [(Cat, Map RHS RuleLabel)]
processParserRules (LBNF -> ParserRules
_lbnfParserRules LBNF
lbnf))
      [(NonEmpty Char, Function)]
hsFunctions
      [(NonEmpty Char, Function)]
agdaFunctions
      [(NonEmpty Char, TokenDef)]
tokens


processASTRulesAgda :: [String]
                    -> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
                    -> [(Type, [(Label, [Type])])]
processASTRulesAgda :: [String]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, [Type])])]
processASTRulesAgda [String]
fNames [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules =
  [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
avoidResWordsASTRulesAgda ([(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])])
-> [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
forall a b. (a -> b) -> a -> b
$ [String]
-> [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
filterRules [String]
fNames ([(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])])
-> [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
forall a b. (a -> b) -> a -> b
$ (Type, [(Label, ([Type], (Integer, ARHS)))])
-> (Type, [(Label, [Type])])
toAgdaRules ((Type, [(Label, ([Type], (Integer, ARHS)))])
 -> (Type, [(Label, [Type])]))
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, [Type])])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules

-- Remove category precedence and ARHS from AST rules
toAgdaRules :: (Type, [(Label, ([Type], (Integer, ARHS)))])
            -> (Type, [(Label, [Type])])
toAgdaRules :: (Type, [(Label, ([Type], (Integer, ARHS)))])
-> (Type, [(Label, [Type])])
toAgdaRules (Type
r,[(Label, ([Type], (Integer, ARHS)))]
l) = (Type
r, (([Type], (Integer, ARHS)) -> [Type])
-> (Label, ([Type], (Integer, ARHS))) -> (Label, [Type])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([Type], (Integer, ARHS)) -> [Type]
forall a b. (a, b) -> a
fst ((Label, ([Type], (Integer, ARHS))) -> (Label, [Type]))
-> [(Label, ([Type], (Integer, ARHS)))] -> [(Label, [Type])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Label, ([Type], (Integer, ARHS)))]
l)

filterRules :: [String]
            -> [(Type, [(Label, [Type])])]
            -> [(Type, [(Label, [Type])])]
filterRules :: [String]
-> [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
filterRules [String]
fNames [(Type, [(Label, [Type])])]
rules =
  ((Type, [(Label, [Type])]) -> Bool)
-> [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
forall a. (a -> Bool) -> [a] -> [a]
filter
  (\(Type
_,[(Label, [Type])]
l) -> Bool -> Bool
not ([(Label, [Type])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Label, [Type])]
l))
  (([(Label, [Type])] -> [(Label, [Type])])
-> (Type, [(Label, [Type])]) -> (Type, [(Label, [Type])])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
Data.Bifunctor.second ([String] -> [(Label, [Type])] -> [(Label, [Type])]
filterLabelsAgdaAST [String]
fNames) ((Type, [(Label, [Type])]) -> (Type, [(Label, [Type])]))
-> [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Type, [(Label, [Type])])]
rules)

-- | Filter @Label@s that will be printed in the Agda AST datatypes.

filterLabelsAgdaAST :: [String]
                    -> [(Label, [Type])]
                    -> [(Label, [Type])]
filterLabelsAgdaAST :: [String] -> [(Label, [Type])] -> [(Label, [Type])]
filterLabelsAgdaAST [String]
fNames =
  ((Label, [Type]) -> Bool) -> [(Label, [Type])] -> [(Label, [Type])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Label
l,[Type]
_) -> Label -> Bool
isALabel Label
l Bool -> Bool -> Bool
&& String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (Label -> String
printLabelName Label
l) [String]
fNames)