{-# LANGUAGE OverloadedStrings #-}

module BNFC.Backend.Agda.Parser (agdaParser) where

import BNFC.CF

import BNFC.Options.GlobalOptions

import BNFC.Prelude

import BNFC.Backend.CommonInterface.Backend
import BNFC.Backend.Common.Utils as Utils

import BNFC.Backend.Agda.Options
import BNFC.Backend.Agda.State
import BNFC.Backend.Agda.Utilities.ReservedWords
import BNFC.Backend.Agda.Utilities.Utils
import BNFC.Backend.Haskell.Options (TokenText (..))
import BNFC.Backend.Haskell.Parser (cf2parser)
import BNFC.Backend.Haskell.Utilities.Parser
import BNFC.Backend.Haskell.Utilities.Utils

import Control.Monad.State

import           Data.List       (intersperse)
import qualified Data.Map as Map
import           Data.String     (fromString)

import Prettyprinter
import System.FilePath (takeBaseName)


agdaParser :: LBNF -> State AgdaBackendState Result
agdaParser lbnf = do
  st <- get
  let cfName      = takeBaseName $ optInput $ globalOpt st
      rules       = parserRules st
      rulesCats   = fst <$> rules
      astCats     = printTypeName . avoidResWordsType . fst <$> agdaAstRules st
      tokenCats   = toList . avoidAgdaReservedWords . fst <$> tokens st
      builtins    = builtinsToImport rulesCats (Map.keys $ _lbnfParserBuiltins lbnf)
      categories  = astCats ++ builtins ++ tokenCats
      toks        = lexerParserTokens st
      inDirectory = inDir $ agdaOpts st
      nSpace      = nameSpace $ agdaOpts st
      funct       = functor $ agdaOpts st
      parserAgda  =
        cf2agdaparser lbnf rulesCats categories cfName inDirectory nSpace
      parserHaskell = cf2parser lbnf rules cfName inDirectory nSpace TextToken toks funct
  return
    [ (mkFilePath inDirectory nSpace cfName "Parser" "agda", parserAgda)
    , (mkFilePath inDirectory nSpace cfName "Par" "y", parserHaskell)
    ]

    where
      -- Import builtins which were used as list categories.
      builtinsToImport :: [Cat] -> [BuiltinCat] -> [String]
      builtinsToImport cats builtins = let
        builtinsListCats = printCatName <$> filter (\a -> isCatList a && isCatBuiltin a) cats
        builtins' = toList . printBuiltinCat <$> builtins
        in filter (`elem` builtinsListCats) builtins'


cf2agdaparser :: LBNF
              -> [Cat]
              -> [String]
              -> String
              -> Bool
              -> Maybe String
              -> String
cf2agdaparser lbnf rulesCats categories cfName inDir nameSpace =
  docToString defaultLayoutOptions $ cf2doc lbnf rulesCats categories cfName inDir nameSpace

cf2doc :: LBNF
       -> [Cat]
       -> [String]
       -> String
       -> Bool
       -> Maybe String
       -> Doc ()
cf2doc lbnf rulesCats cats cfName inDir nameSpace =
  (vsep . intersperse emptyDoc)
    [ header
    , "module" <+> fromString parserName <+> "where"
    , imports NoImportNumeric (layoutsAreUsed lbnf) False False
    , importCats agdaASTName cats
    , importPragmas False mods
    , eitherErr
    , "-- Happy parsers"
    , parsers layoutName rulesCats
    ]
  where

    mods :: [ModuleName]
    mods = if layoutsAreUsed lbnf
      then [ mkModule inDir nameSpace cfName "Layout"
           , mkModule inDir nameSpace cfName "Par"
           ]
      else [ mkModule inDir nameSpace cfName "Par"]

    layoutName :: Maybe ModuleName
    layoutName = if layoutsAreUsed lbnf
      then Just $ mkModule inDir nameSpace cfName "Layout"
      else Nothing

    parserName :: ModuleName
    parserName = mkModule inDir nameSpace cfName "Parser"

    agdaASTName :: ModuleName
    agdaASTName = mkModule inDir nameSpace cfName "AST"


header :: Doc ()
header = vsep
  [ "-- File generated by the BNF Converter (bnfc 2.9.4)."
  , emptyDoc
  , "-- Agda bindings for the Haskell parsers."
  ]

-- Import categories from Agda AST module.
importCats :: ModuleName -> [String] -> Doc ()
importCats agdaAST cats = hang 2 $ vsep $
  ["open import" <+> fromString agdaAST <+> "using"]
  ++
  zipWith (\a b -> fromString $ a ++ b) ("( " : repeat "; ") cats
  ++
  [ rparen ]

eitherErr :: Doc ()
eitherErr = vsep
  [ "-- Either monad used for error handling"
  , "data HsEither A B : Set where"
  , "  right : B → HsEither A B"
  , "  left : A → HsEither A B"
  , emptyDoc
  , "Err : Set → Set"
  , "Err = HsEither (#List Char)"
  , emptyDoc
  , "{-# COMPILE GHC HsEither = data Either"
  , "  ( Right"
  , "  | Left"
  , "  ) #-}"
  ]

parsers :: Maybe ModuleName
           -- ^ Grammar uses layout?  If yes, Haskell layout module name.
        -> [Cat]
           -- ^ Bind parsers for these non-terminals.
        -> Doc ()
parsers layout parserCats = vsep
  [ hang 2 $ vsep $ "postulate" : (printRule <$> parserCats)
  , emptyDoc
  , vsep $ printPragmaBind <$> parserCats
  ]

  where
    -- When grammar uses layout, we parametrize the parser by a boolean @tl@
    -- that indicates whether top layout should be used for this parser.
    -- Also, we add @resolveLayout tl@ to the pipeline after lexing.

  printRule :: Cat -> Doc ()
  printRule c = if isJust layout
    then parserBind c <+> colon <+> "#Bool → #String → Err" <+> prCat (avoidResWordsCat c)
    else parserBind c <+> colon <+> "#String → Err" <+> prCat (avoidResWordsCat c)

  parserBind :: Cat -> Doc ()
  parserBind c = "parse" <> fromString (printCatNamePrec' $ avoidResWordsCat c)

  prCat :: Cat -> Doc ()
  prCat c = if isCatList c
    then parens ("#List" <+> fromString (printCatName c))
    else fromString (printCatName c)

  printPragmaBind :: Cat -> Doc ()
  printPragmaBind c = case layout of
    Nothing -> "{-# COMPILE GHC" <+> parserBind c <+> "=" <+>
      parserCatName c <+> ". myLexer #-}"
    Just layoutMod -> "{-# COMPILE GHC" <+> parserBind c <+> "= \\ tl ->" <+>
      parserCatName c <+> dot <+> fromString layoutMod <> ".resolveLayout tl" <+> ". myLexer #-}"