#pragma once

#include "cstddef"  /* size_t, ptrdiff_t */
#include "cstdint"  /* SIZE_MAX */
#include <array>
#include "bit"      /* std::bit_cast (transitive, matches libc++/libstdc++) */
#include "type_traits"

namespace std
{

inline constexpr size_t dynamic_extent = SIZE_MAX;

template <class T, size_t Extent = dynamic_extent>
class span
{
  T *data_;
  size_t size_;

public:
  using element_type = T;
  using value_type = typename std::remove_cv<T>::type;
  using size_type = size_t;
  using difference_type = ptrdiff_t;
  using pointer = T *;
  using const_pointer = const T *;
  using reference = T &;
  using const_reference = const T &;
  using iterator = pointer;
  using const_iterator = const_pointer;

  static constexpr size_t extent = Extent;

  // Constructors
  constexpr span() noexcept : data_(nullptr), size_(0) {}

  constexpr span(pointer ptr, size_type count) noexcept
    : data_(ptr), size_(count)
  {
  }

  constexpr span(pointer first, pointer last)
    : data_(first), size_(static_cast<size_type>(last - first))
  {
    __ESBMC_assert(first <= last, "span: iterator pair out of order");
  }

  template <size_t N>
  constexpr span(T (&arr)[N]) noexcept : data_(arr), size_(N)
  {
  }

  template <size_t N>
  constexpr span(std::array<value_type, N> &arr) noexcept
    : data_(arr.data()), size_(N)
  {
  }

  template <size_t N>
  constexpr span(const std::array<value_type, N> &arr) noexcept
    : data_(arr.data()), size_(N)
  {
  }

  constexpr span(const span &) noexcept = default;
  constexpr span &operator=(const span &) noexcept = default;

  // Iterators
  constexpr iterator begin() const noexcept { return data_; }
  constexpr iterator end() const noexcept { return data_ + size_; }

  // Capacity
  constexpr size_type size() const noexcept { return size_; }
  constexpr size_type size_bytes() const noexcept
  {
    return size_ * sizeof(element_type);
  }
  constexpr bool empty() const noexcept { return size_ == 0; }

  // Element access
  constexpr reference operator[](size_type idx) const
  {
    __ESBMC_assert(idx < size_, "span index out of bounds");
    return data_[idx];
  }
  constexpr reference front() const
  {
    __ESBMC_assert(size_ > 0, "span::front on empty span");
    return data_[0];
  }
  constexpr reference back() const
  {
    __ESBMC_assert(size_ > 0, "span::back on empty span");
    return data_[size_ - 1];
  }
  constexpr pointer data() const noexcept { return data_; }

  // Subviews
  constexpr span first(size_type count) const
  {
    __ESBMC_assert(count <= size_, "span::first count exceeds size");
    return span(data_, count);
  }
  constexpr span last(size_type count) const
  {
    __ESBMC_assert(count <= size_, "span::last count exceeds size");
    return span(data_ + (size_ - count), count);
  }
  constexpr span
  subspan(size_type offset, size_type count = dynamic_extent) const
  {
    __ESBMC_assert(offset <= size_, "span::subspan offset exceeds size");
    size_type n = (count == dynamic_extent) ? (size_ - offset) : count;
    __ESBMC_assert(
      n <= size_ - offset, "span::subspan count exceeds remaining size");
    return span(data_ + offset, n);
  }
};

// Deduction guides (C++17)
template <class T, size_t N>
span(T (&)[N]) -> span<T, N>;

template <class T, size_t N>
span(std::array<T, N> &) -> span<T, N>;

template <class T, size_t N>
span(const std::array<T, N> &) -> span<const T, N>;

template <class T>
span(T *, size_t) -> span<T>;

template <class T>
span(T *, T *) -> span<T>;

} // namespace std
