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

Internal declarations for ConstraintSeq and Typechecker.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
{-# OPTIONS_HADDOCK not-home #-}
module Language.Lean.Internal.Typechecker
  ( Typechecker
  , ConstraintSeq
    -- * Foreign exports
  , ConstraintSeqPtr
  , OutConstraintSeqPtr
  , withConstraintSeq
  , TypecheckerPtr
  , OutTypecheckerPtr
  , withTypechecker
  ) where

import Foreign

import Language.Lean.Internal.Exception
{-# LINE 28 "src/Language/Lean/Internal/Typechecker.chs" #-}













------------------------------------------------------------------------
-- Constraint Sequence


{-# LINE 44 "src/Language/Lean/Internal/Typechecker.chs" #-}


-- | A sequence of constraints
newtype ConstraintSeq = ConstraintSeq (ForeignPtr ConstraintSeq)

-- | Get access to @lean_cnstr_seq@ within IO action.
withConstraintSeq :: ConstraintSeq -> (Ptr ConstraintSeq -> IO a) -> IO a
withConstraintSeq (ConstraintSeq o) = withForeignPtr $! o

-- | Pointer to @lean_cnstr_seq@ for inputs to Lean functions.
type ConstraintSeqPtr = Ptr (ConstraintSeq)
{-# LINE 54 "src/Language/Lean/Internal/Typechecker.chs" #-}

-- | Pointer to @lean_cnstr_seq@ for outputs from Lean functions.
type OutConstraintSeqPtr = Ptr (ConstraintSeqPtr)
{-# LINE 56 "src/Language/Lean/Internal/Typechecker.chs" #-}


instance IsLeanValue ConstraintSeq (Ptr ConstraintSeq) where
  mkLeanValue = fmap ConstraintSeq . newForeignPtr lean_cnstr_seq_del_ptr

foreign import ccall unsafe "&lean_cnstr_seq_del"
  lean_cnstr_seq_del_ptr :: FunPtr (ConstraintSeqPtr -> IO ())

------------------------------------------------------------------------
-- Typechecker

-- | A Lean typechecker
newtype Typechecker = Typechecker (ForeignPtr Typechecker)

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


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


-- | Haskell type for @lean_type_checker@ FFI parameters.
type TypecheckerPtr = Ptr (Typechecker)
{-# LINE 77 "src/Language/Lean/Internal/Typechecker.chs" #-}

-- | Haskell type for @lean_type_checker*@ FFI parameters.
type OutTypecheckerPtr = Ptr (TypecheckerPtr)
{-# LINE 79 "src/Language/Lean/Internal/Typechecker.chs" #-}


instance IsLeanValue Typechecker (Ptr Typechecker) where
  mkLeanValue = fmap Typechecker . newForeignPtr lean_type_checker_del_ptr

foreign import ccall unsafe "&lean_type_checker_del"
  lean_type_checker_del_ptr :: FunPtr (TypecheckerPtr -> IO ())