[Agda] Agda IO program: how to turn off buffering?

[Andrés Sicard-Ramírez]

On Thu, May 9, 2013 at 10:10 PM, stvienna wiener <stvienna at gmail.com> wrote:
>
> How can I call the respective haskell functions, i.e.,  what
> postulates do I need to define?
>
> The two Haskell commands are:
> hSetBuffering stdout NoBuffering
> hFlush stdout

(untested)

open import Foreign.Haskell
open import Data.Maybe

{-# IMPORT System.IO #-}

data Handle : Set where
{-# COMPILED_DATA Handle System.IO.Handle #-}

postulate Int : Set
{-# COMPILED_TYPE Int Int #-}

data BufferMode : Set where
  NoBuffering    : BufferMode
  LineBuffering  : BufferMode
  BlockBuffering : Maybe Int → BufferMode

{-# COMPILED_DATA BufferMode System.IO.BufferMode
System.IO.NoBuffering System.IO.LineBuffering System.IO.BlockBuffering
#-}

postulate hSetBuffering : Handle → BufferMode → Prim.IO Unit
{-# COMPILED hSetBuffering System.IO.hSetBuffering #-}

postulate stdout : Handle
{-# COMPILED stdout System.IO.stdout #-}

postulate hFlush : Handle → IO Unit
{-# COMPILED hFlush System.IO.hFlush #-}

-- 
Andrés