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/assignment.h
      10             : /// \brief The class assignment.
      11             : 
      12             : #ifndef MCRL2_DATA_ASSIGNMENT_H
      13             : #define MCRL2_DATA_ASSIGNMENT_H
      14             : 
      15             : #include "mcrl2/data/undefined.h"
      16             : #include "mcrl2/data/untyped_identifier.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace data
      22             : {
      23             : 
      24             : //--- start generated classes ---//
      25             : /// \\brief Assignment expression
      26             : class assignment_expression: public atermpp::aterm_appl
      27             : {
      28             :   public:
      29             :     /// \\brief Default constructor.
      30           0 :     assignment_expression()
      31           0 :       : atermpp::aterm_appl(core::detail::default_values::WhrDecl)
      32           0 :     {}
      33             : 
      34             :     /// \\brief Constructor.
      35             :     /// \\param term A term
      36       29068 :     explicit assignment_expression(const atermpp::aterm& term)
      37       29068 :       : atermpp::aterm_appl(term)
      38             :     {
      39       29068 :       assert(core::detail::check_rule_WhrDecl(*this));
      40       29068 :     }
      41             : 
      42             :     /// Move semantics
      43        3116 :     assignment_expression(const assignment_expression&) noexcept = default;
      44       14262 :     assignment_expression(assignment_expression&&) noexcept = default;
      45         148 :     assignment_expression& operator=(const assignment_expression&) noexcept = default;
      46           9 :     assignment_expression& operator=(assignment_expression&&) noexcept = default;
      47             : };
      48             : 
      49             : /// \\brief list of assignment_expressions
      50             : typedef atermpp::term_list<assignment_expression> assignment_expression_list;
      51             : 
      52             : /// \\brief vector of assignment_expressions
      53             : typedef std::vector<assignment_expression>    assignment_expression_vector;
      54             : 
      55             : // prototypes
      56             : inline bool is_assignment(const atermpp::aterm_appl& x);
      57             : inline bool is_untyped_identifier_assignment(const atermpp::aterm_appl& x);
      58             : 
      59             : /// \\brief Test for a assignment_expression expression
      60             : /// \\param x A term
      61             : /// \\return True if \\a x is a assignment_expression expression
      62             : inline
      63             : bool is_assignment_expression(const atermpp::aterm_appl& x)
      64             : {
      65             :   return data::is_assignment(x) ||
      66             :          data::is_untyped_identifier_assignment(x);
      67             : }
      68             : 
      69             : // prototype declaration
      70             : std::string pp(const assignment_expression& x);
      71             : 
      72             : /// \\brief Outputs the object to a stream
      73             : /// \\param out An output stream
      74             : /// \\param x Object x
      75             : /// \\return The output stream
      76             : inline
      77             : std::ostream& operator<<(std::ostream& out, const assignment_expression& x)
      78             : {
      79             :   return out << data::pp(x);
      80             : }
      81             : 
      82             : /// \\brief swap overload
      83             : inline void swap(assignment_expression& t1, assignment_expression& t2)
      84             : {
      85             :   t1.swap(t2);
      86             : }
      87             : 
      88             : 
      89             : /// \\brief Assignment of a data expression to a variable
      90             : class assignment: public assignment_expression
      91             : {
      92             :   public:
      93             :     /// \\brief Default constructor.
      94           5 :     assignment()
      95           5 :       : assignment_expression(core::detail::default_values::DataVarIdInit)
      96           5 :     {}
      97             : 
      98             :     /// \\brief Constructor.
      99             :     /// \\param term A term
     100         500 :     explicit assignment(const atermpp::aterm& term)
     101         500 :       : assignment_expression(term)
     102             :     {
     103         500 :       assert(core::detail::check_term_DataVarIdInit(*this));
     104         500 :     }
     105             : 
     106             :     /// \\brief Constructor.
     107       27383 :     assignment(const variable& lhs, const data_expression& rhs)
     108       27383 :       : assignment_expression(atermpp::aterm_appl(core::detail::function_symbol_DataVarIdInit(), lhs, rhs))
     109       27383 :     {}
     110             : 
     111             :     /// Move semantics
     112        3060 :     assignment(const assignment&) noexcept = default;
     113       12377 :     assignment(assignment&&) noexcept = default;
     114           0 :     assignment& operator=(const assignment&) noexcept = default;
     115           9 :     assignment& operator=(assignment&&) noexcept = default;
     116             : 
     117      214502 :     const variable& lhs() const
     118             :     {
     119      214502 :       return atermpp::down_cast<variable>((*this)[0]);
     120             :     }
     121             : 
     122      222059 :     const data_expression& rhs() const
     123             :     {
     124      222059 :       return atermpp::down_cast<data_expression>((*this)[1]);
     125             :     }
     126             : //--- start user section assignment ---//
     127             :     /// \brief Applies the assignment to a variable
     128             :     /// \param[in] x A variable
     129             :     /// \return The value <tt>x[lhs() := rhs()]</tt>.
     130             :     const data_expression& operator()(const variable& x) const
     131             :     {
     132             :       return x == lhs() ? rhs() : x;
     133             :     }
     134             : //--- end user section assignment ---//
     135             : };
     136             : 
     137             : /// \\brief Make_assignment constructs a new term into a given address.
     138             : /// \\ \param t The reference into which the new assignment is constructed. 
     139             : template <class... ARGUMENTS>
     140       29903 : inline void make_assignment(atermpp::aterm_appl& t, const ARGUMENTS&... args)
     141             : {
     142       29903 :   atermpp::make_term_appl(t, core::detail::function_symbol_DataVarIdInit(), args...);
     143       29903 : }
     144             : 
     145             : /// \\brief list of assignments
     146             : typedef atermpp::term_list<assignment> assignment_list;
     147             : 
     148             : /// \\brief vector of assignments
     149             : typedef std::vector<assignment>    assignment_vector;
     150             : 
     151             : /// \\brief Test for a assignment expression
     152             : /// \\param x A term
     153             : /// \\return True if \\a x is a assignment expression
     154             : inline
     155        1262 : bool is_assignment(const atermpp::aterm_appl& x)
     156             : {
     157        1262 :   return x.function() == core::detail::function_symbols::DataVarIdInit;
     158             : }
     159             : 
     160             : // prototype declaration
     161             : std::string pp(const assignment& x);
     162             : 
     163             : /// \\brief Outputs the object to a stream
     164             : /// \\param out An output stream
     165             : /// \\param x Object x
     166             : /// \\return The output stream
     167             : inline
     168           0 : std::ostream& operator<<(std::ostream& out, const assignment& x)
     169             : {
     170           0 :   return out << data::pp(x);
     171             : }
     172             : 
     173             : /// \\brief swap overload
     174             : inline void swap(assignment& t1, assignment& t2)
     175             : {
     176             :   t1.swap(t2);
     177             : }
     178             : 
     179             : 
     180             : /// \\brief Assignment of a data expression to a string
     181             : class untyped_identifier_assignment: public assignment_expression
     182             : {
     183             :   public:
     184             :     /// \\brief Default constructor.
     185           0 :     untyped_identifier_assignment()
     186           0 :       : assignment_expression(core::detail::default_values::UntypedIdentifierAssignment)
     187           0 :     {}
     188             : 
     189             :     /// \\brief Constructor.
     190             :     /// \\param term A term
     191         160 :     explicit untyped_identifier_assignment(const atermpp::aterm& term)
     192         160 :       : assignment_expression(term)
     193             :     {
     194         160 :       assert(core::detail::check_term_UntypedIdentifierAssignment(*this));
     195         160 :     }
     196             : 
     197             :     /// \\brief Constructor.
     198        1020 :     untyped_identifier_assignment(const core::identifier_string& lhs, const data_expression& rhs)
     199        1020 :       : assignment_expression(atermpp::aterm_appl(core::detail::function_symbol_UntypedIdentifierAssignment(), lhs, rhs))
     200        1020 :     {}
     201             : 
     202             :     /// \\brief Constructor.
     203             :     untyped_identifier_assignment(const std::string& lhs, const data_expression& rhs)
     204             :       : assignment_expression(atermpp::aterm_appl(core::detail::function_symbol_UntypedIdentifierAssignment(), core::identifier_string(lhs), rhs))
     205             :     {}
     206             : 
     207             :     /// Move semantics
     208           0 :     untyped_identifier_assignment(const untyped_identifier_assignment&) noexcept = default;
     209        1885 :     untyped_identifier_assignment(untyped_identifier_assignment&&) noexcept = default;
     210             :     untyped_identifier_assignment& operator=(const untyped_identifier_assignment&) noexcept = default;
     211             :     untyped_identifier_assignment& operator=(untyped_identifier_assignment&&) noexcept = default;
     212             : 
     213        8235 :     const core::identifier_string& lhs() const
     214             :     {
     215        8235 :       return atermpp::down_cast<core::identifier_string>((*this)[0]);
     216             :     }
     217             : 
     218        3047 :     const data_expression& rhs() const
     219             :     {
     220        3047 :       return atermpp::down_cast<data_expression>((*this)[1]);
     221             :     }
     222             : //--- start user section untyped_identifier_assignment ---//
     223             :     /// \brief Applies the assignment to a variable
     224             :     /// \param[in] x An identifier string
     225             :     /// \return The value <tt>x[lhs() := rhs()]</tt>.
     226             :     data_expression operator()(const untyped_identifier& x) const
     227             :     {
     228             :       return x == lhs() ? rhs() : data_expression(x);
     229             :     }
     230             : //--- end user section untyped_identifier_assignment ---//
     231             : };
     232             : 
     233             : /// \\brief Make_untyped_identifier_assignment constructs a new term into a given address.
     234             : /// \\ \param t The reference into which the new untyped_identifier_assignment is constructed. 
     235             : template <class... ARGUMENTS>
     236        1010 : inline void make_untyped_identifier_assignment(atermpp::aterm_appl& t, const ARGUMENTS&... args)
     237             : {
     238        1010 :   atermpp::make_term_appl(t, core::detail::function_symbol_UntypedIdentifierAssignment(), args...);
     239        1010 : }
     240             : 
     241             : /// \\brief list of untyped_identifier_assignments
     242             : typedef atermpp::term_list<untyped_identifier_assignment> untyped_identifier_assignment_list;
     243             : 
     244             : /// \\brief vector of untyped_identifier_assignments
     245             : typedef std::vector<untyped_identifier_assignment>    untyped_identifier_assignment_vector;
     246             : 
     247             : /// \\brief Test for a untyped_identifier_assignment expression
     248             : /// \\param x A term
     249             : /// \\return True if \\a x is a untyped_identifier_assignment expression
     250             : inline
     251         162 : bool is_untyped_identifier_assignment(const atermpp::aterm_appl& x)
     252             : {
     253         162 :   return x.function() == core::detail::function_symbols::UntypedIdentifierAssignment;
     254             : }
     255             : 
     256             : // prototype declaration
     257             : std::string pp(const untyped_identifier_assignment& x);
     258             : 
     259             : /// \\brief Outputs the object to a stream
     260             : /// \\param out An output stream
     261             : /// \\param x Object x
     262             : /// \\return The output stream
     263             : inline
     264           0 : std::ostream& operator<<(std::ostream& out, const untyped_identifier_assignment& x)
     265             : {
     266           0 :   return out << data::pp(x);
     267             : }
     268             : 
     269             : /// \\brief swap overload
     270             : inline void swap(untyped_identifier_assignment& t1, untyped_identifier_assignment& t2)
     271             : {
     272             :   t1.swap(t2);
     273             : }
     274             : //--- end generated classes ---//
     275             : 
     276             : /// \brief Constructs an assignment_list by pairwise combining a variable and expression
     277             : /// \param variables A sequence of data variables
     278             : /// \param expressions A sequence of data expressions
     279             : /// \return The corresponding assignment list.
     280             : template < typename VariableSequence, typename ExpressionSequence >
     281         443 : assignment_vector make_assignment_vector(VariableSequence const& variables, ExpressionSequence const& expressions)
     282             : {
     283         443 :   std::vector<assignment> result;
     284         443 :   typename ExpressionSequence::const_iterator j=expressions.begin();
     285        1212 :   for(typename VariableSequence::const_iterator i=variables.begin(); i!=variables.end(); ++i, ++j)
     286             :   {
     287         769 :     assert(j!=expressions.end());
     288         769 :     result.push_back(assignment(*i,*j));
     289             :   }
     290         443 :   assert(j==expressions.end());
     291         886 :   return result;
     292           0 : }
     293             : 
     294             : /// \brief Converts an iterator range to data_expression_list
     295             : /// \param variables A sequence of variables.
     296             : /// \param expressions A sequence of variables.
     297             : /// \pre length(variables) == length(expressions)
     298             : /// \note This function uses implementation details of the iterator type
     299             : /// and hence is sometimes efficient than copying all elements of the list.
     300             : template < typename VariableSequence, typename ExpressionSequence >
     301         442 : assignment_list make_assignment_list(const VariableSequence& variables, const ExpressionSequence& expressions)
     302             : {
     303         442 :   std::vector<assignment> result(make_assignment_vector(variables,expressions));
     304         884 :   return assignment_list(result.begin(),result.end());
     305         442 : }
     306             : 
     307             : /// \brief Returns the left hand sides of an assignment list
     308             : /// \param x An assignment list
     309             : inline
     310        1981 : variable_list left_hand_sides(const assignment_list& x)
     311             : {
     312        3969 :   return variable_list(x.begin(), x.end(), [](const assignment& a) { return a.lhs(); });
     313             : }
     314             : 
     315             : /// \brief Returns the right hand sides of an assignment list
     316             : /// \param x An assignment list
     317             : inline
     318           1 : data_expression_list right_hand_sides(const assignment_list& x)
     319             : {
     320           4 :   return data_expression_list(x.begin(), x.end(), [](const assignment& a) { return a.rhs(); });
     321             : }
     322             : 
     323             : // template function overloads
     324             : std::string pp(const assignment_list& x);
     325             : std::string pp(const assignment_vector& x);
     326             : 
     327             : } // namespace data
     328             : 
     329             : } // namespace mcrl2
     330             : 
     331             : #endif // MCRL2_DATA_ASSIGNMENT_H
     332             :