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

Operations for working with Lean declarations.
-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Decl
  ( Env(..)
  , Decl
    -- * Constructors
  , axiom
  , constant
  , definition
  , definitionWith
  , theorem
  , theoremWith
    -- * Projections
  , declName
  , declUnivParams
  , declType
  , DeclView(..)
  , declView
    -- * Certified declarations
  , CertDecl
  , check
  ) where

import Foreign
import Foreign.C
import System.IO.Unsafe (unsafePerformIO)

import Language.Lean.List

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

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

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

import Language.Lean.Internal.Name
{-# LINE 42 "src/Language/Lean/Decl.chs" #-}











------------------------------------------------------------------------
-- Constructors

-- | Create an axiom.
axiom :: Name -- ^ Name of axiom
      -> List Name -- ^ Universe parameters
      -> Expr -- ^ Type of axiom
      -> Decl
axiom nm params tp = tryGetLeanValue $ lean_decl_mk_axiom nm params tp

lean_decl_mk_axiom :: (Name) -> (ListName) -> (Expr) -> (OutDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_decl_mk_axiom a1 a2 a3 a4 a5 =
  (withName) a1 $ \a1' -> 
  (withListName) a2 $ \a2' -> 
  (withExpr) a3 $ \a3' -> 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_decl_mk_axiom'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Create a constant.
--
-- Constants and axioms in Lean are essentially the same thing.
constant :: Name -- ^ Name of constant
         -> List Name -- ^ Universe parameters
         -> Expr -- ^ Type of constant
         -> Decl
constant nm params tp = tryGetLeanValue $ lean_decl_mk_const nm params tp

lean_decl_mk_const :: (Name) -> (ListName) -> (Expr) -> (OutDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_decl_mk_const a1 a2 a3 a4 a5 =
  (withName) a1 $ \a1' -> 
  (withListName) a2 $ \a2' -> 
  (withExpr) a3 $ \a3' -> 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_decl_mk_const'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Create a definition with an explicit definitional height
definition :: Name -- ^ Name of the definition
           -> List Name -- ^ Universe parameters for defintion
           -> Expr -- ^ Type of definition
           -> Expr -- ^ Value of definition
           -> Word32 -- ^ Definitional height
           -> Bool -- ^ Flag that indicates if definition should be lazily unfolded
           -> Decl
definition nm params tp v h o = tryGetLeanValue $ lean_decl_mk_def nm params tp v h o

lean_decl_mk_def :: (Name) -> (ListName) -> (Expr) -> (Expr) -> (Word32) -> (Bool) -> (OutDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_decl_mk_def a1 a2 a3 a4 a5 a6 a7 a8 =
  (withName) a1 $ \a1' -> 
  (withListName) a2 $ \a2' -> 
  (withExpr) a3 $ \a3' -> 
  (withExpr) a4 $ \a4' -> 
  let {a5' = fromIntegral a5} in 
  let {a6' = fromBool a6} in 
  let {a7' = id a7} in 
  let {a8' = id a8} in 
  lean_decl_mk_def'_ a1' a2' a3' a4' a5' a6' a7' a8' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Create a definition with a definitional height
-- computed from the environment.
--
-- The definitional height is computed using information from the environment.
definitionWith :: Env  -- ^ The environment
               -> Name -- ^ Name of the definition
               -> List Name -- ^ Universe parameters for defintion
               -> Expr -- ^ Type of definition
               -> Expr -- ^ Value of definition
               -> Bool -- ^ Flag that indicates if definition should be lazily unfolded
               -> Decl
definitionWith e nm params tp v o =
  tryGetLeanValue $ lean_decl_mk_def_with e nm params tp v o

lean_decl_mk_def_with :: (Env) -> (Name) -> (ListName) -> (Expr) -> (Expr) -> (Bool) -> (OutDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_decl_mk_def_with a1 a2 a3 a4 a5 a6 a7 a8 =
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  (withListName) a3 $ \a3' -> 
  (withExpr) a4 $ \a4' -> 
  (withExpr) a5 $ \a5' -> 
  let {a6' = fromBool a6} in 
  let {a7' = id a7} in 
  let {a8' = id a8} in 
  lean_decl_mk_def_with'_ a1' a2' a3' a4' a5' a6' a7' a8' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Creates a theorem with an explicit definitional height.
--
-- Theorems and definitions are essentially the same thing in Lean, except in
-- the way the normalizer treats them. The normalizer will only unfold theroem
-- if there is nothing else to be done when checking whether two terms are
-- definitionally equal or not.
theorem :: Name      -- ^ Name of the theorem
        -> List Name -- ^ Universe parameters for theorem
        -> Expr      -- ^ Type of the theorem
        -> Expr      -- ^ Proof of the theorem
        -> Word32    -- ^ Definitional height
        -> Decl
theorem nm params tp v h = tryGetLeanValue $ lean_decl_mk_thm nm params tp v h

lean_decl_mk_thm :: (Name) -> (ListName) -> (Expr) -> (Expr) -> (Word32) -> (OutDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_decl_mk_thm a1 a2 a3 a4 a5 a6 a7 =
  (withName) a1 $ \a1' -> 
  (withListName) a2 $ \a2' -> 
  (withExpr) a3 $ \a3' -> 
  (withExpr) a4 $ \a4' -> 
  let {a5' = fromIntegral a5} in 
  let {a6' = id a6} in 
  let {a7' = id a7} in 
  lean_decl_mk_thm'_ a1' a2' a3' a4' a5' a6' a7' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | 'theoremWith' creates a theorem that is relative to an environment.
--
-- Theorems and definitions are essentially the same thing in Lean, except in
-- the way the normalizer treats them. The normalizer will only unfold theroem
-- if there is nothing else to be done when checking whether two terms are
-- definitionally equal or not.
--
-- The definitional height is computed from environment.
theoremWith :: Env       -- ^ The environment
            -> Name      -- ^ The name of the theorem
            -> List Name -- ^ Universe parameters for theorem
            -> Expr      -- ^ Type of the theorem
            -> Expr      -- ^ Proof of the theorem
            -> Decl
theoremWith e nm params tp v = tryGetLeanValue $ lean_decl_mk_thm_with e nm params tp v

lean_decl_mk_thm_with :: (Env) -> (Name) -> (ListName) -> (Expr) -> (Expr) -> (OutDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_decl_mk_thm_with a1 a2 a3 a4 a5 a6 a7 =
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  (withListName) a3 $ \a3' -> 
  (withExpr) a4 $ \a4' -> 
  (withExpr) a5 $ \a5' -> 
  let {a6' = id a6} in 
  let {a7' = id a7} in 
  lean_decl_mk_thm_with'_ a1' a2' a3' a4' a5' a6' a7' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- Projections

-- | The name of a declaration.
declName :: Decl -> Name
declName d = tryGetLeanValue $ lean_decl_get_name d

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

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


-- | The list of universe params for a declaration.
declUnivParams :: Decl -> List Name
declUnivParams d = tryGetLeanValue $ lean_decl_get_univ_params d

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

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


-- | The type of a declaration.
declType :: Decl -> Expr
declType d = tryGetLeanValue $ lean_decl_get_type d

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

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


-- | Information about a declaration
data DeclView
    -- | A constant
  = Constant
    -- | An axiom
  | Axiom
    -- | A definition with the associated value, definitional height, and
    -- whether to lazy unfold it.
  | Definition Expr Word32 Bool
    -- | A theorem with the associated value and definitional height.
  | Theorem Expr Word32
 deriving (Eq, Show)

-- | Return information about a declaration.
declView :: Decl -> DeclView
declView x =
  case lean_decl_get_kind x of
    LEAN_DECL_CONST -> Constant
    LEAN_DECL_AXIOM -> Axiom
    LEAN_DECL_DEF ->
      Definition (tryGetLeanValue $ lean_decl_get_value x)
                 (tryGetLeanValue $ lean_decl_get_height x)
                 (tryGetLeanValue $ lean_decl_get_conv_opt x)
    LEAN_DECL_THM ->
      Theorem (tryGetLeanValue $ lean_decl_get_value x)
              (tryGetLeanValue $ lean_decl_get_height x)

data DeclKind = LEAN_DECL_CONST
              | LEAN_DECL_AXIOM
              | LEAN_DECL_DEF
              | LEAN_DECL_THM
  deriving (Enum,Eq)

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


lean_decl_get_kind :: (Decl) -> (DeclKind)
lean_decl_get_kind a1 =
  unsafePerformIO $
  (withDecl) a1 $ \a1' -> 
  let {res = lean_decl_get_kind'_ a1'} in
  let {res' = (toEnum . fromIntegral) res} in
  return (res')

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


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

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


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

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


lean_decl_get_conv_opt :: (Decl) -> (Ptr CInt) -> (OutExceptionPtr) -> IO ((Bool))
lean_decl_get_conv_opt a1 a2 a3 =
  (withDecl) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_decl_get_conv_opt'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- Certified declarations

-- | Creates a cerified declaration by type checking it within a
-- given environment.
check :: Env -> Decl -> CertDecl
check e d = tryGetLeanValue $ lean_decl_check e d

lean_decl_check :: (Env) -> (Decl) -> (OutCertDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_decl_check a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withDecl) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_decl_check'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_mk_axiom"
  lean_decl_mk_axiom'_ :: ((NamePtr) -> ((ListNamePtr) -> ((ExprPtr) -> ((OutDeclPtr) -> ((OutExceptionPtr) -> (IO CInt))))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_mk_const"
  lean_decl_mk_const'_ :: ((NamePtr) -> ((ListNamePtr) -> ((ExprPtr) -> ((OutDeclPtr) -> ((OutExceptionPtr) -> (IO CInt))))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_mk_def"
  lean_decl_mk_def'_ :: ((NamePtr) -> ((ListNamePtr) -> ((ExprPtr) -> ((ExprPtr) -> (CUInt -> (CInt -> ((OutDeclPtr) -> ((OutExceptionPtr) -> (IO CInt)))))))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_mk_def_with"
  lean_decl_mk_def_with'_ :: ((EnvPtr) -> ((NamePtr) -> ((ListNamePtr) -> ((ExprPtr) -> ((ExprPtr) -> (CInt -> ((OutDeclPtr) -> ((OutExceptionPtr) -> (IO CInt)))))))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_mk_thm"
  lean_decl_mk_thm'_ :: ((NamePtr) -> ((ListNamePtr) -> ((ExprPtr) -> ((ExprPtr) -> (CUInt -> ((OutDeclPtr) -> ((OutExceptionPtr) -> (IO CInt))))))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_mk_thm_with"
  lean_decl_mk_thm_with'_ :: ((EnvPtr) -> ((NamePtr) -> ((ListNamePtr) -> ((ExprPtr) -> ((ExprPtr) -> ((OutDeclPtr) -> ((OutExceptionPtr) -> (IO CInt))))))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_get_name"
  lean_decl_get_name'_ :: ((DeclPtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_get_univ_params"
  lean_decl_get_univ_params'_ :: ((DeclPtr) -> ((OutListNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_get_type"
  lean_decl_get_type'_ :: ((DeclPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_get_kind"
  lean_decl_get_kind'_ :: ((DeclPtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_get_value"
  lean_decl_get_value'_ :: ((DeclPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_get_height"
  lean_decl_get_height'_ :: ((DeclPtr) -> ((Ptr CUInt) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_get_conv_opt"
  lean_decl_get_conv_opt'_ :: ((DeclPtr) -> ((Ptr CInt) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Decl.chs.h lean_decl_check"
  lean_decl_check'_ :: ((EnvPtr) -> ((DeclPtr) -> ((OutCertDeclPtr) -> ((OutExceptionPtr) -> (IO CInt)))))