------------------------------------------------------------------------
-- System.IO
------------------------------------------------------------------------
-- (The sectioning below mostly follows Haskell System.IO documentation)

module System.IO where
{-# IMPORT System.IO #-}

open import IO.Primitive public
open import Category.Monad
open import Data.Unit
open import Data.Char
open import Data.String hiding ( Costring )
open import Foreign.Haskell
open import FFI.Pair
open import Data.Maybe
open import FFI.Int

private Costring = Colist Char

open import Level

IOMonad : RawMonad IO
IOMonad = record { return = return; _>>=_ = _>>=_ }
open RawMonad IOMonad public using (_>>_ ; _<$>_; _⊛_)

------------------------------------------------------------------------
-- Files and Handles

FilePath : Set
FilePath = String

postulate Handle : Set
{-# COMPILED_TYPE Handle System.IO.Handle #-}

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

------------------------------------------------------------------------
-- Opening and closing files

-- Opening files

-- Closing files

postulate hClose : Handle -> IO Unit
{-# COMPILED hClose System.IO.hClose #-}

-- ---------------------------------------------------------------------------
-- Buffering modes

data Maybe' (A : Set) : Set where
    just : A → Maybe' A
    nothing : Maybe' A

{-# COMPILED_DATA Maybe' Maybe Just Nothing #-}

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 → IO Unit
{-# COMPILED hSetBuffering System.IO.hSetBuffering #-}


------------------------------------------------------------------------
-- Text input and output

-- Text input

-- Text output

postulate hPutStr : Handle -> String -> IO Unit
{-# COMPILED hPutStr System.IO.hPutStr #-}

------------------------------------------------------------------------
-- Temporary Files

postulate openTempFile : FilePath -> String -> IO (FilePath ×' Handle)

{-# COMPILED openTempFile System.IO.openTempFile #-}

-----------------------------------------------------------------------
-- (IO.Primitive.putStrLn is for Costring)

postulate putStrLn' : String -> IO Unit
{-# COMPILED putStrLn' System.IO.putStrLn #-}

postulate getLine' : IO String
{-# COMPILED getLine' System.IO.getLine #-}

{-
open import Foreign.Haskell
open import Data.String hiding ( Costring )
open import Data.Char
open import Foreign.Haskell
Costring = Foreign.Haskell.Colist Char
open import Data.Product
open import Category.Monad
open import FFI.Pair

------------------------------------------------------------------------
-- The IO monad
postulate
  IO : Set -> Set

{-# COMPILED_TYPE IO IO #-}

postulate
  return : {A : Set} -> A -> IO A
  _>>=_  : {A B : Set} -> IO A -> (A -> IO B) -> IO B

{-# COMPILED return (\_ -> return :: a -> IO a) #-}
{-# COMPILED _>>=_  (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}

IOMonad : RawMonad IO
IOMonad = record { return = return; _>>=_ = _>>=_ }
open RawMonad IOMonad public using (_>>_ ; _<$>_; _⊛_)


------------------------------------------------------------------------
-- Files and Handles

FilePath : Set
FilePath = String

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

------------------------------------------------------------------------
-- Opening and closing files

-- Opening files

-- Closing files

postulate hClose : Handle -> IO Unit
{-# COMPILED hClose hClose #-}

-- Special cases

postulate
  readFile  : FilePath -> IO Costring
  writeFile : FilePath -> Costring -> IO Unit

{-# COMPILED readFile    System.IO.readFile    #-}
{-# COMPILED writeFile   System.IO.writeFile   #-}


------------------------------------------------------------------------
-- Text input and output

-- Text input

-- Text output

postulate hPutStr : Handle -> String -> IO Unit
{-# COMPILED hPutStr System.IO.hPutStr #-}

-- Special cases for standard input and output

postulate
  getContents : IO Costring
  putStr      : Costring -> IO Unit
  putStrLn    : Costring -> IO Unit

{-# COMPILED getContents System.IO.getContents #-}
{-# COMPILED putStr      System.IO.putStr      #-}
{-# COMPILED putStrLn    System.IO.putStrLn    #-}


-}