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/lps/rewriters/one_point_rule_rewrite.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_ONE_POINT_RULE_REWRITE_H
      13             : #define MCRL2_LPS_ONE_POINT_RULE_REWRITE_H
      14             : 
      15             : #include "mcrl2/data/rewriters/one_point_rule_rewriter.h"
      16             : #include "mcrl2/lps/builder.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace lps {
      21             : 
      22             : namespace detail {
      23             : 
      24             : 
      25             : 
      26             : struct one_point_rule_rewrite_builder: public lps::data_expression_builder<one_point_rule_rewrite_builder>
      27             : {
      28             :   typedef lps::data_expression_builder<one_point_rule_rewrite_builder> super;
      29             :   using super::apply;
      30             :   using super::update;
      31             : 
      32             :   data::one_point_rule_rewriter r;
      33             : 
      34             :   template <class T>
      35           5 :   void apply(T& result, const data::data_expression& x)
      36             :   {
      37           5 :     result = r(x);
      38           5 :   }
      39             : };
      40             : 
      41             : } // namespace detail
      42             : 
      43             : /// \brief Applies the one point rule rewriter to all embedded data expressions in an object x
      44             : /// \param x an object containing data expressions
      45             : template <typename T>
      46           1 : void one_point_rule_rewrite(T& x, typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr)
      47             : {
      48             :   detail::one_point_rule_rewrite_builder f;
      49           1 :   f.update(x);
      50           1 : }
      51             : 
      52             : /// \brief Applies the one point rule rewriter to all embedded data expressions in an object x
      53             : /// \param x an object containing data expressions
      54             : /// \return the rewrite result
      55             : template <typename T>
      56             : T one_point_rule_rewrite(const T& x, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr)
      57             : {
      58             :   T result;
      59             :   detail::one_point_rule_rewrite_builder f;
      60             :   f.apply(result, x);
      61             :   return result;
      62             : }
      63             : 
      64             : } // namespace lps
      65             : 
      66             : } // namespace mcrl2
      67             : 
      68             : #endif // MCRL2_LPS_ONE_POINT_RULE_REWRITE_H