mCRL2
Loading...
Searching...
No Matches
builder.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
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/core/builder.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_CORE_BUILDER_H
13#define MCRL2_CORE_BUILDER_H
14
15#include "mcrl2/atermpp/aterm_list.h"
16#include "mcrl2/atermpp/concepts.h"
17
18
19
20namespace mcrl2::core
21{
22
23/**
24 * \brief expression builder that visits all sub expressions
25 *
26 * Types:
27 * \arg Derived the type of a derived class, as per CRTP
28 *
29 **/
30template <typename Derived>
31struct builder
32{
33 // Enter object
34 template <typename T>
35 void enter(const T&)
36 {}
37
38 // Leave object
39 template <typename T>
40 void leave(const T&)
41 {}
42
43 template <typename T>
44 requires (!std::ranges::range<T>)
45 void update(T& x)
46 {
47 T result;
48 static_cast<Derived*>(this)->apply(result, x);
49 x = result;
50 }
51
52 // container visit
53 template <std::ranges::range T>
54 void update(T& x)
55 {
56 for (auto& v: x)
57 {
58 static_cast<Derived*>(this)->update(v);
59 }
60 }
61
62 // aterm set visit
63 template <typename T>
64 void update(std::set<T>& x)
65 {
66 std::set<T> result;
67 for (T v: x)
68 {
69 static_cast<Derived*>(this)->update(v);
71 }
72 result.swap(x);
73 }
74
75 // term_list visit copy
76 template <atermpp::IsATerm T, atermpp::IsATerm U>
78 {
79 atermpp::make_term_list<T>(static_cast<atermpp::term_list<T>&>(result),
80 x.begin(),
81 x.end(),
82 [&](T& result, const U& v) { static_cast<Derived*>(this)->apply(result, v); } );
83 }
84};
85
86
87// apply a builder without additional template arguments
88template <template <class> class Builder>
90{
92
93public:
94
95 using super::enter;
96 using super::leave;
97 using super::apply;
98 using super::update;
99};
100
101template <template <class> class Builder>
104{
105 return apply_builder<Builder>();
106}
107
108// apply a builder with one additional template argument
109template <template <class> class Builder, class Arg1>
111{
113
114public:
115 using super::enter;
116 using super::leave;
117 using super::apply;
118 using super::update;
119
120 apply_builder_arg1(const Arg1& arg1)
121 : super(arg1)
122 {}
123};
124
125template <template <class> class Builder, class Arg1>
128{
129 return apply_builder_arg1<Builder, Arg1>(arg1);
130}
131
132// apply a builder with two additional template arguments
133template <template <class> class Builder, class Arg1, class Arg2>
135{
137
138public:
139 using super::enter;
140 using super::leave;
141 using super::apply;
142 using super::update;
143
144 apply_builder_arg2(const Arg1& arg1, const Arg2& arg2)
145 : super(arg1, arg2)
146 {}
147};
148
149template <template <class> class Builder, class Arg1, class Arg2>
152{
153 return apply_builder_arg2<Builder, Arg1, Arg2>(arg1, arg2);
154}
155
156
157// apply a builder without additional template arguments
158template <template <class> class Builder, class Function>
160{
162
163 using super::enter;
164 using super::leave;
165 using super::apply;
166 using super::update;
167
168 using argument_type = typename Function::argument_type; ///< The argument_type is required to restrict the overloads of apply(x) to that type.
169 using result_type = typename Function::result_type; ///< The argument_type is required to restrict the overloads of apply(x) to that type.
170 const Function& f_;
171
172 template <class T>
173 void apply(T& result, const argument_type& x) // -> decltype(f_(x))
174 {
175 // static_cast<result_type&>(result) = f_(x);
176 result = static_cast<T>(f_(x));
177 }
178
179 update_apply_builder(const Function& f)
180 : f_(f)
181 {}
182};
183
184template <template <class> class Builder, class Function>
187{
188 return update_apply_builder<Builder, Function>(f);
189}
190
191// apply a builder with one additional template argument
192template <template <class> class Builder, class Function, class Arg1>
194{
196
197 using super::enter;
198 using super::leave;
199 using super::apply;
200 using super::update;
201
202 using argument_type = typename Function::argument_type; ///< The argument_type is required to restrict the overloads of apply(x) to that type.
203 using result_type = typename Function::result_type;
204 const Function& f_;
205
206 template <class T>
207 void apply(T& result, const argument_type& x) // -> decltype(f_(x))
208 {
209 result = f_(x);
210 }
211
212 update_apply_builder_arg1(const Function& f, const Arg1& arg1):
213 super(arg1),
214 f_(f)
215 {}
216};
217
218template <template <class> class Builder, class Function, class Arg1>
221{
222 return update_apply_builder_arg1<Builder, Function, Arg1>(f);
223}
224
225} // namespace mcrl2::core
226
227
228
229#endif // MCRL2_CORE_BUILDER_H
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
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::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
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.
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
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
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