Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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/substitutions/sequence_sequence_substitution.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_SUBSTITUTIONS_SEQUENCE_SEQUENCE_SUBSTITUTION_H
      13             : #define MCRL2_DATA_SUBSTITUTIONS_SEQUENCE_SEQUENCE_SUBSTITUTION_H
      14             : 
      15             : #include "mcrl2/data/is_simple_substitution.h"
      16             : #include "mcrl2/data/undefined.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace data {
      21             : 
      22             : /// \brief Generic substitution function. The substitution is stored as a sequence
      23             : /// of variables and a sequence of expressions.
      24             : template <typename VariableContainer, typename ExpressionContainer>
      25             : struct sequence_sequence_substitution
      26             : {
      27             :   /// \brief type used to represent variables
      28             :   typedef typename VariableContainer::value_type variable_type;
      29             : 
      30             :   /// \brief type used to represent expressions
      31             :   typedef typename ExpressionContainer::value_type  expression_type;
      32             : 
      33             :   using argument_type = variable_type;
      34             :   using result_type = expression_type;
      35             : 
      36             :   const VariableContainer& variables;
      37             :   const ExpressionContainer& expressions;
      38             : 
      39           5 :   sequence_sequence_substitution(const VariableContainer& variables_, const ExpressionContainer& expressions_)
      40           5 :     : variables(variables_),
      41           5 :       expressions(expressions_)
      42             :   {
      43           5 :     assert(variables.size() == expressions.size());
      44           5 :   }
      45             : 
      46          20 :   expression_type operator()(const variable_type& v) const
      47             :   {
      48          20 :     typename VariableContainer::const_iterator i = variables.begin();
      49          20 :     typename ExpressionContainer::const_iterator j = expressions.begin();
      50             : 
      51          40 :     for (; i != variables.end(); ++i, ++j)
      52             :     {
      53          40 :       if (*i == v)
      54             :       {
      55          20 :         return *j;
      56             :       }
      57             :     }
      58           0 :     return expression_type(v);
      59             :   }
      60             : 
      61           0 :   std::string to_string() const
      62             :   {
      63           0 :     std::ostringstream out;
      64           0 :     out << "[";
      65           0 :     typename VariableContainer::const_iterator i = variables.begin();
      66           0 :     typename ExpressionContainer::const_iterator j = expressions.begin();
      67           0 :     for (; i != variables.end(); ++i, ++j)
      68             :     {
      69           0 :       out << (i == variables.begin() ? "" : "; ") << *i << " := " << *j;
      70             :     }
      71           0 :     out << "]";
      72           0 :     return out.str();
      73           0 :   }
      74             : };
      75             : 
      76             : /// \brief Utility function for creating a sequence_sequence_substitution.
      77             : template <typename VariableContainer, typename ExpressionContainer>
      78             : sequence_sequence_substitution<VariableContainer, ExpressionContainer>
      79           5 : make_sequence_sequence_substitution(const VariableContainer& vc, const ExpressionContainer& ec)
      80             : {
      81           5 :   return sequence_sequence_substitution<VariableContainer, ExpressionContainer>(vc, ec);
      82             : }
      83             : 
      84             : template <typename VariableContainer, typename ExpressionContainer>
      85           0 : std::ostream& operator<<(std::ostream& out, const sequence_sequence_substitution<VariableContainer, ExpressionContainer>& sigma)
      86             : {
      87           0 :   return out << sigma.to_string();
      88             : }
      89             : 
      90             : template <typename VariableContainer, typename ExpressionContainer>
      91             : bool is_simple_substitution(const sequence_sequence_substitution<VariableContainer, ExpressionContainer>& sigma)
      92             : {
      93             :   auto i = sigma.variables.begin();
      94             :   auto j = sigma.expressions.begin();
      95             :   for (i = sigma.variables.begin(); i != sigma.variables.end(); ++i, ++j)
      96             :   {
      97             :     if (!is_simple_substitution(*i, *j))
      98             :     {
      99             :       return false;
     100             :     }
     101             :   }
     102             :   return true;
     103             : }
     104             : 
     105             : } // namespace data
     106             : 
     107             : } // namespace mcrl2
     108             : 
     109             : #endif // MCRL2_DATA_SUBSTITUTIONS_SEQUENCE_SEQUENCE_SUBSTITUTION_H