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

Operations for Lean options
-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Options
  ( Options
  , emptyOptions
  , joinOptions
  , nullOptions
  , containsOption
  , boolOption
  , doubleOption
  , intOption
  , uintOption
  , stringOption
  ) where

import Control.Exception (throw)
import Control.Lens
import Data.Maybe (fromMaybe)
import Foreign
import Foreign.C
import System.IO.Unsafe

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

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

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

import Language.Lean.Internal.String
{-# LINE 40 "src/Language/Lean/Options.chs" #-}








lean_options_set_bool :: (Options) -> (Name) -> (Bool) -> (Ptr OptionsPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_set_bool a1 a2 a3 a4 a5 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = fromBool a3} in 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_options_set_bool'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


lean_options_set_int :: (Options) -> (Name) -> (Int32) -> (Ptr OptionsPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_set_int a1 a2 a3 a4 a5 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = fromIntegral a3} in 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_options_set_int'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


lean_options_set_unsigned :: (Options) -> (Name) -> (Word32) -> (Ptr OptionsPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_set_unsigned a1 a2 a3 a4 a5 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = fromIntegral a3} in 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_options_set_unsigned'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


lean_options_set_double :: (Options) -> (Name) -> (Double) -> (Ptr OptionsPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_set_double a1 a2 a3 a4 a5 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = realToFrac a3} in 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_options_set_double'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


lean_options_set_string :: (Options) -> (Name) -> (String) -> (Ptr OptionsPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_set_string a1 a2 a3 a4 a5 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  withLeanStringPtr a3 $ \a3' -> 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_options_set_string'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Returns true if options are empty.
nullOptions :: (Options) -> (Bool)
nullOptions a1 =
  unsafePerformIO $
  (withOptions) a1 $ \a1' -> 
  let {res = nullOptions'_ a1'} in
  let {res' = toBool res} in
  return (res')

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


-- | Indicate whether name is set in the lean options.
containsOption :: (Options) -> (Name) -> (Bool)
containsOption a1 a2 =
  unsafePerformIO $
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {res = containsOption'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

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


lean_options_get_bool :: (Options) -> (Name) -> (Ptr CInt) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_get_bool a1 a2 a3 a4 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_options_get_bool'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


lean_options_get_int :: (Options) -> (Name) -> (Ptr CInt) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_get_int a1 a2 a3 a4 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_options_get_int'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


lean_options_get_unsigned :: (Options) -> (Name) -> (Ptr CUInt) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_get_unsigned a1 a2 a3 a4 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_options_get_unsigned'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


lean_options_get_double :: (Options) -> (Name) -> (Ptr CDouble) -> (OutExceptionPtr) -> IO ((Bool))
lean_options_get_double a1 a2 a3 a4 =
  (withOptions) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_options_get_double'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


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

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


-- | Retrieves a value for a Lean option
optionsGet :: (LeanPartialFn a -> b)
           -> (Options -> Name -> LeanPartialFn a)
           -> Options
           -> Name
           -> Maybe b
optionsGet tryGetVal leanGetter o nm
  | o `containsOption` nm = Just (tryGetVal $ leanGetter o nm)
  | otherwise = Nothing

-- | Sets a Lean option with a new value
optionsSet :: (Options -> Name -> a -> LeanPartialFn OptionsPtr)
           -> Options
           -> Name
           -> a
           -> Options
optionsSet leanSetter o nm v = tryGetLeanValue $ leanSetter o nm v

-- | Lens for getting and setting boolean options without
--   rewriting equivalent values
simpleLensEq :: (Eq a) => (s -> Name -> Maybe a) -> (s -> Name -> a -> s) -> Name -> Simple Lens s a
simpleLensEq getter setter nm f o = fmap setFun (f oldVal)
  where
    maybeVal = getter o nm
    -- This will only throw an error if f demands oldVal
    oldVal = fromMaybe (throw (leanOtherException msg)) maybeVal
      where msg = "options object does not contain entry " ++ show nm
    setFun newVal
     | Just v <- maybeVal, v == newVal = o
     | otherwise = setter o nm newVal

-- | Access the lean option with the given name as a Boolean.
boolOption :: Name -> Simple Lens Options Bool
boolOption = simpleLensEq optGet optSet
  where
    optGet = optionsGet tryGetLeanValue lean_options_get_bool
    optSet = optionsSet lean_options_set_bool

-- | Access the lean option with the given name as a signed integer.
intOption :: Name -> Simple Lens Options Int32
intOption = simpleLensEq optGet optSet
  where
    optGet = optionsGet tryGetLeanValue lean_options_get_int
    optSet = optionsSet lean_options_set_int

-- | Access the lean option with the given name as an unsigned integer.
uintOption :: Name -> Simple Lens Options Word32
uintOption = simpleLensEq optGet optSet
  where
    optGet = optionsGet tryGetLeanValue lean_options_get_unsigned
    optSet = optionsSet lean_options_set_unsigned

-- | Access the lean option with the given name as a floating point value.
doubleOption :: Name -> Simple Lens Options Double
doubleOption = simpleLensEq optGet optSet
  where
    optGet = optionsGet tryGetLeanValue lean_options_get_double
    optSet = optionsSet lean_options_set_double

-- | Access the lean option with the given name as a string.
stringOption :: Name -> Simple Lens Options String
stringOption = simpleLensEq optGet optSet
  where
    optGet = optionsGet tryGetLeanValue lean_options_get_string
    optSet = optionsSet lean_options_set_string

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

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

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

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

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

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

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

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

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

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

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

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