{-# LANGUAGE OverloadedStrings #-}

module BNFC.Backend.Agda.IOLib (agdaIOLib) where

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 Data.String     (fromString)

import Prettyprinter
import System.FilePath (takeBaseName)

agdaIOLib :: State AgdaBackendState Result
agdaIOLib = do
  st <- get
  let
    cfName      = takeBaseName $ optInput $ globalOpt st
    inDirectory = inDir $ agdaOpts st
    nSpace      = nameSpace $ agdaOpts st
    ioLib       = cf2IOLib cfName inDirectory nSpace
  return [(mkFilePath inDirectory nSpace cfName "IOLib" "agda", ioLib)]

cf2IOLib :: String -> Bool -> Maybe String -> String
cf2IOLib cfName inDir nameSpace =
  docToString defaultLayoutOptions $ cf2doc cfName inDir nameSpace

cf2doc :: String -> Bool -> Maybe String -> Doc ()
cf2doc cfName inDir nameSpace = vsep
  [ "-- File generated by the BNF Converter."
  , emptyDoc
  , "-- Basic I/O library."
  , emptyDoc
  , "module" <+> fromString ioLibName <+> "where"
  , emptyDoc
  , "open import Agda.Builtin.IO     public using (IO)"
  , "open import Agda.Builtin.List   public using (List; []; _∷_)"
  , "open import Agda.Builtin.String public using (String)"
  , "  renaming (primStringFromList to stringFromList)"
  , "open import Agda.Builtin.Unit   public using (⊤)"
  , emptyDoc
  , "-- I/O monad."
  , emptyDoc
  , "postulate"
  , "  return : ∀ {a} {A : Set a} → A → IO A"
  , "  _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B"
  , emptyDoc
  , "{-# COMPILE GHC return = \\ _ _ -> return    #-}"
  , "{-# COMPILE GHC _>>=_  = \\ _ _ _ _ -> (>>=) #-}"
  , emptyDoc
  , "infixl 1 _>>=_ _>>_"
  , emptyDoc
  , "_>>_  : ∀ {b} {B : Set b} → IO ⊤ → IO B → IO B"
  , "_>>_ = λ m m' → m >>= λ _ → m'"
  , emptyDoc
  , "-- Co-bind and functoriality."
  , emptyDoc
  , "infixr 1 _=<<_ _<$>_"
  , emptyDoc
  , "_=<<_  : ∀ {a b} {A : Set a} {B : Set b} → (A → IO B) → IO A → IO B"
  , "k =<< m = m >>= k"
  , emptyDoc
  , "_<$>_  : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → IO A → IO B"
  , "f <$> m = do"
  , "  a ← m"
  , "  return (f a)"
  , emptyDoc
  , "-- Binding basic I/O functionality."
  , emptyDoc
  , "{-# FOREIGN GHC import qualified Data.Text #-}"
  , "{-# FOREIGN GHC import qualified Data.Text.IO #-}"
  , "{-# FOREIGN GHC import qualified System.Exit #-}"
  , "{-# FOREIGN GHC import qualified System.Environment #-}"
  , "{-# FOREIGN GHC import qualified System.IO #-}"
  , emptyDoc
  , "postulate"
  , "  exitFailure    : ∀{a} {A : Set a} → IO A"
  , "  getArgs        : IO (List String)"
  , "  putStrLn       : String → IO ⊤"
  , "  readFiniteFile : String → IO String"
  , emptyDoc
  , "{-# COMPILE GHC exitFailure    = \\ _ _ -> System.Exit.exitFailure #-}"
  , "{-# COMPILE GHC getArgs        = fmap (map Data.Text.pack) System.Environment.getArgs #-}"
  , "{-# COMPILE GHC putStrLn       = System.IO.putStrLn . Data.Text.unpack #-}"
  , "{-# COMPILE GHC readFiniteFile = Data.Text.IO.readFile . Data.Text.unpack #-}"
  ]

  where

    ioLibName :: ModuleName
    ioLibName = mkModule inDir nameSpace cfName "IOLib"