An application of a data expression to a number of arguments. More...

#include <application.h>

Inheritance diagram for mcrl2::data::application:

Public Types
typedef atermpp::term_appl_iterator< data_expression >	const_iterator
	An iterator to traverse the arguments of an application.

Public Types inherited from atermpp::aterm
typedef std::size_t	size_type
	An unsigned integral type.

typedef ptrdiff_t	difference_type
	A signed integral type.

typedef term_appl_iterator< aterm >	iterator
	Iterator used to iterate through an term_appl.

typedef term_appl_iterator< aterm >	const_iterator
	Const iterator used to iterate through an term_appl.

Public Member Functions
	application ()
	Default constructor.

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)
	Constructor.

	application (const atermpp::aterm &term)
	Constructor.

template<typename Container >
	application (const data_expression &head, const Container &arguments, typename atermpp::enable_if_container< Container, data_expression >::type *=nullptr)
	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 *=nullptr)
	Constructor.

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)
	Constructor.

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)
	Constructor.

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)
	Constructor.

	application (const application &) noexcept=default
	Move semantics.

	application (application &&) noexcept=default

application &	operator= (const application &) noexcept=default

application &	operator= (application &&) noexcept=default

const data_expression &	head () const
	Get the function at the head of this expression.

const data_expression &	operator[] (std::size_t index) const
	Get the i-th argument of this expression.

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.

std::size_t	size () const

Public Member Functions inherited from mcrl2::data::data_expression
	data_expression ()
	\brief Default constructor X3.

	data_expression (const atermpp::aterm &term)

	data_expression (const data_expression &) noexcept=default
	Move semantics.

	data_expression (data_expression &&) noexcept=default

data_expression &	operator= (const data_expression &) noexcept=default

data_expression &	operator= (data_expression &&) noexcept=default

bool	is_default_data_expression () const
	A function to efficiently determine whether a data expression is made by the default constructor.

application	operator() (const data_expression &e) const
	Apply a data expression to a data expression.

application	operator() (const data_expression &e1, const data_expression &e2) const
	Apply a data expression to two data expressions.

application	operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3) const
	Apply a data expression to three data expressions.

application	operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4) const
	Apply a data expression to four data expressions.

application	operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5) const
	Apply a data expression to five data expressions.

application	operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5, const data_expression &e6) const
	Apply a data expression to six data expressions.

sort_expression	sort () const
	Returns the sort of the data expression.

Public Member Functions inherited from atermpp::aterm
	aterm ()
	Default constructor.

	aterm (const aterm &other) noexcept=default
	This class has user-declared copy constructor so declare default copy and move operators.

aterm &	operator= (const aterm &other) noexcept=default

	aterm (aterm &&other) noexcept=default

aterm &	operator= (aterm &&other) noexcept=default

template<class ForwardIterator , typename std::enable_if< mcrl2::utilities::is_iterator< ForwardIterator >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::output_iterator_tag >::value >::type * = nullptr>
	aterm (const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
	Constructor that provides an aterm based on a function symbol and forward iterator providing the arguments.

template<class InputIterator , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr, typename std::enable_if< std::is_same< typename InputIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr>
	aterm (const function_symbol &sym, InputIterator begin, InputIterator end)
	Constructor that provides an aterm based on a function symbol and an input iterator providing the arguments.

template<class InputIterator , class TermConverter , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr>
	aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter)

	aterm (const function_symbol &sym)
	Constructor.

template<typename ... Terms>
	aterm (const function_symbol &symbol, const Terms &...arguments)
	Constructor for n-arity function application.

const function_symbol &	function () const
	Returns the function symbol belonging to an aterm.

size_type	size () const
	Returns the number of arguments of this term.

bool	empty () const
	Returns true if the term has no arguments.

const_iterator	begin () const
	Returns an iterator pointing to the first argument.

const_iterator	end () const
	Returns a const_iterator pointing past the last argument.

constexpr size_type	max_size () const
	Returns the largest possible number of arguments.

const aterm &	operator[] (const size_type i) const
	Returns the i-th argument.

Public Member Functions inherited from atermpp::aterm_core
	aterm_core () noexcept
	Default constructor.

	~aterm_core () noexcept
	Standard destructor.

	aterm_core (const detail::_aterm *t) noexcept
	Constructor based on an internal term data structure. This is not for public use.

	aterm_core (const aterm_core &other) noexcept
	Copy constructor.

	aterm_core (aterm_core &&other) noexcept
	Move constructor.

aterm_core &	operator= (const aterm_core &other) noexcept
	Assignment operator.

aterm_core &	assign (const aterm_core &other, detail::thread_aterm_pool &pool) noexcept
	Assignment operator, to be used if busy and forbidden flags are explicitly available.

template<bool CHECK_BUSY_FLAG = true>
aterm_core &	unprotected_assign (const aterm_core &other) noexcept
	Assignment operator, to be used when the busy flags do not need to be set.

aterm_core &	operator= (aterm_core &&other) noexcept
	Move assignment operator.

Public Member Functions inherited from atermpp::unprotected_aterm_core
	unprotected_aterm_core () noexcept
	Default constuctor.

	unprotected_aterm_core (const detail::_aterm *term) noexcept
	Constructor.

