15#ifndef MCRL2_DATA_LIST1_H
16#define MCRL2_DATA_LIST1_H
90 return atermpp::down_cast<function_symbol>(e).name() ==
empty_name();
122 return atermpp::down_cast<function_symbol>(e).name() ==
cons_name();
191 static_cast< void >(s);
222 return atermpp::down_cast<function_symbol>(e).name() ==
in_name();
286 return atermpp::down_cast<function_symbol>(e).name() ==
count_name();
348 return atermpp::down_cast<function_symbol>(e).name() ==
snoc_name();
412 return atermpp::down_cast<function_symbol>(e).name() ==
concat_name();
476 return atermpp::down_cast<function_symbol>(e).name() ==
element_at_name();
540 return atermpp::down_cast<function_symbol>(e).name() ==
head_name();
602 return atermpp::down_cast<function_symbol>(e).name() ==
tail_name();
664 return atermpp::down_cast<function_symbol>(e).name() ==
rhead_name();
726 return atermpp::down_cast<function_symbol>(e).name() ==
rtail_name();
822 static_cast< void >(s);
834 return atermpp::down_cast<application>(e)[0];
846 return atermpp::down_cast<application>(e)[1];
858 return atermpp::down_cast<application>(e)[0];
876 result.push_back(
data_equation(
variable_list({vd, ve, vs, vt}),
equal_to(
cons_(s, vd, vs),
cons_(s, ve, vt)),
sort_bool::and_(
equal_to(vd, ve),
equal_to(vs, vt))));
879 result.push_back(
data_equation(
variable_list({vd, ve, vs, vt}),
less(
cons_(s, vd, vs),
cons_(s, ve, vt)),
sort_bool::or_(
sort_bool::and_(
equal_to(vd, ve),
less(vs, vt)),
less(vd, ve))));
882 result.push_back(
data_equation(
variable_list({vd, ve, vs, vt}),
less_equal(
cons_(s, vd, vs),
cons_(s, ve, vt)),
sort_bool::or_(
sort_bool::and_(
equal_to(vd, ve),
less_equal(vs, vt)),
less(vd, ve))));
884 result.push_back(
data_equation(
variable_list({vd, ve, vs}),
in(s, vd,
cons_(s, ve, vs)),
sort_bool::or_(
equal_to(vd, ve),
in(s, vd, vs))));
888 result.push_back(
data_equation(
variable_list({vd, ve, vs}),
snoc(s,
cons_(s, vd, vs), ve),
cons_(s, vd,
snoc(s, vs, ve))));
890 result.push_back(
data_equation(
variable_list({vd, vs, vt}),
concat(s,
cons_(s, vd, vs), vt),
cons_(s, vd,
concat(s, vs, vt))));
893 result.push_back(
data_equation(
variable_list({vd, vp, vs}),
element_at(s,
cons_(s, vd, vs),
sort_nat::cnat(vp)),
element_at(s, vs,
sort_nat::pred(vp))));
897 result.push_back(
data_equation(
variable_list({vd, ve, vs}),
rhead(s,
cons_(s, vd,
cons_(s, ve, vs))),
rhead(s,
cons_(s, ve, vs))));
899 result.push_back(
data_equation(
variable_list({vd, ve, vs}),
rtail(s,
cons_(s, vd,
cons_(s, ve, vs))),
cons_(s, vd,
rtail(s,
cons_(s, ve, vs)))));
Term containing a string.
An application of a data expression to a number of arguments.
const container_type & container_name() const
\brief Container type for lists
The class container_sort.
The class function symbol.
Exception classes for use in libraries and tools.
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
const basic_sort & bool_()
Constructor for sort expression Bool.
const function_symbol & and_()
Constructor for function symbol &&.
const function_symbol & false_()
Constructor for function symbol false.
const function_symbol & or_()
Constructor for function symbol ||.
const function_symbol & true_()
Constructor for function symbol true.
const core::identifier_string & rtail_name()
Generate identifier rtail.
const core::identifier_string & snoc_name()
Generate identifier <|.
bool is_rhead_function_symbol(const atermpp::aterm &e)
Recogniser for function rhead.
bool is_rhead_application(const atermpp::aterm &e)
Recogniser for application of rhead.
bool is_snoc_function_symbol(const atermpp::aterm &e)
Recogniser for function <|.
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
function_symbol_vector list_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for list.
const core::identifier_string & tail_name()
Generate identifier tail.
bool is_tail_application(const atermpp::aterm &e)
Recogniser for application of tail.
bool is_element_at_function_symbol(const atermpp::aterm &e)
Recogniser for function ..
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_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
const core::identifier_string & rhead_name()
Generate identifier rhead.
function_symbol_vector list_generate_functions_code(const sort_expression &s)
Give all system defined mappings 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 core::identifier_string & in_name()
Generate identifier in.
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
bool is_rtail_function_symbol(const atermpp::aterm &e)
Recogniser for function rtail.
bool is_concat_application(const atermpp::aterm &e)
Recogniser for application of ++.
const core::identifier_string & head_name()
Generate identifier head.
const core::identifier_string & cons_name()
Generate identifier |>.
const core::identifier_string & concat_name()
Generate identifier ++.
function_symbol rtail(const sort_expression &s)
Constructor for function symbol rtail.
const core::identifier_string & count_name()
Generate identifier #.
void make_cons_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol |>.
data_equation_vector list_generate_equations_code(const sort_expression &s)
Give all system defined equations for list.
void make_rhead(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol rhead.
bool is_tail_function_symbol(const atermpp::aterm &e)
Recogniser for function tail.
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.
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
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...
function_symbol_vector list_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for list.
bool is_rtail_application(const atermpp::aterm &e)
Recogniser for application of rtail.
function_symbol empty(const sort_expression &s)
Constructor for function symbol [].
function_symbol element_at(const sort_expression &s)
Constructor for function symbol ..
const core::identifier_string & empty_name()
Generate identifier [].
function_symbol_vector list_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for list.
void make_concat(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol ++.
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.
const core::identifier_string & element_at_name()
Generate identifier ..
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of |>.
bool is_snoc_application(const atermpp::aterm &e)
Recogniser for application of <|.
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
function_symbol snoc(const sort_expression &s)
Constructor for function symbol <|.
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
bool is_element_at_application(const atermpp::aterm &e)
Recogniser for application of ..
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
void make_head(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol head.
function_symbol rhead(const sort_expression &s)
Constructor for function symbol rhead.
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_count_application(const atermpp::aterm &e)
Recogniser for application of #.
void make_rtail(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol rtail.
bool is_head_application(const atermpp::aterm &e)
Recogniser for application of head.
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
function_symbol tail(const sort_expression &s)
Constructor for function symbol tail.
void make_tail(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol tail.
function_symbol cons_(const sort_expression &s)
Constructor for function symbol |>.
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function |>.
bool is_concat_function_symbol(const atermpp::aterm &e)
Recogniser for function ++.
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
bool is_head_function_symbol(const atermpp::aterm &e)
Recogniser for function head.
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function [].
function_symbol concat(const sort_expression &s)
Constructor for function symbol ++.
bool is_list(const sort_expression &e)
Recogniser for sort expression List(s)
function_symbol succ(const sort_expression &s0)
const function_symbol & c0()
Constructor for function symbol @c0.
const function_symbol & cnat()
Constructor for function symbol @cNat.
const basic_sort & nat()
Constructor for sort expression Nat.
const function_symbol & pred()
Constructor for function symbol pred.
const basic_sort & pos()
Constructor for sort expression Pos.
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
atermpp::term_list< variable > variable_list
\brief list of variables
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
void make_application(atermpp::aterm &result)
Make function for an application.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Standard functions that are available for all sorts.