12#ifndef MCRL2_CORE_BUILDER_H
13#define MCRL2_CORE_BUILDER_H
15#include "mcrl2/atermpp/aterm_list.h"
16#include "mcrl2/atermpp/concepts.h"
24
25
26
27
28
29
30template <
typename Derived>
88template <
template <
class>
class Builder>
101template <
template <
class>
class Builder>
105 return apply_builder<Builder>();
109template <
template <
class>
class Builder,
class Arg1>
125template <
template <
class>
class Builder,
class Arg1>
129 return apply_builder_arg1<Builder, Arg1>(arg1);
133template <
template <
class>
class Builder,
class Arg1,
class Arg2>
149template <
template <
class>
class Builder,
class Arg1,
class Arg2>
153 return apply_builder_arg2<Builder, Arg1, Arg2>(arg1, arg2);
158template <
template <
class>
class Builder,
class Function>
168 using argument_type =
typename Function::argument_type;
169 using result_type =
typename Function::result_type;
173 void apply(T& result,
const argument_type& x)
176 result =
static_cast<T>(
f_(x
));
184template <
template <
class>
class Builder,
class Function>
188 return update_apply_builder<Builder, Function>(f);
192template <
template <
class>
class Builder,
class Function,
class Arg1>
202 using argument_type =
typename Function::argument_type;
203 using result_type =
typename Function::result_type;
207 void apply(T& result,
const argument_type& x)
218template <
template <
class>
class Builder,
class Function,
class Arg1>
222 return update_apply_builder_arg1<Builder, Function, Arg1>(f);
A unordered_map class in which aterms can be stored.
apply_builder_arg1(const Arg1 &arg1)
apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
update_apply_builder_arg1(const Function &f, const Arg1 &arg1)
void apply(T &result, const argument_type &x)
An abstraction expression.
const variable_list & variables() const
const data_expression & body() const
const basic_sort & name() const
const sort_expression & reference() const
\brief Assignment expression
\brief Assignment of a data expression to a variable
const data_expression & rhs() const
const variable & lhs() const
universal quantification.
container_sort(const container_type &container_name, const sort_expression &element_sort)
\brief Constructor Z14.
const container_type & container_name() const
const sort_expression & element_sort() const
container_sort(const atermpp::aterm &term)
const data_expression & lhs() const
const data_expression & condition() const
const data_expression & rhs() const
const variable_list & variables() const
sort_expression sort() const
Returns the sort of the data expression.
existential quantification.
universal quantification.
const sort_expression & codomain() const
const sort_expression_list & domain() const
const core::identifier_string & name() const
const sort_expression & sort() const
universal quantification.
sort_expression & operator=(sort_expression &&) noexcept=default
\brief An argument of a constructor of a structured sort
const core::identifier_string & name() const
const sort_expression & sort() const
\brief A constructor for a structured sort
const core::identifier_string & name() const
const core::identifier_string & recogniser() const
const structured_sort_constructor_argument_list & arguments() const
const structured_sort_constructor_list & constructors() const
\brief An untyped parameter
const core::identifier_string & name() const
const data_expression_list & arguments() const
\brief Assignment of a data expression to a string
const core::identifier_string & lhs() const
const data_expression & rhs() const
\brief An untyped identifier
\brief Multiple possible sorts
const sort_expression_list & sorts() const
universal quantification.
\brief Untyped sort variable
\brief Unknown sort expression
untyped_sort()
\brief Default constructor X3.
const core::identifier_string & name() const
const sort_expression & sort() const
\brief A where expression
const data_expression & body() const
const assignment_expression_list & declarations() const
D_ParserTables parser_tables_mcrl2
apply_builder< Builder > make_apply_builder()
update_apply_builder_arg1< Builder, Function, Arg1 > make_update_apply_builder_arg1(const Function &f)
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
apply_builder_arg1< Builder, Arg1 > make_apply_builder_arg1(const Arg1 &arg1)
update_apply_builder< Builder, Function > make_update_apply_builder(const Function &f)
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
data_expression parse_data_expression(const std::string &text)
data_specification parse_data_specification_new(const std::string &text)
variable_list parse_variable_declaration_list(const std::string &text)
variable_list parse_variables(const std::string &text)
sort_expression parse_sort_expression(const std::string &text)
Namespace for system defined sort bool_.
const basic_sort & bool_()
Constructor for sort expression Bool.
std::string pp(const data::structured_sort_constructor_argument &x, bool arg0)
data::data_equation normalize_sorts(const data::data_equation &x, const data::sort_specification &sortspec)
void normalize_sorts(data::data_equation_vector &x, const data::sort_specification &sortspec)
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
data::data_equation_list normalize_sorts(const data::data_equation_list &x, const data::sort_specification &sortspec)
std::string pp(const data::exists &x, bool arg0)
std::string pp(const data::untyped_identifier_assignment &x, bool arg0)
std::set< data::variable > find_all_variables(const data::data_expression_list &x)
std::string pp(const data::list_container &x, bool arg0)
std::set< data::sort_expression > find_sort_expressions(const data::data_expression &x)
data::data_equation translate_user_notation(const data::data_equation &x)
bool is_application(const data_expression &t)
Returns true if the term t is an application.
std::string pp(const data::container_type &x, bool arg0)
std::set< data::variable > find_all_variables(const data::data_expression &x)
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
std::string pp(const data::set_container &x, bool arg0)
bool is_untyped_possible_sorts(const atermpp::aterm &x)
Returns true if the term t is an expression for multiple possible sorts.
bool is_untyped_sort(const atermpp::aterm &x)
Returns true if the term t is the unknown sort.
std::string pp(const data::untyped_set_or_bag_comprehension_binder &x, bool arg0)
data::data_expression translate_user_notation(const data::data_expression &x)
std::string pp(const data::sort_expression_vector &x, bool arg0)
std::string pp(const data::untyped_sort &x, bool arg0)
std::string pp(const data::data_equation &x, bool arg0)
std::string pp(const data::forall &x, bool arg0)
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
std::string pp(const data::assignment_list &x, bool arg0)
std::string pp(const data::untyped_identifier &x, bool arg0)
std::string pp(const data::function_symbol_list &x, bool arg0)
bool is_untyped_identifier(const atermpp::aterm &x)
Returns true if the term t is an identifier.
std::string pp(const data::lambda_binder &x, bool arg0)
std::set< data::variable > find_all_variables(const data::function_symbol &x)
std::string pp(const data::application &x, bool arg0)
std::string pp(const data::function_sort &x, bool arg0)
std::string pp(const data::abstraction &x, bool arg0)
std::string pp(const data::bag_comprehension_binder &x, bool arg0)
std::string pp(const data::set_comprehension_binder &x, bool arg0)
std::string pp(const data::assignment &x, bool arg0)
std::string pp(const data::structured_sort &x, bool arg0)
std::string pp(const data::basic_sort &x, bool arg0)
std::string pp(const data::exists_binder &x, bool arg0)
std::string pp(const data::bag_comprehension &x, bool arg0)
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
std::string pp(const data::variable &x, bool arg0)
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
bool is_untyped_sort_variable(const atermpp::aterm &x)
std::string pp(const data::where_clause &x, bool arg0)
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
std::string pp(const data::bag_container &x, bool arg0)
std::string pp(const data::alias &x, bool arg0)
std::set< data::variable > find_free_variables(const data::data_expression &x)
std::set< data::variable > find_all_variables(const data::variable_list &x)
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
bool is_assignment(const atermpp::aterm &x)
std::string pp(const data::structured_sort_constructor &x, bool arg0)
std::set< data::sort_expression > find_sort_expressions(const data::sort_expression &x)
std::string pp(const data::data_specification &x, bool arg0)
std::string pp(const data::data_equation_list &x, bool arg0)
std::string pp(const data::fset_container &x, bool arg0)
std::string pp(const data::sort_expression &x, bool arg0)
std::string pp(const data::untyped_set_or_bag_comprehension &x, bool arg0)
std::pair< basic_sort_vector, alias_vector > parse_sort_specification(const std::string &text)
data::sort_expression normalize_sorts(const data::sort_expression &x, const data::sort_specification &sortspec)
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
std::string pp(const data::variable_list &x, bool arg0)
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
std::set< data::variable > find_free_variables(const data::data_expression_list &x)
std::string pp(const data::data_expression &x, bool arg0)
std::string pp(const data::lambda &x, bool arg0)
bool is_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a bag comprehension.
std::string pp(const data::fbag_container &x, bool arg0)
bool is_set_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set comprehension.
std::string pp(const data::structured_sort_constructor_list &x, bool arg0)
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
std::string pp(const data::container_sort &x, bool arg0)
data::variable_list normalize_sorts(const data::variable_list &x, const data::sort_specification &sortspec)
data::data_expression normalize_sorts(const data::data_expression &x, const data::sort_specification &sortspec)
std::string pp(const data::untyped_sort_variable &x, bool arg0)
std::string pp(const data::untyped_data_parameter &x, bool arg0)
std::string pp(const data::binder_type &x, bool arg0)
bool is_lambda(const atermpp::aterm &x)
Returns true if the term t is a lambda abstraction.
bool is_untyped_identifier_assignment(const atermpp::aterm &x)
std::set< data::variable > find_all_variables(const data::variable &x)
std::set< core::identifier_string > find_identifiers(const data::variable_list &x)
bool search_variable(const data::data_expression &x, const data::variable &v)
std::string pp(const data::sort_expression_list &x, bool arg0)
std::string pp(const data::forall_binder &x, bool arg0)
std::string pp(const data::untyped_possible_sorts &x, bool arg0)
std::string pp(const data::function_symbol &x, bool arg0)
std::set< data::variable > substitution_variables(const mutable_map_substitution<> &sigma)
std::string pp(const data::machine_number &x, bool arg0)
std::string pp(const data::assignment_expression &x, bool arg0)
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
std::string pp(const data::set_comprehension &x, bool arg0)
std::string pp(const data::data_expression_list &x, bool arg0)
expression builder that visits all sub expressions
void apply(T &result, const argument_type &x)
update_apply_builder(const Function &f)
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::data_equation &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::structured_sort_constructor_argument &x)
void apply(T &result, const data::container_sort &x)
void apply(T &result, const data::alias &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::untyped_possible_sorts &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::basic_sort &x)
void apply(T &result, const data::data_equation &x)
void apply(T &result, const data::untyped_sort &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::structured_sort &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::function_sort &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::structured_sort_constructor &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::sort_expression &x)
void apply(T &result, const data::untyped_sort_variable &x)
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::data_equation &x)
data_expression_actions(const core::parser &parser_)
data::data_expression parse_DataExpr(const core::parse_node &node) const
data_specification_actions(const core::parser &parser_)
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
normalize_sorts_function(const sort_specification &sort_spec)
sort_expression operator()(const sort_expression &e) const
Normalise sorts.
const std::map< sort_expression, sort_expression > & m_normalised_aliases
data::sort_expression parse_SortExpr(const core::parse_node &node, data::sort_expression_list *product=nullptr) const
data_specification construct_data_specification() const