mcrl2::data::application¶
Include file:
#include "mcrl2/data/application.h
-
class
mcrl2::data::application¶ An application of a data expression to a number of arguments.
Private types¶
-
type
mcrl2::data::application::iterator¶ typedef for
data_expression::iterator
Public types¶
-
type
mcrl2::data::application::const_iterator¶ typedef for
atermpp::term_appl_iterator< data_expression >An iterator to traverse the arguments of an application.
There is a subtle difference with the arguments of an iterator on the arguments of an aterm_appl from which an application is derived. As an application has a head as its first argument, the iterator of the aterm_appl starts at this head, where the iterator of the application starts at the first argument. This also means that t[n] for t an application is equal to t[n+1] if t is interpreted as an aterm_appl.
Public member functions¶
-
application()¶ Default constructor.
-
application(application&&) noexcept = default¶
-
application(const application&) noexcept = default¶ Move semantics.
-
application(const data_expression &head, const Container &arguments, typename atermpp::enable_if_container<Container, data_expression>::type * = nullptr)¶ Constructor.
-
application(const data_expression &head, const data_expression &arg1, const Terms&... other_arguments)¶ Constructor.
-
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)¶ Constructor.
Construct at term head(arg_first,…,arg_last) where convert_arguments has been applied to the head and all the arguments. parameter head This is the new head for the application. parameter first This is a forward iterator yielding the first argument. parameter last This is an iterator beyond the last argument. parameter convert_arguments This is a function applied to optionally the head and the arguments. parameter skip_first_argument A boolean which is true if the function must not be applied to the head.
-
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)¶ Constructor.
Construct at term head(arg_first,…,arg_last) where convert_arguments has been applied to the head and all the arguments. parameter head This is the new head for the application. parameter first This is a forward iterator yielding the first argument. parameter last This is an iterator beyond the last argument. parameter convert_arguments This is a function applied to optionally the head and the arguments. parameter skip_first_argument A boolean which is true if the function must not be applied to the head.
-
application(const data_expression &head, FwdIter first, FwdIter last, typename std::enable_if<!std::is_base_of<data_expression, FwdIter>::value>::type * = nullptr)¶ Constructor.
-
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)¶ Constructor.
-
const_iterator
begin() const Returns an iterator pointing to the first argument of the application.
-
const_iterator
end() const Returns an iterator pointing past the last argument of the application.
-
const data_expression &
head() const¶ Get the function at the head of this expression.
-
application &
operator=(application&&) noexcept = default¶
-
application &
operator=(const application&) noexcept = default¶
-
const data_expression &
operator[](std::size_t index) const Get the i-th argument of this expression.
-
std::size_t
size() const Returns: The number of arguments of this application.
