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/process/replace.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PROCESS_REPLACE_H
13 : #define MCRL2_PROCESS_REPLACE_H
14 :
15 : #include "mcrl2/data/replace.h"
16 : #include "mcrl2/process/replace_capture_avoiding.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace process
22 : {
23 :
24 : //--- start generated process 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<process::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<process::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<process::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<process::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<process::data_expression_builder>(sigma).update(x);
77 : }
78 :
79 : template <typename T, typename Substitution>
80 1 : 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 1 : T result;
86 1 : core::make_update_apply_builder<process::data_expression_builder>(sigma).apply(result, x);
87 1 : return result;
88 0 : }
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<process::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<process::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<process::data_expression_builder, process::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<process::data_expression_builder, process::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<process::data_expression_builder, process::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<process::data_expression_builder, process::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
161 : return result;
162 : }
163 : //--- end generated process replace code ---//
164 :
165 : struct process_identifier_assignment
166 : {
167 : process_identifier lhs;
168 : process_identifier rhs;
169 :
170 : typedef process_identifier result_type;
171 : typedef process_identifier argument_type;
172 :
173 1 : process_identifier_assignment(const process_identifier& lhs_, const process_identifier& rhs_)
174 1 : : lhs(lhs_), rhs(rhs_)
175 1 : {}
176 :
177 2 : process_identifier operator()(const process_identifier& x) const
178 : {
179 2 : if (x == lhs)
180 : {
181 2 : return rhs;
182 : }
183 0 : return x;
184 : }
185 : };
186 :
187 : template <typename T, typename Substitution>
188 : void replace_process_identifiers(T& x,
189 : const Substitution& sigma,
190 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type* = 0
191 : )
192 : {
193 : core::make_update_apply_builder<process::process_identifier_builder>(sigma).update(x);
194 : }
195 :
196 : template <typename T, typename Substitution>
197 8 : T replace_process_identifiers(const T& x,
198 : const Substitution& sigma,
199 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type* = nullptr
200 : )
201 : {
202 8 : T result;
203 8 : core::make_update_apply_builder<process::process_identifier_builder>(sigma).apply(result, x);
204 8 : return result;
205 0 : }
206 :
207 : } // namespace process
208 :
209 : } // namespace mcrl2
210 :
211 : #endif // MCRL2_PROCESS_REPLACE_H
|
