------------------------------------------------------------------------
-- The Agda standard library
--
-- IO: basic types and functions
------------------------------------------------------------------------

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

module IO.Base where

open import Level
open import Codata.Musical.Notation
open import Data.Bool.Base using (Bool; true; false; not)
open import Agda.Builtin.Maybe using (Maybe; nothing; just)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
import Agda.Builtin.Unit as Unit0
open import Data.Unit.Polymorphic.Base
open import Function.Base using (_∘′_; const; flip)
import IO.Primitive.Core as Prim

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

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

-- One cannot write "infinitely large" computations with the
-- postulated IO monad in IO.Primitive without turning off the
-- termination checker (or going via the FFI, or perhaps abusing
-- something else). The following coinductive deep embedding is
-- introduced to avoid this problem. Possible non-termination is
-- isolated to the run function below.

data IO (A : Set a) : Set (suc a) where
  lift : (m : Prim.IO A)  IO A
  pure : (x : A)  IO A
  bind : {B : Set a} (m :  (IO B)) (f : (x : B)   (IO A))  IO A
  seq  : {B : Set a} (m₁ :  (IO B)) (m₂ :  (IO A))  IO A

lift! : IO A  IO (Lift b A)
lift!         (lift io)   = lift (io Prim.>>= λ a  Prim.pure (Level.lift a))
lift!         (pure a)    = pure (Level.lift a)
lift! {b = b} (bind m f)  = bind ( lift! {b = b} ( m))
                                  x   lift! ( (f (lower x))))
lift! {b = b} (seq m₁ m₂) = seq ( lift! {b = b} ( m₁))
                                ( lift! ( m₂))

module _ {A B : Set a} where

  infixl 1 _<$>_ _<*>_ _>>=_ _>>_
  infixr 1 _=<<_

  _<*>_ : IO (A  B)  IO A  IO B
  mf <*> mx = bind ( mf) λ f   (bind ( mx) λ x   pure (f x))

  _<$>_ : (A  B)  IO A  IO B
  f <$> m = pure f <*> m

  _<$_ : B  IO A  IO B
  b <$ m = (const b) <$> m

  _>>=_ : IO A  (A  IO B)  IO B
  m >>= f = bind ( m) λ x   f x

  _=<<_ : (A  IO B)  IO A  IO B
  _=<<_ = flip _>>=_

  _>>_ : IO A  IO B  IO B
  m₁ >> m₂ = seq ( m₁) ( m₂)

  _<<_ : IO B  IO A  IO B
  _<<_ = flip _>>_

------------------------------------------------------------------------
-- Running programs

-- A value of type `IO A` is a description of a computation that may
-- eventually produce an `A`. The `run` function converts this
-- description of a computation into calls to primitive functions that
-- will actually perform it.

{-# NON_TERMINATING #-}
run : IO A  Prim.IO A
run (lift m)    = m
run (pure x)    = Prim.pure x
run (bind m f)  = run ( m ) Prim.>>= λ x  run ( (f x))
run (seq m₁ m₂) = run ( m₁) Prim.>>= λ _  run ( m₂)

-- The entrypoint of an Agda program will be assigned type `Main` and
-- implemented using `run` on some `IO ⊤` program.

Main : Set
Main = Prim.IO {0ℓ} 

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

-- Make a unit-returning primitive level polymorphic
lift′ : Prim.IO Unit0.⊤  IO {a} 
lift′ io = lift (io Prim.>>= λ _  Prim.pure _)

-- Throw away the result
ignore : IO A  IO 
ignore io = io >> pure _


------------------------------------------------------------------------
-- Conditional executions

-- Only run the action if the boolean is true
when : Bool  IO {a}   IO 
when true m = m
when false _ = pure _

-- Only run the action if the boolean is false
unless : Bool  IO {a}   IO 
unless = when ∘′ not

-- Run the action if the `Maybe` computation was successful
whenJust : Maybe A  (A  IO {a} )  IO 
whenJust (just a) k = k a
whenJust nothing  _ = pure _

-- Run the action if the `E ⊎_` computation was successful
whenInj₂ : E  A  (A  IO {a} )  IO 
whenInj₂ (inj₂ a) k = k a
whenInj₂ (inj₁ _) _ = pure _


------------------------------------------------------------------------
-- Loops

-- Keep running the action forever
forever : IO {a}   IO {a} 
forever act = seq ( act) ( forever act)

-- Keep running an IO action until we get a value. Convenient when user
-- input is involved and it may be malformed.
untilJust : IO (Maybe A)  IO A
-- Note that here we are forced to use `bind` & the musical notation
-- explicitly to guarantee that the corecursive call is guarded
untilJust m = bind ( m) λ where
  nothing    untilJust m
  (just a)   pure a

untilInj₂ : {A B : Set a}  (A  IO (A  B))  A  IO B
untilInj₂ f x = bind ( f x) λ where
  (inj₁ x′)   untilInj₂ f x′
  (inj₂ y)   pure y







------------------------------------------------------------------------
-- DEPRECATIONS

untilRight = untilInj₂
{-# WARNING_ON_USAGE untilRight
"Warning: untilRight was deprecated in v2.1.
Please use untilInj₂ instead."
#-}