------------------------------------------------------------------------
-- 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
import Data.Unit.Base as Unit0
open import Function.Base using (_∘_; flip)
import IO.Primitive 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

------------------------------------------------------------------------
-- 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∞
           )