mcrl2::data::sort_list Namespace Reference

Namespace for system defined sort list. More...

Typedefs
using	implementation_map = std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > >

Functions
container_sort	list (const sort_expression &s)
	Constructor for sort expression List(S)
bool	is_list (const sort_expression &e)
	Recogniser for sort expression List(s)
const core::identifier_string &	empty_name ()
	Generate identifier [].
function_symbol	empty (const sort_expression &s)
	Constructor for function symbol [].
bool	is_empty_function_symbol (const atermpp::aterm &e)
	Recogniser for function [].
const core::identifier_string &	cons_name ()
	Generate identifier |>.
function_symbol	cons_ (const sort_expression &s)
	Constructor for function symbol |>.
bool	is_cons_function_symbol (const atermpp::aterm &e)
	Recogniser for function |>.
application	cons_ (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol |>.
void	make_cons (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol |>.
bool	is_cons_application (const atermpp::aterm &e)
	Recogniser for application of |>.
function_symbol_vector	list_generate_constructors_code (const sort_expression &s)
	Give all system defined constructors for list.
function_symbol_vector	list_mCRL2_usable_constructors (const sort_expression &s)
	Give all defined constructors which can be used in mCRL2 specs for list.
implementation_map	list_cpp_implementable_constructors (const sort_expression &)
	Give all system defined constructors which have an implementation in C++ and not in rewrite rules for list.
const core::identifier_string &	in_name ()
	Generate identifier in.
function_symbol	in (const sort_expression &s)
	Constructor for function symbol in.
bool	is_in_function_symbol (const atermpp::aterm &e)
	Recogniser for function in.
application	in (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol in.
void	make_in (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol in.
bool	is_in_application (const atermpp::aterm &e)
	Recogniser for application of in.
const core::identifier_string &	count_name ()
	Generate identifier #.
function_symbol	count (const sort_expression &s)
	Constructor for function symbol #.
bool	is_count_function_symbol (const atermpp::aterm &e)
	Recogniser for function #.
application	count (const sort_expression &s, const data_expression &arg0)
	Application of function symbol #.
void	make_count (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol #.
bool	is_count_application (const atermpp::aterm &e)
	Recogniser for application of #.
const core::identifier_string &	snoc_name ()
	Generate identifier <|.
function_symbol	snoc (const sort_expression &s)
	Constructor for function symbol <|.
bool	is_snoc_function_symbol (const atermpp::aterm &e)
	Recogniser for function <|.
application	snoc (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol <|.
void	make_snoc (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol <|.
bool	is_snoc_application (const atermpp::aterm &e)
	Recogniser for application of <|.
const core::identifier_string &	concat_name ()
	Generate identifier ++.
function_symbol	concat (const sort_expression &s)
	Constructor for function symbol ++.
bool	is_concat_function_symbol (const atermpp::aterm &e)
	Recogniser for function ++.
application	concat (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol ++.
void	make_concat (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol ++.
bool	is_concat_application (const atermpp::aterm &e)
	Recogniser for application of ++.
const core::identifier_string &	element_at_name ()
	Generate identifier ..
function_symbol	element_at (const sort_expression &s)
	Constructor for function symbol ..
bool	is_element_at_function_symbol (const atermpp::aterm &e)
	Recogniser for function ..
application	element_at (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol ..
void	make_element_at (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol ..
bool	is_element_at_application (const atermpp::aterm &e)
	Recogniser for application of ..
const core::identifier_string &	head_name ()
	Generate identifier head.
function_symbol	head (const sort_expression &s)
	Constructor for function symbol head.
bool	is_head_function_symbol (const atermpp::aterm &e)
	Recogniser for function head.
application	head (const sort_expression &s, const data_expression &arg0)
	Application of function symbol head.
void	make_head (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol head.
bool	is_head_application (const atermpp::aterm &e)
	Recogniser for application of head.
const core::identifier_string &	tail_name ()
	Generate identifier tail.
function_symbol	tail (const sort_expression &s)
	Constructor for function symbol tail.
bool	is_tail_function_symbol (const atermpp::aterm &e)
	Recogniser for function tail.
application	tail (const sort_expression &s, const data_expression &arg0)
	Application of function symbol tail.
void	make_tail (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol tail.
bool	is_tail_application (const atermpp::aterm &e)
	Recogniser for application of tail.
const core::identifier_string &	rhead_name ()
	Generate identifier rhead.
function_symbol	rhead (const sort_expression &s)
	Constructor for function symbol rhead.
bool	is_rhead_function_symbol (const atermpp::aterm &e)
	Recogniser for function rhead.
application	rhead (const sort_expression &s, const data_expression &arg0)
	Application of function symbol rhead.
void	make_rhead (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol rhead.
bool	is_rhead_application (const atermpp::aterm &e)
	Recogniser for application of rhead.
const core::identifier_string &	rtail_name ()
	Generate identifier rtail.
function_symbol	rtail (const sort_expression &s)
	Constructor for function symbol rtail.
bool	is_rtail_function_symbol (const atermpp::aterm &e)
	Recogniser for function rtail.
application	rtail (const sort_expression &s, const data_expression &arg0)
	Application of function symbol rtail.
void	make_rtail (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol rtail.
bool	is_rtail_application (const atermpp::aterm &e)
	Recogniser for application of rtail.
function_symbol_vector	list_generate_functions_code (const sort_expression &s)
	Give all system defined mappings for list.
function_symbol_vector	list_generate_constructors_and_functions_code (const sort_expression &s)
	Give all system defined mappings and constructors for list.
function_symbol_vector	list_mCRL2_usable_mappings (const sort_expression &s)
	Give all system defined mappings that can be used in mCRL2 specs for list.
implementation_map	list_cpp_implementable_mappings (const sort_expression &)
	Give all system defined mappings that are to be implemented in C++ code for list.
const data_expression &	left (const data_expression &e)
	Function for projecting out argument. left from an application.
const data_expression &	right (const data_expression &e)
	Function for projecting out argument. right from an application.
const data_expression &	arg (const data_expression &e)
	Function for projecting out argument. arg from an application.
data_equation_vector	list_generate_equations_code (const sort_expression &s)
	Give all system defined equations for list.
template<typename Sequence >
application	list (const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=nullptr)
	Constructs a list expression from a range of expressions.
core::identifier_string const &	list_enumeration_name ()
	Generate identifier list_enumeration.
function_symbol	list_enumeration (const sort_expression &s)
	Constructor for function symbol list_enumeration.
bool	is_list_enumeration_function_symbol (const atermpp::aterm &e)
	Recogniser for function list_enumeration.
template<typename Sequence >
data_expression	list_enumeration (const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=nullptr)
	Application of function symbol list_enumeration.
data_expression	list_enumeration (const sort_expression &s, data_expression_list const &range)
	Application of function symbol list_enumeration.
bool	is_list_enumeration_application (const atermpp::aterm &e)
	Recogniser for application of list_enumeration.

Detailed Description

Namespace for system defined sort list.

Typedef Documentation

implementation_map

typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > mcrl2::data::sort_list::implementation_map

Definition at line 180 of file list1.h.

Function Documentation

arg()

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

inline

Function for projecting out argument. arg from an application.

Parameters

e	A data expression.

Precondition

arg is defined for e.

Returns

The argument of e that corresponds to arg.

Definition at line 850 of file list1.h.

concat() [1/2]

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

inline

Constructor for function symbol ++.

Parameters

s	A sort expression.

Returns

Function symbol concat.

Definition at line 394 of file list1.h.

concat() [2/2]

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

inline

Application of function symbol ++.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of ++ to a number of arguments.

Definition at line 419 of file list1.h.

concat_name()

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

inline

Generate identifier ++.

Returns

Identifier ++.

Definition at line 384 of file list1.h.

cons_() [1/2]

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

inline

Constructor for function symbol |>.

Parameters

s	A sort expression.

Returns

Function symbol cons_.

Definition at line 105 of file list1.h.

cons_() [2/2]

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

inline

Application of function symbol |>.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of |> to a number of arguments.

Definition at line 130 of file list1.h.

cons_name()

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

inline

Generate identifier |>.

Returns

Identifier |>.

Definition at line 95 of file list1.h.

count() [1/2]

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

inline

Constructor for function symbol #.

Parameters

s	A sort expression.

Returns

Function symbol count.

Definition at line 268 of file list1.h.

count() [2/2]

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

inline

Application of function symbol #.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of # to a number of arguments.

Definition at line 292 of file list1.h.

count_name()

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

inline

Generate identifier #.

Returns

Identifier #.

Definition at line 258 of file list1.h.

element_at() [1/2]

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

inline

Constructor for function symbol ..

Parameters

s	A sort expression.

Returns

Function symbol element_at.

Definition at line 458 of file list1.h.

element_at() [2/2]

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

inline

Application of function symbol ..

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of . to a number of arguments.

Definition at line 483 of file list1.h.

element_at_name()

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

inline

Generate identifier ..

Returns

Identifier ..

Definition at line 448 of file list1.h.

empty()

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

inline

Constructor for function symbol [].

Parameters

s	A sort expression.

Returns

Function symbol empty.

Definition at line 73 of file list1.h.

empty_name()

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

inline

Generate identifier [].

Returns

Identifier [].

Definition at line 63 of file list1.h.

head() [1/2]

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

inline

Constructor for function symbol head.

Parameters

s	A sort expression.

Returns

Function symbol head.

Definition at line 522 of file list1.h.

head() [2/2]

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

inline

Application of function symbol head.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of head to a number of arguments.

Definition at line 546 of file list1.h.

head_name()

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

inline

Generate identifier head.

Returns

Identifier head.

Definition at line 512 of file list1.h.

in() [1/2]

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

inline

Constructor for function symbol in.

Parameters

s	A sort expression.

Returns

Function symbol in.

Definition at line 204 of file list1.h.

in() [2/2]

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

inline

Application of function symbol in.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of in to a number of arguments.

Definition at line 229 of file list1.h.

in_name()

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

inline

Generate identifier in.

Returns

Identifier in.

Definition at line 194 of file list1.h.

is_concat_application()

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

inline

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.

Definition at line 440 of file list1.h.

is_concat_function_symbol()

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

inline

Recogniser for function ++.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching ++.

Definition at line 404 of file list1.h.

is_cons_application()

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

inline

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.

Definition at line 151 of file list1.h.

is_cons_function_symbol()

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

inline

Recogniser for function |>.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching |>.

Definition at line 115 of file list1.h.

is_count_application()

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

inline

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.

Definition at line 312 of file list1.h.

is_count_function_symbol()

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

inline

Recogniser for function #.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching #.

Definition at line 278 of file list1.h.

is_element_at_application()

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

inline

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.

Definition at line 504 of file list1.h.

is_element_at_function_symbol()

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

inline

Recogniser for function ..

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching ..

Definition at line 468 of file list1.h.

is_empty_function_symbol()

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

inline

Recogniser for function [].

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching [].

Definition at line 83 of file list1.h.

is_head_application()

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

inline

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.

Definition at line 566 of file list1.h.

is_head_function_symbol()

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

inline

Recogniser for function head.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching head.

Definition at line 532 of file list1.h.

is_in_application()

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

inline

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.

Definition at line 250 of file list1.h.

is_in_function_symbol()

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

inline

Recogniser for function in.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching in.

Definition at line 214 of file list1.h.

is_list()

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

inline

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

Definition at line 50 of file list1.h.

is_list_enumeration_application()

bool mcrl2::data::sort_list::is_list_enumeration_application ( const atermpp::aterm &  e )

inline

Recogniser for application of list_enumeration.

Parameters

e	A data expression

Returns

true iff e is an application of function symbol list_enumeration to a number of arguments

Definition at line 131 of file standard_container_utility.h.

is_list_enumeration_function_symbol()

bool mcrl2::data::sort_list::is_list_enumeration_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function list_enumeration.

Parameters

e	A data expression

Returns

true iff e is the function symbol matching list_enumeration

Definition at line 73 of file standard_container_utility.h.

is_rhead_application()

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

inline

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.

Definition at line 690 of file list1.h.

is_rhead_function_symbol()

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

inline

Recogniser for function rhead.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching rhead.

Definition at line 656 of file list1.h.

is_rtail_application()

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

inline

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.

Definition at line 752 of file list1.h.

is_rtail_function_symbol()

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

inline

Recogniser for function rtail.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching rtail.

Definition at line 718 of file list1.h.

is_snoc_application()

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

inline

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.

Definition at line 376 of file list1.h.

is_snoc_function_symbol()

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

inline

Recogniser for function <|.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching <|.

Definition at line 340 of file list1.h.

is_tail_application()

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

inline

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.

Definition at line 628 of file list1.h.

is_tail_function_symbol()

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

inline

Recogniser for function tail.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching tail.

Definition at line 594 of file list1.h.

left()

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

inline

Function for projecting out argument. left from an application.

Parameters

e	A data expression.

Precondition

left is defined for e.

Returns

The argument of e that corresponds to left.

Definition at line 826 of file list1.h.

list() [1/2]

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

inline

Constructor for sort expression List(S)

Parameters

s	A sort expression

Returns

Sort expression list(s)

Definition at line 39 of file list1.h.

list() [2/2]

template<typename Sequence >

application mcrl2::data::sort_list::list ( const sort_expression &  s, Sequence const &  range, typename atermpp::enable_if_container< Sequence, data_expression >::type *  = nullptr  )

inline

Constructs a list expression from a range of expressions.

Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Parameters

[in]	s	the sort of list elements
[in]	range	an iterator range of elements of sort s

Definition at line 35 of file standard_container_utility.h.

list_cpp_implementable_constructors()

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

inline

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.

Definition at line 185 of file list1.h.

list_cpp_implementable_mappings()

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

inline

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

Definition at line 815 of file list1.h.

list_enumeration() [1/3]

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

inline

Constructor for function symbol list_enumeration.

Parameters

s	A sort expression

Returns

Function symbol list_enumeration

Definition at line 63 of file standard_container_utility.h.

list_enumeration() [2/3]

data_expression mcrl2::data::sort_list::list_enumeration ( const sort_expression &  s, data_expression_list const &  range  )

inline

Application of function symbol list_enumeration.

Parameters

s	A sort expression
range	A range of data expressions

Returns

Application of list_enum to the data expressions in range.

Definition at line 112 of file standard_container_utility.h.

list_enumeration() [3/3]

template<typename Sequence >

data_expression mcrl2::data::sort_list::list_enumeration ( const sort_expression &  s, Sequence const &  range, typename atermpp::enable_if_container< Sequence, data_expression >::type *  = nullptr  )

inline

Application of function symbol list_enumeration.

Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Parameters

s	A sort expression
range	A range of data expressions

Returns

Application of list_enum to the data expressions in range.

Definition at line 91 of file standard_container_utility.h.

list_enumeration_name()

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

inline

Generate identifier list_enumeration.

Returns

Identifier list_enumeration

Definition at line 53 of file standard_container_utility.h.

list_generate_constructors_and_functions_code()

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

inline

Give all system defined mappings and constructors for list.

Parameters

s	A sort expression

Returns

All system defined mappings for list

Definition at line 779 of file list1.h.

list_generate_constructors_code()

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

inline

Give all system defined constructors for list.

Parameters

s	A sort expression.

Returns

All system defined constructors for list.

Definition at line 159 of file list1.h.

list_generate_equations_code()

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

inline

Give all system defined equations for list.

Parameters

s	A sort expression

Returns

All system defined equations for sort list

Definition at line 860 of file list1.h.

list_generate_functions_code()

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

inline

Give all system defined mappings for list.

Parameters

s	A sort expression

Returns

All system defined mappings for list

Definition at line 760 of file list1.h.

list_mCRL2_usable_constructors()

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

inline

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.

Definition at line 171 of file list1.h.

list_mCRL2_usable_mappings()

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

inline

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

Definition at line 793 of file list1.h.

make_concat()

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

inline

Make an application of function symbol ++.

Parameters

[out]	result	The data expression where the ++ expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 430 of file list1.h.

make_cons()

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

inline

Make an application of function symbol |>.

Parameters

[out]	result	The data expression where the |> expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 141 of file list1.h.

make_count()

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

inline

Make an application of function symbol #.

Parameters

[out]	result	The data expression where the # expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 302 of file list1.h.

make_element_at()

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

inline

Make an application of function symbol ..

Parameters

[out]	result	The data expression where the . expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 494 of file list1.h.

make_head()

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

inline

Make an application of function symbol head.

Parameters

[out]	result	The data expression where the head expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 556 of file list1.h.

make_in()

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

inline

Make an application of function symbol in.

Parameters

[out]	result	The data expression where the in expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 240 of file list1.h.

make_rhead()

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

inline

Make an application of function symbol rhead.

Parameters

[out]	result	The data expression where the rhead expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 680 of file list1.h.

make_rtail()

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

inline

Make an application of function symbol rtail.

Parameters

[out]	result	The data expression where the rtail expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 742 of file list1.h.

make_snoc()

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

inline

Make an application of function symbol <|.

Parameters

[out]	result	The data expression where the <| expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 366 of file list1.h.

make_tail()

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

inline

Make an application of function symbol tail.

Parameters

[out]	result	The data expression where the tail expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 618 of file list1.h.

rhead() [1/2]

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

inline

Constructor for function symbol rhead.

Parameters

s	A sort expression.

Returns

Function symbol rhead.

Definition at line 646 of file list1.h.

rhead() [2/2]

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

inline

Application of function symbol rhead.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of rhead to a number of arguments.

Definition at line 670 of file list1.h.

rhead_name()

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

inline

Generate identifier rhead.

Returns

Identifier rhead.

Definition at line 636 of file list1.h.

right()

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

inline

Function for projecting out argument. right from an application.

Parameters

e	A data expression.

Precondition

right is defined for e.

Returns

The argument of e that corresponds to right.

Definition at line 838 of file list1.h.

rtail() [1/2]

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

inline

Constructor for function symbol rtail.

Parameters

s	A sort expression.

Returns

Function symbol rtail.

Definition at line 708 of file list1.h.

rtail() [2/2]

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

inline

Application of function symbol rtail.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of rtail to a number of arguments.

Definition at line 732 of file list1.h.

rtail_name()

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

inline

Generate identifier rtail.

Returns

Identifier rtail.

Definition at line 698 of file list1.h.

snoc() [1/2]

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

inline

Constructor for function symbol <|.

Parameters

s	A sort expression.

Returns

Function symbol snoc.

Definition at line 330 of file list1.h.

snoc() [2/2]

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

inline

Application of function symbol <|.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of <| to a number of arguments.

Definition at line 355 of file list1.h.

snoc_name()

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

inline

Generate identifier <|.

Returns

Identifier <|.

Definition at line 320 of file list1.h.

tail() [1/2]

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

inline

Constructor for function symbol tail.

Parameters

s	A sort expression.

Returns

Function symbol tail.

Definition at line 584 of file list1.h.

tail() [2/2]

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

inline

Application of function symbol tail.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of tail to a number of arguments.

Definition at line 608 of file list1.h.

tail_name()

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

inline

Generate identifier tail.

Returns

Identifier tail.

Definition at line 574 of file list1.h.