mcrl2/data/application.h

Include file:

#include "mcrl2/data/application.h"

The class application.

Functions

const data_expression &mcrl2::data::binary_left(const application &x)
const data_expression &mcrl2::data::binary_left1(const data_expression &x)
const data_expression &mcrl2::data::binary_right(const application &x)
const data_expression &mcrl2::data::binary_right1(const data_expression &x)
void mcrl2::data::make_application(atermpp::aterm &result)

Make function for an application.

Parameters:

  • result variable into which the application is constructed.
static void mcrl2::data::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)

Constructor.

Construct at term head(arg_first,…,arg_last) where convert_arguments has been applied to the head and all the arguments.

Parameters:

  • result variable into which the application is constructed. 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.
void mcrl2::data::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)

Constructor.

Construct at term head(arg_first,…,arg_last) where convert_arguments has been applied to the head and all the arguments.

Parameters:

  • result variable into which the application is constructed. 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.
void mcrl2::data::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)

Constructor.

Parameters:

  • result variable into which the application is constructed.
void mcrl2::data::make_application(atermpp::aterm &result, const HEAD &head, const TERM &arg1, const Terms&... other_arguments)

Constructor.

Parameters:

  • result variable into which the application is constructed.
void mcrl2::data::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)

Constructor.

Parameters:

  • result variable into which the application is constructed.
void mcrl2::data::make_application(data_expression &result, const data_expression &head, const Container &arguments, typename atermpp::enable_if_container<Container, data_expression>::type * = nullptr)

Constructor.

Parameters:

  • result variable into which the application is constructed.
std::ostream &mcrl2::data::operator<<(std::ostream &out, const application &x)

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

void mcrl2::data::swap(application &t1, application &t2)

swap overload

const data_expression &mcrl2::data::unary_operand(const application &x)
const data_expression &mcrl2::data::unary_operand1(const data_expression &x)

Functions

bool mcrl2::data::detail::check_whether_sorts_match(const HEAD &head_lambda, const CONTAINER &l)
bool mcrl2::data::detail::contains_untyped_sort(const sort_expression &s)
const data_expression &mcrl2::data::detail::evaluate_lambda_data_expression(const data_expression &t)
data_expression mcrl2::data::detail::evaluate_lambda_data_expression(const TERM &t, typename std::enable_if<std::is_invocable_r<const data_expression, TERM, void>::value>::type * = nullptr)
data_expression mcrl2::data::detail::evaluate_lambda_data_expression(const TERM &t, typename std::enable_if<std::is_invocable_r<void, TERM, data_expression&>::value>::type * = nullptr)
data_expression_list mcrl2::data::detail::get_arguments()
data_expression_list mcrl2::data::detail::get_arguments(const HEAD &h, const ARGUMENTS&... args)