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

Operations for Lean expressions.
-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Expr
  ( MacroDef
  , Expr
  , BinderKind(..)
    -- * Constructors
  , varExpr
  , sortExpr
  , constExpr
  , appExpr
  , lambdaExpr
  , piExpr
  , macroExpr
  , localExpr
  , localExtExpr
  , metavarExpr
    -- * View
  , ExprView(..)
  , exprView
    -- * Operations
  , exprLt
  , exprToString
  ) where

import Foreign
import Foreign.C
import System.IO.Unsafe

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

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

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

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










------------------------------------------------------------------------
-- Expression constructors

-- | Create a variable with de-Bruijn index @i@. This is a bound variable.
varExpr :: Word32 -> Expr
varExpr i = tryGetLeanValue $ lean_expr_mk_var i

lean_expr_mk_var :: (Word32) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_mk_var a1 a2 a3 =
  let {a1' = fromIntegral a1} in 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_expr_mk_var'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 64 "src/Language/Lean/Expr.chs" #-}


-- | Creates a type for the given universe
sortExpr :: Univ -> Expr
sortExpr u = tryGetLeanValue $ lean_expr_mk_sort u

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

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


-- | Create a constant with a given name and universe parameters
constExpr :: Name -> List Univ -> Expr
constExpr nm params = tryGetLeanValue $ lean_expr_mk_const nm params

lean_expr_mk_const :: (Name) -> (ListUniv) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_mk_const a1 a2 a3 a4 =
  (withName) a1 $ \a1' -> 
  (withListUniv) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_expr_mk_const'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Create a function application for expressions
appExpr :: Expr -> Expr -> Expr
appExpr f a = tryGetLeanValue $ lean_expr_mk_app f a

lean_expr_mk_app :: (Expr) -> (Expr) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_mk_app a1 a2 a3 a4 =
  (withExpr) a1 $ \a1' -> 
  (withExpr) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_expr_mk_app'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Create a lambda abstraction for expressions
lambdaExpr :: BinderKind -> Name -> Expr -> Expr -> Expr
lambdaExpr k nm tp b = tryGetLeanValue $ lean_expr_mk_lambda nm tp b k

lean_expr_mk_lambda :: (Name) -> (Expr) -> (Expr) -> (BinderKind) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_mk_lambda a1 a2 a3 a4 a5 a6 =
  (withName) a1 $ \a1' -> 
  (withExpr) a2 $ \a2' -> 
  (withExpr) a3 $ \a3' -> 
  let {a4' = (fromIntegral . fromEnum) a4} in 
  let {a5' = id a5} in 
  let {a6' = id a6} in 
  lean_expr_mk_lambda'_ a1' a2' a3' a4' a5' a6' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 109 "src/Language/Lean/Expr.chs" #-}


-- | Create a pi abstraction for expressions
piExpr :: BinderKind -> Name -> Expr -> Expr -> Expr
piExpr k nm tp b = tryGetLeanValue $ lean_expr_mk_pi nm tp b k

lean_expr_mk_pi :: (Name) -> (Expr) -> (Expr) -> (BinderKind) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_mk_pi a1 a2 a3 a4 a5 a6 =
  (withName) a1 $ \a1' -> 
  (withExpr) a2 $ \a2' -> 
  (withExpr) a3 $ \a3' -> 
  let {a4' = (fromIntegral . fromEnum) a4} in 
  let {a5' = id a5} in 
  let {a6' = id a6} in 
  lean_expr_mk_pi'_ a1' a2' a3' a4' a5' a6' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 122 "src/Language/Lean/Expr.chs" #-}


-- | Create a macro application for expressions
macroExpr :: MacroDef -> List Expr -> Expr
macroExpr m args = tryGetLeanValue $ lean_expr_mk_macro m args

lean_expr_mk_macro :: (MacroDef) -> (ListExpr) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_mk_macro a1 a2 a3 a4 =
  (withMacroDef) a1 $ \a1' -> 
  (withListExpr) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_expr_mk_macro'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | Create a local constant with the given name and type.
localExpr :: Name -> Expr -> Expr
localExpr nm tp = tryGetLeanValue $ lean_expr_mk_local nm tp

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

{-# LINE 144 "src/Language/Lean/Expr.chs" #-}


-- | Create a local constant with additional parameters
localExtExpr :: BinderKind -- ^ The binder kind for expression
             -> Name -- ^ The name of expression
             -> Name -- ^ The pretty print name
             -> Expr -- ^ The type of the expression
             -> Expr
localExtExpr k nm ppnm tp = tryGetLeanValue $ lean_expr_mk_local_ext nm ppnm tp k

lean_expr_mk_local_ext :: (Name) -> (Name) -> (Expr) -> (BinderKind) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_mk_local_ext a1 a2 a3 a4 a5 a6 =
  (withName) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  (withExpr) a3 $ \a3' -> 
  let {a4' = (fromIntegral . fromEnum) a4} in 
  let {a5' = id a5} in 
  let {a6' = id a6} in 
  lean_expr_mk_local_ext'_ a1' a2' a3' a4' a5' a6' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 161 "src/Language/Lean/Expr.chs" #-}


-- | Create a metavariable with the given name @nm@ and type @tp@.
metavarExpr :: Name -> Expr -> Expr
metavarExpr nm tp = tryGetLeanValue $ lean_expr_mk_metavar nm tp

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

{-# LINE 172 "src/Language/Lean/Expr.chs" #-}


------------------------------------------------------------------------
-- Expression view

-- | Information about the expression.
data ExprView
  = ExprVar Word32
  | ExprSort Univ
  | ExprConst Name (List Univ)
  | ExprLocal BinderKind Name Name Expr
  | ExprMeta Name Expr
  | ExprApp Expr Expr
  | ExprLambda BinderKind Name Expr Expr
  | ExprPi     BinderKind Name Expr Expr
  | ExprMacro MacroDef (List Expr)
  deriving (Eq, Show)

-- | View information about the structure of an expression.
exprView :: Expr -> ExprView
exprView x =
  case lean_expr_get_kind x of
    LEAN_EXPR_VAR ->
      ExprVar (tryGetLeanValue $ lean_expr_get_var_idx x)
    LEAN_EXPR_SORT ->
      ExprSort (tryGetLeanValue $ lean_expr_get_sort_univ x)
    LEAN_EXPR_CONST ->
      ExprConst (tryGetLeanValue $ lean_expr_get_const_name x)
                (tryGetLeanValue $ lean_expr_get_const_univs x)
    LEAN_EXPR_LOCAL ->
      ExprLocal (tryGetEnum $ lean_expr_get_local_binder_kind x)
                (tryGetLeanValue $ lean_expr_get_mlocal_name x)
                (tryGetLeanValue $ lean_expr_get_local_pp_name x)
                (tryGetLeanValue $ lean_expr_get_mlocal_type x)
    LEAN_EXPR_META ->
      ExprMeta  (tryGetLeanValue $ lean_expr_get_mlocal_name x)
                (tryGetLeanValue $ lean_expr_get_mlocal_type x)
    LEAN_EXPR_APP ->
      ExprApp (tryGetLeanValue $ lean_expr_get_app_fun x)
              (tryGetLeanValue $ lean_expr_get_app_arg x)
    LEAN_EXPR_LAMBDA ->
      ExprLambda (tryGetEnum $ lean_expr_get_binding_binder_kind x)
                 (tryGetLeanValue $ lean_expr_get_binding_name x)
                 (tryGetLeanValue $ lean_expr_get_binding_domain x)
                 (tryGetLeanValue $ lean_expr_get_binding_body x)
    LEAN_EXPR_PI ->
      ExprPi (tryGetEnum $ lean_expr_get_binding_binder_kind x)
             (tryGetLeanValue $ lean_expr_get_binding_name x)
             (tryGetLeanValue $ lean_expr_get_binding_domain x)
             (tryGetLeanValue $ lean_expr_get_binding_body x)
    LEAN_EXPR_MACRO ->
      ExprMacro (tryGetLeanValue $ lean_expr_get_macro_def x)
                (tryGetLeanValue $ lean_expr_get_macro_args x)

data ExprKind = LEAN_EXPR_VAR
              | LEAN_EXPR_SORT
              | LEAN_EXPR_CONST
              | LEAN_EXPR_LOCAL
              | LEAN_EXPR_META
              | LEAN_EXPR_APP
              | LEAN_EXPR_LAMBDA
              | LEAN_EXPR_PI
              | LEAN_EXPR_MACRO
  deriving (Enum,Eq)

{-# LINE 227 "src/Language/Lean/Expr.chs" #-}


lean_expr_get_kind :: (Expr) -> (ExprKind)
lean_expr_get_kind a1 =
  unsafePerformIO $
  (withExpr) a1 $ \a1' -> 
  let {res = lean_expr_get_kind'_ a1'} in
  let {res' = (toEnum . fromIntegral) res} in
  return (res')

{-# LINE 230 "src/Language/Lean/Expr.chs" #-}


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

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


lean_expr_get_sort_univ :: (Expr) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_get_sort_univ a1 a2 a3 =
  (withExpr) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_expr_get_sort_univ'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


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

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


lean_expr_get_const_univs :: (Expr) -> (OutListUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_get_const_univs a1 a2 a3 =
  (withExpr) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_expr_get_const_univs'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


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

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


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

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


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

{-# LINE 251 "src/Language/Lean/Expr.chs" #-}


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

{-# LINE 254 "src/Language/Lean/Expr.chs" #-}


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

{-# LINE 257 "src/Language/Lean/Expr.chs" #-}


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

{-# LINE 260 "src/Language/Lean/Expr.chs" #-}


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

{-# LINE 263 "src/Language/Lean/Expr.chs" #-}


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

{-# LINE 266 "src/Language/Lean/Expr.chs" #-}


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

{-# LINE 269 "src/Language/Lean/Expr.chs" #-}


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

{-# LINE 272 "src/Language/Lean/Expr.chs" #-}


lean_expr_get_macro_def :: (Expr) -> (OutMacroDefPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_expr_get_macro_def a1 a2 a3 =
  (withExpr) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_expr_get_macro_def'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 275 "src/Language/Lean/Expr.chs" #-}


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

{-# LINE 278 "src/Language/Lean/Expr.chs" #-}


foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_var"
  lean_expr_mk_var'_ :: (CUInt -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_sort"
  lean_expr_mk_sort'_ :: ((UnivPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_const"
  lean_expr_mk_const'_ :: ((NamePtr) -> ((ListUnivPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_app"
  lean_expr_mk_app'_ :: ((ExprPtr) -> ((ExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_lambda"
  lean_expr_mk_lambda'_ :: ((NamePtr) -> ((ExprPtr) -> ((ExprPtr) -> (CInt -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_pi"
  lean_expr_mk_pi'_ :: ((NamePtr) -> ((ExprPtr) -> ((ExprPtr) -> (CInt -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_macro"
  lean_expr_mk_macro'_ :: ((MacroDefPtr) -> ((ListExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_local"
  lean_expr_mk_local'_ :: ((NamePtr) -> ((ExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_local_ext"
  lean_expr_mk_local_ext'_ :: ((NamePtr) -> ((NamePtr) -> ((ExprPtr) -> (CInt -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_mk_metavar"
  lean_expr_mk_metavar'_ :: ((NamePtr) -> ((ExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_kind"
  lean_expr_get_kind'_ :: ((ExprPtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_var_idx"
  lean_expr_get_var_idx'_ :: ((ExprPtr) -> ((Ptr CUInt) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_sort_univ"
  lean_expr_get_sort_univ'_ :: ((ExprPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_const_name"
  lean_expr_get_const_name'_ :: ((ExprPtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_const_univs"
  lean_expr_get_const_univs'_ :: ((ExprPtr) -> ((OutListUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_app_fun"
  lean_expr_get_app_fun'_ :: ((ExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_app_arg"
  lean_expr_get_app_arg'_ :: ((ExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_mlocal_name"
  lean_expr_get_mlocal_name'_ :: ((ExprPtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_mlocal_type"
  lean_expr_get_mlocal_type'_ :: ((ExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_local_pp_name"
  lean_expr_get_local_pp_name'_ :: ((ExprPtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_local_binder_kind"
  lean_expr_get_local_binder_kind'_ :: ((ExprPtr) -> ((Ptr CInt) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_binding_name"
  lean_expr_get_binding_name'_ :: ((ExprPtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_binding_domain"
  lean_expr_get_binding_domain'_ :: ((ExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_binding_body"
  lean_expr_get_binding_body'_ :: ((ExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_binding_binder_kind"
  lean_expr_get_binding_binder_kind'_ :: ((ExprPtr) -> ((Ptr CInt) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_macro_def"
  lean_expr_get_macro_def'_ :: ((ExprPtr) -> ((OutMacroDefPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Expr.chs.h lean_expr_get_macro_args"
  lean_expr_get_macro_args'_ :: ((ExprPtr) -> ((OutListExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))