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

Internal declarations for Lean options and typeclass instances
for @Options@ type.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Trustworthy #-}
{-# OPTIONS_HADDOCK not-home #-}
module Language.Lean.Internal.Options
  ( Options
  , emptyOptions
  , joinOptions
    -- * Low level FFI interfaces.
  , OptionsPtr
  , OutOptionsPtr
  , withOptions
  ) where

import Foreign
import Foreign.C
import System.IO.Unsafe

import Language.Lean.Internal.Exception
{-# LINE 29 "src/Language/Lean/Internal/Options.chs" #-}

import Language.Lean.Internal.Exception.Unsafe







-- Use nocode and manually generate for haddock.

{-# LINE 39 "src/Language/Lean/Internal/Options.chs" #-}


-- | A set of Lean configuration options
newtype Options = Options (ForeignPtr Options)

-- | Function @c2hs@ uses to pass @Options@ values to Lean
withOptions :: Options -> (Ptr Options -> IO a) -> IO a
withOptions (Options o) = withForeignPtr $! o

-- | Haskell type for @lean_options@ FFI parameters.
type OptionsPtr = Ptr (Options)
{-# LINE 49 "src/Language/Lean/Internal/Options.chs" #-}

-- | Haskell type for @lean_options*@ FFI parameters.
type OutOptionsPtr = Ptr (OptionsPtr)
{-# LINE 51 "src/Language/Lean/Internal/Options.chs" #-}


foreign import ccall unsafe "&lean_options_del"
  lean_options_del_ptr :: FunPtr (OptionsPtr -> IO ())

instance IsLeanValue Options (Ptr Options) where
  mkLeanValue = fmap Options . newForeignPtr lean_options_del_ptr

------------------------------------------------------------------------
-- Monoid instance

instance Monoid Options where
  mempty  = emptyOptions
  mappend = joinOptions

-- | An empty set of options
emptyOptions :: Options
emptyOptions = tryGetLeanValue lean_options_mk_empty

-- | Combine two options where the assignments from the second
-- argument override the assignments from the first.
joinOptions :: Options -> Options -> Options
joinOptions x y = tryGetLeanValue $ lean_options_join x y

lean_options_mk_empty :: (OutOptionsPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_mk_empty a1 a2 =
  let {a1' = id a1} in 
  let {a2' = id a2} in 
  lean_options_mk_empty'_ a1' a2' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 78 "src/Language/Lean/Internal/Options.chs" #-}


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

{-# LINE 85 "src/Language/Lean/Internal/Options.chs" #-}


------------------------------------------------------------------------
-- Eq instance

instance Eq Options where
  (==) = lean_options_eq

lean_options_eq :: (Options) -> (Options) -> (Bool)
lean_options_eq a1 a2 =
  unsafePerformIO $
  (withOptions) a1 $ \a1' -> 
  (withOptions) a2 $ \a2' -> 
  let {res = lean_options_eq'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 94 "src/Language/Lean/Internal/Options.chs" #-}


------------------------------------------------------------------------
-- Show instance

instance Show Options where
  show = showOption

showOption :: Options -> String
showOption x = tryGetLeanValue $ lean_options_to_string x

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

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


foreign import ccall unsafe "Language/Lean/Internal/Options.chs.h lean_options_mk_empty"
  lean_options_mk_empty'_ :: ((OutOptionsPtr) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/Internal/Options.chs.h lean_options_join"
  lean_options_join'_ :: ((OptionsPtr) -> ((OptionsPtr) -> ((OutOptionsPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Options.chs.h lean_options_eq"
  lean_options_eq'_ :: ((OptionsPtr) -> ((OptionsPtr) -> CInt))

foreign import ccall unsafe "Language/Lean/Internal/Options.chs.h lean_options_to_string"
  lean_options_to_string'_ :: ((OptionsPtr) -> ((Ptr (Ptr CChar)) -> ((OutExceptionPtr) -> (IO CInt))))