application.h

Go to the documentation of this file.

// Author(s): Jeroen Keiren, Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/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)
//
 
#ifndef MCRL2_DATA_VARIABLE_H
#include "mcrl2/data/variable.h"
#endif
 
#ifndef MCRL2_DATA_APPLICATION_H
#define MCRL2_DATA_APPLICATION_H
 
namespace mcrl2
{
 
namespace data
{
 
namespace detail
{
 
// The class and the specialisation below are intended to
// make the type of the term_appl_prepend_iterator a forward iterator,
// unless it is based on an input iterator, in which case it should be an
// input iterator.
template <class IteratorTag>
class prepend_iterator_tag_convertor
{
  public:
    typedef std::forward_iterator_tag iterator_category;
};
 
template <>
class prepend_iterator_tag_convertor<std::input_iterator_tag>
{
  public:
    typedef std::input_iterator_tag iterator_category;
};
 
// Iterator for term_appl which prepends a data_expression to a list convertible to data_expressions.
template <class Iterator >
class term_appl_prepend_iterator
{
  private:
    typedef std::iterator_traits<int*> traits;
 
  public:
    // The value_type.
    typedef data_expression value_type;
    // The reference type.
    typedef const data_expression& reference;
    // The pointer type.
    typedef const data_expression* pointer;
    // Difference type
    typedef ptrdiff_t difference_type;
    // The iterator category.
    // The iterator category is a forward_iterator, unless Iterator is an input iterator, in which case
    // it is an input iterator.
    typedef typename prepend_iterator_tag_convertor<traits::iterator_category>::iterator_category iterator_category;
 
  protected:
    Iterator m_it;
    pointer m_prepend;
 
  private:
    // Prevent the use of the following operators in this class, including the
    // postfix increment.
    reference operator[](difference_type n) const;
    term_appl_prepend_iterator operator++(int);
    term_appl_prepend_iterator& operator--();
    term_appl_prepend_iterator& operator--(int);
    term_appl_prepend_iterator& operator+=(difference_type n);
    term_appl_prepend_iterator& operator-=(difference_type n);
    term_appl_prepend_iterator operator+(difference_type n) const;
    term_appl_prepend_iterator operator-(difference_type n) const;
    difference_type operator-(const term_appl_prepend_iterator& other) const;
    difference_type distance_to(const term_appl_prepend_iterator& other) const;
 
  public:
    // Constructor.
    term_appl_prepend_iterator(Iterator it,
                               pointer prepend=nullptr)
      : m_it(it), m_prepend(prepend)
    {}
 
    // The copy constructor.
    term_appl_prepend_iterator(const term_appl_prepend_iterator& other)
      : m_it(other.m_it),
        m_prepend(other.m_prepend)
    {
    }
 
    // The assignment operator.
    // other The term to be assigned.
    // Returns a reference to the assigned iterator.
    term_appl_prepend_iterator& operator=(const term_appl_prepend_iterator& other)
    {
      m_it=other.m_it;
      m_prepend=other.m_prepend;
      return *this;
    }
 
    // The dereference operator.
    // Return the dereferenced term.
    reference operator*() const
    {
      if (m_prepend)
      {
        return *m_prepend;
      }
      return *(this->m_it);
    }
 
    // Dereference the current iterator.
    pointer operator->() const
    {
      if (m_prepend)
      {
        return m_prepend;
      }
      return &*(this->m_it);
    }
 
    // Prefix increment.
    // Returns the iterator after it is incremented.
    term_appl_prepend_iterator& operator++()
    {
      if (m_prepend)
      {
        m_prepend = nullptr;
      }
      else
      {
        ++(this->m_it);
      }
      return *this;
    }
 
    // Equality of iterators.
    bool operator ==(const term_appl_prepend_iterator& other) const
    {
      return m_prepend==other.m_prepend && this->m_it==other.m_it;
    }
 
    // Inequality of iterators.
    bool operator !=(const term_appl_prepend_iterator& other) const
    {
      return !(*this==other);
    }
 
