Line data Source code
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/abstraction.h 10 : /// \brief The class abstraction. 11 : 12 : #ifndef MCRL2_DATA_ABSTRACTION_H 13 : #define MCRL2_DATA_ABSTRACTION_H 14 : 15 : #include "mcrl2/data/binder_type.h" 16 : #include "mcrl2/data/data_expression.h" 17 : 18 : namespace mcrl2 19 : { 20 : 21 : namespace data 22 : { 23 : 24 : /// \brief An abstraction expression. 25 : class abstraction: public data_expression 26 : { 27 : public: 28 : /// \brief Default constructor. 29 6 : abstraction() 30 6 : : data_expression(core::detail::default_values::Binder) 31 6 : {} 32 : 33 : /// \brief Constructor. 34 : /// \param term A term 35 105409 : explicit abstraction(const atermpp::aterm& term) 36 105409 : : data_expression(term) 37 : { 38 105409 : assert(core::detail::check_term_Binder(*this)); 39 105409 : } 40 : 41 : /// \brief Constructor. 42 26948 : abstraction(const binder_type& binding_operator, const variable_list& variables, const data_expression& body) 43 26948 : : data_expression(atermpp::aterm_appl(core::detail::function_symbol_Binder(), binding_operator, variables, body)) 44 26948 : {} 45 : 46 : /// \brief Constructor. 47 : template <typename Container> 48 11 : abstraction(const binder_type& binding_operator, const Container& variables, const data_expression& body, typename atermpp::enable_if_container<Container, variable>::type* = nullptr) 49 11 : : data_expression(atermpp::aterm_appl(core::detail::function_symbol_Binder(), binding_operator, variable_list(variables.begin(), variables.end()), body)) 50 11 : {} 51 : 52 : /// Move semantics 53 4 : abstraction(const abstraction&) noexcept = default; 54 : abstraction(abstraction&&) noexcept = default; 55 : abstraction& operator=(const abstraction&) noexcept = default; 56 : abstraction& operator=(abstraction&&) noexcept = default; 57 : 58 40147 : const binder_type& binding_operator() const 59 : { 60 40147 : return atermpp::down_cast<const binder_type>((*this)[0]); 61 : } 62 : 63 44576 : const variable_list& variables() const 64 : { 65 44576 : return atermpp::down_cast<const variable_list>((*this)[1]); 66 : } 67 : 68 42656 : const data_expression& body() const 69 : { 70 42656 : return atermpp::down_cast<const data_expression>((*this)[2]); 71 : } 72 : }; 73 : 74 : template <class... ARGUMENTS> 75 23669 : void make_abstraction(atermpp::aterm& result, ARGUMENTS... arguments) 76 : { 77 23669 : make_term_appl(result, core::detail::function_symbol_Binder(), arguments...); 78 23669 : } 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 87 : std::string pp(const abstraction& x); 88 : 89 : /// \\brief Outputs the object to a stream 90 : /// \\param out An output stream 91 : /// \\param x Object x 92 : /// \\return The output stream 93 : inline 94 : std::ostream& operator<<(std::ostream& out, const abstraction& x) 95 : { 96 : return out << data::pp(x); 97 : } 98 : 99 : /// \\brief swap overload 100 : inline 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 :