{-# LANGUAGE OverloadedStrings #-}

module BNFC.Backend.Agda.Main (agdaMain) 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.Haskell.Utilities.Utils

import Control.Monad.State

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

import Prettyprinter
import System.FilePath (takeBaseName)

agdaMain :: LBNF -> State AgdaBackendState Result
agdaMain lbnf = do
  st <- get
  let
    cfName      = takeBaseName $ optInput $ globalOpt st
    inDirectory = inDir $ agdaOpts st
    nSpace      = nameSpace $ agdaOpts st
    main        = cf2main lbnf cfName inDirectory nSpace
  return [(mkFilePath inDirectory nSpace cfName "Main" "agda", main)]

cf2main :: LBNF -> String -> Bool -> Maybe String -> String
cf2main lbnf cfName inDir nameSpace =
  docToString defaultLayoutOptions $ cf2doc lbnf cfName inDir nameSpace

cf2doc :: LBNF -> String -> Bool -> Maybe String -> Doc ()
cf2doc lbnf cfName inDir nameSpace = vsep $ concat
  [ [ "-- File generated by the BNF Converter."
    , emptyDoc
    , "-- Test for Agda binding of parser. Requires Agda >= 2.5.4."
    , emptyDoc
    ]
  , ["module" <+> fromString mainName <+> "where"
    , emptyDoc
    ]
  , Utils.when (layoutsAreUsed lbnf) [ "open import Agda.Builtin.Bool using (true)" ]
  , [ "open import" <+> fromString ioLibName
    , "open import" <+> fromString astName <+> "using" <+> parens printFun
    , "open import" <+> fromString parserName <+> "using" <+>
      parens (hsep ["HsEither;", parseFun])
    , emptyDoc
    , "main : IO ⊤"
    , "main = do"
    , "  file ∷ [] ← getArgs where"
    , "    _ → do"
    , "      putStrLn \"usage: Main <SourceFile>\""
    , "      exitFailure"
    , "  HsEither.right result ←" <+>
      (if layoutsAreUsed lbnf
      then parseFun <+> "true"
      else parseFun)
      <+> "<$> readFiniteFile file where"
    , "    HsEither.left msg → do"
    , "      putStrLn \"PARSE FAILED\\n\""
    , "      putStrLn (stringFromList msg)"
    , "      exitFailure"
    , "  putStrLn \"PARSE SUCCESSFUL\\n\""
    , "  putStrLn" <+> parens (printFun <+> "result")
    ]
  ]
  where

    parseFun :: Doc ()
    parseFun = "parse" <> fromString (printCatName firstCat)

    printFun :: Doc ()
    printFun = "print" <> fromString (printCatName firstCat)

    -- Top parser.
    firstCat :: Cat
    firstCat = head entrypoints

    -- Entrypoints sorted according to their declaration order in the grammar file.
    entrypoints :: [Cat]
    entrypoints = fst <$> sortBy (compare `on` snd) (Map.toList $ _lbnfEntryPoints lbnf)

    -- Agda module names.
    astName :: ModuleName
    astName = mkModule inDir nameSpace cfName "AST"
    ioLibName :: ModuleName
    ioLibName = mkModule inDir nameSpace cfName "IOLib"
    mainName :: ModuleName
    mainName = mkModule inDir nameSpace cfName "Main"
    parserName :: ModuleName
    parserName = mkModule inDir nameSpace cfName "Parser"