    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- IO
    ------------------------------------------------------------------------

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

    module IO where

    open import Codata.Musical.Notation
    open import Codata.Musical.Costring
    open import Data.Unit.Polymorphic.Base
    open import Data.String.Base using (String)
    import Data.Unit.Base as Unit0
    open import Function.Base using (_∘_; flip)
    import IO.Primitive.Core as Prim
    open import Level

    private
      variable
        a b : Level
        A : Set a
        B : Set b

    ------------------------------------------------------------------------
    -- Re-exporting the basic type and functions

    open import IO.Base public
    open import IO.Handle public

    ------------------------------------------------------------------------
    -- Utilities

    module Colist where

      open import Codata.Musical.Colist.Base

      sequence : Colist (IO A) → IO (Colist A)
      sequence []       = pure []
      sequence (c ∷ cs) = bind (♯ c)               λ x  → ♯
                          bind (♯ sequence (♭ cs)) λ xs → ♯
                          pure (x ∷ ♯ xs)

      -- The reason for not defining sequence′ in terms of sequence is
      -- efficiency (the unused results could cause unnecessary memory use).

      sequence′ : Colist (IO A) → IO ⊤
      sequence′ []       = pure _
      sequence′ (c ∷ cs) = seq (♯ c) (♯ sequence′ (♭ cs))

      mapM : (A → IO B) → Colist A → IO (Colist B)
      mapM f = sequence ∘ map f

      mapM′ : (A → IO B) → Colist A → IO ⊤
      mapM′ f = sequence′ ∘ map f

      forM : Colist A → (A → IO B) → IO (Colist B)
      forM = flip mapM

      forM′ : Colist A → (A → IO B) → IO ⊤
      forM′ = flip mapM′

    module List where

      open import Data.List.Base

      sequence : List (IO A) → IO (List A)
      sequence []       = ⦇ [] ⦈
      sequence (c ∷ cs) = ⦇ c ∷ sequence cs ⦈

      -- The reason for not defining sequence′ in terms of sequence is
      -- efficiency (the unused results could cause unnecessary memory use).

      sequence′ : List (IO A) → IO ⊤
      sequence′ []       = pure _
      sequence′ (c ∷ cs) = c >> sequence′ cs

      mapM : (A → IO B) → List A → IO (List B)
      mapM f = sequence ∘ map f

      mapM′ : (A → IO B) → List A → IO ⊤
      mapM′ f = sequence′ ∘ map f

      forM : List A → (A → IO B) → IO (List B)
      forM = flip mapM

      forM′ : List A → (A → IO B) → IO ⊤
      forM′ = flip mapM′

    ------------------------------------------------------------------------
    -- 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.

    open import IO.Finite public
      renaming (readFile to readFiniteFile)

    open import IO.Infinite public
      renaming ( writeFile  to writeFile∞
               ; appendFile to appendFile∞
               ; putStr     to putStr∞
               ; putStrLn   to putStrLn∞
               )