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 pbes/include/mcrl2/pbes/rewrite.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_REWRITE_H
13 : #define MCRL2_PBES_REWRITE_H
14 :
15 : #include "mcrl2/data/rewrite.h"
16 : #include "mcrl2/pbes/builder.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace pbes_system {
21 :
22 : namespace detail
23 : {
24 :
25 : template <template <class> class Builder, class Rewriter>
26 : struct rewrite_pbes_expressions_builder: public Builder<rewrite_pbes_expressions_builder<Builder, Rewriter> >
27 : {
28 : typedef Builder<rewrite_pbes_expressions_builder<Builder, Rewriter> > super;
29 : using super::apply;
30 : using super::update;
31 :
32 : const Rewriter& R;
33 :
34 94 : rewrite_pbes_expressions_builder(const Rewriter& R_)
35 94 : : R(R_)
36 94 : {}
37 :
38 : template <class T>
39 203 : void apply(T& result, const pbes_expression& x)
40 : {
41 203 : result = R(x);
42 203 : }
43 :
44 94 : void update(pbes_system::pbes& x)
45 : {
46 94 : super::update(x);
47 : // Handle the initial state. It is skipped by the builder because the type is not pbes_expression
48 94 : pbes_expression initial_state;
49 94 : apply(initial_state, static_cast<pbes_expression>(x.initial_state()));
50 94 : x.initial_state() = atermpp::down_cast<propositional_variable_instantiation>(initial_state);
51 94 : }
52 : };
53 :
54 : template <template <class> class Builder, class Rewriter>
55 : rewrite_pbes_expressions_builder<Builder, Rewriter>
56 94 : make_rewrite_pbes_expressions_builder(const Rewriter& R)
57 : {
58 94 : return rewrite_pbes_expressions_builder<Builder, Rewriter>(R);
59 : }
60 :
61 : template <template <class> class Builder, class Rewriter, class Substitution>
62 : struct rewrite_pbes_expressions_with_substitution_builder: public Builder<rewrite_pbes_expressions_with_substitution_builder<Builder, Rewriter, Substitution> >
63 : {
64 : typedef Builder<rewrite_pbes_expressions_with_substitution_builder<Builder, Rewriter, Substitution> > super;
65 : using super::apply;
66 :
67 : const Rewriter& R;
68 : Substitution& sigma;
69 :
70 : rewrite_pbes_expressions_with_substitution_builder(const Rewriter& R_, Substitution& sigma_)
71 : : R(R_),
72 : sigma(sigma_)
73 : {}
74 :
75 : template <class T>
76 : void apply(T& result, const pbes_expression& x)
77 : {
78 : result = R(x, sigma);
79 : }
80 : };
81 :
82 : template <template <class> class Builder, class Rewriter, class Substitution>
83 : rewrite_pbes_expressions_with_substitution_builder<Builder, Rewriter, Substitution>
84 : make_rewrite_pbes_expressions_with_substitution_builder(const Rewriter& R, Substitution sigma)
85 : {
86 : return rewrite_pbes_expressions_with_substitution_builder<Builder, Rewriter, Substitution>(R, sigma);
87 : }
88 : /// \endcond
89 :
90 : } // namespace detail
91 :
92 : //--- start generated pbes_system rewrite code ---//
93 : /// \\brief Rewrites all embedded expressions in an object x
94 : /// \\param x an object containing expressions
95 : /// \\param R a rewriter
96 : template <typename T, typename Rewriter>
97 : void rewrite(T& x,
98 : Rewriter R,
99 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
100 : )
101 : {
102 : data::detail::make_rewrite_data_expressions_builder<pbes_system::data_expression_builder>(R).update(x);
103 : }
104 :
105 : /// \\brief Rewrites all embedded expressions in an object x
106 : /// \\param x an object containing expressions
107 : /// \\param R a rewriter
108 : /// \\return the rewrite result
109 : template <typename T, typename Rewriter>
110 : T rewrite(const T& x,
111 : Rewriter R,
112 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
113 : )
114 : {
115 : T result;
116 : data::detail::make_rewrite_data_expressions_builder<pbes_system::data_expression_builder>(R).apply(result, x);
117 : return result;
118 : }
119 :
120 : /// \\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly
121 : /// \\param x an object containing expressions
122 : /// \\param R a rewriter
123 : /// \\param sigma a substitution
124 : template <typename T, typename Rewriter, typename Substitution>
125 : void rewrite(T& x,
126 : Rewriter R,
127 : const Substitution& sigma,
128 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
129 : )
130 : {
131 : data::detail::make_rewrite_data_expressions_with_substitution_builder<pbes_system::data_expression_builder>(R, sigma).update(x);
132 : }
133 :
134 : /// \\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly
135 : /// \\param x an object containing expressions
136 : /// \\param R a rewriter
137 : /// \\param sigma a substitution
138 : /// \\return the rewrite result
139 : template <typename T, typename Rewriter, typename Substitution>
140 : T rewrite(const T& x,
141 : Rewriter R,
142 : const Substitution& sigma,
143 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
144 : )
145 : {
146 : T result;
147 : data::detail::make_rewrite_data_expressions_with_substitution_builder<pbes_system::data_expression_builder>(R, sigma).apply(result, x);
148 : return result;
149 : }
150 : //--- end generated pbes_system rewrite code ---//
151 :
152 : /// \brief Rewrites all embedded pbes expressions in an object x
153 : /// \param x an object containing expressions
154 : /// \param R a pbes rewriter
155 : template <typename T, typename Rewriter>
156 94 : void pbes_rewrite(T& x,
157 : const Rewriter& R,
158 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
159 : )
160 : {
161 94 : pbes_system::detail::make_rewrite_pbes_expressions_builder<pbes_system::pbes_expression_builder>(R).update(x);
162 94 : }
163 :
164 : /// \brief Rewrites all embedded pbes expressions in an object x
165 : /// \param x an object containing expressions
166 : /// \param R a pbes rewriter
167 : /// \return the rewrite result
168 : template <typename T, typename Rewriter>
169 : T pbes_rewrite(const T& x,
170 : const Rewriter& R,
171 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = 0
172 : )
173 : {
174 : T result;
175 : pbes_system::detail::make_rewrite_pbes_expressions_builder<pbes_system::pbes_expression_builder>(R).apply(result, x);
176 : return result;
177 : }
178 :
179 : /// \brief Rewrites all embedded pbes expressions in an object x, and applies a substitution to variables on the fly
180 : /// \param x an object containing expressions
181 : /// \param R a pbes rewriter
182 : /// \param sigma a substitution
183 : template <typename T, typename Rewriter, typename Substitution>
184 : void pbes_rewrite(T& x,
185 : const Rewriter& R,
186 : Substitution sigma,
187 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
188 : )
189 : {
190 : pbes_system::detail::make_rewrite_pbes_expressions_with_substitution_builder<pbes_system::pbes_expression_builder>(R, sigma).update(x);
191 : }
192 :
193 : /// \brief Rewrites all embedded pbes expressions in an object x, and applies a substitution to variables on the fly
194 : /// \param x an object containing expressions
195 : /// \param R a pbes rewriter
196 : /// \param sigma a substitution
197 : /// \return the rewrite result
198 : template <typename T, typename Rewriter, typename Substitution>
199 : T pbes_rewrite(const T& x,
200 : const Rewriter& R,
201 : Substitution sigma,
202 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = 0
203 : )
204 : {
205 : T result;
206 : pbes_system::detail::make_rewrite_pbes_expressions_with_substitution_builder<pbes_system::pbes_expression_builder>(R, sigma).apply(result, x);
207 : return result;
208 : }
209 :
210 : } // namespace pbes_system
211 :
212 : } // namespace mcrl2
213 :
214 : #endif // MCRL2_PBES_REWRITE_H
|
