-- GENERATED by C->Haskell Compiler, version 0.25.2 Snowboundest, 31 Oct 2014 (Haskell)
-- Edit the ORIGNAL .chs file instead!


{-# LINE 1 "src/Language/Lean/Internal/IOS.chs" #-}
{-|
Module      : Language.Lean.Internal.IOS
Copyright   : (c) Galois Inc, 2015
License     : Apache-2
Maintainer  : jhendrix@galois.com, lcasburn@galois.com

Internal declarations for IOState.
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_HADDOCK not-home #-}
module Language.Lean.Internal.IOS
  ( IOState
  , withIOState
  , someIOS
  , type IOStateType(..)
  , SomeIOState
  , SomeIOStatePtr
  , OutSomeIOStatePtr
  , withSomeIOState
  , BufferedIOState
  , withBufferedIOState
  ) where

import Foreign
import System.IO (stderr, stdout)


import Language.Lean.Internal.Exception
{-# LINE 36 "src/Language/Lean/Internal/IOS.chs" #-}













_unused :: a
_unused = undefined stderr stdout

-- | Internal state used for bindings
newtype SomeIOState = SomeIOState (ForeignPtr SomeIOState)

foreign import ccall unsafe "&lean_ios_del"
  lean_ios_del_ptr :: FunPtr (Ptr SomeIOState -> IO ())


-- | This describes the type of the @IOState@.
data IOStateType
   = Standard -- ^ A standard 'IOState'
   | Buffered -- ^ A buffered 'IOState'

-- | The IO State object
--
-- Lean uses two channels for sending output to the user:
--
--  * A /regular/ output channel, which consists of messages normally
--    printed to 'stdout'.
--  * A /diagnostic/ output channel, which consists of debugging
--    messages that are normally printed to 'stderr'.
--
-- This module currently provides two different 'IOState' types:
--
--  * A /standard/ IO state that sends regular output to 'stdout' and
--    diagnostic output to 'stderr'.
--  * A /buffered/ IO state type that stores output internally, and
--    provides methods for getting output as strings.
--
-- To prevent users from accidentally using the wrong type of output,
-- the 'IOState' has an extra type-level parameter used to
-- indicate the type of channel.  Most Lean operations support both
-- types of channels and either can be used.  Operations specific
-- to a particular channel can use this type parameter to ensure
-- users do not call the function on the wrong type of channel.  In
-- addition, we provide a function @stateTypeRepr@ to allow users
-- to determine the type of channel.
newtype IOState (tp :: IOStateType) = IOState (ForeignPtr SomeIOState)

-- | Lift an arbitray IOState to SomeIOState
someIOS :: IOState tp -> SomeIOState
someIOS (IOState p) = SomeIOState (castForeignPtr p)

instance IsLeanValue (IOState tp) (Ptr SomeIOState) where
  mkLeanValue = fmap IOState . newForeignPtr lean_ios_del_ptr

-- | Run a computation with an io state.
withIOState :: IOState tp -> (Ptr SomeIOState -> IO a) -> IO a
withIOState (IOState ptr) f = seq ptr $ withForeignPtr ptr (f . castPtr)

-- | Type synonym for @c2hs@ to use specifically for functions that
-- expected buffered IO state.
type BufferedIOState = IOState 'Buffered

-- | Function @c2hs@ uses to pass 'BufferedIOState' values to Lean
withBufferedIOState :: IOState 'Buffered -> (Ptr SomeIOState -> IO a) -> IO a
withBufferedIOState = withIOState


{-# LINE 109 "src/Language/Lean/Internal/IOS.chs" #-}


-- | Function @c2hs@ uses to pass 'SomeIOState' values to Lean
withSomeIOState :: SomeIOState -> (Ptr SomeIOState -> IO a) -> IO a
withSomeIOState (SomeIOState p) f = seq p $ withForeignPtr p (f . castPtr)


{-# LINE 115 "src/Language/Lean/Internal/IOS.chs" #-}


-- | Haskell type for @lean_ios@ FFI parameters.
type SomeIOStatePtr = Ptr SomeIOState

-- | Haskell type for @lean_ios*@ FFI parameters.
type OutSomeIOStatePtr = Ptr (SomeIOStatePtr)
{-# LINE 121 "src/Language/Lean/Internal/IOS.chs" #-}