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

Internal declarations for inductive types and declarations.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Trustworthy #-}
{-# OPTIONS_HADDOCK not-home #-}
module Language.Lean.Internal.Inductive
  ( InductiveType
  , InductiveTypePtr
  , OutInductiveTypePtr
  , withInductiveType
  , ListInductiveType
  , ListInductiveTypePtr
  , OutListInductiveTypePtr
  , withListInductiveType
  , InductiveDecl
  , InductiveDeclPtr
  , OutInductiveDeclPtr
  , withInductiveDecl
  ) where

import Control.Lens (toListOf)
import Foreign
import Foreign.C
import Language.Lean.List
import System.IO.Unsafe

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

import Language.Lean.Internal.Exception.Unsafe











------------------------------------------------------------------------
-- InductiveType declarations


{-# LINE 52 "src/Language/Lean/Internal/Inductive.chs" #-}


-- | An inductive type
newtype InductiveType = InductiveType (ForeignPtr InductiveType)

-- | Access raw @lean_inductive_type@ within IO action.
withInductiveType :: InductiveType -> (Ptr InductiveType -> IO a) -> IO a
withInductiveType (InductiveType o) = withForeignPtr $! o

-- | Haskell type for @lean_inductive_type@ FFI parameters.
type InductiveTypePtr = Ptr (InductiveType)
{-# LINE 62 "src/Language/Lean/Internal/Inductive.chs" #-}

-- | Haskell type for @lean_inductive_type*@ FFI parameters.
type OutInductiveTypePtr = Ptr (InductiveTypePtr)
{-# LINE 64 "src/Language/Lean/Internal/Inductive.chs" #-}


instance IsLeanValue InductiveType (Ptr InductiveType) where
  mkLeanValue = fmap InductiveType . newForeignPtr lean_inductive_type_del_ptr

foreign import ccall unsafe "&lean_inductive_type_del"
  lean_inductive_type_del_ptr :: FunPtr (InductiveTypePtr -> IO ())

------------------------------------------------------------------------
-- List InductiveType declarations

-- | A list of inductive types (constructor not actually exported)
newtype instance List InductiveType = ListInductiveType (ForeignPtr (List InductiveType))


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


-- | Haskell type for @lean_list_inductive_type@ FFI parameters.
type ListInductiveTypePtr = Ptr (ListInductiveType)
{-# LINE 81 "src/Language/Lean/Internal/Inductive.chs" #-}

-- | Haskell type for @lean_list_inductive_type*@ FFI parameters.
type OutListInductiveTypePtr = Ptr (ListInductiveTypePtr)
{-# LINE 83 "src/Language/Lean/Internal/Inductive.chs" #-}


-- | Synonym for @List InductiveType@
type ListInductiveType = List InductiveType

-- | Access raw @lean_list_inductive_type@ within IO action.
withListInductiveType :: List InductiveType -> (Ptr (List InductiveType) -> IO a) -> IO a
withListInductiveType (ListInductiveType p) = withForeignPtr $! p

instance IsLeanValue (List InductiveType) (Ptr (List InductiveType)) where
  mkLeanValue = fmap ListInductiveType . newForeignPtr lean_list_inductive_type_del_ptr

foreign import ccall unsafe "&lean_list_inductive_type_del"
  lean_list_inductive_type_del_ptr :: FunPtr (ListInductiveTypePtr -> IO ())

------------------------------------------------------------------------
-- List InductiveType Eq instance

instance Eq (List InductiveType) where
  (==) = lean_list_inductive_type_eq

lean_list_inductive_type_eq :: (ListInductiveType) -> (ListInductiveType) -> (Bool)
lean_list_inductive_type_eq a1 a2 =
  unsafePerformIO $
  (withListInductiveType) a1 $ \a1' -> 
  (withListInductiveType) a2 $ \a2' -> 
  let {res = lean_list_inductive_type_eq'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 107 "src/Language/Lean/Internal/Inductive.chs" #-}


------------------------------------------------------------------------
-- List InductiveType IsListIso instance

instance IsListIso (List InductiveType) where
  nil = tryGetLeanValue $ lean_list_inductive_type_mk_nil
  h <| r = tryGetLeanValue $ lean_list_inductive_type_mk_cons h r

  listView l =
    if lean_list_inductive_type_is_cons l then
      tryGetLeanValue (lean_list_inductive_type_head l)
        :< tryGetLeanValue (lean_list_inductive_type_tail l)
    else
      Nil

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

{-# LINE 126 "src/Language/Lean/Internal/Inductive.chs" #-}


lean_list_inductive_type_mk_cons :: (InductiveType) -> (ListInductiveType) -> (OutListInductiveTypePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_inductive_type_mk_cons a1 a2 a3 a4 =
  (withInductiveType) a1 $ \a1' -> 
  (withListInductiveType) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_list_inductive_type_mk_cons'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 133 "src/Language/Lean/Internal/Inductive.chs" #-}


lean_list_inductive_type_is_cons :: (ListInductiveType) -> (Bool)
lean_list_inductive_type_is_cons a1 =
  unsafePerformIO $
  (withListInductiveType) a1 $ \a1' -> 
  let {res = lean_list_inductive_type_is_cons'_ a1'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 137 "src/Language/Lean/Internal/Inductive.chs" #-}


lean_list_inductive_type_head :: (ListInductiveType) -> (OutInductiveTypePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_inductive_type_head a1 a2 a3 =
  (withListInductiveType) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_list_inductive_type_head'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 143 "src/Language/Lean/Internal/Inductive.chs" #-}


lean_list_inductive_type_tail :: (ListInductiveType) -> (OutListInductiveTypePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_inductive_type_tail a1 a2 a3 =
  (withListInductiveType) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_list_inductive_type_tail'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 149 "src/Language/Lean/Internal/Inductive.chs" #-}


------------------------------------------------------------------------
-- List InductiveType IsList instance

instance IsList (List InductiveType) where
  type Item (List InductiveType) = InductiveType
  fromList = fromListDefault
  toList = toListOf traverseList

------------------------------------------------------------------------
-- InductiveDecl declarations


{-# LINE 162 "src/Language/Lean/Internal/Inductive.chs" #-}


-- | An inductive declaration
--
-- A single inductive declaration may define one or more Lean inductive
-- types.  The inductive types must have the same parameters.
newtype InductiveDecl = InductiveDecl (ForeignPtr InductiveDecl)

-- | Access raw @lean_inductive_decl@ within IO action.
withInductiveDecl :: InductiveDecl -> (Ptr InductiveDecl -> IO a) -> IO a
withInductiveDecl (InductiveDecl o) = withForeignPtr $! o

-- | Haskell type for @lean_inductive_decl@ FFI parameters.
type InductiveDeclPtr = Ptr (InductiveDecl)
{-# LINE 175 "src/Language/Lean/Internal/Inductive.chs" #-}

-- | Haskell type for @lean_inductive_decl*@ FFI parameters.
type OutInductiveDeclPtr = Ptr (InductiveDeclPtr)
{-# LINE 177 "src/Language/Lean/Internal/Inductive.chs" #-}


instance IsLeanValue InductiveDecl (Ptr InductiveDecl) where
  mkLeanValue = fmap InductiveDecl . newForeignPtr lean_inductive_decl_del_ptr

foreign import ccall unsafe "&lean_inductive_decl_del"
  lean_inductive_decl_del_ptr :: FunPtr (InductiveDeclPtr -> IO ())

foreign import ccall unsafe "Language/Lean/Internal/Inductive.chs.h lean_list_inductive_type_eq"
  lean_list_inductive_type_eq'_ :: ((ListInductiveTypePtr) -> ((ListInductiveTypePtr) -> CInt))

foreign import ccall unsafe "Language/Lean/Internal/Inductive.chs.h lean_list_inductive_type_mk_nil"
  lean_list_inductive_type_mk_nil'_ :: ((OutListInductiveTypePtr) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/Internal/Inductive.chs.h lean_list_inductive_type_mk_cons"
  lean_list_inductive_type_mk_cons'_ :: ((InductiveTypePtr) -> ((ListInductiveTypePtr) -> ((OutListInductiveTypePtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Inductive.chs.h lean_list_inductive_type_is_cons"
  lean_list_inductive_type_is_cons'_ :: ((ListInductiveTypePtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Internal/Inductive.chs.h lean_list_inductive_type_head"
  lean_list_inductive_type_head'_ :: ((ListInductiveTypePtr) -> ((OutInductiveTypePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Internal/Inductive.chs.h lean_list_inductive_type_tail"
  lean_list_inductive_type_tail'_ :: ((ListInductiveTypePtr) -> ((OutListInductiveTypePtr) -> ((OutExceptionPtr) -> (IO CInt))))