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 data/include/mcrl2/data/rewrite.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_REWRITE_H
13 : #define MCRL2_DATA_REWRITE_H
14 :
15 : #include "mcrl2/data/builder.h"
16 :
17 : namespace mcrl2 {
18 :
19 : namespace data {
20 :
21 : namespace detail
22 : {
23 :
24 : template <template <class> class Builder, class Rewriter>
25 : struct rewrite_data_expressions_builder: public Builder<rewrite_data_expressions_builder<Builder, Rewriter> >
26 : {
27 : typedef Builder<rewrite_data_expressions_builder<Builder, Rewriter> > super;
28 : using super::enter;
29 : using super::leave;
30 : using super::apply;
31 : using super::update;
32 :
33 : Rewriter R;
34 :
35 735 : rewrite_data_expressions_builder(Rewriter R_)
36 735 : : R(R_)
37 735 : {}
38 :
39 : template <class T>
40 1047 : void apply(T& result, const data_expression& x)
41 : {
42 1047 : result = R(x);
43 1047 : }
44 : };
45 :
46 : template <template <class> class Builder, class Rewriter>
47 : rewrite_data_expressions_builder<Builder, Rewriter>
48 735 : make_rewrite_data_expressions_builder(Rewriter R)
49 : {
50 735 : return rewrite_data_expressions_builder<Builder, Rewriter>(R);
51 : }
52 :
53 : template <template <class> class Builder, class Rewriter, class Substitution>
54 : struct rewrite_data_expressions_with_substitution_builder: public Builder<rewrite_data_expressions_with_substitution_builder<Builder, Rewriter, Substitution> >
55 : {
56 : typedef Builder<rewrite_data_expressions_with_substitution_builder<Builder, Rewriter, Substitution> > super;
57 : using super::enter;
58 : using super::leave;
59 : using super::apply;
60 : using super::update;
61 :
62 : Rewriter R;
63 : Substitution sigma;
64 :
65 742 : rewrite_data_expressions_with_substitution_builder(Rewriter R_, Substitution sigma_)
66 742 : : R(R_),
67 742 : sigma(sigma_)
68 742 : {}
69 :
70 : template <class T>
71 7414 : void apply(T& result, const data_expression& x)
72 : {
73 7414 : result = R(x, sigma);
74 7414 : }
75 : };
76 :
77 : template <template <class> class Builder, class Rewriter, class Substitution>
78 : rewrite_data_expressions_with_substitution_builder<Builder, Rewriter, Substitution>
79 742 : make_rewrite_data_expressions_with_substitution_builder(Rewriter R, Substitution sigma)
80 : {
81 742 : return rewrite_data_expressions_with_substitution_builder<Builder, Rewriter, Substitution>(R, sigma);
82 : }
83 :
84 : } // namespace detail
85 :
86 : //--- start generated data rewrite code ---//
87 : /// \\brief Rewrites all embedded expressions in an object x
88 : /// \\param x an object containing expressions
89 : /// \\param R a rewriter
90 : template <typename T, typename Rewriter>
91 : void rewrite(T& x,
92 : Rewriter R,
93 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
94 : )
95 : {
96 : data::detail::make_rewrite_data_expressions_builder<data::data_expression_builder>(R).update(x);
97 : }
98 :
99 : /// \\brief Rewrites all embedded expressions in an object x
100 : /// \\param x an object containing expressions
101 : /// \\param R a rewriter
102 : /// \\return the rewrite result
103 : template <typename T, typename Rewriter>
104 : T rewrite(const T& x,
105 : Rewriter R,
106 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
107 : )
108 : {
109 : T result;
110 : data::detail::make_rewrite_data_expressions_builder<data::data_expression_builder>(R).apply(result, x);
111 : return result;
112 : }
113 :
114 : /// \\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly
115 : /// \\param x an object containing expressions
116 : /// \\param R a rewriter
117 : /// \\param sigma a substitution
118 : template <typename T, typename Rewriter, typename Substitution>
119 : void rewrite(T& x,
120 : Rewriter R,
121 : const Substitution& sigma,
122 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
123 : )
124 : {
125 : data::detail::make_rewrite_data_expressions_with_substitution_builder<data::data_expression_builder>(R, sigma).update(x);
126 : }
127 :
128 : /// \\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly
129 : /// \\param x an object containing expressions
130 : /// \\param R a rewriter
131 : /// \\param sigma a substitution
132 : /// \\return the rewrite result
133 : template <typename T, typename Rewriter, typename Substitution>
134 : T rewrite(const T& x,
135 : Rewriter R,
136 : const Substitution& sigma,
137 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
138 : )
139 : {
140 : T result;
141 : data::detail::make_rewrite_data_expressions_with_substitution_builder<data::data_expression_builder>(R, sigma).apply(result, x);
142 : return result;
143 : }
144 : //--- end generated data rewrite code ---//
145 :
146 : } // namespace data
147 :
148 : } // namespace mcrl2
149 :
150 : #endif // MCRL2_DATA_REWRITE_H
|