// Author(s): Jeroen Keiren
// Copyright: see the accompanying file COPYING or copy at
// https://svn.win.tue.nl/trac/MCRL2/browser/trunk/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
/// \file mcrl2/data/application.h
/// \brief The class application.

// This is to avoid incomplete type errors when including this header standalone
#ifndef MCRL2_DATA_DATA_EXPRESSION_H
#include "mcrl2/data/data_expression.h"
#endif

#ifndef MCRL2_DATA_APPLICATION_H
#define MCRL2_DATA_APPLICATION_H

#include "boost/iterator/iterator_adaptor.hpp"
#include "mcrl2/atermpp/aterm_list.h"
#include "mcrl2/atermpp/make_list.h"
#include "mcrl2/utilities/workarounds.h" // for nullptr on older compilers

namespace mcrl2
{

namespace data
{

/// \brief Iterator for term_appl which prepends a single term to the list.
template <typename ForwardIterator >
class term_appl_prepend_iterator: public boost::iterator_facade<
  term_appl_prepend_iterator<ForwardIterator>,    // Derived
  data_expression,                                // Value
  boost::forward_traversal_tag,                   // CategoryOrTraversal
  const data_expression&                          // Reference
  >
{
  public:

    /// \brief Constructor.
    /// \param t A term
    term_appl_prepend_iterator(ForwardIterator it,
                               const data_expression* prepend=nullptr)
      : m_it(it), m_prepend(prepend)
    {}

  private:
    friend class boost::iterator_core_access;

    /// \brief Equality check
    /// \param other An iterator
    /// \return True if the iterators are equal
    bool equal(term_appl_prepend_iterator const& other) const
    {
      return this->m_prepend == other.m_prepend && this->m_it == other.m_it;
    }

    /// \brief Dereference operator
    /// \return The value that the iterator references
    const data_expression &dereference() const
    {
      if (m_prepend)
      {
        return *m_prepend;
      }

      return *m_it;
    }

    /// \brief Increments the iterator
    void increment()
    {
      if (m_prepend)
      {
        m_prepend = nullptr;
      }
      else
      {
        ++m_it;
      }
    }

    ForwardIterator m_it;
    const data_expression *m_prepend;
};

/// \brief Iterator for term_appl which prepends a single term to the list.
template <typename ForwardIterator, class ArgumentConverter>
class transforming_term_appl_prepend_iterator: public boost::iterator_facade<
  transforming_term_appl_prepend_iterator<ForwardIterator, ArgumentConverter>, // Derived
  data_expression,                                                // Value
  boost::forward_traversal_tag,                                   // CategoryOrTraversal
  const data_expression&                                          // Reference
  >
{
  public:

    /// \brief Constructor.
    /// \param t A term
    transforming_term_appl_prepend_iterator(ForwardIterator it,
                                            const data_expression* prepend,
                                            const ArgumentConverter arg_convert)
      : m_it(it), m_prepend(prepend), m_argument_converter(arg_convert)
    {}

  private:
    friend class boost::iterator_core_access;

    /// \brief Equality check
    /// \param other An iterator
    /// \return True if the iterators are equal
    bool equal(const transforming_term_appl_prepend_iterator& other) const
    {
      return this->m_prepend == other.m_prepend && this->m_it == other.m_it;
    }

    /// \brief Dereference operator
    /// \return The value that the iterator references
    const data_expression& dereference() const
    {
      if (m_prepend)
      {
        return *m_prepend;
      }

      m_stable_store=m_argument_converter(*m_it);
      return m_stable_store;
    }

    /// \brief Increments the iterator
    void increment()
    {
      if (m_prepend)
      {
        m_prepend = nullptr;
      }
      else
      {
        ++m_it;
      }
    }

    mutable data_expression m_stable_store;
    ForwardIterator m_it;
    const data_expression *m_prepend;
    ArgumentConverter m_argument_converter;
};

/// \brief An application of a data expression to a number of arguments
class application: public data_expression
{
  public:
    /// \brief Default constructor.
    application()
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(0)))
    {}

