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

Declares internal datatypes for Lean environment, declarations, and
certified declarations.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
{-# OPTIONS_HADDOCK not-home #-}
module Language.Lean.Internal.Decl
  ( -- * Environment
    Env(..)
  , EnvPtr
  , OutEnvPtr
  , withEnv
    -- * Declaration
  , Decl
  , DeclPtr
  , OutDeclPtr
  , withDecl
    -- * Certified declaration
  , CertDecl
  , CertDeclPtr
  , OutCertDeclPtr
  , withCertDecl
  ) where

import Foreign

import Language.Lean.Internal.Exception
{-# LINE 35 "src/Language/Lean/Internal/Decl.chs" #-}











------------------------------------------------------------------------
-- Env declaration


{-# LINE 49 "src/Language/Lean/Internal/Decl.chs" #-}


-- | A Lean environment
newtype Env = Env (ForeignPtr Env)

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

-- | Haskell type for @lean_env@ FFI parameters.
type EnvPtr = Ptr (Env)
{-# LINE 59 "src/Language/Lean/Internal/Decl.chs" #-}

-- | Haskell type for @lean_env*@ FFI parameters.
type OutEnvPtr = Ptr (EnvPtr)
{-# LINE 61 "src/Language/Lean/Internal/Decl.chs" #-}


instance IsLeanValue Env (Ptr Env) where
   mkLeanValue = \v -> fmap Env $ newForeignPtr lean_env_del_ptr v

foreign import ccall unsafe "&lean_env_del"
  lean_env_del_ptr :: FunPtr (EnvPtr -> IO ())

------------------------------------------------------------------------
-- Decl declaration


{-# LINE 72 "src/Language/Lean/Internal/Decl.chs" #-}


-- | A Lean declaration
newtype Decl = Decl (ForeignPtr Decl)

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

-- | Haskell type for @lean_decl@ FFI parameters.
type DeclPtr = Ptr (Decl)
{-# LINE 82 "src/Language/Lean/Internal/Decl.chs" #-}


-- | Haskell type for @lean_decl*@ FFI parameters.
type OutDeclPtr = Ptr (DeclPtr)
{-# LINE 85 "src/Language/Lean/Internal/Decl.chs" #-}


instance IsLeanValue Decl (Ptr Decl) where
   mkLeanValue = fmap Decl . newForeignPtr lean_decl_del_ptr

foreign import ccall unsafe "&lean_decl_del"
  lean_decl_del_ptr :: FunPtr (DeclPtr -> IO ())

------------------------------------------------------------------------
-- CertDecl declaration


{-# LINE 96 "src/Language/Lean/Internal/Decl.chs" #-}


-- | A Lean certified declaration
newtype CertDecl = CertDecl (ForeignPtr CertDecl)

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

-- | Haskell type for @lean_cert_decl@ FFI parameters.
type CertDeclPtr = Ptr (CertDecl)
{-# LINE 106 "src/Language/Lean/Internal/Decl.chs" #-}


-- | Haskell type for @lean_cert_decl*@ FFI parameters.
type OutCertDeclPtr = Ptr (CertDeclPtr)
{-# LINE 109 "src/Language/Lean/Internal/Decl.chs" #-}


instance IsLeanValue CertDecl (Ptr CertDecl) where
   mkLeanValue = fmap CertDecl . newForeignPtr lean_cert_decl_del_ptr

foreign import ccall unsafe "&lean_cert_decl_del"
  lean_cert_decl_del_ptr :: FunPtr (CertDeclPtr -> IO ())