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