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

stvienna wiener stvienna at gmail.com
Fri May 10 05:10:32 CEST 2013


I have the following issue:
My agda program communicates with another program via an
bi-directional pipe. I am facing some problems and think it may be
related to buffering. Therefore, I want to turn buffering off and/or
flush manually.

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

My current Agda program for test purposes:

-------------
open import Prelude
open import IO.Primitive as Prim

postulate
 getLine : Prim.IO Costring

{-# COMPILED getLine   getLine          #-}

main : _
main = (getLine Prim.>>= λ s → (Prim.putStrLn s))
------------


How can I use the two haskell commands from within my Agda IO program?


Best regards,
Stephan Adelsberg


More information about the Agda mailing list