{-# 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 :: State AgdaBackendState Result
agdaIOLib = 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
    ioLib :: String
ioLib       = String -> Bool -> Maybe String -> String
cf2IOLib String
cfName Bool
inDirectory Maybe String
nSpace
  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
"IOLib" String
"agda", String
ioLib)]

cf2IOLib :: String -> Bool -> Maybe String -> String
cf2IOLib :: String -> Bool -> Maybe String -> String
cf2IOLib String
cfName Bool
inDir Maybe String
nameSpace =
  LayoutOptions -> Doc () -> String
docToString LayoutOptions
defaultLayoutOptions (Doc () -> String) -> Doc () -> String
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Maybe String -> Doc ()
cf2doc String
cfName Bool
inDir Maybe String
nameSpace

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

  where

    ioLibName :: ModuleName
    ioLibName :: String
ioLibName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"IOLib"