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_capture_avoiding.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_H
13 : #define MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_H
14 :
15 : #include "mcrl2/core/detail/print_utility.h"
16 : #include "mcrl2/data/builder.h"
17 : #include "mcrl2/data/find.h"
18 :
19 : namespace mcrl2 {
20 :
21 : namespace data {
22 :
23 : namespace detail {
24 :
25 : // Wraps a substitution, such that assignments to variables can be added and removed.
26 : template <typename Substitution>
27 : struct capture_avoiding_substitution_updater
28 : {
29 : Substitution& sigma;
30 : data::set_identifier_generator& id_generator;
31 : std::map<variable, std::list<variable>> updates;
32 :
33 12853 : capture_avoiding_substitution_updater(Substitution& sigma_, data::set_identifier_generator& id_generator_)
34 12853 : : sigma(sigma_), id_generator(id_generator_)
35 12853 : {}
36 :
37 : // adds the assignment [v := v'] to sigma, and returns v'
38 234 : variable add_fresh_variable_assignment(const variable& v)
39 : {
40 468 : variable v1(id_generator(v.name()), v.sort());
41 234 : updates[v].push_back(v1);
42 234 : return v1;
43 0 : }
44 :
45 : // removes the assignment [v := v'] from sigma
46 234 : void remove_fresh_variable_assignment(const variable& v)
47 : {
48 234 : auto i = updates.find(v);
49 234 : id_generator.remove_identifier(i->second.back().name());
50 234 : i->second.pop_back();
51 234 : if (i->second.empty())
52 : {
53 231 : updates.erase(i);
54 : }
55 234 : }
56 :
57 : // adds the assignments [variables := variables'] to sigma, and returns variables'
58 : template <typename VariableContainer>
59 3135 : variable_list add_fresh_variable_assignments(const VariableContainer& variables)
60 : {
61 : return variable_list(
62 : variables.begin(),
63 : variables.end(),
64 230 : [&](const variable& v)
65 : {
66 230 : return add_fresh_variable_assignment(v);
67 : }
68 3135 : );
69 : }
70 :
71 : // removes the assignments [variables := variables'] from sigma
72 : template <typename VariableContainer>
73 3135 : void remove_fresh_variable_assignments(const VariableContainer& variables)
74 : {
75 6500 : for (const variable& v: variables)
76 : {
77 230 : remove_fresh_variable_assignment(v);
78 : }
79 3135 : }
80 :
81 76307 : data_expression operator()(const variable& x)
82 : {
83 76307 : auto i = updates.find(x);
84 76307 : if (i != updates.end())
85 : {
86 345 : return i->second.back();
87 : }
88 : else
89 : {
90 75962 : return sigma(x);
91 : }
92 : }
93 : };
94 :
95 : template <typename Substitution>
96 : std::ostream& operator<<(std::ostream& out, const capture_avoiding_substitution_updater<Substitution>& sigma)
97 : {
98 : std::vector<std::string> updates;
99 : for (const auto& p: sigma.updates)
100 : {
101 : updates.push_back(data::pp(p.first) + " := " + core::detail::print_list(p.second));
102 : }
103 : return out << sigma.sigma << " with updates " << core::detail::print_list(updates);
104 : }
105 :
106 : template <template <class> class Builder, template <template <class> class, class, class> class Binder, class Substitution>
107 : struct replace_capture_avoiding_variables_builder: public Binder<Builder, replace_capture_avoiding_variables_builder<Builder, Binder, Substitution>, Substitution>
108 : {
109 : typedef Binder<Builder, replace_capture_avoiding_variables_builder<Builder, Binder, Substitution>, Substitution> super;
110 : using super::enter;
111 : using super::leave;
112 : using super::apply;
113 : using super::update;
114 :
115 12853 : explicit replace_capture_avoiding_variables_builder(capture_avoiding_substitution_updater<Substitution>& sigma)
116 12853 : : super(sigma)
117 12853 : { }
118 : };
119 :
120 : template <template <class> class Builder, template <template <class> class, class, class> class Binder, class Substitution>
121 : replace_capture_avoiding_variables_builder<Builder, Binder, Substitution>
122 12853 : apply_replace_capture_avoiding_variables_builder(capture_avoiding_substitution_updater<Substitution>& sigma)
123 : {
124 12853 : return replace_capture_avoiding_variables_builder<Builder, Binder, Substitution>(sigma);
125 : }
126 :
127 : template <template <class> class Builder, class Derived, class Substitution>
128 : struct add_capture_avoiding_replacement: public Builder<Derived>
129 : {
130 : typedef Builder<Derived> super;
131 : using super::enter;
132 : using super::leave;
133 : using super::apply;
134 : using super::update;
135 :
136 : capture_avoiding_substitution_updater<Substitution>& sigma;
137 :
138 12853 : explicit add_capture_avoiding_replacement(capture_avoiding_substitution_updater<Substitution>& sigma_)
139 12853 : : sigma(sigma_)
140 12853 : { }
141 :
142 : // applies the substitution to the right hand sides of the assignments
143 : template <class T>
144 3119 : void apply(atermpp::term_list<T>& result, const assignment_list& x)
145 : {
146 3119 : result = assignment_list(
147 : x.begin(),
148 : x.end(),
149 48304 : [&](data::assignment&r, const data::assignment& a)
150 : {
151 48304 : data::make_assignment(r, a.lhs(), [&](data_expression& r){ apply(r, a.rhs() ); } );
152 : }
153 : );
154 3119 : }
155 :
156 : template <class T>
157 76307 : void apply(T& result, const variable& v)
158 : {
159 76307 : result = sigma(v);
160 76307 : }
161 :
162 : template <class T>
163 3 : void apply(T& result, const data::where_clause& x)
164 : {
165 3 : const auto& declarations = atermpp::container_cast<data::assignment_list>(x.declarations());
166 :
167 3 : auto declarations1 = data::assignment_list(
168 : declarations.begin(),
169 : declarations.end(),
170 12 : [&](const assignment& a)
171 : {
172 4 : const data::variable& v = a.lhs();
173 4 : const data_expression& x1 = a.rhs();
174 : // add the assignment [v := v'] to sigma
175 4 : data::variable v1 = sigma.add_fresh_variable_assignment(v);
176 4 : data::data_expression rhs;
177 4 : apply(rhs, x1);
178 8 : return assignment(v1, rhs);
179 4 : }
180 : );
181 3 : data::data_expression body;
182 3 : apply(body, x.body());
183 3 : make_where_clause(result, body, declarations1);
184 :
185 : // remove the assignments [v := v'] from sigma
186 10 : for (const assignment& a: declarations)
187 : {
188 4 : const variable& v = a.lhs();
189 4 : sigma.remove_fresh_variable_assignment(v);
190 : }
191 3 : }
192 :
193 : template <class T>
194 100 : void apply(T& result, const data::forall& x)
195 : {
196 100 : variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
197 100 : data::data_expression body;
198 100 : apply(body, x.body());
199 100 : data::make_forall(result, v1, body);
200 100 : sigma.remove_fresh_variable_assignments(x.variables());
201 100 : }
202 :
203 : template <class T>
204 0 : void apply(T& result, const data::exists& x)
205 : {
206 0 : variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
207 0 : data::data_expression body;
208 0 : apply(body, x.body());
209 0 : data::make_exists(result, v1, body);
210 0 : sigma.remove_fresh_variable_assignments(x.variables());
211 0 : }
212 :
213 : template <class T>
214 0 : void apply(T& result, const data::lambda& x)
215 : {
216 0 : variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
217 0 : data::data_expression body;
218 0 : apply(body, x.body());
219 0 : data::make_lambda(result, v1, body);
220 0 : sigma.remove_fresh_variable_assignments(x.variables());
221 0 : }
222 :
223 : template <class T>
224 : void apply(T& /* result */, data_equation& /* x */)
225 : {
226 : throw mcrl2::runtime_error("not implemented yet");
227 : }
228 : };
229 :
230 : } // namespace detail
231 :
232 : //--- start generated data replace_capture_avoiding code ---//
233 : /// \\brief Applies sigma as a capture avoiding substitution to x.
234 : /// \\param x The object to which the subsitution is applied.
235 : /// \\param sigma A substitution.
236 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
237 : template <typename T, typename Substitution>
238 : void replace_variables_capture_avoiding(T& x,
239 : Substitution& sigma,
240 : data::set_identifier_generator& id_generator,
241 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
242 : )
243 : {
244 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
245 : data::detail::apply_replace_capture_avoiding_variables_builder<data::data_expression_builder, data::detail::add_capture_avoiding_replacement>(sigma1).update(x);
246 : }
247 :
248 : /// \\brief Applies sigma as a capture avoiding substitution to x.
249 : /// \\param x The object to which the substiution is applied.
250 : /// \\param sigma A substitution.
251 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
252 : template <typename T, typename Substitution>
253 10197 : T replace_variables_capture_avoiding(const T& x,
254 : Substitution& sigma,
255 : data::set_identifier_generator& id_generator,
256 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
257 : )
258 : {
259 10197 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
260 10197 : T result;
261 10197 : data::detail::apply_replace_capture_avoiding_variables_builder<data::data_expression_builder, data::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
262 20394 : return result;
263 10197 : }
264 :
265 : /// \\brief Applies sigma as a capture avoiding substitution to x.
266 : /// \\param x The object to which the subsitution is applied.
267 : /// \\param sigma A substitution.
268 : template <typename T, typename Substitution>
269 : void replace_variables_capture_avoiding(T& x,
270 : Substitution& sigma,
271 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
272 : )
273 : {
274 : data::set_identifier_generator id_generator;
275 : id_generator.add_identifiers(data::find_identifiers(x));
276 : for (const data::variable& v: substitution_variables(sigma))
277 : {
278 : id_generator.add_identifier(v.name());
279 : }
280 : data::replace_variables_capture_avoiding(x, sigma, id_generator);
281 : }
282 :
283 : /// \\brief Applies sigma as a capture avoiding substitution to x.
284 : /// \\param x The object to which the substiution is applied.
285 : /// \\param sigma A substitution.
286 : template <typename T, typename Substitution>
287 6405 : T replace_variables_capture_avoiding(const T& x,
288 : Substitution& sigma,
289 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
290 : )
291 : {
292 6405 : data::set_identifier_generator id_generator;
293 6405 : id_generator.add_identifiers(data::find_identifiers(x));
294 12433 : for (const data::variable& v: substitution_variables(sigma))
295 : {
296 6028 : id_generator.add_identifier(v.name());
297 : }
298 12810 : return data::replace_variables_capture_avoiding(x, sigma, id_generator);
299 6405 : }
300 : //--- end generated data replace_capture_avoiding code ---//
301 :
302 : } // namespace data
303 :
304 : } // namespace mcrl2
305 :
306 : #endif // MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_H
|
