    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Primitive IO: simple bindings to Haskell types and functions
    -- manipulating potentially infinite objects
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --guardedness #-}

    module IO.Primitive.Infinite where

    -- NOTE: the contents of this module should be accessed via `IO` or
    -- `IO.Infinite`.

    open import Codata.Musical.Costring using (Costring)
    open import Agda.Builtin.String using (String)
    open import Agda.Builtin.Unit renaming (⊤ to Unit)

    ------------------------------------------------------------------------
    -- The IO monad

    open import Agda.Builtin.IO public using (IO)

    ------------------------------------------------------------------------
    -- Simple lazy IO

    -- Note that the functions below produce commands which, when
    -- executed, may raise exceptions.

    -- Note also that the semantics of these functions depends on the
    -- version of the Haskell base library. If the version is 4.2.0.0 (or
    -- later?), then the functions use the character encoding specified by
    -- the locale. For older versions of the library (going back to at
    -- least version 3) the functions use ISO-8859-1.

    postulate
      getContents : IO Costring
      readFile    : String → IO Costring
      writeFile   : String → Costring → IO Unit
      appendFile  : String → Costring → IO Unit
      putStr      : Costring → IO Unit
      putStrLn    : Costring → IO Unit

    {-# FOREIGN GHC import qualified Data.Text    #-}

    {-# FOREIGN GHC

      fromColist :: MAlonzo.Code.Codata.Musical.Colist.Base.AgdaColist a -> [a]
      fromColist MAlonzo.Code.Codata.Musical.Colist.Base.Nil         = []
      fromColist (MAlonzo.Code.Codata.Musical.Colist.Base.Cons x xs) =
        x : fromColist (MAlonzo.RTE.flat xs)

      toColist :: [a] -> MAlonzo.Code.Codata.Musical.Colist.Base.AgdaColist a
      toColist []       = MAlonzo.Code.Codata.Musical.Colist.Base.Nil
      toColist (x : xs) =
        MAlonzo.Code.Codata.Musical.Colist.Base.Cons x (MAlonzo.RTE.Sharp (toColist xs))
    #-}

    {-# COMPILE GHC getContents    = fmap toColist getContents                          #-}
    {-# COMPILE GHC readFile       = fmap toColist . readFile . Data.Text.unpack        #-}
    {-# COMPILE GHC writeFile      = \x -> writeFile (Data.Text.unpack x) . fromColist  #-}
    {-# COMPILE GHC appendFile     = \x -> appendFile (Data.Text.unpack x) . fromColist #-}
    {-# COMPILE GHC putStr         = putStr . fromColist                                #-}
    {-# COMPILE GHC putStrLn       = putStrLn . fromColist                              #-}
    {-# COMPILE UHC getContents    = UHC.Agda.Builtins.primGetContents     #-}
    {-# COMPILE UHC readFile       = UHC.Agda.Builtins.primReadFile        #-}
    {-# COMPILE UHC writeFile      = UHC.Agda.Builtins.primWriteFile       #-}
    {-# COMPILE UHC appendFile     = UHC.Agda.Builtins.primAppendFile      #-}
    {-# COMPILE UHC putStr         = UHC.Agda.Builtins.primPutStr          #-}
    {-# COMPILE UHC putStrLn       = UHC.Agda.Builtins.primPutStrLn        #-}