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