------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive IO: simple bindings to Haskell types and functions
------------------------------------------------------------------------
 
-- NOTE: the contents of this module should be accessed via `IO`.
 
{-# OPTIONS --cubical-compatible #-}
 
module IO.Primitive.Core where
 
open import Level using (Level)
private
  variable
    a : Level
    A B : Set a
 
------------------------------------------------------------------------
-- The IO monad
 
open import Agda.Builtin.IO public
  using (IO)
 
infixl  _>>=_
 
postulate
  pure : A → IO A
  _>>=_  : IO A → (A → IO B) → IO B
 
{-# COMPILE GHC pure = \_ _ -> return    #-}
{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
{-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
{-# COMPILE UHC _>>=_  = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
 
-- Haskell-style alternative syntax
return : A → IO A
return = pure
 
_>>_ : IO A → IO B → IO B
a >> b = a >>= λ _ → b