module Lean.Raw.C.Name where

import Foreign
import Foreign.C.Types

import Lean.Raw.C.Exception (Exception)
import Lean.Wrapper

#include <lean.h>

data Struct

instance Drop Struct where drop = drop'
foreign import ccall unsafe "&lean_name_del" drop' :: FunPtr (Ptr Struct -> IO ())

type Name = Ptr Struct

foreign import ccall unsafe "lean_name_del" drop :: Name -> IO ()
foreign import ccall unsafe "lean_name_mk_anonymous" mkAnonymous :: Ptr Name -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_name_mk_str" mkStr :: Name -> Ptr CChar -> Ptr Name -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_name_mk_idx" mkIdx :: Name -> CUInt -> Ptr Name -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_name_eq" eq :: Name -> Name -> IO CInt
foreign import ccall unsafe "lean_name_lt" lt :: Name -> Name -> IO CInt
foreign import ccall unsafe "lean_name_to_string" toString :: Name -> Ptr (Ptr CChar) -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_name_is_anonymous" isAnonymous :: Name -> IO CInt
foreign import ccall unsafe "lean_name_is_str" isStr :: Name -> IO CInt
foreign import ccall unsafe "lean_name_is_idx" isIdx :: Name -> IO CInt
foreign import ccall unsafe "lean_name_get_prefix" getPrefix :: Name -> Ptr Name -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_name_get_str" getStr :: Name -> Ptr (Ptr CChar) -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_name_get_idx" getIdx :: Name -> Ptr CUInt -> Ptr Exception -> IO CInt

data ListStruct

type ListName = Ptr ListStruct

foreign import ccall unsafe "lean_list_name_del" dropList :: ListName -> IO ()
foreign import ccall unsafe "lean_list_name_mk_nil" mkNil :: Ptr ListName -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_list_name_mk_cons" mkCons :: Name -> ListName -> Ptr ListName -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_list_name_eq" eqList :: ListName -> ListName -> IO CInt
foreign import ccall unsafe "lean_list_name_head" head :: ListName -> Ptr Name -> Ptr Exception -> IO CInt
foreign import ccall unsafe "lean_list_name_del" tail :: ListName -> Ptr ListName -> Ptr Exception -> IO CInt