------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive IO handles: simple bindings to Haskell types and functions
------------------------------------------------------------------------

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

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

module IO.Primitive.Handle where

open import Data.Maybe.Base using (Maybe)
open import Data.Nat.Base using (ℕ)

data BufferMode : Set where
  noBuffering lineBuffering : BufferMode
  blockBuffering : Maybe ℕ → BufferMode
{-# FOREIGN GHC import System.IO #-}
{-# FOREIGN GHC
    data AgdaBufferMode
      = AgdaNoBuffering
      | AgdaLineBuffering
      | AgdaBlockBuffering (Maybe Integer)
    toBufferMode :: AgdaBufferMode -> BufferMode
    toBufferMode x = case x of
      AgdaNoBuffering       -> NoBuffering
      AgdaLineBuffering     -> LineBuffering
      AgdaBlockBuffering mi -> BlockBuffering (fromIntegral <$> mi)
    fromBufferMode :: BufferMode -> AgdaBufferMode
    fromBufferMode x = case x of
      NoBuffering       -> AgdaNoBuffering
      LineBuffering     -> AgdaLineBuffering
      BlockBuffering mi -> AgdaBlockBuffering (fromIntegral <$> mi)
#-}

{-# COMPILE GHC BufferMode = data AgdaBufferMode
                           ( AgdaNoBuffering
                           | AgdaLineBuffering
                           | AgdaBlockBuffering
                           )
#-}

open import Data.Unit.Base using (⊤)
open import IO.Primitive.Core using (IO)

postulate
  Handle : Set
  stdin stdout stderr : Handle
  hSetBuffering : Handle → BufferMode → IO ⊤
  hGetBuffering : Handle → IO BufferMode
  hFlush : Handle → IO ⊤

{-# FOREIGN GHC import System.IO #-}
{-# COMPILE GHC Handle = type Handle #-}
{-# COMPILE GHC stdin = stdin #-}
{-# COMPILE GHC stdout = stdout #-}
{-# COMPILE GHC stderr = stderr #-}
{-# COMPILE GHC hSetBuffering = \ h -> hSetBuffering h . toBufferMode #-}
{-# COMPILE GHC hGetBuffering = fmap fromBufferMode . hGetBuffering #-}
{-# COMPILE GHC hFlush = hFlush #-}