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/modal_formula/replace.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_REPLACE_H
13 : #define MCRL2_MODAL_FORMULA_REPLACE_H
14 :
15 : #include "mcrl2/lps/replace.h"
16 : #include "mcrl2/modal_formula/replace_capture_avoiding.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace action_formulas
22 : {
23 :
24 : //--- start generated action_formulas replace code ---//
25 : template <typename T, typename Substitution>
26 : void replace_sort_expressions(T& x,
27 : const Substitution& sigma,
28 : bool innermost,
29 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
30 : )
31 : {
32 : data::detail::make_replace_sort_expressions_builder<action_formulas::sort_expression_builder>(sigma, innermost).update(x);
33 : }
34 :
35 : template <typename T, typename Substitution>
36 : T replace_sort_expressions(const T& x,
37 : const Substitution& sigma,
38 : bool innermost,
39 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
40 : )
41 : {
42 : T result;
43 : data::detail::make_replace_sort_expressions_builder<action_formulas::sort_expression_builder>(sigma, innermost).apply(result, x);
44 : return result;
45 : }
46 :
47 : template <typename T, typename Substitution>
48 : void replace_data_expressions(T& x,
49 : const Substitution& sigma,
50 : bool innermost,
51 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
52 : )
53 : {
54 : data::detail::make_replace_data_expressions_builder<action_formulas::data_expression_builder>(sigma, innermost).update(x);
55 : }
56 :
57 : template <typename T, typename Substitution>
58 : T replace_data_expressions(const T& x,
59 : const Substitution& sigma,
60 : bool innermost,
61 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
62 : )
63 : {
64 : T result;
65 : data::detail::make_replace_data_expressions_builder<action_formulas::data_expression_builder>(sigma, innermost).apply(result, x);
66 : return result;
67 : }
68 :
69 :
70 : template <typename T, typename Substitution>
71 : void replace_variables(T& x,
72 : const Substitution& sigma,
73 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
74 : )
75 : {
76 : core::make_update_apply_builder<action_formulas::data_expression_builder>(sigma).update(x);
77 : }
78 :
79 : template <typename T, typename Substitution>
80 : T replace_variables(const T& x,
81 : const Substitution& sigma,
82 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
83 : )
84 : {
85 : T result;
86 : core::make_update_apply_builder<action_formulas::data_expression_builder>(sigma).apply(result, x);
87 : return result;
88 : }
89 :
90 : template <typename T, typename Substitution>
91 : void replace_all_variables(T& x,
92 : const Substitution& sigma,
93 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
94 : )
95 : {
96 : core::make_update_apply_builder<action_formulas::variable_builder>(sigma).update(x);
97 : }
98 :
99 : template <typename T, typename Substitution>
100 : T replace_all_variables(const T& x,
101 : const Substitution& sigma,
102 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
103 : )
104 : {
105 : T result;
106 : core::make_update_apply_builder<action_formulas::variable_builder>(sigma).apply(result, x);
107 : return result;
108 : }
109 :
110 : /// \\brief Applies the substitution sigma to x.
111 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
112 : template <typename T, typename Substitution>
113 : void replace_free_variables(T& x,
114 : const Substitution& sigma,
115 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
116 : )
117 : {
118 : assert(data::is_simple_substitution(sigma));
119 : data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).update(x);
120 : }
121 :
122 : /// \\brief Applies the substitution sigma to x.
123 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
124 : template <typename T, typename Substitution>
125 : T replace_free_variables(const T& x,
126 : const Substitution& sigma,
127 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
128 : )
129 : {
130 : assert(data::is_simple_substitution(sigma));
131 : T result;
132 : data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).apply(result, x);
133 : return result;
134 : }
135 :
136 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
137 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
138 : template <typename T, typename Substitution, typename VariableContainer>
139 : void replace_free_variables(T& x,
140 : const Substitution& sigma,
141 : const VariableContainer& bound_variables,
142 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
143 : )
144 : {
145 : assert(data::is_simple_substitution(sigma));
146 : data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
147 : }
148 :
149 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
150 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
151 : template <typename T, typename Substitution, typename VariableContainer>
152 : T replace_free_variables(const T& x,
153 : const Substitution& sigma,
154 : const VariableContainer& bound_variables,
155 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
156 : )
157 : {
158 : assert(data::is_simple_substitution(sigma));
159 : T result;
160 : data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
161 : return result;
162 : }
163 : //--- end generated action_formulas replace code ---//
164 :
165 : } // namespace action_formulas
166 :
167 : namespace regular_formulas
168 : {
169 :
170 : //--- start generated regular_formulas replace code ---//
171 : template <typename T, typename Substitution>
172 : void replace_sort_expressions(T& x,
173 : const Substitution& sigma,
174 : bool innermost,
175 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
176 : )
177 : {
178 : data::detail::make_replace_sort_expressions_builder<regular_formulas::sort_expression_builder>(sigma, innermost).update(x);
179 : }
180 :
181 : template <typename T, typename Substitution>
182 : T replace_sort_expressions(const T& x,
183 : const Substitution& sigma,
184 : bool innermost,
185 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
186 : )
187 : {
188 : T result;
189 : data::detail::make_replace_sort_expressions_builder<regular_formulas::sort_expression_builder>(sigma, innermost).apply(result, x);
190 : return result;
191 : }
192 :
193 : template <typename T, typename Substitution>
194 : void replace_data_expressions(T& x,
195 : const Substitution& sigma,
196 : bool innermost,
197 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
198 : )
199 : {
200 : data::detail::make_replace_data_expressions_builder<regular_formulas::data_expression_builder>(sigma, innermost).update(x);
201 : }
202 :
203 : template <typename T, typename Substitution>
204 : T replace_data_expressions(const T& x,
205 : const Substitution& sigma,
206 : bool innermost,
207 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
208 : )
209 : {
210 : T result;
211 : data::detail::make_replace_data_expressions_builder<regular_formulas::data_expression_builder>(sigma, innermost).apply(result, x);
212 : return result;
213 : }
214 :
215 :
216 : template <typename T, typename Substitution>
217 : void replace_variables(T& x,
218 : const Substitution& sigma,
219 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
220 : )
221 : {
222 : core::make_update_apply_builder<regular_formulas::data_expression_builder>(sigma).update(x);
223 : }
224 :
225 : template <typename T, typename Substitution>
226 : T replace_variables(const T& x,
227 : const Substitution& sigma,
228 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
229 : )
230 : {
231 : T result;
232 : core::make_update_apply_builder<regular_formulas::data_expression_builder>(sigma).apply(result, x);
233 : return result;
234 : }
235 :
236 : template <typename T, typename Substitution>
237 : void replace_all_variables(T& x,
238 : const Substitution& sigma,
239 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
240 : )
241 : {
242 : core::make_update_apply_builder<regular_formulas::variable_builder>(sigma).update(x);
243 : }
244 :
245 : template <typename T, typename Substitution>
246 : T replace_all_variables(const T& x,
247 : const Substitution& sigma,
248 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
249 : )
250 : {
251 : T result;
252 : core::make_update_apply_builder<regular_formulas::variable_builder>(sigma).apply(result, x);
253 : return result;
254 : }
255 :
256 : /// \\brief Applies the substitution sigma to x.
257 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
258 : template <typename T, typename Substitution>
259 : void replace_free_variables(T& x,
260 : const Substitution& sigma,
261 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
262 : )
263 : {
264 : assert(data::is_simple_substitution(sigma));
265 : data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).update(x);
266 : }
267 :
268 : /// \\brief Applies the substitution sigma to x.
269 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
270 : template <typename T, typename Substitution>
271 : T replace_free_variables(const T& x,
272 : const Substitution& sigma,
273 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
274 : )
275 : {
276 : assert(data::is_simple_substitution(sigma));
277 : T result;
278 : data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).apply(result, x);
279 : return result;
280 : }
281 :
282 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
283 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
284 : template <typename T, typename Substitution, typename VariableContainer>
285 : void replace_free_variables(T& x,
286 : const Substitution& sigma,
287 : const VariableContainer& bound_variables,
288 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
289 : )
290 : {
291 : assert(data::is_simple_substitution(sigma));
292 : data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
293 : }
294 :
295 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
296 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
297 : template <typename T, typename Substitution, typename VariableContainer>
298 : T replace_free_variables(const T& x,
299 : const Substitution& sigma,
300 : const VariableContainer& bound_variables,
301 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
302 : )
303 : {
304 : assert(data::is_simple_substitution(sigma));
305 : T result;
306 : data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
307 : return result;
308 : }
309 : //--- end generated regular_formulas replace code ---//
310 :
311 : } // namespace regular_formulas
312 :
313 : namespace state_formulas
314 : {
315 :
316 : //--- start generated state_formulas replace code ---//
317 : template <typename T, typename Substitution>
318 : void replace_sort_expressions(T& x,
319 : const Substitution& sigma,
320 : bool innermost,
321 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
322 : )
323 : {
324 : data::detail::make_replace_sort_expressions_builder<state_formulas::sort_expression_builder>(sigma, innermost).update(x);
325 : }
326 :
327 : template <typename T, typename Substitution>
328 : T replace_sort_expressions(const T& x,
329 : const Substitution& sigma,
330 : bool innermost,
331 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
332 : )
333 : {
334 : T result;
335 : data::detail::make_replace_sort_expressions_builder<state_formulas::sort_expression_builder>(sigma, innermost).apply(result, x);
336 : return result;
337 : }
338 :
339 : template <typename T, typename Substitution>
340 : void replace_data_expressions(T& x,
341 : const Substitution& sigma,
342 : bool innermost,
343 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
344 : )
345 : {
346 : data::detail::make_replace_data_expressions_builder<state_formulas::data_expression_builder>(sigma, innermost).update(x);
347 : }
348 :
349 : template <typename T, typename Substitution>
350 : T replace_data_expressions(const T& x,
351 : const Substitution& sigma,
352 : bool innermost,
353 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
354 : )
355 : {
356 : T result;
357 : data::detail::make_replace_data_expressions_builder<state_formulas::data_expression_builder>(sigma, innermost).apply(result, x);
358 : return result;
359 : }
360 :
361 :
362 : template <typename T, typename Substitution>
363 : void replace_variables(T& x,
364 : const Substitution& sigma,
365 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
366 : )
367 : {
368 : core::make_update_apply_builder<state_formulas::data_expression_builder>(sigma).update(x);
369 : }
370 :
371 : template <typename T, typename Substitution>
372 : T replace_variables(const T& x,
373 : const Substitution& sigma,
374 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
375 : )
376 : {
377 : T result;
378 : core::make_update_apply_builder<state_formulas::data_expression_builder>(sigma).apply(result, x);
379 : return result;
380 : }
381 :
382 : template <typename T, typename Substitution>
383 : void replace_all_variables(T& x,
384 : const Substitution& sigma,
385 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
386 : )
387 : {
388 : core::make_update_apply_builder<state_formulas::variable_builder>(sigma).update(x);
389 : }
390 :
391 : template <typename T, typename Substitution>
392 : T replace_all_variables(const T& x,
393 : const Substitution& sigma,
394 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
395 : )
396 : {
397 : T result;
398 : core::make_update_apply_builder<state_formulas::variable_builder>(sigma).apply(result, x);
399 : return result;
400 : }
401 :
402 : /// \\brief Applies the substitution sigma to x.
403 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
404 : template <typename T, typename Substitution>
405 : void replace_free_variables(T& x,
406 : const Substitution& sigma,
407 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
408 : )
409 : {
410 : assert(data::is_simple_substitution(sigma));
411 : data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).update(x);
412 : }
413 :
414 : /// \\brief Applies the substitution sigma to x.
415 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
416 : template <typename T, typename Substitution>
417 : T replace_free_variables(const T& x,
418 : const Substitution& sigma,
419 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
420 : )
421 : {
422 : assert(data::is_simple_substitution(sigma));
423 : T result;
424 : data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).apply(result, x);
425 : return result;
426 : }
427 :
428 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
429 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
430 : template <typename T, typename Substitution, typename VariableContainer>
431 : void replace_free_variables(T& x,
432 : const Substitution& sigma,
433 : const VariableContainer& bound_variables,
434 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
435 : )
436 : {
437 : assert(data::is_simple_substitution(sigma));
438 : data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
439 : }
440 :
441 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
442 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
443 : template <typename T, typename Substitution, typename VariableContainer>
444 : T replace_free_variables(const T& x,
445 : const Substitution& sigma,
446 : const VariableContainer& bound_variables,
447 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
448 : )
449 : {
450 : assert(data::is_simple_substitution(sigma));
451 : T result;
452 : data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
453 : return result;
454 : }
455 : //--- end generated state_formulas replace code ---//
456 :
457 : namespace detail
458 : {
459 :
460 : /// \cond INTERNAL_DOCS
461 : template <template <class> class Builder, class Substitution>
462 : struct substitute_state_formulas_builder: public Builder<substitute_state_formulas_builder<Builder, Substitution> >
463 : {
464 : typedef Builder<substitute_state_formulas_builder<Builder, Substitution> > super;
465 : using super::enter;
466 : using super::leave;
467 : using super::update;
468 : using super::apply;
469 :
470 : Substitution sigma;
471 : bool innermost;
472 :
473 1 : substitute_state_formulas_builder(Substitution sigma_, bool innermost_)
474 1 : : sigma(sigma_),
475 1 : innermost(innermost_)
476 1 : {}
477 :
478 : template <class T>
479 5 : void apply(T& result, const state_formula& x)
480 : {
481 5 : if (innermost)
482 : {
483 5 : state_formula y;
484 5 : super::apply(y, x);
485 5 : result = sigma(y);
486 5 : return;
487 5 : }
488 0 : result = sigma(x);
489 : }
490 : };
491 :
492 : template <template <class> class Builder, class Substitution>
493 : substitute_state_formulas_builder<Builder, Substitution>
494 1 : make_replace_state_formulas_builder(Substitution sigma, bool innermost)
495 : {
496 1 : return substitute_state_formulas_builder<Builder, Substitution>(sigma, innermost);
497 : }
498 : /// \endcond
499 :
500 : } // namespace detail
501 :
502 : template <typename T, typename Substitution>
503 : void replace_state_formulas(T& x,
504 : Substitution sigma,
505 : bool innermost = true,
506 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
507 : )
508 : {
509 : state_formulas::detail::make_replace_state_formulas_builder<state_formulas::state_formula_builder>(sigma, innermost).update(x);
510 : }
511 :
512 : template <typename T, typename Substitution>
513 1 : T replace_state_formulas(const T& x,
514 : Substitution sigma,
515 : bool innermost = true,
516 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
517 : )
518 : {
519 1 : T result;
520 1 : state_formulas::detail::make_replace_state_formulas_builder<state_formulas::state_formula_builder>(sigma, innermost).apply(result, x);
521 1 : return result;
522 0 : }
523 :
524 : } // namespace state_formulas
525 :
526 : } // namespace mcrl2
527 :
528 : #endif // MCRL2_MODAL_FORMULA_REPLACE_H
|