-- 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/IOS.chs" #-}
{-|
Module      : Language.Lean.IOS
Copyright   : (c) Galois Inc, 2015
License     : Apache-2
Maintainer  : jhendrix@galois.com, lcasburn@galois.com

Operations for creating and manipulating an 'IOState', an object
for controlling how Lean sends console output to the user.

-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.IOS
  ( IOState
  , type IOStateType(..)
    -- * Standard IOState
  , mkStandardIOState
  , mkStandardIOStateWithOptions
    -- * Buffered IOState
  , mkBufferedIOState
  , mkBufferedIOStateWithOptions
  , getRegularOutput
  , getDiagnosticOutput
  , resetRegularOutput
  , resetDiagnosticOutput
    -- * Operations on IO State
  , IOStateTypeRepr(..)
  , stateTypeRepr
  , getStateOptions
  , setStateOptions
    -- * Operations using IOState
  , ppExpr
  ) where

import Foreign
import Foreign.C
import System.IO.Unsafe
import Unsafe.Coerce (unsafeCoerce)

import Language.Lean.Internal.Decl
{-# LINE 45 "src/Language/Lean/IOS.chs" #-}

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

import Language.Lean.Internal.Expr
{-# LINE 47 "src/Language/Lean/IOS.chs" #-}

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

import Language.Lean.Internal.Options
{-# LINE 49 "src/Language/Lean/IOS.chs" #-}













------------------------------------------------------------------------
-- Standard IOState

-- | Create a standard IO state object with default options.
mkStandardIOState :: IO (IOState 'Standard)
mkStandardIOState = mkStandardIOStateWithOptions emptyOptions

-- | Create a standard IO state object with the given options.
mkStandardIOStateWithOptions :: Options -> IO (IOState 'Standard)
mkStandardIOStateWithOptions o = tryAllocLeanValue $ lean_ios_mk_std o

lean_ios_mk_std :: (Options) -> (OutSomeIOStatePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_ios_mk_std a1 a2 a3 =
  (withOptions) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_ios_mk_std'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- Buffered IOState

-- | Create IO state object that sends the regular and diagnostic output to
-- string buffers with the given options.
mkBufferedIOState :: IO (IOState 'Buffered)
mkBufferedIOState = mkBufferedIOStateWithOptions emptyOptions

-- | Create IO state object that sends the regular and diagnostic output to
-- string buffers with the given options.
mkBufferedIOStateWithOptions :: Options -> IO (IOState 'Buffered)
mkBufferedIOStateWithOptions o = tryAllocLeanValue $ lean_ios_mk_buffered o

lean_ios_mk_buffered :: (Options) -> (OutSomeIOStatePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_ios_mk_buffered a1 a2 a3 =
  (withOptions) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_ios_mk_buffered'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Return the regular output associated with a state.
getRegularOutput :: IOState 'Buffered -> IO String
getRegularOutput s = tryAllocLeanValue $ lean_ios_get_regular s

lean_ios_get_regular :: (BufferedIOState) -> (Ptr CString) -> (OutExceptionPtr) -> IO ((Bool))
lean_ios_get_regular a1 a2 a3 =
  (withBufferedIOState) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_ios_get_regular'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Reset the regular output associated with a state.
resetRegularOutput :: IOState 'Buffered -> IO ()
resetRegularOutput s = runLeanPartialAction $ lean_ios_reset_regular s

lean_ios_reset_regular :: (BufferedIOState) -> (OutExceptionPtr) -> IO ((Bool))
lean_ios_reset_regular a1 a2 =
  (withBufferedIOState) a1 $ \a1' -> 
  let {a2' = id a2} in 
  lean_ios_reset_regular'_ a1' a2' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Return the diagnostic output associated with a state.
getDiagnosticOutput :: IOState 'Buffered -> IO String
getDiagnosticOutput s = tryAllocLeanValue $ lean_ios_get_diagnostic s

lean_ios_get_diagnostic :: (BufferedIOState) -> (Ptr CString) -> (OutExceptionPtr) -> IO ((Bool))
lean_ios_get_diagnostic a1 a2 a3 =
  (withBufferedIOState) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_ios_get_diagnostic'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Clear the diagnostic output associated with a state.
resetDiagnosticOutput :: IOState 'Buffered -> IO ()
resetDiagnosticOutput s = runLeanPartialAction $ lean_ios_reset_diagnostic s

lean_ios_reset_diagnostic :: (BufferedIOState) -> (OutExceptionPtr) -> IO ((Bool))
lean_ios_reset_diagnostic a1 a2 =
  (withBufferedIOState) a1 $ \a1' -> 
  let {a2' = id a2} in 
  lean_ios_reset_diagnostic'_ a1' a2' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- IOState introspection

-- | Flag indicating the type of state.
--
-- This is implemented as a GADT to allow client code to specialize an
-- @IOState@ to the appropriate subtype.
data IOStateTypeRepr (tp :: IOStateType) where
  StandardRepr :: IOStateTypeRepr 'Standard
  BufferedRepr :: IOStateTypeRepr 'Buffered

deriving instance Show (IOStateTypeRepr tp)

-- | Get the type of the channel
stateTypeRepr :: IOState tp -> IOStateTypeRepr tp
stateTypeRepr s
  | lean_ios_is_std (someIOS s) = unsafeCoerce StandardRepr
  | otherwise                   = unsafeCoerce BufferedRepr

-- Return true if this is a IO state
lean_ios_is_std :: (SomeIOState) -> (Bool)
lean_ios_is_std a1 =
  unsafePerformIO $
  (withSomeIOState) a1 $ \a1' -> 
  let {res = lean_ios_is_std'_ a1'} in
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- IOState options

-- | Get the options associated with the state.
getStateOptions :: IOState tp -> IO Options
getStateOptions ios = tryAllocLeanValue $ lean_ios_get_options (someIOS ios)

lean_ios_get_options :: (SomeIOState) -> (OutOptionsPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_ios_get_options a1 a2 a3 =
  (withSomeIOState) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_ios_get_options'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Set the options associated with the state.
setStateOptions :: IOState tp -> Options -> IO ()
setStateOptions ios ops = runLeanPartialAction $ lean_ios_set_options (someIOS ios) ops

lean_ios_set_options :: (SomeIOState) -> (Options) -> (OutExceptionPtr) -> IO ((Bool))
lean_ios_set_options a1 a2 a3 =
  (withSomeIOState) a1 $ \a1' -> 
  (withOptions) a2 $ \a2' -> 
  let {a3' = id a3} in 
  lean_ios_set_options'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- Pretty print expression

-- | Pretty print an expression
ppExpr :: Env -> IOState tp -> Expr -> IO String
ppExpr env s e = tryAllocLeanValue $ lean_expr_to_pp_string env (someIOS s) e

lean_expr_to_pp_string :: (Env) -> (SomeIOState) -> (Expr) -> (Ptr CString) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_to_pp_string a1 a2 a3 a4 a5 =
  (withEnv) a1 $ \a1' -> 
  (withSomeIOState) a2 $ \a2' -> 
  (withExpr) a3 $ \a3' -> 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_expr_to_pp_string'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_mk_std"
  lean_ios_mk_std'_ :: ((OptionsPtr) -> ((OutSomeIOStatePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_mk_buffered"
  lean_ios_mk_buffered'_ :: ((OptionsPtr) -> ((OutSomeIOStatePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_get_regular"
  lean_ios_get_regular'_ :: ((Ptr (SomeIOState)) -> ((Ptr (Ptr CChar)) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_reset_regular"
  lean_ios_reset_regular'_ :: ((Ptr (SomeIOState)) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_get_diagnostic"
  lean_ios_get_diagnostic'_ :: ((Ptr (SomeIOState)) -> ((Ptr (Ptr CChar)) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_reset_diagnostic"
  lean_ios_reset_diagnostic'_ :: ((Ptr (SomeIOState)) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_is_std"
  lean_ios_is_std'_ :: ((Ptr (SomeIOState)) -> CInt)

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_get_options"
  lean_ios_get_options'_ :: ((Ptr (SomeIOState)) -> ((OutOptionsPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_ios_set_options"
  lean_ios_set_options'_ :: ((Ptr (SomeIOState)) -> ((OptionsPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/IOS.chs.h lean_expr_to_pp_string"
  lean_expr_to_pp_string'_ :: ((EnvPtr) -> ((Ptr (SomeIOState)) -> ((ExprPtr) -> ((Ptr (Ptr CChar)) -> ((OutExceptionPtr) -> (IO CInt))))))