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/replace.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_REPLACE_H
13 : #define MCRL2_DATA_REPLACE_H
14 :
15 : #include "mcrl2/data/is_simple_substitution.h"
16 : #include "mcrl2/data/replace_capture_avoiding.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace data
22 : {
23 :
24 : namespace detail
25 : {
26 :
27 : /// \cond INTERNAL_DOCS
28 : template <template <class> class Builder, class Substitution>
29 : struct replace_sort_expressions_builder: public Builder<replace_sort_expressions_builder<Builder, Substitution> >
30 : {
31 : typedef Builder<replace_sort_expressions_builder<Builder, Substitution> > super;
32 : using super::enter;
33 : using super::leave;
34 : using super::apply;
35 : using super::update;
36 :
37 : const Substitution& sigma;
38 : bool innermost;
39 :
40 7129 : replace_sort_expressions_builder(const Substitution& sigma_, bool innermost_)
41 7129 : : sigma(sigma_),
42 7129 : innermost(innermost_)
43 7129 : {}
44 :
45 : template <class T>
46 14266 : void apply(T& result, const sort_expression& x)
47 : {
48 14266 : if (innermost)
49 : {
50 14265 : super::apply(result, x);
51 14265 : result = sigma(result);
52 14265 : return;
53 : }
54 1 : result = sigma(x);
55 1 : return;
56 : }
57 : };
58 :
59 : template <template <class> class Builder, class Substitution>
60 : replace_sort_expressions_builder<Builder, Substitution>
61 7129 : make_replace_sort_expressions_builder(const Substitution& sigma, bool innermost)
62 : {
63 7129 : return replace_sort_expressions_builder<Builder, Substitution>(sigma, innermost);
64 : }
65 :
66 : template <template <class> class Builder, class Substitution>
67 : struct replace_data_expressions_builder: public Builder<replace_data_expressions_builder<Builder, Substitution> >
68 : {
69 : typedef Builder<replace_data_expressions_builder<Builder, Substitution> > super;
70 : using super::enter;
71 : using super::leave;
72 : using super::apply;
73 : using super::update;
74 :
75 : Substitution sigma;
76 : bool innermost;
77 :
78 0 : replace_data_expressions_builder(Substitution sigma_, bool innermost_)
79 0 : : sigma(sigma_),
80 0 : innermost(innermost_)
81 0 : {}
82 :
83 : template <class T>
84 0 : void apply(T& result, const data_expression& x)
85 : {
86 0 : if (innermost)
87 : {
88 0 : data_expression y;
89 0 : super::apply(y, x);
90 0 : result = sigma(y);
91 0 : return;
92 0 : }
93 0 : result = sigma(x);
94 : }
95 : };
96 :
97 : template <template <class> class Builder, class Substitution>
98 : replace_data_expressions_builder<Builder, Substitution>
99 0 : make_replace_data_expressions_builder(const Substitution& sigma, bool innermost)
100 : {
101 0 : return replace_data_expressions_builder<Builder, Substitution>(sigma, innermost);
102 : }
103 :
104 : template <template <class> class Builder, template <template <class> class, class> class Binder, class Substitution>
105 : struct replace_free_variables_builder: public Binder<Builder, replace_free_variables_builder<Builder, Binder, Substitution> >
106 : {
107 : typedef Binder<Builder, replace_free_variables_builder<Builder, Binder, Substitution> > super;
108 : using super::enter;
109 : using super::leave;
110 : using super::apply;
111 : using super::update;
112 : using super::is_bound;
113 : using super::bound_variables;
114 : using super::increase_bind_count;
115 :
116 : const Substitution& sigma;
117 :
118 539 : explicit replace_free_variables_builder(const Substitution& sigma_)
119 539 : : sigma(sigma_)
120 539 : {}
121 :
122 : template <typename VariableContainer>
123 : replace_free_variables_builder(const Substitution& sigma_, const VariableContainer& bound_variables)
124 : : sigma(sigma_)
125 : {
126 : increase_bind_count(bound_variables);
127 : }
128 :
129 : template <class T>
130 3917 : void apply(T& result, const variable& v)
131 : {
132 3917 : if (is_bound(v))
133 : {
134 2669 : result = v;
135 2669 : return;
136 : }
137 1248 : result = sigma(v);
138 : }
139 : };
140 :
141 : template <template <class> class Builder, template <template <class> class, class> class Binder, class Substitution>
142 : replace_free_variables_builder<Builder, Binder, Substitution>
143 539 : make_replace_free_variables_builder(const Substitution& sigma)
144 : {
145 539 : return replace_free_variables_builder<Builder, Binder, Substitution>(sigma);
146 : }
147 :
148 : template <template <class> class Builder, template <template <class> class, class> class Binder, class Substitution, class VariableContainer>
149 : replace_free_variables_builder<Builder, Binder, Substitution>
150 : make_replace_free_variables_builder(const Substitution& sigma, const VariableContainer& bound_variables)
151 : {
152 : return replace_free_variables_builder<Builder, Binder, Substitution>(sigma, bound_variables);
153 : }
154 :
155 : /// \endcond
156 :
157 : } // namespace detail
158 :
159 : /// \brief Returns the variables appearing in the right hand sides of the substitution.
160 : template <typename Substitution>
161 : std::set<data::variable> substitution_variables(const Substitution& /* sigma */)
162 : {
163 : throw mcrl2::runtime_error("substitution_variables is undefined!");
164 : }
165 :
166 : //--- start generated data replace code ---//
167 : template <typename T, typename Substitution>
168 : void replace_sort_expressions(T& x,
169 : const Substitution& sigma,
170 : bool innermost,
171 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
172 : )
173 : {
174 : data::detail::make_replace_sort_expressions_builder<data::sort_expression_builder>(sigma, innermost).update(x);
175 : }
176 :
177 : template <typename T, typename Substitution>
178 7129 : T replace_sort_expressions(const T& x,
179 : const Substitution& sigma,
180 : bool innermost,
181 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
182 : )
183 : {
184 7129 : T result;
185 7129 : data::detail::make_replace_sort_expressions_builder<data::sort_expression_builder>(sigma, innermost).apply(result, x);
186 7129 : return result;
187 0 : }
188 :
189 : template <typename T, typename Substitution>
190 : void replace_data_expressions(T& x,
191 : const Substitution& sigma,
192 : bool innermost,
193 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
194 : )
195 : {
196 : data::detail::make_replace_data_expressions_builder<data::data_expression_builder>(sigma, innermost).update(x);
197 : }
198 :
199 : template <typename T, typename Substitution>
200 0 : T replace_data_expressions(const T& x,
201 : const Substitution& sigma,
202 : bool innermost,
203 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
204 : )
205 : {
206 0 : T result;
207 0 : data::detail::make_replace_data_expressions_builder<data::data_expression_builder>(sigma, innermost).apply(result, x);
208 0 : return result;
209 0 : }
210 :
211 :
212 : template <typename T, typename Substitution>
213 : void replace_variables(T& x,
214 : const Substitution& sigma,
215 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
216 : )
217 : {
218 : core::make_update_apply_builder<data::data_expression_builder>(sigma).update(x);
219 : }
220 :
221 : template <typename T, typename Substitution>
222 12378 : T replace_variables(const T& x,
223 : const Substitution& sigma,
224 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
225 : )
226 : {
227 12378 : T result;
228 12378 : core::make_update_apply_builder<data::data_expression_builder>(sigma).apply(result, x);
229 12378 : return result;
230 0 : }
231 :
232 : template <typename T, typename Substitution>
233 : void replace_all_variables(T& x,
234 : const Substitution& sigma,
235 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
236 : )
237 : {
238 : core::make_update_apply_builder<data::variable_builder>(sigma).update(x);
239 : }
240 :
241 : template <typename T, typename Substitution>
242 0 : T replace_all_variables(const T& x,
243 : const Substitution& sigma,
244 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
245 : )
246 : {
247 0 : T result;
248 0 : core::make_update_apply_builder<data::variable_builder>(sigma).apply(result, x);
249 0 : return result;
250 0 : }
251 :
252 : /// \\brief Applies the substitution sigma to x.
253 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
254 : template <typename T, typename Substitution>
255 : void replace_free_variables(T& x,
256 : const Substitution& sigma,
257 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
258 : )
259 : {
260 : assert(data::is_simple_substitution(sigma));
261 : data::detail::make_replace_free_variables_builder<data::data_expression_builder, data::add_data_variable_builder_binding>(sigma).update(x);
262 : }
263 :
264 : /// \\brief Applies the substitution sigma to x.
265 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
266 : template <typename T, typename Substitution>
267 105 : T replace_free_variables(const T& x,
268 : const Substitution& sigma,
269 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
270 : )
271 : {
272 105 : assert(data::is_simple_substitution(sigma));
273 105 : T result;
274 105 : data::detail::make_replace_free_variables_builder<data::data_expression_builder, data::add_data_variable_builder_binding>(sigma).apply(result, x);
275 105 : return result;
276 0 : }
277 :
278 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
279 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
280 : template <typename T, typename Substitution, typename VariableContainer>
281 : void replace_free_variables(T& x,
282 : const Substitution& sigma,
283 : const VariableContainer& bound_variables,
284 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
285 : )
286 : {
287 : assert(data::is_simple_substitution(sigma));
288 : data::detail::make_replace_free_variables_builder<data::data_expression_builder, data::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
289 : }
290 :
291 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
292 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
293 : template <typename T, typename Substitution, typename VariableContainer>
294 : T replace_free_variables(const T& x,
295 : const Substitution& sigma,
296 : const VariableContainer& bound_variables,
297 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
298 : )
299 : {
300 : assert(data::is_simple_substitution(sigma));
301 : T result;
302 : data::detail::make_replace_free_variables_builder<data::data_expression_builder, data::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
303 : return result;
304 : }
305 : //--- end generated data replace code ---//
306 :
307 : template <typename T, typename Substitution>
308 : void substitute_sorts(T& x,
309 : const Substitution& sigma,
310 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type* = 0
311 : )
312 : {
313 : core::make_update_apply_builder<data::sort_expression_builder>(sigma).update(x);
314 : }
315 :
316 : template <typename T, typename Substitution>
317 : T substitute_sorts(const T& x,
318 : const Substitution& sigma,
319 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type* = 0
320 : )
321 : {
322 : T result;
323 : core::make_update_apply_builder<data::sort_expression_builder>(sigma).apply(result, x);
324 : return result;
325 : }
326 :
327 : } // namespace data
328 :
329 : } // namespace mcrl2
330 :
331 : #endif // MCRL2_DATA_REPLACE_H
|
