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

Operations for creating inductive types and declarations.
-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Inductive
  ( -- * Inductive type
    InductiveType
  , inductiveType
  , inductiveTypeName
  , inductiveTypeType
  , inductiveTypeConstructors
  , recursorName
    -- * Inductive declarations
  , InductiveDecl
  , inductiveDecl
  , inductiveDeclUnivParams
  , inductiveDeclNumParams
  , inductiveDeclTypes
    -- * Environment operations
  , addInductiveDecl
  , lookupInductiveDecl
  , lookupConstructorInductiveTypeName
  , lookupRecursorInductiveTypeName
  , lookupInductiveTypeNumIndices
  , lookupInductiveTypeNumMinorPremises
  , inductiveTypeHasDepElim
  ) where

import Foreign
import Foreign.C
import Language.Lean.List

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

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

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

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

import Language.Lean.Internal.Name
{-# LINE 44 "src/Language/Lean/Inductive.chs" #-}












------------------------------------------------------------------------
-- Constructing InductiveType

-- | Creates an inductive type
inductiveType :: Name -- ^ Name of the inductive type
              -> Expr -- ^ Type of the inductive type
              -> List Expr -- ^ Constructors (must be a list of local constants)
              -> InductiveType
inductiveType n t cs = tryGetLeanValue $ lean_inductive_type_mk n t cs

lean_inductive_type_mk :: (Name) -> (Expr) -> (ListExpr) -> (OutInductiveTypePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_inductive_type_mk a1 a2 a3 a4 a5 =
  (withName) a1 $ \a1' -> 
  (withExpr) a2 $ \a2' -> 
  (withListExpr) a3 $ \a3' -> 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_inductive_type_mk'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- Inductive Types

-- | Get the name of a inductive type.
inductiveTypeName :: InductiveType -> Name
inductiveTypeName tp = tryGetLeanValue $ lean_inductive_type_get_name tp

lean_inductive_type_get_name :: (InductiveType) -> (OutNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_inductive_type_get_name a1 a2 a3 =
  (withInductiveType) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_inductive_type_get_name'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Get the type of a inductive type.
inductiveTypeType :: InductiveType -> Expr
inductiveTypeType tp = tryGetLeanValue $ lean_inductive_type_get_type tp

lean_inductive_type_get_type :: (InductiveType) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_inductive_type_get_type a1 a2 a3 =
  (withInductiveType) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_inductive_type_get_type'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Get the list of constructors associated with the given inductive type.
inductiveTypeConstructors :: InductiveType -> List Expr
inductiveTypeConstructors tp = tryGetLeanValue $ lean_inductive_type_get_constructors tp

lean_inductive_type_get_constructors :: (InductiveType) -> (OutListExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_inductive_type_get_constructors a1 a2 a3 =
  (withInductiveType) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_inductive_type_get_constructors'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- recursorName

-- | Get the name of the recursor (aka eliminator) associated with a inductive type with
-- given name.
recursorName :: Name -> Name
recursorName n = tryGetLeanValue $ lean_get_recursor_name n

lean_get_recursor_name :: (Name) -> (OutNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_get_recursor_name a1 a2 a3 =
  (withName) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_get_recursor_name'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- Constructing InductiveDecls

-- | A inductive datatype declaration
--
-- The remaining inductive datatype arguments are treated as indices.
inductiveDecl :: List Name -- ^ Universe parameters
              -> Word32 -- ^ Number of parameters
              -> List InductiveType -- ^ List of inductive types
              -> InductiveDecl
inductiveDecl ps n types = tryGetLeanValue $ lean_inductive_decl_mk ps n types

lean_inductive_decl_mk :: (ListName) -> (Word32) -> (ListInductiveType) -> (OutInductiveDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_inductive_decl_mk a1 a2 a3 a4 a5 =
  (withListName) a1 $ \a1' -> 
  let {a2' = fromIntegral a2} in 
  (withListInductiveType) a3 $ \a3' -> 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_inductive_decl_mk'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- InductiveDecl projections

-- | Get the list of universe parameter names for the given inductive declaration.
inductiveDeclUnivParams :: InductiveDecl -> List Name
inductiveDeclUnivParams d = tryGetLeanValue $ lean_inductive_decl_get_univ_params d

lean_inductive_decl_get_univ_params :: (InductiveDecl) -> (OutListNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_inductive_decl_get_univ_params a1 a2 a3 =
  (withInductiveDecl) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_inductive_decl_get_univ_params'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Get the number of parameters for the in the declaration.
inductiveDeclNumParams :: InductiveDecl -> Word32
inductiveDeclNumParams d = tryGetLeanValue $ lean_inductive_decl_get_num_params d

lean_inductive_decl_get_num_params :: (InductiveDecl) -> (Ptr CUInt) -> (OutExceptionPtr) -> IO ((Bool))
lean_inductive_decl_get_num_params a1 a2 a3 =
  (withInductiveDecl) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_inductive_decl_get_num_params'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Get  the list of inductive types in the inductive declaration
inductiveDeclTypes :: InductiveDecl -> List InductiveType
inductiveDeclTypes d = tryGetLeanValue $ lean_inductive_decl_get_types d

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

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


------------------------------------------------------------------------
-- InductiveDecl operations

-- | Add the inductive declaration to the given environment.
addInductiveDecl :: InductiveDecl -> Env -> Env
addInductiveDecl d e = tryGetLeanValue $ lean_env_add_inductive e d

lean_env_add_inductive :: (Env) -> (InductiveDecl) -> (OutEnvPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_add_inductive a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withInductiveDecl) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_env_add_inductive'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Return the inductive declaration that introduced type with the given
-- name in the environment (or 'Nothing' if no inductive type by that name exists).
lookupInductiveDecl :: Env -> Name -> Maybe InductiveDecl
lookupInductiveDecl e nm = tryGetLeanMaybeValue $ lean_env_is_inductive_type e nm

lean_env_is_inductive_type :: (Env) -> (Name) -> (OutInductiveDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_is_inductive_type a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_env_is_inductive_type'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | If the given name is a constructor in the envionment, this returns
-- the name of the associated inductive type.
--
-- If the name is not a constructor, then this returns 'Nothing'.
lookupConstructorInductiveTypeName :: Env -> Name -> Maybe Name
lookupConstructorInductiveTypeName e nm =
  tryGetLeanMaybeValue $ lean_env_is_constructor e nm

lean_env_is_constructor :: (Env) -> (Name) -> (OutNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_is_constructor a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_env_is_constructor'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | If the given name is a recursor in the given environment, this returns the
-- name of the associated inductive type.
--
-- If the name is not a recursor, then this returns 'Nothing'.
lookupRecursorInductiveTypeName :: Env -> Name -> Maybe Name
lookupRecursorInductiveTypeName e nm = tryGetLeanMaybeValue $ lean_env_is_recursor e nm

lean_env_is_recursor :: (Env) -> (Name) -> (OutNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_is_recursor a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_env_is_recursor'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Given the name of an inductive type in the environment, this returns
-- the number of indices.
--
-- If the name is not an inductive type, then this returns 'Nothing'.
lookupInductiveTypeNumIndices :: Env -> Name -> Maybe Word32
lookupInductiveTypeNumIndices e nm =
  tryGetLeanMaybeValue $ lean_env_get_inductive_type_num_indices e nm

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

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


-- | Given the name of an inductive type in the environment, this returns
-- the number of minor premises for the recursor associated to this type.
--
-- If the name is not an inductive type, then this returns 'Nothing'.
lookupInductiveTypeNumMinorPremises :: Env -> Name -> Maybe Word32
lookupInductiveTypeNumMinorPremises e nm =
  tryGetLeanMaybeValue $ lean_env_get_inductive_type_num_minor_premises e nm

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

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


-- | Given a name, this returns true if the name is for a inductive
-- type that supports dependent elimination.
inductiveTypeHasDepElim :: Env -> Name -> Bool
inductiveTypeHasDepElim e nm =
  tryGetLeanValue $ lean_env_get_inductive_type_has_dep_elim e nm

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

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


foreign import ccall unsafe "Language/Lean/Inductive.chs.h lean_inductive_type_mk"
  lean_inductive_type_mk'_ :: ((NamePtr) -> ((ExprPtr) -> ((ListExprPtr) -> ((OutInductiveTypePtr) -> ((OutExceptionPtr) -> (IO CInt))))))

foreign import ccall unsafe "Language/Lean/Inductive.chs.h lean_inductive_type_get_name"
  lean_inductive_type_get_name'_ :: ((InductiveTypePtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Inductive.chs.h lean_inductive_type_get_type"
  lean_inductive_type_get_type'_ :: ((InductiveTypePtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Inductive.chs.h lean_inductive_type_get_constructors"
  lean_inductive_type_get_constructors'_ :: ((InductiveTypePtr) -> ((OutListExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Inductive.chs.h lean_get_recursor_name"
  lean_get_recursor_name'_ :: ((NamePtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Inductive.chs.h lean_inductive_decl_mk"
  lean_inductive_decl_mk'_ :: ((ListNamePtr) -> (CUInt -> ((ListInductiveTypePtr) -> ((OutInductiveDeclPtr) -> ((OutExceptionPtr) -> (IO CInt))))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_inductive_decl_get_univ_params"
  lean_inductive_decl_get_univ_params'_ :: ((InductiveDeclPtr) -> ((OutListNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_inductive_decl_get_num_params"
  lean_inductive_decl_get_num_params'_ :: ((InductiveDeclPtr) -> ((Ptr CUInt) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_inductive_decl_get_types"
  lean_inductive_decl_get_types'_ :: ((InductiveDeclPtr) -> ((OutListInductiveTypePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_env_add_inductive"
  lean_env_add_inductive'_ :: ((EnvPtr) -> ((InductiveDeclPtr) -> ((OutEnvPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_env_is_inductive_type"
  lean_env_is_inductive_type'_ :: ((EnvPtr) -> ((NamePtr) -> ((OutInductiveDeclPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_env_is_constructor"
  lean_env_is_constructor'_ :: ((EnvPtr) -> ((NamePtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_env_is_recursor"
  lean_env_is_recursor'_ :: ((EnvPtr) -> ((NamePtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_env_get_inductive_type_num_indices"
  lean_env_get_inductive_type_num_indices'_ :: ((EnvPtr) -> ((NamePtr) -> ((Ptr CUInt) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_env_get_inductive_type_num_minor_premises"
  lean_env_get_inductive_type_num_minor_premises'_ :: ((EnvPtr) -> ((NamePtr) -> ((Ptr CUInt) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall safe "Language/Lean/Inductive.chs.h lean_env_get_inductive_type_has_dep_elim"
  lean_env_get_inductive_type_has_dep_elim'_ :: ((EnvPtr) -> ((NamePtr) -> ((Ptr CInt) -> ((OutExceptionPtr) -> (IO CInt)))))