mCRL2
Loading...
Searching...
No Matches
abstraction.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_ABSTRACTION_H
13#define MCRL2_DATA_ABSTRACTION_H
14
17
18namespace mcrl2
19{
20
21namespace data
22{
23
26{
27 public:
30 : data_expression(core::detail::default_values::Binder)
31 {}
32
35 explicit abstraction(const atermpp::aterm& term)
36 : data_expression(term)
37 {
39 }
40
43 : data_expression(atermpp::aterm_appl(core::detail::function_symbol_Binder(), binding_operator, variables, body))
44 {}
45
47 template <typename Container>
49 : data_expression(atermpp::aterm_appl(core::detail::function_symbol_Binder(), binding_operator, variable_list(variables.begin(), variables.end()), body))
50 {}
51
53 abstraction(const abstraction&) noexcept = default;
54 abstraction(abstraction&&) noexcept = default;
55 abstraction& operator=(const abstraction&) noexcept = default;
56 abstraction& operator=(abstraction&&) noexcept = default;
57
59 {
60 return atermpp::down_cast<const binder_type>((*this)[0]);
61 }
62
63 const variable_list& variables() const
64 {
65 return atermpp::down_cast<const variable_list>((*this)[1]);
66 }
67
68 const data_expression& body() const
69 {
70 return atermpp::down_cast<const data_expression>((*this)[2]);
71 }
72};
73
74template <class... ARGUMENTS>
75void make_abstraction(atermpp::aterm& result, ARGUMENTS... arguments)
76{
77 make_term_appl(result, core::detail::function_symbol_Binder(), arguments...);
78}
79
80/* inline void make_abstraction(atermpp::aterm& result, const binder_type& binding_operator, const variable_list& variables, const data_expression& body)
81{
82 make_term_appl(result, core::detail::function_symbol_Binder(), binding_operator, variables, body);
83} */
84
85//--- start generated class abstraction ---//
86// prototype declaration
87std::string pp(const abstraction& x);
88
93inline
94std::ostream& operator<<(std::ostream& out, const abstraction& x)
95{
96 return out << data::pp(x);
97}
98
100inline void swap(abstraction& t1, abstraction& t2)
101{
102 t1.swap(t2);
103}
104//--- end generated class abstraction ---//
105
106} // namespace data
107
108} // namespace mcrl2
109
110#endif // MCRL2_DATA_ABSTRACTION_H
111
The class binder_type.
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
void swap(unprotected_aterm &t) noexcept
Swaps this term with its argument.
Definition aterm.h:156
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
abstraction(const atermpp::aterm &term)
Constructor.
Definition abstraction.h:35
abstraction(const binder_type &binding_operator, const variable_list &variables, const data_expression &body)
Constructor.
Definition abstraction.h:42
abstraction(const abstraction &) noexcept=default
Move semantics.
abstraction(const binder_type &binding_operator, const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Constructor.
Definition abstraction.h:48
const data_expression & body() const
Definition abstraction.h:68
abstraction(abstraction &&) noexcept=default
abstraction()
Default constructor.
Definition abstraction.h:29
const binder_type & binding_operator() const
Definition abstraction.h:58
const_iterator end() const
const_iterator begin() const
The class data_expression.
The main namespace for the aterm++ library.
Definition algorithm.h:21
const atermpp::function_symbol & function_symbol_Binder()
bool check_term_Binder(const Term &t)
void swap(abstraction &t1, abstraction &t2)
\brief swap overload
std::string pp(const abstraction &x)
Definition data.cpp:39
void make_abstraction(atermpp::aterm &result, ARGUMENTS... arguments)
Definition abstraction.h:75
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