    // Comparison of iterators.
    bool operator <(const term_appl_prepend_iterator& other) const
    {
      return m_prepend < other.m_prepend || (m_prepend==other.m_prepend && this->m_it<other.m_it);
    }
 
    // Comparison of iterators.
    bool operator <=(const term_appl_prepend_iterator& other) const
    {
      return m_prepend < other.m_prepend || (m_prepend==other.m_prepend && this->m_it<=other.m_it);
    }
 
    // Comparison of iterators.
    bool operator >(const term_appl_prepend_iterator& other) const
    {
      return other<*this;
    }
 
    // Comparison of iterators.
    bool operator >=(const term_appl_prepend_iterator& other) const
    {
      return other<=*this;
    }
};
 
// The class below transforms a function that is to be applied to
// the arguments of an application into a function that is not applied
// to the head, and only applied to the arguments. 
template <class ArgumentConverter>
class skip_function_application_to_head
{
  protected:
    ArgumentConverter& m_f;
    std::size_t m_current_index;
    const bool m_skip_head;
  public:
    skip_function_application_to_head(ArgumentConverter&f, const bool skip_head )
     : m_f(f),
       m_current_index(0),
       m_skip_head(skip_head)
    {}
 
    data_expression operator()(const data_expression& d)
    {
      if (m_skip_head && m_current_index++==0)
      {
        return d;
      }
      return m_f(d);
    }
};
 
// The class below transforms a function that is to be applied to
// the arguments of an application into a function that is not applied
// to the head, and only applied to the arguments. 
template <class ArgumentConverter>
class skip_function_application_to_head_assignment
{
  protected:
    ArgumentConverter& m_f;
    std::size_t m_current_index;
    const bool m_skip_head;
  public:
    skip_function_application_to_head_assignment(ArgumentConverter& f, const bool skip_head )
     : m_f(f),
       m_current_index(0),
       m_skip_head(skip_head)
    {}
 
    void operator()(data_expression& result, const data_expression& d)
    {
      if (m_skip_head && m_current_index++==0)
      {
        result=d;
        return;
      }
      m_f(result,d);
      return;
    }
};
 
 
inline bool contains_untyped_sort(const sort_expression& s)
{
  if (is_untyped_sort(s))
  {
    return true;
  }
  if (is_function_sort(s))
  {
    const function_sort& fs=atermpp::down_cast<function_sort>(s);
    if (contains_untyped_sort(fs.codomain()))
    {
      return true;
    }
    for(const sort_expression& sd: fs.domain())
    {
      if (contains_untyped_sort(sd))
      {
        return true;
      }
    }
  }
  if (is_container_sort(s))
  {
    if (contains_untyped_sort(atermpp::down_cast<container_sort>(s).element_sort()))
    {
      return true;
    }
  }
  assert(is_structured_sort(s) || is_basic_sort(s));
  return true;
}
 
inline const data_expression& evaluate_lambda_data_expression(const data_expression& t)
{
  return t;
}
 
template <class TERM> 
inline data_expression evaluate_lambda_data_expression(
               const TERM& t,
               typename std::enable_if<std::is_invocable_r<void, TERM, data_expression&>::value>::type* = nullptr) 
{
  data_expression result;
  t(result);
  return result;
}
 
template <class TERM >
inline data_expression evaluate_lambda_data_expression(
               const TERM& t, 
               typename std::enable_if<std::is_invocable_r<const data_expression, TERM, void>::value>::type* = nullptr)
{
  return t();
}
 
template <class HEAD, class CONTAINER>
inline bool check_whether_sorts_match(const HEAD& head_lambda, const CONTAINER& l)
{
  data_expression head = evaluate_lambda_data_expression(head_lambda);
  if (contains_untyped_sort(head.sort()))
  {
    // Most likely head is a just parsed, untyped object.
    return true;
  }
  function_sort fs(head.sort());
  if ((fs.domain().size()==1 && contains_untyped_sort(fs.domain().front())) ||
      (l.size()==1 && contains_untyped_sort(l.front().sort())))
  {
    // This is most likely an application from or to an Rewritten@@term, used in the jitty rewriter
    // to indicate that a term is in normal form.
    return true;
  }
  // Check that the sorts of the function domain of the head matches those of the arguments.
  if (fs.domain().size()!=l.size())
  {
    return false;
  }
  typename CONTAINER::const_iterator i=l.begin();
  for(const sort_expression& s: fs.domain())
  {
    if (!contains_untyped_sort(i->sort()) && s!=i->sort())
    {
      return false;
    }
    ++i;
  }
  return true;
}
 
inline data_expression_list get_arguments()
{
  return data_expression_list();
}
 
template <class HEAD, class... ARGUMENTS>
inline
data_expression_list get_arguments(const HEAD& h, const ARGUMENTS&... args)
{
  data_expression_list result=get_arguments(args...);
  result.push_front(evaluate_lambda_data_expression(h));
  return result;
}
 
/* template <class HEAD, class... CONTAINER>
inline bool check_whether_sorts_match(const HEAD& head_lambda, const CONTAINER&... l)
{
  data_expression_list arguments=get_arguments(l...);
  return check_whether_sorts_match(head_lambda, arguments);
} */
 
} // namespace detail
 
class application: public data_expression
{
  public:
    application()
      : data_expression(atermpp::aterm(core::detail::function_symbol_DataAppl(0)))
    {}
 
