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_symbol.h
      10             : /// \brief The class function symbol.
      11             : 
      12             : #ifndef MCRL2_DATA_FUNCTION_SYMBOL_H
      13             : #define MCRL2_DATA_FUNCTION_SYMBOL_H
      14             : 
      15             : #include "mcrl2/data/application.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace data
      21             : {
      22             : 
      23             : typedef std::pair<core::identifier_string, sort_expression> function_symbol_key_type;
      24             : 
      25             : //--- start generated class function_symbol ---//
      26             : /// \\brief A function symbol
      27             : class function_symbol: public data_expression
      28             : {
      29             :   public:
      30             : 
      31             : 
      32             :     /// Move semantics
      33     4688853 :     function_symbol(const function_symbol&) noexcept = default;
      34     4062677 :     function_symbol(function_symbol&&) noexcept = default;
      35        2527 :     function_symbol& operator=(const function_symbol&) noexcept = default;
      36        1035 :     function_symbol& operator=(function_symbol&&) noexcept = default;
      37             : 
      38    19481223 :     const core::identifier_string& name() const
      39             :     {
      40    19481223 :       return atermpp::down_cast<core::identifier_string>((*this)[0]);
      41             :     }
      42             : 
      43    33999919 :     const sort_expression& sort() const
      44             :     {
      45    33999919 :       return atermpp::down_cast<sort_expression>((*this)[1]);
      46             :     }
      47             : //--- start user section function_symbol ---//
      48             :     /// \brief Default constructor.
      49        1680 :     function_symbol()
      50        1680 :       : data_expression(core::detail::default_values::OpId)
      51        1680 :     {}
      52             : 
      53             :     /// \brief Constructor.
      54             :     /// \param term A term
      55    47102932 :     explicit function_symbol(const atermpp::aterm& term)
      56    47102932 :       : data_expression(term)
      57             :     {
      58    47102932 :       assert(core::detail::check_term_OpId(*this));
      59    47102932 :     }
      60             : 
      61             :     /// \brief Constructor.
      62     4951344 :     function_symbol(const core::identifier_string& name, const sort_expression& sort)
      63     4951344 :     {
      64             :       atermpp::make_term_appl_with_index<function_symbol, std::pair<core::identifier_string, sort_expression> >
      65     4951344 :                       (*this, core::detail::function_symbol_OpId(), name, sort);
      66     4951344 :     }
      67             : 
      68             : 
      69             :     /// \brief Constructor.
      70       65796 :     function_symbol(const std::string& name, const sort_expression& sort)
      71       65796 :     { 
      72             :       atermpp::make_term_appl_with_index<function_symbol, std::pair<core::identifier_string, sort_expression> >
      73       65796 :                       (*this, core::detail::function_symbol_OpId(), core::identifier_string(name), sort);
      74       65796 :     }
      75             : 
      76             : //--- end user section function_symbol ---//
      77             : };
      78             : 
      79             : /// \\brief Make_function_symbol constructs a new term into a given address.
      80             : /// \\ \param t The reference into which the new function_symbol is constructed. 
      81             : template <class... ARGUMENTS>
      82    14703897 : inline void make_function_symbol(atermpp::aterm_appl& t, const ARGUMENTS&... args)
      83             : {
      84    14703897 :   atermpp::make_term_appl_with_index<function_symbol,std::pair<core::identifier_string, sort_expression>>(t, core::detail::function_symbol_OpId(), args...);
      85    14703897 : }
      86             : 
      87             : /// \\brief list of function_symbols
      88             : typedef atermpp::term_list<function_symbol> function_symbol_list;
      89             : 
      90             : /// \\brief vector of function_symbols
      91             : typedef std::vector<function_symbol>    function_symbol_vector;
      92             : 
      93             : // prototype declaration
      94             : std::string pp(const function_symbol& x);
      95             : 
      96             : /// \\brief Outputs the object to a stream
      97             : /// \\param out An output stream
      98             : /// \\param x Object x
      99             : /// \\return The output stream
     100             : inline
     101        1883 : std::ostream& operator<<(std::ostream& out, const function_symbol& x)
     102             : {
     103        1883 :   return out << data::pp(x);
     104             : }
     105             : 
     106             : /// \\brief swap overload
     107             : inline void swap(function_symbol& t1, function_symbol& t2)
     108             : {
     109             :   t1.swap(t2);
     110             : }
     111             : //--- end generated class function_symbol ---//
     112             : 
     113             : // template function overloads
     114             : std::string pp(const function_symbol_list& x);
     115             : std::string pp(const function_symbol_vector& x);
     116             : std::set<data::variable> find_all_variables(const data::function_symbol& x);
     117             : 
     118             : } // namespace data
     119             : 
     120             : } // namespace mcrl2
     121             : 
     122             : #endif // MCRL2_DATA_FUNCTION_SYMBOL_H
     123             :