mCRL2
Loading...
Searching...
No Matches
alias.h
Go to the documentation of this file.
1// Author(s): Jeroen Keiren
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/data/alias.h
10/// \brief The class alias.
11
12#ifndef MCRL2_DATA_ALIAS_H
13#define MCRL2_DATA_ALIAS_H
14
15#include "mcrl2/data/basic_sort.h"
16
17namespace mcrl2::data
18{
19
20//--- start generated class alias ---//
21/// \\brief A sort alias
22class alias: public atermpp::aterm
23{
24 public:
25 /// \\brief Default constructor X3.
28 {}
29
30 /// \\brief Constructor Z9.
31 /// \\param term A term
32 explicit alias(const atermpp::aterm& term)
33 : atermpp::aterm(term)
34 {
35 assert(core::detail::check_term_SortRef(*this));
36 }
37
38 /// \\brief Constructor Z12.
39 alias(const basic_sort& name, const sort_expression& reference)
41 {}
42
43 /// Move semantics
44 alias(const alias&) noexcept = default;
45 alias(alias&&) noexcept = default;
46 alias& operator=(const alias&) noexcept = default;
47 alias& operator=(alias&&) noexcept = default;
48
49 const basic_sort& name() const
50 {
51 return atermpp::down_cast<basic_sort>((*this)[0]);
52 }
53
55 {
56 return atermpp::down_cast<sort_expression>((*this)[1]);
57 }
58};
59
60/// \\brief The function make_alias constructs a new term into a given address.
61/// \\ \param t The reference into which the new alias is constructed.
62template <class... ARGUMENTS>
63inline void make_alias(atermpp::aterm& t, const ARGUMENTS&... args)
64{
65 atermpp::make_term_appl(t, core::detail::function_symbol_SortRef(), args...);
66}
67
68/// \\brief list of aliass
69using alias_list = atermpp::term_list<alias>;
70
71/// \\brief vector of aliass
73
74/// \\brief Test for a alias expression
75/// \\param x A term
76/// \\return True if \\a x is a alias expression
77inline
78bool is_alias(const atermpp::aterm& x)
79{
80 return x.function() == core::detail::function_symbols::SortRef;
81}
82
83// prototype declaration
84std::string pp(const alias& x, bool precedence_aware = true);
85
86/// \\brief Outputs the object to a stream
87/// \\param out An output stream
88/// \\param x Object x
89/// \\return The output stream
90inline
92{
93 return out << data::pp(x);
94}
95
96/// \\brief swap overload
97inline void swap(alias& t1, alias& t2) noexcept
98{
99 t1.swap(t2);
100}
101//--- end generated class alias ---//
102
103} // namespace mcrl2::data
104
105#endif // MCRL2_DATA_ALIAS_H
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
A list of aterm objects.
Definition aterm_list.h:26
A unordered_map class in which aterms can be stored.
apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:120
apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:144
update_apply_builder_arg1(const Function &f, const Arg1 &arg1)
Definition builder.h:212
void apply(T &result, const argument_type &x)
Definition builder.h:207
An abstraction expression.
Definition abstraction.h:23
const variable_list & variables() const
Definition abstraction.h:60
const data_expression & body() const
Definition abstraction.h:65
\brief A sort alias
Definition alias.h:23
alias()
\brief Default constructor X3.
Definition alias.h:26
alias(const alias &) noexcept=default
Move semantics.
alias & operator=(const alias &) noexcept=default
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
Definition alias.h:39
alias(alias &&) noexcept=default
alias(const atermpp::aterm &term)
Definition alias.h:32
alias & operator=(alias &&) noexcept=default
const basic_sort & name() const
Definition alias.h:49
const sort_expression & reference() const
Definition alias.h:54
\brief Assignment expression
Definition assignment.h:24
\brief Assignment of a data expression to a variable
Definition assignment.h:88
const data_expression & rhs() const
Definition assignment.h:119
const variable & lhs() const
Definition assignment.h:114
universal quantification.
\brief A basic sort
Definition basic_sort.h:25
\brief A container sort
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)
\brief A data equation
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.
Definition data.cpp:107
existential quantification.
Definition exists.h:23
universal quantification.
Definition forall.h:25
\brief A function sort
const sort_expression & codomain() const
const sort_expression_list & domain() const
\brief A function symbol
const core::identifier_string & name() const
const sort_expression & sort() const
function symbol.
Definition lambda.h:24
\brief A machine number
universal quantification.
\brief A sort expression
sort_expression & operator=(sort_expression &&) noexcept=default
\brief An argument of a constructor of a structured sort
\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
const core::identifier_string & name() const
const data_expression_list & arguments() const
\brief Assignment of a data expression to a string
Definition assignment.h:179
const core::identifier_string & lhs() const
Definition assignment.h:210
const data_expression & rhs() const
Definition assignment.h:215
\brief An untyped identifier
const sort_expression_list & sorts() const
\brief Unknown sort expression
untyped_sort()
\brief Default constructor X3.
\brief A data variable
Definition variable.h:25
const core::identifier_string & name() const
Definition variable.h:35
const sort_expression & sort() const
Definition variable.h:40
\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()
Definition builder.h:103
update_apply_builder_arg1< Builder, Function, Arg1 > make_update_apply_builder_arg1(const Function &f)
Definition builder.h:220
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)
Definition builder.h:127
update_apply_builder< Builder, Function > make_update_apply_builder(const Function &f)
Definition builder.h:186
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:151
data_expression parse_data_expression(const std::string &text)
Definition data.cpp:217
data_specification parse_data_specification_new(const std::string &text)
Definition data.cpp:228
variable_list parse_variable_declaration_list(const std::string &text)
Definition data.cpp:239
variable_list parse_variables(const std::string &text)
Definition data.cpp:206
sort_expression parse_sort_expression(const std::string &text)
Definition data.cpp:196
Namespace for system defined sort bool_.
Definition bool.h:29
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:41
std::string pp(const data::structured_sort_constructor_argument &x, bool arg0)
Definition data.cpp:71
data::data_equation normalize_sorts(const data::data_equation &x, const data::sort_specification &sortspec)
Definition data.cpp:82
void normalize_sorts(data::data_equation_vector &x, const data::sort_specification &sortspec)
Definition data.cpp:84
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)
Definition data.cpp:83
std::string pp(const data::exists &x, bool arg0)
Definition data.cpp:53
std::string pp(const data::untyped_identifier_assignment &x, bool arg0)
Definition data.cpp:74
std::set< data::variable > find_all_variables(const data::data_expression_list &x)
Definition data.cpp:94
std::string pp(const data::list_container &x, bool arg0)
Definition data.cpp:63
std::set< data::sort_expression > find_sort_expressions(const data::data_expression &x)
Definition data.cpp:91
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:89
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)
Definition data.cpp:49
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:93
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)
Definition data.cpp:67
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)
Definition data.cpp:77
data::data_expression translate_user_notation(const data::data_expression &x)
Definition data.cpp:88
std::string pp(const data::sort_expression_vector &x, bool arg0)
Definition data.cpp:25
std::string pp(const data::untyped_sort &x, bool arg0)
Definition data.cpp:78
std::string pp(const data::data_equation &x, bool arg0)
Definition data.cpp:50
std::string pp(const data::forall &x, bool arg0)
Definition data.cpp:56
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)
Definition data.cpp:28
std::string pp(const data::untyped_identifier &x, bool arg0)
Definition data.cpp:73
std::string pp(const data::function_symbol_list &x, bool arg0)
Definition data.cpp:32
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)
Definition data.cpp:62
std::ostream & operator<<(std::ostream &out, const alias &x)
Definition alias.h:91
std::set< data::variable > find_all_variables(const data::function_symbol &x)
Definition data.cpp:95
std::string pp(const data::application &x, bool arg0)
Definition data.cpp:40
std::string pp(const data::function_sort &x, bool arg0)
Definition data.cpp:59
void make_alias(atermpp::aterm &t, const ARGUMENTS &... args)
Definition alias.h:63
std::string pp(const data::abstraction &x, bool arg0)
Definition data.cpp:38
std::string pp(const data::bag_comprehension_binder &x, bool arg0)
Definition data.cpp:44
std::string pp(const data::set_comprehension_binder &x, bool arg0)
Definition data.cpp:66
std::string pp(const data::assignment &x, bool arg0)
Definition data.cpp:41
std::string pp(const data::structured_sort &x, bool arg0)
Definition data.cpp:69
std::string pp(const data::basic_sort &x, bool arg0)
Definition data.cpp:46
std::string pp(const data::exists_binder &x, bool arg0)
Definition data.cpp:54
std::string pp(const data::bag_comprehension &x, bool arg0)
Definition data.cpp:43
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)
Definition data.cpp:80
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)
Definition data.cpp:81
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:90
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
Definition data.cpp:100
std::string pp(const data::bag_container &x, bool arg0)
Definition data.cpp:45
std::string pp(const data::alias &x, bool arg0)
Definition data.cpp:39
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:98
std::set< data::variable > find_all_variables(const data::variable_list &x)
Definition data.cpp:97
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
void swap(alias &t1, alias &t2) noexcept
\brief swap overload
Definition alias.h:97
bool is_assignment(const atermpp::aterm &x)
Definition assignment.h:152
std::string pp(const data::structured_sort_constructor &x, bool arg0)
Definition data.cpp:70
std::set< data::sort_expression > find_sort_expressions(const data::sort_expression &x)
Definition data.cpp:92
std::string pp(const data::data_specification &x, bool arg0)
Definition data.cpp:52
std::string pp(const data::data_equation_list &x, bool arg0)
Definition data.cpp:36
std::string pp(const data::fset_container &x, bool arg0)
Definition data.cpp:58
std::string pp(const data::sort_expression &x, bool arg0)
Definition data.cpp:68
std::string pp(const data::untyped_set_or_bag_comprehension &x, bool arg0)
Definition data.cpp:76
std::pair< basic_sort_vector, alias_vector > parse_sort_specification(const std::string &text)
Definition data.cpp:251
data::sort_expression normalize_sorts(const data::sort_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
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)
Definition data.cpp:30
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)
Definition data.cpp:99
std::string pp(const data::data_expression &x, bool arg0)
Definition data.cpp:51
std::string pp(const data::lambda &x, bool arg0)
Definition data.cpp:61
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)
Definition data.cpp:55
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)
Definition data.cpp:34
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)
Definition data.cpp:48
data::variable_list normalize_sorts(const data::variable_list &x, const data::sort_specification &sortspec)
Definition data.cpp:87
data::data_expression normalize_sorts(const data::data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:85
std::string pp(const data::untyped_sort_variable &x, bool arg0)
Definition data.cpp:79
std::string pp(const data::untyped_data_parameter &x, bool arg0)
Definition data.cpp:72
std::string pp(const data::binder_type &x, bool arg0)
Definition data.cpp:47
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)
Definition assignment.h:248
bool is_alias(const atermpp::aterm &x)
Definition alias.h:78
std::set< data::variable > find_all_variables(const data::variable &x)
Definition data.cpp:96
std::set< core::identifier_string > find_identifiers(const data::variable_list &x)
Definition data.cpp:101
bool search_variable(const data::data_expression &x, const data::variable &v)
Definition data.cpp:102
std::string pp(const data::sort_expression_list &x, bool arg0)
Definition data.cpp:24
std::string pp(const data::forall_binder &x, bool arg0)
Definition data.cpp:57
std::string pp(const data::untyped_possible_sorts &x, bool arg0)
Definition data.cpp:75
std::string pp(const data::function_symbol &x, bool arg0)
Definition data.cpp:60
std::set< data::variable > substitution_variables(const mutable_map_substitution<> &sigma)
Definition data.cpp:184
std::string pp(const data::machine_number &x, bool arg0)
Definition data.cpp:64
std::string pp(const data::assignment_expression &x, bool arg0)
Definition data.cpp:42
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)
Definition data.cpp:65
std::string pp(const data::data_expression_list &x, bool arg0)
Definition data.cpp:26
expression builder that visits all sub expressions
Definition builder.h:32
void leave(const T &)
Definition builder.h:40
void enter(const T &)
Definition builder.h:35
static const atermpp::aterm SortRef
void apply(T &result, const argument_type &x)
Definition builder.h:173
update_apply_builder(const Function &f)
Definition builder.h:179
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:511
void apply(T &result, const data::machine_number &x)
Definition builder.h:445
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:471
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:578
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:519
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:454
void apply(T &result, const data::data_equation &x)
Definition builder.h:527
void apply(T &result, const data::function_symbol &x)
Definition builder.h:416
void apply(T &result, const data::assignment &x)
Definition builder.h:463
void apply(T &result, const data::abstraction &x)
Definition builder.h:593
void apply(T &result, const data::forall &x)
Definition builder.h:479
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:535
void apply(T &result, const data::exists &x)
Definition builder.h:487
void apply(T &result, const data::where_clause &x)
Definition builder.h:437
void apply(T &result, const data::application &x)
Definition builder.h:425
void apply(T &result, const data::variable &x)
Definition builder.h:407
void apply(T &result, const data::data_expression &x)
Definition builder.h:543
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:503
void apply(T &result, const data::lambda &x)
Definition builder.h:495
void apply(T &result, const data::assignment &x)
Definition builder.h:108
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:207
void apply(T &result, const data::structured_sort_constructor_argument &x)
Definition builder.h:231
void apply(T &result, const data::container_sort &x)
Definition builder.h:133
void apply(T &result, const data::alias &x)
Definition builder.h:247
void apply(T &result, const data::exists &x)
Definition builder.h:191
void apply(T &result, const data::machine_number &x)
Definition builder.h:90
void apply(T &result, const data::function_symbol &x)
Definition builder.h:62
void apply(T &result, const data::untyped_possible_sorts &x)
Definition builder.h:166
void apply(T &result, const data::forall &x)
Definition builder.h:183
void apply(T &result, const data::basic_sort &x)
Definition builder.h:124
void apply(T &result, const data::data_equation &x)
Definition builder.h:255
void apply(T &result, const data::untyped_sort &x)
Definition builder.h:157
void apply(T &result, const data::abstraction &x)
Definition builder.h:356
void apply(T &result, const data::application &x)
Definition builder.h:70
void apply(T &result, const data::variable &x)
Definition builder.h:54
void apply(T &result, const data::structured_sort &x)
Definition builder.h:141
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:116
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:263
void apply(T &result, const data::function_sort &x)
Definition builder.h:149
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:99
void apply(T &result, const data::structured_sort_constructor &x)
Definition builder.h:239
void apply(T &result, const data::lambda &x)
Definition builder.h:199
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:223
void apply(T &result, const data::where_clause &x)
Definition builder.h:82
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:306
void apply(T &result, const data::data_expression &x)
Definition builder.h:271
void apply(T &result, const data::sort_expression &x)
Definition builder.h:321
void apply(T &result, const data::untyped_sort_variable &x)
Definition builder.h:174
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:215
void apply(T &result, const data::abstraction &x)
Definition builder.h:829
void apply(T &result, const data::application &x)
Definition builder.h:661
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:771
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:690
void apply(T &result, const data::data_expression &x)
Definition builder.h:779
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:814
void apply(T &result, const data::where_clause &x)
Definition builder.h:673
void apply(T &result, const data::forall &x)
Definition builder.h:715
void apply(T &result, const data::function_symbol &x)
Definition builder.h:652
void apply(T &result, const data::exists &x)
Definition builder.h:723
void apply(T &result, const data::lambda &x)
Definition builder.h:731
void apply(T &result, const data::variable &x)
Definition builder.h:643
void apply(T &result, const data::assignment &x)
Definition builder.h:699
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:707
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:755
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:739
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:747
void apply(T &result, const data::machine_number &x)
Definition builder.h:681
void apply(T &result, const data::data_equation &x)
Definition builder.h:763
data_expression_actions(const core::parser &parser_)
Definition parse_impl.h:138
data::data_expression parse_DataExpr(const core::parse_node &node) const
Definition parse_impl.h:208
data_specification_actions(const core::parser &parser_)
Definition parse_impl.h:297
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
Definition parse_impl.h:458
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
Definition parse_impl.h:32
\brief Builder class
Definition builder.h:864