    template<typename ...Terms,
             typename = std::enable_if_t<std::conjunction_v<std::is_convertible<Terms, data_expression>...>> >
    application(const data_expression& head,
                const data_expression& arg1,
                const Terms& ...other_arguments
               )
      : data_expression(atermpp::aterm(
              core::detail::function_symbol_DataAppl(sizeof...(Terms)+2),head,arg1,other_arguments...))
    {
      assert(detail::check_whether_sorts_match(head, detail::get_arguments(arg1, other_arguments...)));
    }
 
    explicit application(const atermpp::aterm& term)
      : data_expression(term)
    {
      assert(core::detail::check_term_DataAppl(*this));
    }
 
    template <typename Container>
    application(const data_expression& head,
                const Container& arguments,
                typename atermpp::enable_if_container<Container, data_expression>::type* = nullptr)
      : data_expression(atermpp::aterm(core::detail::function_symbol_DataAppl(arguments.size() + 1),
                                         detail::term_appl_prepend_iterator<typename Container::const_iterator>(arguments.begin(), &head),
                                         detail::term_appl_prepend_iterator<typename Container::const_iterator>(arguments.end())))
    {
      assert(arguments.size()>0);
      assert(detail::check_whether_sorts_match(head,arguments));
    }
 
  private:
    // forbid the use of iterator, which is silently inherited from
    // aterm. Modifying the arguments of an application through the iterator
    // is not allowed!
    typedef data_expression::iterator iterator;
 
  public:
 
    typedef atermpp::term_appl_iterator<data_expression> const_iterator;
 
    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* = nullptr)
      : data_expression(atermpp::aterm(core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
                                         detail::term_appl_prepend_iterator<FwdIter>(first, &head),
                                         detail::term_appl_prepend_iterator<FwdIter>(last)))
    {
      assert(first!=last);
      assert(detail::check_whether_sorts_match(head,data_expression_list(begin(), end())));
    }
 
    template <typename FwdIter>
    application(const std::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::aterm(core::detail::function_symbol_DataAppl(arity + 1),
                                         detail::term_appl_prepend_iterator<FwdIter>(first, &head),
                                         detail::term_appl_prepend_iterator<FwdIter>(last)))
    {
      assert(arity>0);
      assert(std::distance(first, last)==arity);
      assert(detail::check_whether_sorts_match(head,data_expression_list(begin(), end())));
    }
 
 
    template <typename FwdIter, class ArgumentConverter>
    application(const data_expression& head,
                FwdIter first,
                FwdIter last,
                ArgumentConverter convert_arguments,
                const bool skip_first_argument=false,
                typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr,
                typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = nullptr )
                // typename std::enable_if< std::is_convertible<typename std::invoke_result<ArgumentConverter,typename FwdIter::value_type>::type, data_expression>::value>::type* = nullptr)
      : data_expression(atermpp::aterm(
                                 core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
                                 detail::term_appl_prepend_iterator<FwdIter>(first, &head),
                                 detail::term_appl_prepend_iterator<FwdIter>(last),
                                 detail::skip_function_application_to_head(convert_arguments,skip_first_argument)))
    {
      assert(first!=last);
      assert(detail::check_whether_sorts_match(head,data_expression_list(begin(), end())));
    } 
 