bool	type_is_appl () const noexcept
	Dynamic check whether the term is an aterm.

bool	type_is_int () const noexcept
	Dynamic check whether the term is an aterm_int.

bool	type_is_list () const noexcept
	Dynamic check whether the term is an aterm_list.

bool	operator== (const unprotected_aterm_core &t) const
	Comparison operator.

bool	operator!= (const unprotected_aterm_core &t) const
	Inequality operator on two unprotected aterms.

bool	operator< (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	operator> (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	operator<= (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	operator>= (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	defined () const
	Returns true if this term is not equal to the term assigned by the default constructor of aterms, aterm_appls and aterm_int.

void	swap (unprotected_aterm_core &t) noexcept
	Swaps this term with its argument.

const function_symbol &	function () const
	Yields the function symbol in an aterm.

Private Types
typedef data_expression::iterator	iterator

Additional Inherited Members
Protected Member Functions inherited from atermpp::aterm
	aterm (detail::_term_appl *t)
	Constructor.

Protected Attributes inherited from atermpp::unprotected_aterm_core
const detail::_aterm *	m_term

Detailed Description

An application of a data expression to a number of arguments.

Definition at line 352 of file application.h.

Member Typedef Documentation

◆ const_iterator

typedef atermpp::term_appl_iterator<data_expression> mcrl2::data::application::const_iterator

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 from which an application is derived. As an application has a head as its first argument, the iterator of the aterm 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.

Definition at line 410 of file application.h.

◆ iterator

typedef data_expression::iterator mcrl2::data::application::iterator

private

Definition at line 398 of file application.h.

Constructor & Destructor Documentation

◆ application() [1/10]

mcrl2::data::application::application ( )

inline

Default constructor.

Definition at line 356 of file application.h.

◆ application() [2/10]

template<typename ... Terms, typename = std::enable_if_t<std::conjunction_v<std::is_convertible<Terms, data_expression>...>>>

mcrl2::data::application::application	(	const data_expression &	head,
		const data_expression &	arg1,
		const Terms &...	other_arguments
	)

inline

Constructor.

Definition at line 363 of file application.h.

◆ application() [3/10]

mcrl2::data::application::application ( const atermpp::aterm & term )

inlineexplicit

Constructor.

Parameters

term A term

Definition at line 375 of file application.h.

◆ application() [4/10]

template<typename Container >

mcrl2::data::application::application	(	const data_expression &	head,
		const Container &	arguments,
		typename atermpp::enable_if_container< Container, data_expression >::type *	= `nullptr`
	)

inline

Constructor.

Definition at line 383 of file application.h.

◆ application() [5/10]

template<typename FwdIter >

mcrl2::data::application::application	(	const data_expression &	head,
		FwdIter	first,
		FwdIter	last,
		typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *	= `nullptr`
	)

inline

Constructor.

Definition at line 414 of file application.h.

◆ application() [6/10]

template<typename FwdIter >

mcrl2::data::application::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`
	)

inline

Constructor.

Definition at line 428 of file application.h.

◆ application() [7/10]

template<typename FwdIter , class ArgumentConverter >

mcrl2::data::application::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`
	)

inline

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.

Definition at line 452 of file application.h.

◆ application() [8/10]

template<typename FwdIter , class ArgumentConverter >

mcrl2::data::application::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`
	)

inline

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.

Definition at line 479 of file application.h.

◆ application() [9/10]

mcrl2::data::application::application ( const application & )

defaultnoexcept

Move semantics.

◆ application() [10/10]

mcrl2::data::application::application ( application && )

defaultnoexcept

Member Function Documentation

◆ begin()

const_iterator mcrl2::data::application::begin ( ) const

inline

Returns an iterator pointing to the first argument of the application.

Definition at line 519 of file application.h.

◆ end()

const_iterator mcrl2::data::application::end ( ) const

inline

Returns an iterator pointing past the last argument of the application.

Definition at line 526 of file application.h.

◆ head()

const data_expression & mcrl2::data::application::head ( ) const

inline

Get the function at the head of this expression.

Definition at line 505 of file application.h.

◆ operator=() [1/2]

application & mcrl2::data::application::operator= ( application && )

defaultnoexcept

◆ operator=() [2/2]

application & mcrl2::data::application::operator= ( const application & )

defaultnoexcept

◆ operator[]()

const data_expression & mcrl2::data::application::operator[] ( std::size_t index ) const

inline

Get the i-th argument of this expression.

Definition at line 511 of file application.h.

◆ size()

std::size_t mcrl2::data::application::size ( ) const

inline

Returns: The number of arguments of this application.

Definition at line 532 of file application.h.

The documentation for this class was generated from the following file:

data/include/mcrl2/data/application.h

Public Types

Public Member Functions

Private Types

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ iterator

Constructor & Destructor Documentation

◆ application() [1/10]

◆ application() [2/10]

◆ application() [3/10]

◆ application() [4/10]

◆ application() [5/10]

◆ application() [6/10]

◆ application() [7/10]

◆ application() [8/10]

◆ application() [9/10]

◆ application() [10/10]

Member Function Documentation

◆ begin()

◆ end()

◆ head()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator[]()

◆ size()