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/sort_expression.h
      10             : /// \brief The class sort_expression.
      11             : 
      12             : #ifndef MCRL2_DATA_SORT_EXPRESSION_H
      13             : #define MCRL2_DATA_SORT_EXPRESSION_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             : /// \brief Returns true if the term t is a basic sort
      25    21696782 : inline bool is_basic_sort(const atermpp::aterm_appl& x)
      26             : {
      27    21696782 :   return x.function() == core::detail::function_symbols::SortId;
      28             : }
      29             : 
      30             : /// \brief Returns true if the term t is a function sort
      31    93637528 : inline bool is_function_sort(const atermpp::aterm_appl& x)
      32             : {
      33    93637528 :   return x.function() == core::detail::function_symbols::SortArrow;
      34             : }
      35             : 
      36             : /// \brief Returns true if the term t is a container sort
      37    65191974 : inline bool is_container_sort(const atermpp::aterm_appl& x)
      38             : {
      39    65191974 :   return x.function() == core::detail::function_symbols::SortCons;
      40             : }
      41             : 
      42             : /// \brief Returns true if the term t is a structured sort
      43    63131409 : inline bool is_structured_sort(const atermpp::aterm_appl& x)
      44             : {
      45    63131409 :   return x.function() == core::detail::function_symbols::SortStruct;
      46             : }
      47             : 
      48             : /// \brief Returns true if the term t is the unknown sort
      49    22437811 : inline bool is_untyped_sort(const atermpp::aterm_appl& x)
      50             : {
      51    22437811 :   return x.function() == core::detail::function_symbols::UntypedSortUnknown;
      52             : }
      53             : 
      54             : /// \brief Returns true if the term t is an expression for multiple possible sorts
      55      565773 : inline bool is_untyped_possible_sorts(const atermpp::aterm_appl& x)
      56             : {
      57      565773 :   return x.function() == core::detail::function_symbols::UntypedSortsPossible;
      58             : }
      59             : 
      60             : //--- start generated class sort_expression ---//
      61             : /// \\brief A sort expression
      62             : class sort_expression: public atermpp::aterm_appl
      63             : {
      64             :   public:
      65             :     /// \\brief Default constructor.
      66     2386253 :     sort_expression()
      67     2386253 :       : atermpp::aterm_appl(core::detail::default_values::SortExpr)
      68     2386253 :     {}
      69             : 
      70             :     /// \\brief Constructor.
      71             :     /// \\param term A term
      72   159731467 :     explicit sort_expression(const atermpp::aterm& term)
      73   159731467 :       : atermpp::aterm_appl(term)
      74             :     {
      75   159731467 :       assert(core::detail::check_rule_SortExpr(*this));
      76   159731467 :     }
      77             : 
      78             :     /// Move semantics
      79   101005733 :     sort_expression(const sort_expression&) noexcept = default;
      80    96384610 :     sort_expression(sort_expression&&) noexcept = default;
      81     1461325 :     sort_expression& operator=(const sort_expression&) noexcept = default;
      82    44136387 :     sort_expression& operator=(sort_expression&&) noexcept = default;
      83             : //--- start user section sort_expression ---//
      84             :     /// \brief Returns the target sort of this expression.
      85             :     /// \return For a function sort D->E, return the target sort of E. Otherwise return this sort.
      86             :     inline
      87       11303 :     const sort_expression& target_sort() const
      88             :     {
      89       11303 :       if (is_function_sort(*this))
      90             :       {
      91        6647 :         return atermpp::down_cast<const sort_expression>((*this)[1]);
      92             :       }
      93             :       else
      94             :       {
      95        4656 :         return *this;
      96             :       }
      97             :     }
      98             : //--- end user section sort_expression ---//
      99             : };
     100             : 
     101             : /// \\brief list of sort_expressions
     102             : typedef atermpp::term_list<sort_expression> sort_expression_list;
     103             : 
     104             : /// \\brief vector of sort_expressions
     105             : typedef std::vector<sort_expression>    sort_expression_vector;
     106             : 
     107             : // prototype declaration
     108             : std::string pp(const sort_expression& x);
     109             : 
     110             : /// \\brief Outputs the object to a stream
     111             : /// \\param out An output stream
     112             : /// \\param x Object x
     113             : /// \\return The output stream
     114             : inline
     115        2675 : std::ostream& operator<<(std::ostream& out, const sort_expression& x)
     116             : {
     117        2675 :   return out << data::pp(x);
     118             : }
     119             : 
     120             : /// \\brief swap overload
     121             : inline void swap(sort_expression& t1, sort_expression& t2)
     122             : {
     123             :   t1.swap(t2);
     124             : }
     125             : //--- end generated class sort_expression ---//
     126             : 
     127             : /// \brief Test for a sort_expression expression
     128             : /// \param x A term
     129             : /// \return True if it is a sort_expression expression
     130             : inline
     131             : bool is_sort_expression(const atermpp::aterm_appl& x)
     132             : {
     133             :   return is_basic_sort(x)             ||
     134             :          is_function_sort(x)          ||
     135             :          is_container_sort(x)         ||
     136             :          is_structured_sort(x)        ||
     137             :          is_untyped_sort(x)           ||
     138             :          is_untyped_possible_sorts(x);
     139             : }
     140             : 
     141             : // template function overloads
     142             : std::string pp(const sort_expression_list& x);
     143             : std::string pp(const sort_expression_vector& x);
     144             : std::set<data::sort_expression> find_sort_expressions(const data::sort_expression& x);
     145             : 
     146             : } // namespace data
     147             : 
     148             : } // namespace mcrl2
     149             : 
     150             : namespace std
     151             : {
     152             : 
     153             : template <>
     154             : struct hash<mcrl2::data::sort_expression>
     155             : {
     156    19763890 :   std::size_t operator()(const mcrl2::data::sort_expression& x) const
     157             :   {
     158    19763890 :     return hash<atermpp::aterm>()(x);
     159             :   }
     160             : };
     161             : 
     162             : } // namespace std
     163             : 
     164             : #endif // MCRL2_DATA_SORT_EXPRESSION_H
     165             :