mCRL2
Loading...
Searching...
No Matches
data_expression.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//
11
12#ifndef MCRL2_DATA_DATA_EXPRESSION_H
13#define MCRL2_DATA_DATA_EXPRESSION_H
14
18
19namespace mcrl2
20{
21
22namespace data
23{
24
26inline bool is_abstraction(const atermpp::aterm& x)
27{
29}
30
32inline bool is_lambda(const atermpp::aterm_appl& x)
33{
34 return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Lambda;
35}
36
38inline bool is_forall(const atermpp::aterm_appl& x)
39{
40 return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Forall;
41}
42
44inline bool is_exists(const atermpp::aterm_appl& x)
45{
46 return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Exists;
47}
48
51{
52 return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::SetComp;
53}
54
57{
58 return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::BagComp;
59}
60
63{
64 return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::UntypedSetBagComp;
65}
66
69{
71}
72
74inline bool is_variable(const atermpp::aterm& x)
75{
77}
78
85{
87}
88
93{
95}
96
99{
101}
102
105{
107}
108
109class application; // prototype
110
121
122//--- start generated class data_expression ---//
125{
126 public:
129 : atermpp::aterm_appl(core::detail::default_values::DataExpr)
130 {}
131
134 explicit data_expression(const atermpp::aterm& term)
135 : atermpp::aterm_appl(term)
136 {
138 }
139
141 data_expression(const data_expression&) noexcept = default;
142 data_expression(data_expression&&) noexcept = default;
143 data_expression& operator=(const data_expression&) noexcept = default;
144 data_expression& operator=(data_expression&&) noexcept = default;
145//--- start user section data_expression ---//
149 {
151 }
152
153 application operator()(const data_expression& e) const;
154
156 const data_expression& e2) const;
157
159 const data_expression& e2,
160 const data_expression& e3) const;
161
163 const data_expression& e2,
164 const data_expression& e3,
165 const data_expression& e4) const;
166
168
169 sort_expression sort() const;
170
171 private:
172 // The following methods are not to be used in a data_expression.
173 // They are restricted to a data_appl.
176
177//--- end user section data_expression ---//
178};
179
182
184typedef std::vector<data_expression> data_expression_vector;
185
186// prototype declaration
187std::string pp(const data_expression& x);
188
193inline
194std::ostream& operator<<(std::ostream& out, const data_expression& x)
195{
196 return out << data::pp(x);
197}
198
201{
202 t1.swap(t2);
203}
204//--- end generated class data_expression ---//
205
207{
209}
210
214inline
216{
217 return is_lambda(x) ||
218 is_forall(x) ||
219 is_exists(x) ||
224 is_variable(x) ||
225 is_application(x) ||
226 is_where_clause(x) ||
228}
229
234template < typename Container >
236{
237 return data_expression_list(r.begin(),r.end());
238}
239
240class variable;
241
242// template function overloads
243std::string pp(const data_expression_list& x);
244std::string pp(const data_expression_vector& x);
246std::set<data::sort_expression> find_sort_expressions(const data::data_expression& x);
247std::set<data::variable> find_all_variables(const data::data_expression& x);
248std::set<data::variable> find_all_variables(const data::data_expression_list& x);
249std::set<data::variable> find_free_variables(const data::data_expression& x);
250std::set<data::variable> find_free_variables(const data::data_expression_list& x);
252
253inline
255{
256 return find_free_variables(x).empty();
257}
258
261
262} // namespace data
263
264} // namespace mcrl2
265
266// The trick of including application.h only at this point is needed to break
267// the circular dependencies between application and data_expression. This
268// dependency was introduced to allow the application operator to be defined for
269// all data expression types.
270#ifndef MCRL2_DATA_APPLICATION_H
272#endif
273
274namespace mcrl2
275{
276namespace data
277{
280inline bool is_application(const data_expression& t)
281{
282 return !(is_function_symbol(t) ||
283 is_variable(t) ||
284 is_where_clause(t) ||
285 is_abstraction(t) ||
287}
288
290inline
292{
293 return atermpp::down_cast<data_expression_list>(static_cast<const atermpp::aterm&>(l));
294}
295
297inline
299{
300 return application(*this, e);
301}
302
304inline
306{
307 return application(*this, e1, e2);
308}
309
311inline
313{
314 return application(*this, e1, e2, e3);
315}
316
318inline
320{
321 return application(*this, e1, e2, e3, e4);
322}
323
324} // namespace data
325} // namespace mcrl2
326
327
328namespace std
329{
330
331template<>
332struct hash<mcrl2::data::data_expression>
333{
334 std::size_t operator()(const mcrl2::data::data_expression& v) const
335 {
336 const hash<atermpp::aterm> hasher;
337 return hasher(v);
338 }
339};
340
341} // namespace std
342
343
344
345#endif // MCRL2_DATA_DATA_EXPRESSION_H
346
The class application.
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
Iterator for term_appl.
const function_symbol & function() const
Returns the function symbol belonging to an aterm_appl.
Definition aterm_appl.h:174
A list of aterm objects.
Definition aterm_list.h:23
const function_symbol & function() const
Yields the function symbol in an aterm.
Definition aterm.h:165
void swap(unprotected_aterm &t) noexcept
Swaps this term with its argument.
Definition aterm.h:156
An application of a data expression to a number of arguments.
data_expression(const atermpp::aterm &term)
data_expression()
\brief Default constructor.
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
const_iterator end() const
application operator()(const data_expression &e) const
Apply a data expression to a data expression.
data_expression(const data_expression &) noexcept=default
Move semantics.
data_expression(data_expression &&) noexcept=default
const_iterator begin() const
bool is_default_data_expression() const
A function to efficiently determine whether a data expression is made by the default constructor.
\brief A sort expression
\brief A data variable
Definition variable.h:28
The class container_sort.
The class function_sort.
The main namespace for the aterm++ library.
Definition algorithm.h:21
bool gsIsDataAppl(const atermpp::aterm_appl &Term)
bool gsIsDataAppl_no_check(const atermpp::aterm_appl &Term)
bool check_rule_DataExpr(const Term &t)
void make_data_expression(data_expression &result)
bool is_untyped_identifier(const atermpp::aterm_appl &x)
Returns true if the term t is an identifier.
variable_list free_variables(const data_expression &x)
Definition data.cpp:188
bool is_lambda(const atermpp::aterm_appl &x)
Returns true if the term t is a lambda abstraction.
bool is_exists(const atermpp::aterm_appl &x)
Returns true if the term t is an existential quantification.
void swap(abstraction &t1, abstraction &t2)
\brief swap overload
data_expression_list make_data_expression_list(Container const &r, typename atermpp::enable_if_container< Container, data_expression >::type *=nullptr)
Converts an container with data expressions to data_expression_list.
bool is_where_clause(const atermpp::aterm_appl &x)
Returns true if the term t is a where clause.
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:89
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm_appl &x)
Returns true if the term t is a set/bag comprehension.
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:93
bool is_function_symbol(const atermpp::aterm_appl &x)
Returns true if the term t is a function symbol.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
bool is_data_expression(const atermpp::aterm_appl &x)
Test for a data_expression expression.
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
std::string pp(const abstraction &x)
Definition data.cpp:39
bool is_set_comprehension(const atermpp::aterm_appl &x)
Returns true if the term t is a set comprehension.
bool is_application(const atermpp::aterm_appl &x)
Returns true if the term t is an application.
bool is_forall(const atermpp::aterm_appl &x)
Returns true if the term t is a universal quantification.
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:90
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:98
bool is_bag_comprehension(const atermpp::aterm_appl &x)
Returns true if the term t is a bag comprehension.
atermpp::term_list< variable > variable_list
\brief list of variables
bool is_application_no_check(const atermpp::aterm_appl &x)
Returns true if the term t is an application, but it does not check whether an application symbol of ...
const data_expression_list & variable_list_to_data_expression_list(const variable_list &l)
Transform a variable_list into a data_expression_list.
bool is_constant(const data_expression &x)
bool search_variable(const data::data_expression &x, const data::variable &v)
Definition data.cpp:102
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:94
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
static const atermpp::aterm_appl DataExpr
static const atermpp::function_symbol Lambda
static const atermpp::function_symbol BagComp
static const atermpp::function_symbol Forall
static const atermpp::function_symbol Whr
static const atermpp::function_symbol Exists
static const atermpp::function_symbol OpId
static const atermpp::function_symbol SetComp
static const atermpp::function_symbol Binder
static const atermpp::function_symbol DataVarId
static const atermpp::function_symbol UntypedIdentifier
static const atermpp::function_symbol UntypedSetBagComp
std::size_t operator()(const mcrl2::data::data_expression &v) const
#define hash(l, r, m)
Definition tree_set.cpp:23
add your file description here.