LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - binder_type.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 35 35 100.0 %
Date: 2024-03-08 02:52:28 Functions: 14 14 100.0 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14