    template <typename FwdIter, class ArgumentConverter>
    application(const data_expression& head,
                FwdIter first,
                FwdIter last,
                ArgumentConverter convert_arguments,
                const bool skip_first_argument=false,
                typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr,
                typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = nullptr,
                typename std::enable_if<std::is_same<typename std::invoke_result<ArgumentConverter,data_expression&,typename FwdIter::value_type>::type, void>::value>::type* = nullptr)
 
      : data_expression(atermpp::aterm(
                                 core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
                                 detail::term_appl_prepend_iterator<FwdIter>(first, &head),
                                 detail::term_appl_prepend_iterator<FwdIter>(last),
                                 detail::skip_function_application_to_head_assignment(convert_arguments,skip_first_argument)))
    {
      assert(first!=last);
      assert(detail::check_whether_sorts_match(head,data_expression_list(begin(), end())));
    }
 
    application(const application&) noexcept = default;
    application(application&&) noexcept = default;
    application& operator=(const application&) noexcept = default;
    application& operator=(application&&) noexcept = default;
 
    const data_expression& head() const
    {
      return atermpp::down_cast<data_expression>(atermpp::aterm::operator[](0));
    }
 
    const data_expression& operator[](std::size_t index) const
    {
      assert(index<size());
      return atermpp::down_cast<data_expression>(atermpp::aterm::operator[](index+1));
    }
 
    const_iterator begin() const
    {
      return atermpp::detail::aterm_appl_iterator_cast<data_expression>(atermpp::aterm::begin()+1);
    }
 
    const_iterator end() const
    {
      return atermpp::detail::aterm_appl_iterator_cast<data_expression>(atermpp::aterm::end());
    }
 
