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/function_sort.h
      10             : /// \brief The class function_sort.
      11             : 
      12             : #ifndef MCRL2_DATA_FUNCTION_SORT_H
      13             : #define MCRL2_DATA_FUNCTION_SORT_H
      14             : 
      15             : #include "mcrl2/data/sort_expression.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace data
      21             : {
      22             : 
      23             : //--- start generated class function_sort ---//
      24             : /// \\brief A function sort
      25             : class function_sort: public sort_expression
      26             : {
      27             :   public:
      28             :     /// \\brief Default constructor.
      29         159 :     function_sort()
      30         159 :       : sort_expression(core::detail::default_values::SortArrow)
      31         159 :     {}
      32             : 
      33             :     /// \\brief Constructor.
      34             :     /// \\param term A term
      35    41004232 :     explicit function_sort(const atermpp::aterm& term)
      36    41004232 :       : sort_expression(term)
      37             :     {
      38    41004232 :       assert(core::detail::check_term_SortArrow(*this));
      39    41004232 :     }
      40             : 
      41             :     /// \\brief Constructor.
      42     5460222 :     function_sort(const sort_expression_list& domain, const sort_expression& codomain)
      43     5460222 :       : sort_expression(atermpp::aterm_appl(core::detail::function_symbol_SortArrow(), domain, codomain))
      44     5460222 :     {}
      45             : 
      46             :     /// \\brief Constructor.
      47             :     template <typename Container>
      48    12451814 :     function_sort(const Container& domain, const sort_expression& codomain, typename atermpp::enable_if_container<Container, sort_expression>::type* = nullptr)
      49    12451814 :       : sort_expression(atermpp::aterm_appl(core::detail::function_symbol_SortArrow(), sort_expression_list(domain.begin(), domain.end()), codomain))
      50    12451814 :     {}
      51             : 
      52             :     /// Move semantics
      53       13665 :     function_sort(const function_sort&) noexcept = default;
      54         924 :     function_sort(function_sort&&) noexcept = default;
      55         271 :     function_sort& operator=(const function_sort&) noexcept = default;
      56             :     function_sort& operator=(function_sort&&) noexcept = default;
      57             : 
      58    18150580 :     const sort_expression_list& domain() const
      59             :     {
      60    18150580 :       return atermpp::down_cast<sort_expression_list>((*this)[0]);
      61             :     }
      62             : 
      63    28289063 :     const sort_expression& codomain() const
      64             :     {
      65    28289063 :       return atermpp::down_cast<sort_expression>((*this)[1]);
      66             :     }
      67             : };
      68             : 
      69             : /// \\brief Make_function_sort constructs a new term into a given address.
      70             : /// \\ \param t The reference into which the new function_sort is constructed. 
      71             : template <class... ARGUMENTS>
      72         297 : inline void make_function_sort(atermpp::aterm_appl& t, const ARGUMENTS&... args)
      73             : {
      74         297 :   atermpp::make_term_appl(t, core::detail::function_symbol_SortArrow(), args...);
      75         297 : }
      76             : 
      77             : // prototype declaration
      78             : std::string pp(const function_sort& x);
      79             : 
      80             : /// \\brief Outputs the object to a stream
      81             : /// \\param out An output stream
      82             : /// \\param x Object x
      83             : /// \\return The output stream
      84             : inline
      85           0 : std::ostream& operator<<(std::ostream& out, const function_sort& x)
      86             : {
      87           0 :   return out << data::pp(x);
      88             : }
      89             : 
      90             : /// \\brief swap overload
      91             : inline void swap(function_sort& t1, function_sort& t2)
      92             : {
      93             :   t1.swap(t2);
      94             : }
      95             : //--- end generated class function_sort ---//
      96             : 
      97             : /// \brief list of function sorts
      98             : typedef atermpp::term_list<function_sort> function_sort_list;
      99             : /// \brief vector of function sorts
     100             : typedef std::vector<function_sort> function_sort_vector;
     101             : 
     102             : /// \brief Convenience constructor for function sort with domain size 1
     103             : ///
     104             : /// \param[in] dom1 The first sort of the domain.
     105             : /// \param[in] codomain The codomain of the sort.
     106             : /// \post *this represents dom1 -> codomain
     107      984289 : inline function_sort make_function_sort_(const sort_expression& dom1,
     108             :                                          const sort_expression& codomain)
     109             : {
     110     1968578 :   return function_sort({ dom1 }, codomain);
     111             : }
     112             : 
     113             : /// \brief Convenience constructor for function sort with domain size 2
     114             : ///
     115             : /// \param[in] dom1 The first sort of the domain.
     116             : /// \param[in] dom2 The second sort of the domain.
     117             : /// \param[in] codomain The codomain of the sort.
     118             : /// \post *this represents dom1 # dom2 -> codomain
     119     3700940 : inline function_sort make_function_sort_(const sort_expression& dom1,
     120             :                                          const sort_expression& dom2,
     121             :                                          const sort_expression& codomain)
     122             : {
     123    11102820 :   return function_sort({ dom1, dom2 }, codomain);
     124             : }
     125             : 
     126             : /// \brief Convenience constructor for function sort with domain size 3
     127             : ///
     128             : /// \param[in] dom1 The first sort of the domain.
     129             : /// \param[in] dom2 The second sort of the domain.
     130             : /// \param[in] dom3 The third sort of the domain.
     131             : /// \param[in] codomain The codomain of the sort.
     132             : /// \post *this represents dom1 # dom2 # dom3 -> codomain
     133      648160 : inline function_sort make_function_sort_(const sort_expression& dom1,
     134             :                                          const sort_expression& dom2,
     135             :                                          const sort_expression& dom3,
     136             :                                          const sort_expression& codomain)
     137             : {
     138     2592640 :   return function_sort({ dom1, dom2, dom3 }, codomain);
     139             : }
     140             : 
     141             : /// \brief Convenience constructor for function sort with domain size 4
     142             : ///
     143             : /// \param[in] dom1 The first sort of the domain.
     144             : /// \param[in] dom2 The second sort of the domain.
     145             : /// \param[in] dom3 The third sort of the domain.
     146             : /// \param[in] dom4 The fourth sort of the domain.
     147             : /// \param[in] codomain The codomain of the sort.
     148             : /// \post *this represents dom1 # dom2 # dom3 # dom4 -> codomain
     149       10352 : inline function_sort make_function_sort_(const sort_expression& dom1,
     150             :                                          const sort_expression& dom2,
     151             :                                          const sort_expression& dom3,
     152             :                                          const sort_expression& dom4,
     153             :                                          const sort_expression& codomain)
     154             : {
     155       51760 :   return function_sort({ dom1, dom2, dom3, dom4 }, codomain);
     156             : }
     157             : 
     158             : } // namespace data
     159             : 
     160             : } // namespace mcrl2
     161             : 
     162             : #endif // MCRL2_DATA_FUNCTION_SORT_H
     163             :