[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