mcrl2/data/list.h

Include file:

#include "mcrl2/data/list.h"

The standard sort list.

This file was generated from the data sort specification mcrl2/data/build/list.spec.

Typedefs

type mcrl2::data::sort_list::implementation_map

typedef for std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > >

Functions

const data_expression &mcrl2::data::sort_list::arg(const data_expression &e)

Function for projecting out argument. arg from an application.

Parameters:

• e A data expression.

Pre: arg is defined for e.

Returns: The argument of e that corresponds to arg.

function_symbol mcrl2::data::sort_list::concat(const sort_expression &s)

Constructor for function symbol ++.

Parameters:

• s A sort expression.

Returns: Function symbol concat.

application mcrl2::data::sort_list::concat(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol ++.

Parameters:

• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

Returns: Application of ++ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::concat_name()

Generate identifier ++.

Returns: Identifier ++.

function_symbol mcrl2::data::sort_list::cons_(const sort_expression &s)

Constructor for function symbol |>.

Parameters:

• s A sort expression.

Returns: Function symbol cons_.

application mcrl2::data::sort_list::cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol |>.

Parameters:

• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

Returns: Application of |> to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::cons_name()

Generate identifier |>.

Returns: Identifier |>.

function_symbol mcrl2::data::sort_list::count(const sort_expression &s)

Constructor for function symbol #.

Parameters:

• s A sort expression.

Returns: Function symbol count.

application mcrl2::data::sort_list::count(const sort_expression &s, const data_expression &arg0)

Application of function symbol #.

Parameters:

• s A sort expression.
• arg0 A data expression.

Returns: Application of # to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::count_name()

Generate identifier #.

Returns: Identifier #.

function_symbol mcrl2::data::sort_list::element_at(const sort_expression &s)

Constructor for function symbol ..

Parameters:

• s A sort expression.

Returns: Function symbol element_at.

application mcrl2::data::sort_list::element_at(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol ..

Parameters:

• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

Returns: Application of . to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::element_at_name()

Generate identifier ..

Returns: Identifier ..

function_symbol mcrl2::data::sort_list::empty(const sort_expression &s)

Constructor for function symbol [].

Parameters:

• s A sort expression.

Returns: Function symbol empty.

const core::identifier_string &mcrl2::data::sort_list::empty_name()

Generate identifier [].

Returns: Identifier [].

function_symbol mcrl2::data::sort_list::head(const sort_expression &s)

Constructor for function symbol head.

Parameters:

• s A sort expression.

Returns: Function symbol head.

application mcrl2::data::sort_list::head(const sort_expression &s, const data_expression &arg0)

Application of function symbol head.

Parameters:

• s A sort expression.
• arg0 A data expression.

Returns: Application of head to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::head_name()

Generate identifier head.

Returns: Identifier head.

function_symbol mcrl2::data::sort_list::in(const sort_expression &s)

Constructor for function symbol in.

Parameters:

• s A sort expression.

Returns: Function symbol in.

application mcrl2::data::sort_list::in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol in.

Parameters:

• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

Returns: Application of in to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::in_name()

Generate identifier in.

Returns: Identifier in.

bool mcrl2::data::sort_list::is_concat_application(const atermpp::aterm_appl &e)

Recogniser for application of ++.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol concat to a number of arguments.

bool mcrl2::data::sort_list::is_concat_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function ++.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching ++.

bool mcrl2::data::sort_list::is_cons_application(const atermpp::aterm_appl &e)

Recogniser for application of |>.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol cons_ to a number of arguments.

bool mcrl2::data::sort_list::is_cons_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function |>.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching |>.

bool mcrl2::data::sort_list::is_count_application(const atermpp::aterm_appl &e)

Recogniser for application of #.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol count to a number of arguments.

bool mcrl2::data::sort_list::is_count_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function #.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching #.

bool mcrl2::data::sort_list::is_element_at_application(const atermpp::aterm_appl &e)

Recogniser for application of ..

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol element_at to a number of arguments.

bool mcrl2::data::sort_list::is_element_at_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function ..

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching ..

bool mcrl2::data::sort_list::is_empty_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function [].

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching [].

bool mcrl2::data::sort_list::is_head_application(const atermpp::aterm_appl &e)

Recogniser for application of head.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol head to a number of arguments.

bool mcrl2::data::sort_list::is_head_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function head.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching head.

bool mcrl2::data::sort_list::is_in_application(const atermpp::aterm_appl &e)

Recogniser for application of in.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol in to a number of arguments.

bool mcrl2::data::sort_list::is_in_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function in.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching in.

bool mcrl2::data::sort_list::is_list(const sort_expression &e)

Recogniser for sort expression List(s)

Parameters:

• e A sort expression

Returns: true iff e is a container sort of which the name matches list

bool mcrl2::data::sort_list::is_rhead_application(const atermpp::aterm_appl &e)

Recogniser for application of rhead.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol rhead to a number of arguments.

bool mcrl2::data::sort_list::is_rhead_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function rhead.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching rhead.

bool mcrl2::data::sort_list::is_rtail_application(const atermpp::aterm_appl &e)

Recogniser for application of rtail.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol rtail to a number of arguments.

bool mcrl2::data::sort_list::is_rtail_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function rtail.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching rtail.

bool mcrl2::data::sort_list::is_snoc_application(const atermpp::aterm_appl &e)

Recogniser for application of <|.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol snoc to a number of arguments.

bool mcrl2::data::sort_list::is_snoc_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function <|.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching <|.

bool mcrl2::data::sort_list::is_tail_application(const atermpp::aterm_appl &e)

Recogniser for application of tail.

Parameters:

• e A data expression.

Returns: true iff e is an application of function symbol tail to a number of arguments.

bool mcrl2::data::sort_list::is_tail_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function tail.

Parameters:

• e A data expression.

Returns: true iff e is the function symbol matching tail.

const data_expression &mcrl2::data::sort_list::left(const data_expression &e)

Function for projecting out argument. left from an application.

Parameters:

• e A data expression.

Pre: left is defined for e.

Returns: The argument of e that corresponds to left.

container_sort mcrl2::data::sort_list::list(const sort_expression &s)

Constructor for sort expression List(S)

Parameters:

• s A sort expression

Returns: Sort expression list(s)

implementation_map mcrl2::data::sort_list::list_cpp_implementable_constructors(const sort_expression &s)

Give all system defined constructors which have an implementation in C++ and not in rewrite rules for list.

Parameters:

• s A sort expression.

Returns: All system defined constructors that are to be implemented in C++ for list.

implementation_map mcrl2::data::sort_list::list_cpp_implementable_mappings(const sort_expression &s)

Give all system defined mappings that are to be implemented in C++ code for list.

Parameters:

• s A sort expression

Returns: A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for list

function_symbol_vector mcrl2::data::sort_list::list_generate_constructors_and_functions_code(const sort_expression &s)

Give all system defined mappings and constructors for list.

Parameters:

• s A sort expression

Returns: All system defined mappings for list

function_symbol_vector mcrl2::data::sort_list::list_generate_constructors_code(const sort_expression &s)

Give all system defined constructors for list.

Parameters:

• s A sort expression.

Returns: All system defined constructors for list.

data_equation_vector mcrl2::data::sort_list::list_generate_equations_code(const sort_expression &s)

Give all system defined equations for list.

Parameters:

• s A sort expression

Returns: All system defined equations for sort list

function_symbol_vector mcrl2::data::sort_list::list_generate_functions_code(const sort_expression &s)

Give all system defined mappings for list.

Parameters:

• s A sort expression

Returns: All system defined mappings for list

function_symbol_vector mcrl2::data::sort_list::list_mCRL2_usable_constructors(const sort_expression &s)

Give all defined constructors which can be used in mCRL2 specs for list.

Parameters:

• s A sort expression.

Returns: All system defined constructors that can be used in an mCRL2 specification for list.

function_symbol_vector mcrl2::data::sort_list::list_mCRL2_usable_mappings(const sort_expression &s)

Give all system defined mappings that can be used in mCRL2 specs for list.

Parameters:

• s A sort expression

Returns: All system defined mappings for that can be used in mCRL2 specificationis list

void mcrl2::data::sort_list::make_concat(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol ++.

Parameters:

• result The data expression where the ++ expression is put.
• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

void mcrl2::data::sort_list::make_cons_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol |>.

Parameters:

• result The data expression where the |> expression is put.
• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

void mcrl2::data::sort_list::make_count(data_expression &result, const sort_expression &s, const data_expression &arg0)

Make an application of function symbol #.

Parameters:

• result The data expression where the # expression is put.
• s A sort expression.
• arg0 A data expression.

void mcrl2::data::sort_list::make_element_at(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol ..

Parameters:

• result The data expression where the . expression is put.
• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

void mcrl2::data::sort_list::make_head(data_expression &result, const sort_expression &s, const data_expression &arg0)

Make an application of function symbol head.

Parameters:

• result The data expression where the head expression is put.
• s A sort expression.
• arg0 A data expression.

void mcrl2::data::sort_list::make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol in.

Parameters:

• result The data expression where the in expression is put.
• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

void mcrl2::data::sort_list::make_rhead(data_expression &result, const sort_expression &s, const data_expression &arg0)

Make an application of function symbol rhead.

Parameters:

• result The data expression where the rhead expression is put.
• s A sort expression.
• arg0 A data expression.

void mcrl2::data::sort_list::make_rtail(data_expression &result, const sort_expression &s, const data_expression &arg0)

Make an application of function symbol rtail.

Parameters:

• result The data expression where the rtail expression is put.
• s A sort expression.
• arg0 A data expression.

void mcrl2::data::sort_list::make_snoc(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol <|.

Parameters:

• result The data expression where the <| expression is put.
• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

void mcrl2::data::sort_list::make_tail(data_expression &result, const sort_expression &s, const data_expression &arg0)

Make an application of function symbol tail.

Parameters:

• result The data expression where the tail expression is put.
• s A sort expression.
• arg0 A data expression.

function_symbol mcrl2::data::sort_list::rhead(const sort_expression &s)

Constructor for function symbol rhead.

Parameters:

• s A sort expression.

Returns: Function symbol rhead.

application mcrl2::data::sort_list::rhead(const sort_expression &s, const data_expression &arg0)

Application of function symbol rhead.

Parameters:

• s A sort expression.
• arg0 A data expression.

Returns: Application of rhead to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::rhead_name()

Generate identifier rhead.

Returns: Identifier rhead.

const data_expression &mcrl2::data::sort_list::right(const data_expression &e)

Function for projecting out argument. right from an application.

Parameters:

• e A data expression.

Pre: right is defined for e.

Returns: The argument of e that corresponds to right.

function_symbol mcrl2::data::sort_list::rtail(const sort_expression &s)

Constructor for function symbol rtail.

Parameters:

• s A sort expression.

Returns: Function symbol rtail.

application mcrl2::data::sort_list::rtail(const sort_expression &s, const data_expression &arg0)

Application of function symbol rtail.

Parameters:

• s A sort expression.
• arg0 A data expression.

Returns: Application of rtail to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::rtail_name()

Generate identifier rtail.

Returns: Identifier rtail.

function_symbol mcrl2::data::sort_list::snoc(const sort_expression &s)

Constructor for function symbol <|.

Parameters:

• s A sort expression.

Returns: Function symbol snoc.

application mcrl2::data::sort_list::snoc(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol <|.

Parameters:

• s A sort expression.
• arg0 A data expression.
• arg1 A data expression.

Returns: Application of <| to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::snoc_name()

Generate identifier <|.

Returns: Identifier <|.

function_symbol mcrl2::data::sort_list::tail(const sort_expression &s)

Constructor for function symbol tail.

Parameters:

• s A sort expression.

Returns: Function symbol tail.

application mcrl2::data::sort_list::tail(const sort_expression &s, const data_expression &arg0)

Application of function symbol tail.

Parameters:

• s A sort expression.
• arg0 A data expression.

Returns: Application of tail to a number of arguments.

const core::identifier_string &mcrl2::data::sort_list::tail_name()

Generate identifier tail.

Returns: Identifier tail.