    /// \brief Constructor.
    application(const data_expression& head,
                const data_expression& arg1)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(2),head,arg1))
    {
    }

    /// \brief Constructor.
    application(const data_expression& head,
                const data_expression& arg1,
                const data_expression& arg2)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(3),head,arg1,arg2))
    {
    }

    /// \brief Constructor.
    application(const data_expression& head,
                const data_expression& arg1,
                const data_expression& arg2,
                const data_expression& arg3)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(4),head,arg1,arg2,arg3))
    {
    }

    /// \brief Constructor.
    application(const data_expression& head,
                const data_expression& arg1,
                const data_expression& arg2,
                const data_expression& arg3,
                const data_expression& arg4)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(5),head,arg1,arg2,arg3,arg4))
    {
    }

    /// \brief Constructor
    application(const data_expression& head,
                const data_expression& arg1,
                const data_expression& arg2,
                const data_expression& arg3,
                const data_expression& arg4,
                const data_expression& arg5)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(6),head,arg1,arg2,arg3,arg4,arg5))
    {
    }

    /// \brief Constructor.
    /// \param term A term
    explicit application(const atermpp::aterm& term)
      : data_expression(term)
    {
      assert(core::detail::check_term_DataAppl(*this));
    }

    /// \brief Constructor.
    template <typename Container>
    application(const data_expression& head,
                const Container& arguments,
                typename atermpp::enable_if_container<Container, data_expression>::type* = 0)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(arguments.size() + 1),
                                         term_appl_prepend_iterator<typename Container::const_iterator>(arguments.begin(), &head),
                                         term_appl_prepend_iterator<typename Container::const_iterator>(arguments.end())))
    {
      assert(arguments.size()>0);
    }

  private:
    // forbid the use of iterator, which is silently inherited from
    // aterm_appl. Modifying the arguments of an application through the iterator
    // is not allowed!
    typedef data_expression::iterator iterator;

  public:

    class const_iterator : public boost::iterator_adaptor<
            const_iterator                     // Derived
          , data_expression::const_iterator    // Base
          , const data_expression              // Value
          , boost::random_access_traversal_tag // CategoryOrTraversal
        >
    {
      public:
        explicit const_iterator(const data_expression::const_iterator& p)
          : const_iterator::iterator_adaptor_(p) {}
      private:
        friend class boost::iterator_core_access;
        reference dereference() const
        {
          return atermpp::down_cast<const data_expression>(*base_reference());
        }
    };

    /// \brief Constructor.
    template <typename FwdIter>
    application(const data_expression& head,
                FwdIter first,
                FwdIter last,
                typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = 0)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
                                         term_appl_prepend_iterator<FwdIter>(first, &head),
                                         term_appl_prepend_iterator<FwdIter>(last)))
    {
      assert(first!=last);
    }

    /// \brief Constructor.
    template <typename FwdIter>
    application(const size_t arity,
                const data_expression& head,
                FwdIter first,
                FwdIter last,
                typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = 0)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(arity + 1),
                                         term_appl_prepend_iterator<FwdIter>(first, &head),
                                         term_appl_prepend_iterator<FwdIter>(last)))
    {
      assert(arity>0);
      assert(std::distance(first, last)==arity);
    }


    /// \brief Constructor.
    template <typename FwdIter, class ArgumentConverter>
    application(const data_expression& head,
                FwdIter first,
                FwdIter last,
                ArgumentConverter convert_arguments,
                typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = 0,
                typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = 0)
      : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
                                         transforming_term_appl_prepend_iterator<FwdIter, ArgumentConverter>(first, &head, convert_arguments),
                                         transforming_term_appl_prepend_iterator<FwdIter, ArgumentConverter>(last,nullptr,convert_arguments)))
    {
      assert(first!=last);
    }

    /// \brief Get the function at the head of this expression.
    const data_expression& head() const
    {
      return atermpp::down_cast<const data_expression>(atermpp::aterm_appl::operator[](0));
    }

    /// \brief Get the i-th argument of this expression.
    const data_expression& operator[](size_t index) const
    {
      assert(index<size());
      return atermpp::down_cast<const data_expression>(atermpp::aterm_appl::operator[](index+1));
    }

    /// \brief Returns an iterator pointing to the first argument of the
    ///        application.
    const_iterator begin() const
    {
      return ++const_iterator(data_expression::begin());
    }

    /// \brief Returns an iterator pointing past the last argument of the
    ///        application.
    const_iterator end() const
    {
      return const_iterator(data_expression::end());
    }

    /// \brief Returns an iterator pointing past the last argument of the
    ///        application.
    size_t size() const
    {
      using namespace atermpp;
      return atermpp::aterm_appl::size() - 1;
    }
};

/// \brief swap overload
inline void swap(application& t1, application& t2)
{
  t1.swap(t2);
}

//--- start generated class application ---//
// prototype declaration
std::string pp(const application& x);

/// \brief Outputs the object to a stream
/// \param out An output stream
/// \return The output stream
inline
std::ostream& operator<<(std::ostream& out, const application& x)
{
  return out << data::pp(x);
}
//--- end generated class application ---//

// The precedence function must be declared here. Unfortunately this cannot be done using the include below.
// #include "mcrl2/data/precedence.h"
// Instead we do a forward declare of the precedence function. The user must make sure the file precedence.h is actually included.
// TOOO: fix this by moving the is_??? functions to the file application.h
int left_precedence(const data_expression& x);
int right_precedence(const data_expression& x);
int left_precedence(const application& x);
int right_precedence(const application& x);

inline
const data_expression& unary_operand(const application& x)
{
  return x[0];
}

inline
const data_expression& binary_left(const application& x)
{
  return x[0];
}

inline
const data_expression& binary_right(const application& x)
{
  return x[1];
}

inline
const data_expression& unary_operand1(const data_expression& x)
{
  const application& y = atermpp::down_cast<application>(x);
  return y[0];
}

inline
const data_expression& binary_left1(const data_expression& x)
{
  const application& y = atermpp::down_cast<application>(x);
  return y[0];
}

inline
const data_expression& binary_right1(const data_expression & x)
{
  const application& y = atermpp::down_cast<application>(x);
  return y[1];
}

} // namespace data

} // namespace mcrl2

#endif // MCRL2_DATA_APPLICATION_H
