#ifndef ESBMC_TYPE_TRAITS
#define ESBMC_TYPE_TRAITS

#include "utility" // for remove_reference, declval

namespace std
{

// integral_constant
template <class T, T v>
struct integral_constant
{
  static constexpr T value = v;
  typedef T value_type;
  typedef integral_constant type;
  constexpr operator value_type() const noexcept
  {
    return value;
  }
  constexpr value_type operator()() const noexcept
  {
    return value;
  }
};

typedef integral_constant<bool, true> true_type;
typedef integral_constant<bool, false> false_type;

// conditional
template <bool B, class T, class F>
struct conditional
{
  typedef T type;
};
template <class T, class F>
struct conditional<false, T, F>
{
  typedef F type;
};
template <bool B, class T, class F>
using conditional_t = typename conditional<B, T, F>::type;

// enable_if
template <bool B, class T = void>
struct enable_if
{
};
template <class T>
struct enable_if<true, T>
{
  typedef T type;
};
template <bool B, class T = void>
using enable_if_t = typename enable_if<B, T>::type;

// remove_const / remove_volatile / remove_cv
template <class T>
struct remove_const
{
  typedef T type;
};
template <class T>
struct remove_const<const T>
{
  typedef T type;
};
template <class T>
struct remove_cv
{
  typedef T type;
};
template <class T>
struct remove_cv<const T>
{
  typedef T type;
};
template <class T>
struct remove_cv<volatile T>
{
  typedef T type;
};
template <class T>
struct remove_cv<const volatile T>
{
  typedef T type;
};
template <class T>
using remove_cv_t = typename remove_cv<T>::type;

// remove_pointer
template <class T>
struct remove_pointer
{
  typedef T type;
};
template <class T>
struct remove_pointer<T *>
{
  typedef T type;
};
template <class T>
struct remove_pointer<T *const>
{
  typedef T type;
};
template <class T>
struct remove_pointer<T *volatile>
{
  typedef T type;
};
template <class T>
struct remove_pointer<T *const volatile>
{
  typedef T type;
};

// add_pointer
template <class T>
struct add_pointer
{
  typedef T *type;
};

// is_integral
namespace detail
{
template <class T>
struct is_integral_base : false_type
{
};
template <>
struct is_integral_base<bool> : true_type
{
};
template <>
struct is_integral_base<char> : true_type
{
};
template <>
struct is_integral_base<signed char> : true_type
{
};
template <>
struct is_integral_base<unsigned char> : true_type
{
};
template <>
struct is_integral_base<wchar_t> : true_type
{
};
template <>
struct is_integral_base<short> : true_type
{
};
template <>
struct is_integral_base<unsigned short> : true_type
{
};
template <>
struct is_integral_base<int> : true_type
{
};
template <>
struct is_integral_base<unsigned int> : true_type
{
};
template <>
struct is_integral_base<long> : true_type
{
};
template <>
struct is_integral_base<unsigned long> : true_type
{
};
template <>
struct is_integral_base<long long> : true_type
{
};
template <>
struct is_integral_base<unsigned long long> : true_type
{
};
} // namespace detail

template <class T>
struct is_integral : detail::is_integral_base<remove_cv_t<T>>
{
};
template <class T>
inline constexpr bool is_integral_v = is_integral<T>::value;

// is_floating_point
namespace detail
{
template <class T>
struct is_floating_point_base : false_type
{
};
template <>
struct is_floating_point_base<float> : true_type
{
};
template <>
struct is_floating_point_base<double> : true_type
{
};
template <>
struct is_floating_point_base<long double> : true_type
{
};
} // namespace detail

template <class T>
struct is_floating_point : detail::is_floating_point_base<remove_cv_t<T>>
{
};
template <class T>
inline constexpr bool is_floating_point_v = is_floating_point<T>::value;

// is_arithmetic
template <class T>
struct is_arithmetic
  : integral_constant<bool, is_integral<T>::value || is_floating_point<T>::value>
{
};
template <class T>
inline constexpr bool is_arithmetic_v = is_arithmetic<T>::value;

// is_enum
template <class T>
struct is_enum : integral_constant<bool, __is_enum(T)>
{
};
template <class T>
inline constexpr bool is_enum_v = is_enum<T>::value;

// underlying_type — ::type is only present when T is an enumeration type
template <class T, bool = is_enum<T>::value>
struct underlying_type
{
};
template <class T>
struct underlying_type<T, true>
{
  typedef __underlying_type(T) type;
};
template <class T>
using underlying_type_t = typename underlying_type<T>::type;

// is_signed
template <class T>
struct is_signed : integral_constant<bool, __is_signed(T)>
{
};
template <class T>
inline constexpr bool is_signed_v = is_signed<T>::value;

// is_unsigned
template <class T>
struct is_unsigned : integral_constant<bool, __is_unsigned(T)>
{
};
template <class T>
inline constexpr bool is_unsigned_v = is_unsigned<T>::value;

// is_trivially_copyable (needed by std::bit_cast)
template <class T>
struct is_trivially_copyable
  : integral_constant<bool, __is_trivially_copyable(T)>
{
};
template <class T>
inline constexpr bool is_trivially_copyable_v =
  is_trivially_copyable<T>::value;

// is_array
template <class T>
struct is_array : false_type
{
};
template <class T>
struct is_array<T[]> : true_type
{
};
template <class T, size_t N>
struct is_array<T[N]> : true_type
{
};
template <class T>
inline constexpr bool is_array_v = is_array<T>::value;

// extent — number of elements in the first array dimension (0 for non-arrays)
template <class T, size_t N = 0>
struct extent : integral_constant<size_t, 0>
{
};
template <class T>
struct extent<T[], 0> : integral_constant<size_t, 0>
{
};
template <class T, size_t I>
struct extent<T[I], 0> : integral_constant<size_t, I>
{
};
template <class T, size_t N>
struct extent<T[], N> : extent<T, N - 1>
{
};
template <class T, size_t I, size_t N>
struct extent<T[I], N> : extent<T, N - 1>
{
};
template <class T>
inline constexpr size_t extent_v = extent<T>::value;

// is_same
template <class T, class U>
struct is_same : false_type
{
};
template <class T>
struct is_same<T, T> : true_type
{
};
template <class T, class U>
inline constexpr bool is_same_v = is_same<T, U>::value;

// is_void
template <class T>
struct is_void : is_same<void, remove_cv_t<T>>
{
};
template <class T>
inline constexpr bool is_void_v = is_void<T>::value;

// is_pointer
template <class T>
struct is_pointer : false_type
{
};
template <class T>
struct is_pointer<T *> : true_type
{
};
template <class T>
struct is_pointer<T *const> : true_type
{
};
template <class T>
struct is_pointer<T *volatile> : true_type
{
};
template <class T>
struct is_pointer<T *const volatile> : true_type
{
};
template <class T>
inline constexpr bool is_pointer_v = is_pointer<T>::value;

// is_reference
template <class T>
struct is_lvalue_reference : false_type
{
};
template <class T>
struct is_lvalue_reference<T &> : true_type
{
};
template <class T>
struct is_rvalue_reference : false_type
{
};
template <class T>
struct is_rvalue_reference<T &&> : true_type
{
};
template <class T>
struct is_reference : integral_constant<bool, is_lvalue_reference<T>::value ||
                                                is_rvalue_reference<T>::value>
{
};

// make_unsigned
template <class T>
struct make_unsigned;
template <>
struct make_unsigned<signed char>
{
  typedef unsigned char type;
};
template <>
struct make_unsigned<short>
{
  typedef unsigned short type;
};
template <>
struct make_unsigned<int>
{
  typedef unsigned int type;
};
template <>
struct make_unsigned<long>
{
  typedef unsigned long type;
};
template <>
struct make_unsigned<long long>
{
  typedef unsigned long long type;
};
template <>
struct make_unsigned<unsigned char>
{
  typedef unsigned char type;
};
template <>
struct make_unsigned<unsigned short>
{
  typedef unsigned short type;
};
template <>
struct make_unsigned<unsigned int>
{
  typedef unsigned int type;
};
template <>
struct make_unsigned<unsigned long>
{
  typedef unsigned long type;
};
template <>
struct make_unsigned<unsigned long long>
{
  typedef unsigned long long type;
};
template <class T>
using make_unsigned_t = typename make_unsigned<T>::type;

// make_signed
template <class T>
struct make_signed;
template <>
struct make_signed<unsigned char>
{
  typedef signed char type;
};
template <>
struct make_signed<unsigned short>
{
  typedef short type;
};
template <>
struct make_signed<unsigned int>
{
  typedef int type;
};
template <>
struct make_signed<unsigned long>
{
  typedef long type;
};
template <>
struct make_signed<unsigned long long>
{
  typedef long long type;
};
template <>
struct make_signed<signed char>
{
  typedef signed char type;
};
template <>
struct make_signed<short>
{
  typedef short type;
};
template <>
struct make_signed<int>
{
  typedef int type;
};
template <>
struct make_signed<long>
{
  typedef long type;
};
template <>
struct make_signed<long long>
{
  typedef long long type;
};
template <class T>
using make_signed_t = typename make_signed<T>::type;

// decay
template <class T>
struct decay
{
private:
  typedef remove_reference_t<T> U;

public:
  typedef conditional_t<
    is_array<U>::value,
    typename remove_extent<U>::type *,
    conditional_t<false /* is_function<U> */, U *, remove_cv_t<U>>>
    type;
};
template <class T>
using decay_t = typename decay<T>::type;

// void_t (C++17)
template <class...>
using void_t = void;

namespace detail
{
// SFINAE helper for is_invocable: succeeds iff F(Args...) is a valid call.
template <class F, class... Args>
auto test_invocable(int)
  -> decltype(declval<F>()(declval<Args>()...), true_type{});

template <class F, class... Args>
false_type test_invocable(...);

// SFINAE helper for is_invocable_r: succeeds iff F(Args...) is valid AND
// the result is (void-cast-) convertible to R.
template <class R, class F, class... Args>
auto test_invocable_r(int)
  -> decltype(
    (void)static_cast<R>(declval<F>()(declval<Args>()...)),
    true_type{});

template <class R, class F, class... Args>
false_type test_invocable_r(...);
} // namespace detail

// is_invocable
template <class F, class... Args>
struct is_invocable : decltype(detail::test_invocable<F, Args...>(0))
{
};
template <class F, class... Args>
inline constexpr bool is_invocable_v = is_invocable<F, Args...>::value;

// is_invocable_r
template <class R, class F, class... Args>
struct is_invocable_r : decltype(detail::test_invocable_r<R, F, Args...>(0))
{
};
template <class R, class F, class... Args>
inline constexpr bool is_invocable_r_v = is_invocable_r<R, F, Args...>::value;

// is_constructible (simplified via Clang builtin)
template <class T, class... Args>
struct is_constructible
  : integral_constant<bool, __is_constructible(T, Args...)>
{
};
template <class T, class... Args>
inline constexpr bool is_constructible_v = is_constructible<T, Args...>::value;

// is_convertible (simplified)
namespace detail
{
template <class From, class To>
auto test_convertible(int) -> decltype(static_cast<To>(declval<From>()), true_type{});
template <class From, class To>
false_type test_convertible(...);
} // namespace detail

template <class From, class To>
struct is_convertible : decltype(detail::test_convertible<From, To>(0))
{
};
template <class From, class To>
inline constexpr bool is_convertible_v = is_convertible<From, To>::value;

} // namespace std

#endif // ESBMC_TYPE_TRAITS
