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/binder_type.h 10 : /// \brief The class binder_type. 11 : 12 : #ifndef MCRL2_DATA_BINDER_TYPE_H 13 : #define MCRL2_DATA_BINDER_TYPE_H 14 : 15 : #include "mcrl2/core/detail/default_values.h" 16 : #include "mcrl2/core/detail/soundness_checks.h" 17 : 18 : namespace mcrl2 19 : { 20 : 21 : namespace data 22 : { 23 : 24 : //--- start generated classes ---// 25 : /// \\brief Binder 26 : class binder_type: public atermpp::aterm_appl 27 : { 28 : public: 29 : /// \\brief Default constructor. 30 : binder_type() 31 : : atermpp::aterm_appl(core::detail::default_values::BindingOperator) 32 : {} 33 : 34 : /// \\brief Constructor. 35 : /// \\param term A term 36 116244 : explicit binder_type(const atermpp::aterm& term) 37 116244 : : atermpp::aterm_appl(term) 38 : { 39 116244 : assert(core::detail::check_rule_BindingOperator(*this)); 40 116244 : } 41 : 42 : /// Move semantics 43 276 : binder_type(const binder_type&) noexcept = default; 44 : binder_type(binder_type&&) noexcept = default; 45 : binder_type& operator=(const binder_type&) noexcept = default; 46 : binder_type& operator=(binder_type&&) noexcept = default; 47 : }; 48 : 49 : /// \\brief list of binder_types 50 : typedef atermpp::term_list<binder_type> binder_type_list; 51 : 52 : /// \\brief vector of binder_types 53 : typedef std::vector<binder_type> binder_type_vector; 54 : 55 : // prototype declaration 56 : std::string pp(const binder_type& x); 57 : 58 : /// \\brief Outputs the object to a stream 59 : /// \\param out An output stream 60 : /// \\param x Object x 61 : /// \\return The output stream 62 : inline 63 : std::ostream& operator<<(std::ostream& out, const binder_type& x) 64 : { 65 : return out << data::pp(x); 66 : } 67 : 68 : /// \\brief swap overload 69 : inline void swap(binder_type& t1, binder_type& t2) 70 : { 71 : t1.swap(t2); 72 : } 73 : 74 : 75 : /// \\brief Binder for untyped set or bag comprehension 76 : class untyped_set_or_bag_comprehension_binder: public binder_type 77 : { 78 : public: 79 : /// \\brief Default constructor. 80 55 : untyped_set_or_bag_comprehension_binder() 81 55 : : binder_type(core::detail::default_values::UntypedSetBagComp) 82 55 : {} 83 : 84 : /// \\brief Constructor. 85 : /// \\param term A term 86 : explicit untyped_set_or_bag_comprehension_binder(const atermpp::aterm& term) 87 : : binder_type(term) 88 : { 89 : assert(core::detail::check_term_UntypedSetBagComp(*this)); 90 : } 91 : 92 : /// Move semantics 93 : untyped_set_or_bag_comprehension_binder(const untyped_set_or_bag_comprehension_binder&) noexcept = default; 94 : untyped_set_or_bag_comprehension_binder(untyped_set_or_bag_comprehension_binder&&) noexcept = default; 95 : untyped_set_or_bag_comprehension_binder& operator=(const untyped_set_or_bag_comprehension_binder&) noexcept = default; 96 : untyped_set_or_bag_comprehension_binder& operator=(untyped_set_or_bag_comprehension_binder&&) noexcept = default; 97 : }; 98 : 99 : /// \\brief Test for a untyped_set_or_bag_comprehension_binder expression 100 : /// \\param x A term 101 : /// \\return True if \\a x is a untyped_set_or_bag_comprehension_binder expression 102 : inline 103 259 : bool is_untyped_set_or_bag_comprehension_binder(const atermpp::aterm_appl& x) 104 : { 105 259 : return x.function() == core::detail::function_symbols::UntypedSetBagComp; 106 : } 107 : 108 : // prototype declaration 109 : std::string pp(const untyped_set_or_bag_comprehension_binder& x); 110 : 111 : /// \\brief Outputs the object to a stream 112 : /// \\param out An output stream 113 : /// \\param x Object x 114 : /// \\return The output stream 115 : inline 116 : std::ostream& operator<<(std::ostream& out, const untyped_set_or_bag_comprehension_binder& x) 117 : { 118 : return out << data::pp(x); 119 : } 120 : 121 : /// \\brief swap overload 122 : inline void swap(untyped_set_or_bag_comprehension_binder& t1, untyped_set_or_bag_comprehension_binder& t2) 123 : { 124 : t1.swap(t2); 125 : } 126 : 127 : 128 : /// \\brief Binder for set comprehension 129 : class set_comprehension_binder: public binder_type 130 : { 131 : public: 132 : /// \\brief Default constructor. 133 75 : set_comprehension_binder() 134 75 : : binder_type(core::detail::default_values::SetComp) 135 75 : {} 136 : 137 : /// \\brief Constructor. 138 : /// \\param term A term 139 : explicit set_comprehension_binder(const atermpp::aterm& term) 140 : : binder_type(term) 141 : { 142 : assert(core::detail::check_term_SetComp(*this)); 143 : } 144 : 145 : /// Move semantics 146 : set_comprehension_binder(const set_comprehension_binder&) noexcept = default; 147 : set_comprehension_binder(set_comprehension_binder&&) noexcept = default; 148 : set_comprehension_binder& operator=(const set_comprehension_binder&) noexcept = default; 149 : set_comprehension_binder& operator=(set_comprehension_binder&&) noexcept = default; 150 : }; 151 : 152 : /// \\brief Test for a set_comprehension_binder expression 153 : /// \\param x A term 154 : /// \\return True if \\a x is a set_comprehension_binder expression 155 : inline 156 230 : bool is_set_comprehension_binder(const atermpp::aterm_appl& x) 157 : { 158 230 : return x.function() == core::detail::function_symbols::SetComp; 159 : } 160 : 161 : // prototype declaration 162 : std::string pp(const set_comprehension_binder& x); 163 : 164 : /// \\brief Outputs the object to a stream 165 : /// \\param out An output stream 166 : /// \\param x Object x 167 : /// \\return The output stream 168 : inline 169 : std::ostream& operator<<(std::ostream& out, const set_comprehension_binder& x) 170 : { 171 : return out << data::pp(x); 172 : } 173 : 174 : /// \\brief swap overload 175 : inline void swap(set_comprehension_binder& t1, set_comprehension_binder& t2) 176 : { 177 : t1.swap(t2); 178 : } 179 : 180 : 181 : /// \\brief Binder for bag comprehension 182 : class bag_comprehension_binder: public binder_type 183 : { 184 : public: 185 : /// \\brief Default constructor. 186 40 : bag_comprehension_binder() 187 40 : : binder_type(core::detail::default_values::BagComp) 188 40 : {} 189 : 190 : /// \\brief Constructor. 191 : /// \\param term A term 192 : explicit bag_comprehension_binder(const atermpp::aterm& term) 193 : : binder_type(term) 194 : { 195 : assert(core::detail::check_term_BagComp(*this)); 196 : } 197 : 198 : /// Move semantics 199 : bag_comprehension_binder(const bag_comprehension_binder&) noexcept = default; 200 : bag_comprehension_binder(bag_comprehension_binder&&) noexcept = default; 201 : bag_comprehension_binder& operator=(const bag_comprehension_binder&) noexcept = default; 202 : bag_comprehension_binder& operator=(bag_comprehension_binder&&) noexcept = default; 203 : }; 204 : 205 : /// \\brief Test for a bag_comprehension_binder expression 206 : /// \\param x A term 207 : /// \\return True if \\a x is a bag_comprehension_binder expression 208 : inline 209 230 : bool is_bag_comprehension_binder(const atermpp::aterm_appl& x) 210 : { 211 230 : return x.function() == core::detail::function_symbols::BagComp; 212 : } 213 : 214 : // prototype declaration 215 : std::string pp(const bag_comprehension_binder& x); 216 : 217 : /// \\brief Outputs the object to a stream 218 : /// \\param out An output stream 219 : /// \\param x Object x 220 : /// \\return The output stream 221 : inline 222 : std::ostream& operator<<(std::ostream& out, const bag_comprehension_binder& x) 223 : { 224 : return out << data::pp(x); 225 : } 226 : 227 : /// \\brief swap overload 228 : inline void swap(bag_comprehension_binder& t1, bag_comprehension_binder& t2) 229 : { 230 : t1.swap(t2); 231 : } 232 : 233 : 234 : /// \\brief Binder for universal quantification 235 : class forall_binder: public binder_type 236 : { 237 : public: 238 : /// \\brief Default constructor. 239 64314 : forall_binder() 240 64314 : : binder_type(core::detail::default_values::Forall) 241 64314 : {} 242 : 243 : /// \\brief Constructor. 244 : /// \\param term A term 245 : explicit forall_binder(const atermpp::aterm& term) 246 : : binder_type(term) 247 : { 248 : assert(core::detail::check_term_Forall(*this)); 249 : } 250 : 251 : /// Move semantics 252 : forall_binder(const forall_binder&) noexcept = default; 253 : forall_binder(forall_binder&&) noexcept = default; 254 : forall_binder& operator=(const forall_binder&) noexcept = default; 255 : forall_binder& operator=(forall_binder&&) noexcept = default; 256 : }; 257 : 258 : /// \\brief Test for a forall_binder expression 259 : /// \\param x A term 260 : /// \\return True if \\a x is a forall_binder expression 261 : inline 262 274 : bool is_forall_binder(const atermpp::aterm_appl& x) 263 : { 264 274 : return x.function() == core::detail::function_symbols::Forall; 265 : } 266 : 267 : // prototype declaration 268 : std::string pp(const forall_binder& x); 269 : 270 : /// \\brief Outputs the object to a stream 271 : /// \\param out An output stream 272 : /// \\param x Object x 273 : /// \\return The output stream 274 : inline 275 : std::ostream& operator<<(std::ostream& out, const forall_binder& x) 276 : { 277 : return out << data::pp(x); 278 : } 279 : 280 : /// \\brief swap overload 281 : inline void swap(forall_binder& t1, forall_binder& t2) 282 : { 283 : t1.swap(t2); 284 : } 285 : 286 : 287 : /// \\brief Binder for existential quantification 288 : class exists_binder: public binder_type 289 : { 290 : public: 291 : /// \\brief Default constructor. 292 861 : exists_binder() 293 861 : : binder_type(core::detail::default_values::Exists) 294 861 : {} 295 : 296 : /// \\brief Constructor. 297 : /// \\param term A term 298 : explicit exists_binder(const atermpp::aterm& term) 299 : : binder_type(term) 300 : { 301 : assert(core::detail::check_term_Exists(*this)); 302 : } 303 : 304 : /// Move semantics 305 : exists_binder(const exists_binder&) noexcept = default; 306 : exists_binder(exists_binder&&) noexcept = default; 307 : exists_binder& operator=(const exists_binder&) noexcept = default; 308 : exists_binder& operator=(exists_binder&&) noexcept = default; 309 : }; 310 : 311 : /// \\brief Test for a exists_binder expression 312 : /// \\param x A term 313 : /// \\return True if \\a x is a exists_binder expression 314 : inline 315 176 : bool is_exists_binder(const atermpp::aterm_appl& x) 316 : { 317 176 : return x.function() == core::detail::function_symbols::Exists; 318 : } 319 : 320 : // prototype declaration 321 : std::string pp(const exists_binder& x); 322 : 323 : /// \\brief Outputs the object to a stream 324 : /// \\param out An output stream 325 : /// \\param x Object x 326 : /// \\return The output stream 327 : inline 328 : std::ostream& operator<<(std::ostream& out, const exists_binder& x) 329 : { 330 : return out << data::pp(x); 331 : } 332 : 333 : /// \\brief swap overload 334 : inline void swap(exists_binder& t1, exists_binder& t2) 335 : { 336 : t1.swap(t2); 337 : } 338 : 339 : 340 : /// \\brief Binder for lambda abstraction 341 : class lambda_binder: public binder_type 342 : { 343 : public: 344 : /// \\brief Default constructor. 345 10834 : lambda_binder() 346 10834 : : binder_type(core::detail::default_values::Lambda) 347 10834 : {} 348 : 349 : /// \\brief Constructor. 350 : /// \\param term A term 351 : explicit lambda_binder(const atermpp::aterm& term) 352 : : binder_type(term) 353 : { 354 : assert(core::detail::check_term_Lambda(*this)); 355 : } 356 : 357 : /// Move semantics 358 : lambda_binder(const lambda_binder&) noexcept = default; 359 : lambda_binder(lambda_binder&&) noexcept = default; 360 : lambda_binder& operator=(const lambda_binder&) noexcept = default; 361 : lambda_binder& operator=(lambda_binder&&) noexcept = default; 362 : }; 363 : 364 : /// \\brief Test for a lambda_binder expression 365 : /// \\param x A term 366 : /// \\return True if \\a x is a lambda_binder expression 367 : inline 368 2563 : bool is_lambda_binder(const atermpp::aterm_appl& x) 369 : { 370 2563 : return x.function() == core::detail::function_symbols::Lambda; 371 : } 372 : 373 : // prototype declaration 374 : std::string pp(const lambda_binder& x); 375 : 376 : /// \\brief Outputs the object to a stream 377 : /// \\param out An output stream 378 : /// \\param x Object x 379 : /// \\return The output stream 380 : inline 381 : std::ostream& operator<<(std::ostream& out, const lambda_binder& x) 382 : { 383 : return out << data::pp(x); 384 : } 385 : 386 : /// \\brief swap overload 387 : inline void swap(lambda_binder& t1, lambda_binder& t2) 388 : { 389 : t1.swap(t2); 390 : } 391 : //--- end generated classes ---// 392 : 393 : } // namespace data 394 : 395 : } // namespace mcrl2 396 : 397 : #endif // MCRL2_DATA_BINDER_TYPE_H