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/builder.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_BUILDER_H
13 : #define MCRL2_DATA_BUILDER_H
14 :
15 : #include "mcrl2/core/builder.h"
16 : #include "mcrl2/data/alias.h"
17 : #include "mcrl2/data/bag.h"
18 : #include "mcrl2/data/bag_comprehension.h"
19 : #include "mcrl2/data/exists.h"
20 : #include "mcrl2/data/lambda.h"
21 : #include "mcrl2/data/set_comprehension.h"
22 : #include "mcrl2/data/structured_sort.h"
23 : #include "mcrl2/data/untyped_data_parameter.h"
24 : #include "mcrl2/data/untyped_possible_sorts.h"
25 : #include "mcrl2/data/untyped_set_or_bag_comprehension.h"
26 : #include "mcrl2/data/untyped_sort_variable.h"
27 : #include "mcrl2/data/where_clause.h"
28 :
29 :
30 : namespace mcrl2
31 : {
32 :
33 : namespace data
34 : {
35 :
36 : // Adds sort expression traversal to a builder
37 : //--- start generated add_sort_expressions code ---//
38 : template <template <class> class Builder, class Derived>
39 : struct add_sort_expressions: public Builder<Derived>
40 : {
41 : typedef Builder<Derived> super;
42 : using super::enter;
43 : using super::leave;
44 : using super::update;
45 : using super::apply;
46 :
47 : template <class T>
48 14438508 : void apply(T& result, const data::variable& x)
49 : {
50 :
51 14438508 : static_cast<Derived&>(*this).enter(x);
52 28877016 : data::make_variable(result, x.name(), [&](sort_expression& result){ static_cast<Derived&>(*this).apply(result, x.sort()); });
53 14438508 : static_cast<Derived&>(*this).leave(x);
54 14438508 : }
55 :
56 : template <class T>
57 14703897 : void apply(T& result, const data::function_symbol& x)
58 : {
59 :
60 14703897 : static_cast<Derived&>(*this).enter(x);
61 29407794 : data::make_function_symbol(result, x.name(), [&](sort_expression& result){ static_cast<Derived&>(*this).apply(result, x.sort()); });
62 14703897 : static_cast<Derived&>(*this).leave(x);
63 14703897 : }
64 :
65 : template <class T>
66 8325531 : void apply(T& result, const data::application& x)
67 : {
68 :
69 8325531 : static_cast<Derived&>(*this).enter(x);
70 8325531 : data::make_application(result,
71 : x.head(),
72 : x.begin(),
73 : x.end(),
74 23177214 : [&](data_expression& result, const data::data_expression& t){ static_cast<Derived&>(*this).apply(result,t);} );
75 8325531 : static_cast<Derived&>(*this).leave(x);
76 8325531 : }
77 :
78 : template <class T>
79 176 : void apply(T& result, const data::where_clause& x)
80 : {
81 :
82 176 : static_cast<Derived&>(*this).enter(x);
83 528 : data::make_where_clause(result, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); }, [&](assignment_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.declarations()); });
84 176 : static_cast<Derived&>(*this).leave(x);
85 176 : }
86 :
87 : template <class T>
88 19879 : void apply(T& result, const data::untyped_identifier& x)
89 : {
90 :
91 19879 : result = x;
92 19879 : static_cast<Derived&>(*this).enter(x);
93 : // skip
94 19879 : static_cast<Derived&>(*this).leave(x);
95 19879 : result = x;
96 19879 : }
97 :
98 : template <class T>
99 359 : void apply(T& result, const data::assignment& x)
100 : {
101 :
102 359 : static_cast<Derived&>(*this).enter(x);
103 1077 : data::make_assignment(result, [&](variable& result){ static_cast<Derived&>(*this).apply(result, x.lhs()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
104 359 : static_cast<Derived&>(*this).leave(x);
105 359 : }
106 :
107 : template <class T>
108 988 : void apply(T& result, const data::untyped_identifier_assignment& x)
109 : {
110 :
111 988 : static_cast<Derived&>(*this).enter(x);
112 1976 : data::make_untyped_identifier_assignment(result, x.lhs(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
113 988 : static_cast<Derived&>(*this).leave(x);
114 988 : }
115 :
116 : template <class T>
117 7089 : void apply(T& result, const data::basic_sort& x)
118 : {
119 :
120 7089 : result = x;
121 7089 : static_cast<Derived&>(*this).enter(x);
122 : // skip
123 7089 : static_cast<Derived&>(*this).leave(x);
124 7089 : result = x;
125 7089 : }
126 :
127 : template <class T>
128 748 : void apply(T& result, const data::container_sort& x)
129 : {
130 :
131 748 : static_cast<Derived&>(*this).enter(x);
132 1496 : data::make_container_sort(result, x.container_name(), [&](sort_expression& result){ static_cast<Derived&>(*this).apply(result, x.element_sort()); });
133 748 : static_cast<Derived&>(*this).leave(x);
134 748 : }
135 :
136 : template <class T>
137 6191 : void apply(T& result, const data::structured_sort& x)
138 : {
139 :
140 6191 : static_cast<Derived&>(*this).enter(x);
141 12382 : data::make_structured_sort(result, [&](structured_sort_constructor_list& result){ static_cast<Derived&>(*this).apply(result, x.constructors()); });
142 6191 : static_cast<Derived&>(*this).leave(x);
143 6191 : }
144 :
145 : template <class T>
146 297 : void apply(T& result, const data::function_sort& x)
147 : {
148 :
149 297 : static_cast<Derived&>(*this).enter(x);
150 891 : data::make_function_sort(result, [&](sort_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.domain()); }, [&](sort_expression& result){ static_cast<Derived&>(*this).apply(result, x.codomain()); });
151 297 : static_cast<Derived&>(*this).leave(x);
152 297 : }
153 :
154 : template <class T>
155 448 : void apply(T& result, const data::untyped_sort& x)
156 : {
157 :
158 448 : result = x;
159 448 : static_cast<Derived&>(*this).enter(x);
160 : // skip
161 448 : static_cast<Derived&>(*this).leave(x);
162 448 : result = x;
163 448 : }
164 :
165 : template <class T>
166 0 : void apply(T& result, const data::untyped_possible_sorts& x)
167 : {
168 :
169 0 : static_cast<Derived&>(*this).enter(x);
170 0 : data::make_untyped_possible_sorts(result, [&](sort_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.sorts()); });
171 0 : static_cast<Derived&>(*this).leave(x);
172 0 : }
173 :
174 : template <class T>
175 0 : void apply(T& result, const data::untyped_sort_variable& x)
176 : {
177 :
178 0 : result = x;
179 0 : static_cast<Derived&>(*this).enter(x);
180 : // skip
181 0 : static_cast<Derived&>(*this).leave(x);
182 0 : result = x;
183 0 : }
184 :
185 : template <class T>
186 18977 : void apply(T& result, const data::forall& x)
187 : {
188 :
189 18977 : static_cast<Derived&>(*this).enter(x);
190 56931 : data::make_forall(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
191 18977 : static_cast<Derived&>(*this).leave(x);
192 18977 : }
193 :
194 : template <class T>
195 175 : void apply(T& result, const data::exists& x)
196 : {
197 :
198 175 : static_cast<Derived&>(*this).enter(x);
199 525 : data::make_exists(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
200 175 : static_cast<Derived&>(*this).leave(x);
201 175 : }
202 :
203 : template <class T>
204 180 : void apply(T& result, const data::lambda& x)
205 : {
206 :
207 180 : static_cast<Derived&>(*this).enter(x);
208 540 : data::make_lambda(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
209 180 : static_cast<Derived&>(*this).leave(x);
210 180 : }
211 :
212 : template <class T>
213 25 : void apply(T& result, const data::set_comprehension& x)
214 : {
215 :
216 25 : static_cast<Derived&>(*this).enter(x);
217 75 : data::make_set_comprehension(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
218 25 : static_cast<Derived&>(*this).leave(x);
219 25 : }
220 :
221 : template <class T>
222 16 : void apply(T& result, const data::bag_comprehension& x)
223 : {
224 :
225 16 : static_cast<Derived&>(*this).enter(x);
226 48 : data::make_bag_comprehension(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
227 16 : static_cast<Derived&>(*this).leave(x);
228 16 : }
229 :
230 : template <class T>
231 9 : void apply(T& result, const data::untyped_set_or_bag_comprehension& x)
232 : {
233 :
234 9 : static_cast<Derived&>(*this).enter(x);
235 27 : data::make_untyped_set_or_bag_comprehension(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
236 9 : static_cast<Derived&>(*this).leave(x);
237 9 : }
238 :
239 : template <class T>
240 5813 : void apply(T& result, const data::structured_sort_constructor_argument& x)
241 : {
242 :
243 5813 : static_cast<Derived&>(*this).enter(x);
244 11626 : data::make_structured_sort_constructor_argument(result, x.name(), [&](sort_expression& result){ static_cast<Derived&>(*this).apply(result, x.sort()); });
245 5813 : static_cast<Derived&>(*this).leave(x);
246 5813 : }
247 :
248 : template <class T>
249 17153 : void apply(T& result, const data::structured_sort_constructor& x)
250 : {
251 :
252 17153 : static_cast<Derived&>(*this).enter(x);
253 34306 : data::make_structured_sort_constructor(result, x.name(), [&](structured_sort_constructor_argument_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); }, x.recogniser());
254 17153 : static_cast<Derived&>(*this).leave(x);
255 17153 : }
256 :
257 : template <class T>
258 : void apply(T& result, const data::alias& x)
259 : {
260 :
261 : static_cast<Derived&>(*this).enter(x);
262 : data::make_alias(result, x.name(), [&](sort_expression& result){ static_cast<Derived&>(*this).apply(result, x.reference()); });
263 : static_cast<Derived&>(*this).leave(x);
264 : }
265 :
266 : template <class T>
267 2726675 : void apply(T& result, const data::data_equation& x)
268 : {
269 :
270 2726675 : static_cast<Derived&>(*this).enter(x);
271 13633375 : data::make_data_equation(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.lhs()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
272 2726675 : static_cast<Derived&>(*this).leave(x);
273 2726675 : }
274 :
275 : template <class T>
276 6136 : void apply(T& result, const data::untyped_data_parameter& x)
277 : {
278 :
279 6136 : static_cast<Derived&>(*this).enter(x);
280 12272 : data::make_untyped_data_parameter(result, x.name(), [&](data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
281 6136 : static_cast<Derived&>(*this).leave(x);
282 6136 : }
283 :
284 : template <class T>
285 32678247 : void apply(T& result, const data::data_expression& x)
286 : {
287 :
288 32678247 : static_cast<Derived&>(*this).enter(x);
289 32678247 : if (data::is_abstraction(x))
290 : {
291 19382 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::abstraction>(x));
292 : }
293 32658865 : else if (data::is_variable(x))
294 : {
295 9609379 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
296 : }
297 23049486 : else if (data::is_function_symbol(x))
298 : {
299 14703900 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::function_symbol>(x));
300 : }
301 8345586 : else if (data::is_application(x))
302 : {
303 8325531 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::application>(x));
304 : }
305 20055 : else if (data::is_where_clause(x))
306 : {
307 176 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::where_clause>(x));
308 : }
309 19879 : else if (data::is_untyped_identifier(x))
310 : {
311 19879 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_identifier>(x));
312 : }
313 32678247 : static_cast<Derived&>(*this).leave(x);
314 32678247 : }
315 :
316 : template <class T>
317 194 : void apply(T& result, const data::assignment_expression& x)
318 : {
319 :
320 194 : static_cast<Derived&>(*this).enter(x);
321 194 : if (data::is_assignment(x))
322 : {
323 169 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::assignment>(x));
324 : }
325 25 : else if (data::is_untyped_identifier_assignment(x))
326 : {
327 25 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_identifier_assignment>(x));
328 : }
329 194 : static_cast<Derived&>(*this).leave(x);
330 194 : }
331 :
332 : template <class T>
333 14286 : void apply(T& result, const data::sort_expression& x)
334 : {
335 :
336 14286 : static_cast<Derived&>(*this).enter(x);
337 14286 : if (data::is_basic_sort(x))
338 : {
339 6761 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::basic_sort>(x));
340 : }
341 7525 : else if (data::is_container_sort(x))
342 : {
343 748 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::container_sort>(x));
344 : }
345 6777 : else if (data::is_structured_sort(x))
346 : {
347 6191 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::structured_sort>(x));
348 : }
349 586 : else if (data::is_function_sort(x))
350 : {
351 138 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::function_sort>(x));
352 : }
353 448 : else if (data::is_untyped_sort(x))
354 : {
355 448 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_sort>(x));
356 : }
357 0 : else if (data::is_untyped_possible_sorts(x))
358 : {
359 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_possible_sorts>(x));
360 : }
361 0 : else if (data::is_untyped_sort_variable(x))
362 : {
363 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_sort_variable>(x));
364 : }
365 14286 : static_cast<Derived&>(*this).leave(x);
366 14286 : }
367 :
368 : template <class T>
369 19382 : void apply(T& result, const data::abstraction& x)
370 : {
371 :
372 19382 : static_cast<Derived&>(*this).enter(x);
373 19382 : if (data::is_forall(x))
374 : {
375 18977 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::forall>(x));
376 : }
377 405 : else if (data::is_exists(x))
378 : {
379 175 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::exists>(x));
380 : }
381 230 : else if (data::is_lambda(x))
382 : {
383 180 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::lambda>(x));
384 : }
385 50 : else if (data::is_set_comprehension(x))
386 : {
387 25 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::set_comprehension>(x));
388 : }
389 25 : else if (data::is_bag_comprehension(x))
390 : {
391 16 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::bag_comprehension>(x));
392 : }
393 9 : else if (data::is_untyped_set_or_bag_comprehension(x))
394 : {
395 9 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
396 : }
397 19382 : static_cast<Derived&>(*this).leave(x);
398 19382 : }
399 :
400 : };
401 :
402 : /// \\brief Builder class
403 : template <typename Derived>
404 : struct sort_expression_builder: public add_sort_expressions<core::builder, Derived>
405 : {
406 : };
407 : //--- end generated add_sort_expressions code ---//
408 :
409 : // Adds data expression traversal to a builder
410 : //--- start generated add_data_expressions code ---//
411 : template <template <class> class Builder, class Derived>
412 : struct add_data_expressions: public Builder<Derived>
413 : {
414 : typedef Builder<Derived> super;
415 : using super::enter;
416 : using super::leave;
417 : using super::update;
418 : using super::apply;
419 :
420 : template <class T>
421 30671 : void apply(T& result, const data::variable& x)
422 : {
423 :
424 30671 : result = x;
425 30671 : static_cast<Derived&>(*this).enter(x);
426 : // skip
427 30671 : static_cast<Derived&>(*this).leave(x);
428 30671 : result = x;
429 30671 : }
430 :
431 : template <class T>
432 608992 : void apply(T& result, const data::function_symbol& x)
433 : {
434 :
435 608992 : result = x;
436 608992 : static_cast<Derived&>(*this).enter(x);
437 : // skip
438 608992 : static_cast<Derived&>(*this).leave(x);
439 608992 : result = x;
440 608992 : }
441 :
442 : template <class T>
443 358922 : void apply(T& result, const data::application& x)
444 : {
445 :
446 358922 : static_cast<Derived&>(*this).enter(x);
447 358922 : data::make_application(result,
448 : x.head(),
449 : x.begin(),
450 : x.end(),
451 1002468 : [&](data_expression& result, const data::data_expression& t){ static_cast<Derived&>(*this).apply(result,t);} );
452 358922 : static_cast<Derived&>(*this).leave(x);
453 358922 : }
454 :
455 : template <class T>
456 165 : void apply(T& result, const data::where_clause& x)
457 : {
458 :
459 165 : static_cast<Derived&>(*this).enter(x);
460 495 : data::make_where_clause(result, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); }, [&](assignment_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.declarations()); });
461 165 : static_cast<Derived&>(*this).leave(x);
462 165 : }
463 :
464 : template <class T>
465 4455 : void apply(T& result, const data::untyped_identifier& x)
466 : {
467 :
468 4455 : result = x;
469 4455 : static_cast<Derived&>(*this).enter(x);
470 : // skip
471 4455 : static_cast<Derived&>(*this).leave(x);
472 4455 : result = x;
473 4455 : }
474 :
475 : template <class T>
476 4726 : void apply(T& result, const data::assignment& x)
477 : {
478 :
479 4726 : static_cast<Derived&>(*this).enter(x);
480 9452 : data::make_assignment(result, x.lhs(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
481 4726 : static_cast<Derived&>(*this).leave(x);
482 4726 : }
483 :
484 : template <class T>
485 22 : void apply(T& result, const data::untyped_identifier_assignment& x)
486 : {
487 :
488 22 : static_cast<Derived&>(*this).enter(x);
489 44 : data::make_untyped_identifier_assignment(result, x.lhs(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
490 22 : static_cast<Derived&>(*this).leave(x);
491 22 : }
492 :
493 : template <class T>
494 3 : void apply(T& result, const data::forall& x)
495 : {
496 :
497 3 : static_cast<Derived&>(*this).enter(x);
498 6 : data::make_forall(result, x.variables(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
499 3 : static_cast<Derived&>(*this).leave(x);
500 3 : }
501 :
502 : template <class T>
503 13 : void apply(T& result, const data::exists& x)
504 : {
505 :
506 13 : static_cast<Derived&>(*this).enter(x);
507 26 : data::make_exists(result, x.variables(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
508 13 : static_cast<Derived&>(*this).leave(x);
509 13 : }
510 :
511 : template <class T>
512 1971 : void apply(T& result, const data::lambda& x)
513 : {
514 :
515 1971 : static_cast<Derived&>(*this).enter(x);
516 3942 : data::make_lambda(result, x.variables(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
517 1971 : static_cast<Derived&>(*this).leave(x);
518 1971 : }
519 :
520 : template <class T>
521 0 : void apply(T& result, const data::set_comprehension& x)
522 : {
523 :
524 0 : static_cast<Derived&>(*this).enter(x);
525 0 : data::make_set_comprehension(result, x.variables(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
526 0 : static_cast<Derived&>(*this).leave(x);
527 0 : }
528 :
529 : template <class T>
530 0 : void apply(T& result, const data::bag_comprehension& x)
531 : {
532 :
533 0 : static_cast<Derived&>(*this).enter(x);
534 0 : data::make_bag_comprehension(result, x.variables(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
535 0 : static_cast<Derived&>(*this).leave(x);
536 0 : }
537 :
538 : template <class T>
539 0 : void apply(T& result, const data::untyped_set_or_bag_comprehension& x)
540 : {
541 :
542 0 : static_cast<Derived&>(*this).enter(x);
543 0 : data::make_untyped_set_or_bag_comprehension(result, x.variables(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
544 0 : static_cast<Derived&>(*this).leave(x);
545 0 : }
546 :
547 : template <class T>
548 3793 : void apply(T& result, const data::data_equation& x)
549 : {
550 :
551 3793 : static_cast<Derived&>(*this).enter(x);
552 15172 : data::make_data_equation(result, x.variables(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.lhs()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
553 3793 : static_cast<Derived&>(*this).leave(x);
554 3793 : }
555 :
556 : template <class T>
557 0 : void apply(T& result, const data::untyped_data_parameter& x)
558 : {
559 :
560 0 : static_cast<Derived&>(*this).enter(x);
561 0 : data::make_untyped_data_parameter(result, x.name(), [&](data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
562 0 : static_cast<Derived&>(*this).leave(x);
563 0 : }
564 :
565 : template <class T>
566 1227940 : void apply(T& result, const data::data_expression& x)
567 : {
568 :
569 1227940 : static_cast<Derived&>(*this).enter(x);
570 1227940 : if (data::is_abstraction(x))
571 : {
572 2437 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::abstraction>(x));
573 : }
574 1225503 : else if (data::is_variable(x))
575 : {
576 202436 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
577 : }
578 1023067 : else if (data::is_function_symbol(x))
579 : {
580 641944 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::function_symbol>(x));
581 : }
582 381123 : else if (data::is_application(x))
583 : {
584 376500 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::application>(x));
585 : }
586 4623 : else if (data::is_where_clause(x))
587 : {
588 168 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::where_clause>(x));
589 : }
590 4455 : else if (data::is_untyped_identifier(x))
591 : {
592 4455 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_identifier>(x));
593 : }
594 1227940 : static_cast<Derived&>(*this).leave(x);
595 1227940 : }
596 :
597 : template <class T>
598 166 : void apply(T& result, const data::assignment_expression& x)
599 : {
600 :
601 166 : static_cast<Derived&>(*this).enter(x);
602 166 : if (data::is_assignment(x))
603 : {
604 144 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::assignment>(x));
605 : }
606 22 : else if (data::is_untyped_identifier_assignment(x))
607 : {
608 22 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_identifier_assignment>(x));
609 : }
610 166 : static_cast<Derived&>(*this).leave(x);
611 166 : }
612 :
613 : template <class T>
614 2183 : void apply(T& result, const data::abstraction& x)
615 : {
616 :
617 2183 : static_cast<Derived&>(*this).enter(x);
618 2183 : if (data::is_forall(x))
619 : {
620 111 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::forall>(x));
621 : }
622 2072 : else if (data::is_exists(x))
623 : {
624 21 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::exists>(x));
625 : }
626 2051 : else if (data::is_lambda(x))
627 : {
628 2051 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::lambda>(x));
629 : }
630 0 : else if (data::is_set_comprehension(x))
631 : {
632 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::set_comprehension>(x));
633 : }
634 0 : else if (data::is_bag_comprehension(x))
635 : {
636 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::bag_comprehension>(x));
637 : }
638 0 : else if (data::is_untyped_set_or_bag_comprehension(x))
639 : {
640 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
641 : }
642 2183 : static_cast<Derived&>(*this).leave(x);
643 2183 : }
644 :
645 : };
646 :
647 : /// \\brief Builder class
648 : template <typename Derived>
649 : struct data_expression_builder: public add_data_expressions<core::builder, Derived>
650 : {
651 : };
652 : //--- end generated add_data_expressions code ---//
653 :
654 : //--- start generated add_variables code ---//
655 : template <template <class> class Builder, class Derived>
656 : struct add_variables: public Builder<Derived>
657 : {
658 : typedef Builder<Derived> super;
659 : using super::enter;
660 : using super::leave;
661 : using super::update;
662 : using super::apply;
663 :
664 : template <class T>
665 : void apply(T& result, const data::variable& x)
666 : {
667 :
668 : result = x;
669 : static_cast<Derived&>(*this).enter(x);
670 : // skip
671 : static_cast<Derived&>(*this).leave(x);
672 : result = x;
673 : }
674 :
675 : template <class T>
676 0 : void apply(T& result, const data::function_symbol& x)
677 : {
678 :
679 0 : result = x;
680 0 : static_cast<Derived&>(*this).enter(x);
681 : // skip
682 0 : static_cast<Derived&>(*this).leave(x);
683 0 : result = x;
684 0 : }
685 :
686 : template <class T>
687 0 : void apply(T& result, const data::application& x)
688 : {
689 :
690 0 : static_cast<Derived&>(*this).enter(x);
691 0 : data::make_application(result,
692 : x.head(),
693 : x.begin(),
694 : x.end(),
695 0 : [&](data_expression& result, const data::data_expression& t){ static_cast<Derived&>(*this).apply(result,t);} );
696 0 : static_cast<Derived&>(*this).leave(x);
697 0 : }
698 :
699 : template <class T>
700 0 : void apply(T& result, const data::where_clause& x)
701 : {
702 :
703 0 : static_cast<Derived&>(*this).enter(x);
704 0 : data::make_where_clause(result, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); }, [&](assignment_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.declarations()); });
705 0 : static_cast<Derived&>(*this).leave(x);
706 0 : }
707 :
708 : template <class T>
709 0 : void apply(T& result, const data::untyped_identifier& x)
710 : {
711 :
712 0 : result = x;
713 0 : static_cast<Derived&>(*this).enter(x);
714 : // skip
715 0 : static_cast<Derived&>(*this).leave(x);
716 0 : result = x;
717 0 : }
718 :
719 : template <class T>
720 0 : void apply(T& result, const data::assignment& x)
721 : {
722 :
723 0 : static_cast<Derived&>(*this).enter(x);
724 0 : data::make_assignment(result, [&](variable& result){ static_cast<Derived&>(*this).apply(result, x.lhs()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
725 0 : static_cast<Derived&>(*this).leave(x);
726 0 : }
727 :
728 : template <class T>
729 0 : void apply(T& result, const data::untyped_identifier_assignment& x)
730 : {
731 :
732 0 : static_cast<Derived&>(*this).enter(x);
733 0 : data::make_untyped_identifier_assignment(result, x.lhs(), [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
734 0 : static_cast<Derived&>(*this).leave(x);
735 0 : }
736 :
737 : template <class T>
738 0 : void apply(T& result, const data::forall& x)
739 : {
740 :
741 0 : static_cast<Derived&>(*this).enter(x);
742 0 : data::make_forall(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
743 0 : static_cast<Derived&>(*this).leave(x);
744 0 : }
745 :
746 : template <class T>
747 0 : void apply(T& result, const data::exists& x)
748 : {
749 :
750 0 : static_cast<Derived&>(*this).enter(x);
751 0 : data::make_exists(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
752 0 : static_cast<Derived&>(*this).leave(x);
753 0 : }
754 :
755 : template <class T>
756 0 : void apply(T& result, const data::lambda& x)
757 : {
758 :
759 0 : static_cast<Derived&>(*this).enter(x);
760 0 : data::make_lambda(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
761 0 : static_cast<Derived&>(*this).leave(x);
762 0 : }
763 :
764 : template <class T>
765 0 : void apply(T& result, const data::set_comprehension& x)
766 : {
767 :
768 0 : static_cast<Derived&>(*this).enter(x);
769 0 : data::make_set_comprehension(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
770 0 : static_cast<Derived&>(*this).leave(x);
771 0 : }
772 :
773 : template <class T>
774 0 : void apply(T& result, const data::bag_comprehension& x)
775 : {
776 :
777 0 : static_cast<Derived&>(*this).enter(x);
778 0 : data::make_bag_comprehension(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
779 0 : static_cast<Derived&>(*this).leave(x);
780 0 : }
781 :
782 : template <class T>
783 0 : void apply(T& result, const data::untyped_set_or_bag_comprehension& x)
784 : {
785 :
786 0 : static_cast<Derived&>(*this).enter(x);
787 0 : data::make_untyped_set_or_bag_comprehension(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
788 0 : static_cast<Derived&>(*this).leave(x);
789 0 : }
790 :
791 : template <class T>
792 : void apply(T& result, const data::data_equation& x)
793 : {
794 :
795 : static_cast<Derived&>(*this).enter(x);
796 : data::make_data_equation(result, [&](variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.lhs()); }, [&](data_expression& result){ static_cast<Derived&>(*this).apply(result, x.rhs()); });
797 : static_cast<Derived&>(*this).leave(x);
798 : }
799 :
800 : template <class T>
801 : void apply(T& result, const data::untyped_data_parameter& x)
802 : {
803 :
804 : static_cast<Derived&>(*this).enter(x);
805 : data::make_untyped_data_parameter(result, x.name(), [&](data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
806 : static_cast<Derived&>(*this).leave(x);
807 : }
808 :
809 : template <class T>
810 0 : void apply(T& result, const data::data_expression& x)
811 : {
812 :
813 0 : static_cast<Derived&>(*this).enter(x);
814 0 : if (data::is_abstraction(x))
815 : {
816 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::abstraction>(x));
817 : }
818 0 : else if (data::is_variable(x))
819 : {
820 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
821 : }
822 0 : else if (data::is_function_symbol(x))
823 : {
824 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::function_symbol>(x));
825 : }
826 0 : else if (data::is_application(x))
827 : {
828 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::application>(x));
829 : }
830 0 : else if (data::is_where_clause(x))
831 : {
832 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::where_clause>(x));
833 : }
834 0 : else if (data::is_untyped_identifier(x))
835 : {
836 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_identifier>(x));
837 : }
838 0 : static_cast<Derived&>(*this).leave(x);
839 0 : }
840 :
841 : template <class T>
842 0 : void apply(T& result, const data::assignment_expression& x)
843 : {
844 :
845 0 : static_cast<Derived&>(*this).enter(x);
846 0 : if (data::is_assignment(x))
847 : {
848 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::assignment>(x));
849 : }
850 0 : else if (data::is_untyped_identifier_assignment(x))
851 : {
852 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_identifier_assignment>(x));
853 : }
854 0 : static_cast<Derived&>(*this).leave(x);
855 0 : }
856 :
857 : template <class T>
858 0 : void apply(T& result, const data::abstraction& x)
859 : {
860 :
861 0 : static_cast<Derived&>(*this).enter(x);
862 0 : if (data::is_forall(x))
863 : {
864 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::forall>(x));
865 : }
866 0 : else if (data::is_exists(x))
867 : {
868 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::exists>(x));
869 : }
870 0 : else if (data::is_lambda(x))
871 : {
872 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::lambda>(x));
873 : }
874 0 : else if (data::is_set_comprehension(x))
875 : {
876 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::set_comprehension>(x));
877 : }
878 0 : else if (data::is_bag_comprehension(x))
879 : {
880 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::bag_comprehension>(x));
881 : }
882 0 : else if (data::is_untyped_set_or_bag_comprehension(x))
883 : {
884 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
885 : }
886 0 : static_cast<Derived&>(*this).leave(x);
887 0 : }
888 :
889 : };
890 :
891 : /// \\brief Builder class
892 : template <typename Derived>
893 : struct variable_builder: public add_variables<core::builder, Derived>
894 : {
895 : };
896 : //--- end generated add_variables code ---//
897 :
898 : } // namespace data
899 :
900 : } // namespace mcrl2
901 :
902 : #endif // MCRL2_DATA_BUILDER_H
|
