Namespace for system defined sort list. More...

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

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 &s)
	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 &s)
	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 183 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 855 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 398 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

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

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

Definition at line 423 of file list1.h.

◆ concat_name()

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

inline

Generate identifier ++.

Returns: Identifier ++.

Definition at line 388 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 108 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

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

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

Definition at line 133 of file list1.h.

◆ cons_name()

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

inline

Generate identifier |>.

Returns: Identifier |>.

Definition at line 98 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 272 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

s	A sort expression.
arg0	A data expression.

Returns: Application of # to a number of arguments.

Definition at line 296 of file list1.h.

◆ count_name()

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

inline

Generate identifier #.

Returns: Identifier #.

Definition at line 262 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 462 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

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

Returns: Application of . to a number of arguments.

Definition at line 487 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 452 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 76 of file list1.h.

◆ empty_name()

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

inline

Generate identifier [].

Returns: Identifier [].

Definition at line 66 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 526 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

s	A sort expression.
arg0	A data expression.

Returns: Application of head to a number of arguments.

Definition at line 550 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 516 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 208 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

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

Returns: Application of in to a number of arguments.

Definition at line 233 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 198 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 444 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 408 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 154 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 118 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 316 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 282 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 508 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 472 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 86 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 570 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 536 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 254 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 218 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 53 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 132 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 74 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 694 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 660 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 756 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 722 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 380 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 344 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 632 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 598 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 831 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 42 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 36 of file standard_container_utility.h.

◆ list_cpp_implementable_constructors()

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

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 188 of file list1.h.

◆ list_cpp_implementable_mappings()

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

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 819 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 64 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 113 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 92 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 54 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 783 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 162 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 865 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 764 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 174 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 797 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

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

Definition at line 434 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

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

Definition at line 144 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

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

Definition at line 306 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

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

Definition at line 498 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

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

Definition at line 560 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

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

Definition at line 244 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

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

Definition at line 684 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

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

Definition at line 746 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

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

Definition at line 370 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

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

Definition at line 622 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 650 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

s	A sort expression.
arg0	A data expression.

Returns: Application of rhead to a number of arguments.

Definition at line 674 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 640 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 843 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 712 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

s	A sort expression.
arg0	A data expression.

Returns: Application of rtail to a number of arguments.

Definition at line 736 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 702 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 334 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

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

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

Definition at line 359 of file list1.h.

◆ snoc_name()

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

inline

Generate identifier <|.

Returns: Identifier <|.

Definition at line 324 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 588 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

s	A sort expression.
arg0	A data expression.

Returns: Application of tail to a number of arguments.

Definition at line 612 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 578 of file list1.h.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ implementation_map

Function Documentation

◆ arg()

◆ concat() [1/2]

◆ concat() [2/2]

◆ concat_name()

◆ cons_() [1/2]

◆ cons_() [2/2]

◆ cons_name()

◆ count() [1/2]

◆ count() [2/2]

◆ count_name()

◆ element_at() [1/2]

◆ element_at() [2/2]

◆ element_at_name()

◆ empty()

◆ empty_name()

◆ head() [1/2]

◆ head() [2/2]

◆ head_name()

◆ in() [1/2]

◆ in() [2/2]

◆ in_name()

◆ is_concat_application()

◆ is_concat_function_symbol()

◆ is_cons_application()

◆ is_cons_function_symbol()

◆ is_count_application()

◆ is_count_function_symbol()

◆ is_element_at_application()

◆ is_element_at_function_symbol()

◆ is_empty_function_symbol()

◆ is_head_application()

◆ is_head_function_symbol()

◆ is_in_application()

◆ is_in_function_symbol()

◆ is_list()

◆ is_list_enumeration_application()

◆ is_list_enumeration_function_symbol()

◆ is_rhead_application()

◆ is_rhead_function_symbol()

◆ is_rtail_application()

◆ is_rtail_function_symbol()

◆ is_snoc_application()

◆ is_snoc_function_symbol()

◆ is_tail_application()

◆ is_tail_function_symbol()

◆ left()

◆ list() [1/2]

◆ list() [2/2]

◆ list_cpp_implementable_constructors()

◆ list_cpp_implementable_mappings()

◆ list_enumeration() [1/3]

◆ list_enumeration() [2/3]

◆ list_enumeration() [3/3]

◆ list_enumeration_name()

◆ list_generate_constructors_and_functions_code()

◆ list_generate_constructors_code()

◆ list_generate_equations_code()

◆ list_generate_functions_code()

◆ list_mCRL2_usable_constructors()

◆ list_mCRL2_usable_mappings()

◆ make_concat()

◆ make_cons_()

◆ make_count()

◆ make_element_at()

◆ make_head()

◆ make_in()

◆ make_rhead()

◆ make_rtail()

◆ make_snoc()

◆ make_tail()

◆ rhead() [1/2]

◆ rhead() [2/2]

◆ rhead_name()

◆ right()