    std::size_t size() const
    {
      return atermpp::aterm::size() - 1;
    }
};
 
inline void swap(application& t1, application& t2)
{
  t1.swap(t2);
}
 
inline void make_application(atermpp::aterm& result)
{
  atermpp::make_term_appl(result,core::detail::function_symbol_DataAppl(1));
}
 
/* 
// ---------------------------------------------------------------------------------
// ---------------------------- TYPEDEF --------------------------------------------
// ---------------------------------------------------------------------------------
template <typename TERM, typename = void>
struct yields_a_data_expression
    : public std::false_type
{
};
 
template <typename TERM>
struct yields_a_data_expression<TERM,
                                typename std::enable_if<std::is_convertible<TERM, data_expression>::type>::type >
    : public std::true_type
{}; */
 
template<typename HEAD, typename TERM, typename ...Terms,
                  typename = std::enable_if_t<
                                 std::disjunction<typename std::is_convertible<HEAD, data_expression>,
                                                  typename std::is_invocable_r<void, HEAD, data_expression&>,
                                                  typename std::is_invocable_r<const data_expression, HEAD, void> >::value >,
                  typename = std::enable_if_t<std::conjunction_v<
                                 std::disjunction<typename std::is_convertible<Terms, data_expression>,
                                                  typename std::is_invocable_r<void, Terms, data_expression&>,
                                                  typename std::is_invocable_r<const data_expression, Terms, void> > ...>> > 
inline void make_application(
                atermpp::aterm& result,
                const HEAD& head,
                const TERM& arg1,
                const Terms& ...other_arguments
               )
{
  assert(detail::check_whether_sorts_match(head, detail::get_arguments(arg1, other_arguments...)));
  atermpp::make_term_appl(result,
                          core::detail::function_symbol_DataAppl(sizeof...(Terms)+2),
                          head,
                          arg1, 
                          other_arguments...);
}
 
template <typename Container>
inline void make_application(data_expression& result,
                      const data_expression& head,
                      const Container& arguments,
                      typename atermpp::enable_if_container<Container, data_expression>::type* = nullptr)
{
  assert(arguments.size()>0);
  assert(detail::check_whether_sorts_match(head,arguments));
  atermpp::make_term_appl(result,
                          core::detail::function_symbol_DataAppl(arguments.size() + 1),
                          detail::term_appl_prepend_iterator<typename Container::const_iterator>(arguments.begin(), &head),
                          detail::term_appl_prepend_iterator<typename Container::const_iterator>(arguments.end()));
}
 
template <typename FwdIter>
inline void make_application(atermpp::aterm& result,
                      const data_expression& head,
                      FwdIter first,
                      FwdIter last,
                      typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr)
{
  assert(first!=last);
  atermpp::make_term_appl(result,
                          core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
                          detail::term_appl_prepend_iterator<FwdIter>(first, &head),
                          detail::term_appl_prepend_iterator<FwdIter>(last));
  assert(detail::check_whether_sorts_match(head,data_expression_list(
                                                   atermpp::down_cast<application>(result).begin(), 
                                                   atermpp::down_cast<application>(result).end())));
}
 
template <typename FwdIter>
inline void make_application(atermpp::aterm& result,
                      const std::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)
{
  assert(arity>0);
  assert(std::distance(first, last)==arity);
  atermpp::make_term_appl(result,
                          core::detail::function_symbol_DataAppl(arity + 1),
                          detail::term_appl_prepend_iterator<FwdIter>(first, &head),
                          detail::term_appl_prepend_iterator<FwdIter>(last));
  assert(detail::check_whether_sorts_match(head,data_expression_list(
                                                   atermpp::down_cast<application>(result).begin(),
                                                   atermpp::down_cast<application>(result).end())));
}
 
 
template <typename FwdIter, class ArgumentConverter>
inline void make_application(atermpp::aterm& result,
                      const data_expression& head,
                      FwdIter first,
                      FwdIter last,
                      ArgumentConverter convert_arguments,
                      const bool skip_first_argument=false,
                      typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr,
                      typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = nullptr,
                      typename std::enable_if< std::is_same<typename std::invoke_result<ArgumentConverter,typename FwdIter::value_type>::type, data_expression>::value>::type* = nullptr)
{
  assert(first!=last);
  atermpp::make_term_appl(result,
                          core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
                          detail::term_appl_prepend_iterator<FwdIter>(first, &head),
                          detail::term_appl_prepend_iterator<FwdIter>(last),
                          detail::skip_function_application_to_head(convert_arguments,skip_first_argument));
  assert(detail::check_whether_sorts_match(head,data_expression_list(
                                                   atermpp::down_cast<application>(result).begin(),
                                                   atermpp::down_cast<application>(result).end())));
} 
 
template <typename FwdIter, class ArgumentConverter>
static inline void make_application(
            atermpp::aterm& result,
            const data_expression& head,
            FwdIter first,
            FwdIter last,
            ArgumentConverter convert_arguments,
            const bool skip_first_argument=false,
            typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr,
            typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = nullptr,
            typename std::enable_if<std::is_same<typename std::invoke_result<ArgumentConverter,data_expression&,typename FwdIter::value_type>::type, void>::value>::type* = nullptr)
{
  atermpp::make_term_appl(
                          result,
                          core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
                          detail::term_appl_prepend_iterator<FwdIter>(first, &head),
                          detail::term_appl_prepend_iterator<FwdIter>(last),
                          detail::skip_function_application_to_head_assignment(convert_arguments,skip_first_argument));
}
 
 
//--- start generated class application ---//
// prototype declaration
std::string pp(const application& x);
 
inline
std::ostream& operator<<(std::ostream& out, const application& x)
{
  return out << data::pp(x);
}
//--- end generated class application ---//
 
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