Line data Source code
1 : // Author(s): Jeroen van der Wulp, 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/print.h
10 : /// \brief Provides utilities for pretty printing.
11 :
12 : #ifndef MCRL2_DATA_PRINT_H
13 : #define MCRL2_DATA_PRINT_H
14 :
15 : #include "mcrl2/data/data_specification.h"
16 : #include "mcrl2/data/detail/is_untyped.h"
17 : #include "mcrl2/data/detail/print_utility.h"
18 : #include "mcrl2/data/standard_container_utility.h"
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace data
24 : {
25 :
26 : namespace detail {
27 :
28 : inline
29 150851 : bool is_numeric_cast(const data_expression& x)
30 : {
31 150851 : return data::sort_nat::is_pos2nat_application(x)
32 150704 : || data::sort_int::is_pos2int_application(x)
33 150487 : || data::sort_real::is_pos2real_application(x)
34 150487 : || data::sort_int::is_nat2int_application(x)
35 150487 : || data::sort_real::is_nat2real_application(x)
36 150487 : || data::sort_real::is_int2real_application(x)
37 150452 : || data::sort_nat::is_cnat_application(x)
38 131114 : || data::sort_int::is_cint_application(x)
39 301555 : || data::sort_real::is_creal_application(x)
40 : ;
41 : }
42 :
43 150851 : inline bool look_through_numeric_casts(const data_expression& x, std::function<bool(const data_expression&)> f)
44 : {
45 150851 : if (is_numeric_cast(x))
46 : {
47 20591 : return look_through_numeric_casts(atermpp::down_cast<application>(x)[0], f);
48 : }
49 130260 : return f(x);
50 : }
51 :
52 : /* inline
53 : data_expression remove_numeric_casts(data_expression x)
54 : {
55 : while (is_numeric_cast(x))
56 : {
57 : x = *atermpp::down_cast<application>(x).begin();
58 : }
59 : return x;
60 : } */
61 :
62 : inline
63 19170 : bool is_plus(const application& x)
64 : {
65 38340 : return look_through_numeric_casts(
66 : x,
67 19170 : [](const data_expression& x)
68 19170 : { return sort_int::is_plus_application(x) ||
69 18673 : sort_nat::is_plus_application(x) ||
70 56516 : sort_pos::is_plus_application(x) ||
71 76183 : sort_real::is_plus_application(x); });
72 : }
73 :
74 : inline
75 18734 : bool is_minus(const application& x)
76 : {
77 37468 : return look_through_numeric_casts(
78 : x,
79 18734 : [](const data_expression& x)
80 37445 : { return sort_int::is_minus_application(x) ||
81 74913 : sort_real::is_minus_application(x); });
82 : }
83 :
84 : inline
85 18516 : bool is_mod(const application& x)
86 : {
87 37032 : return look_through_numeric_casts(
88 : x,
89 18516 : [](const data_expression& x)
90 36986 : { return sort_int::is_mod_application(x) ||
91 74018 : sort_nat::is_mod_application(x); });
92 : }
93 :
94 : inline
95 18537 : bool is_div(const application& x)
96 : {
97 37074 : return look_through_numeric_casts(
98 : x,
99 18537 : [](const data_expression& x)
100 37053 : { return sort_int::is_div_application(x) ||
101 74127 : sort_nat::is_div_application(x); });
102 : }
103 :
104 : inline
105 18470 : bool is_divmod(const application& x)
106 : {
107 36940 : return look_through_numeric_casts(
108 : x,
109 18470 : [](const data_expression& x)
110 55410 : { return sort_nat::is_divmod_application(x); });
111 : }
112 :
113 : inline
114 18467 : bool is_divides(const application& x)
115 : {
116 36934 : return look_through_numeric_casts(
117 : x,
118 18467 : [](const data_expression& x)
119 55401 : { return sort_real::is_divides_application(x); });
120 : }
121 :
122 : inline
123 34478 : bool is_implies(const application& x)
124 : {
125 34478 : return sort_bool::is_implies_application(x);
126 : }
127 :
128 : inline
129 18621 : bool is_set_union(const application& x)
130 : {
131 18621 : return sort_set::is_union_application(x);
132 : }
133 :
134 : inline
135 18569 : bool is_set_difference(const application& x)
136 : {
137 18569 : return sort_set::is_difference_application(x);
138 : }
139 :
140 : inline
141 18537 : bool is_bag_join(const application& x)
142 : {
143 18537 : return sort_bag::is_union_application(x);
144 : }
145 :
146 : inline
147 18537 : bool is_bag_difference(const application& x)
148 : {
149 18537 : return sort_bag::is_difference_application(x);
150 : }
151 :
152 : inline
153 34355 : bool is_and(const application& x)
154 : {
155 34355 : return sort_bool::is_and_application(x);
156 : }
157 :
158 : inline
159 34403 : bool is_or(const application& x)
160 : {
161 34403 : return sort_bool::is_or_application(x);
162 : }
163 :
164 : inline
165 32576 : bool is_equal_to(const application& x)
166 : {
167 32576 : return data::is_equal_to_application(x);
168 : }
169 :
170 : inline
171 27120 : bool is_not_equal_to(const application& x)
172 : {
173 27120 : return data::is_not_equal_to_application(x);
174 : }
175 :
176 : inline
177 26994 : bool is_less(const application& x)
178 : {
179 26994 : return data::is_less_application(x);
180 : }
181 :
182 : inline
183 22094 : bool is_less_equal(const application& x)
184 : {
185 22094 : return data::is_less_equal_application(x);
186 : }
187 :
188 : inline
189 21827 : bool is_greater(const application& x)
190 : {
191 21827 : return data::is_greater_application(x);
192 : }
193 :
194 : inline
195 21754 : bool is_greater_equal(const application& x)
196 : {
197 21754 : return data::is_greater_equal_application(x);
198 : }
199 :
200 : inline
201 21750 : bool is_in(const application& x)
202 : {
203 21750 : return sort_list::is_in_application(x);
204 : }
205 :
206 : inline
207 18366 : bool is_times(const application& x)
208 : {
209 36732 : return look_through_numeric_casts(
210 : x,
211 18366 : [](const data_expression& x)
212 55098 : { return sort_int::is_times_application(x); });
213 : }
214 :
215 : inline
216 17649 : bool is_element_at(const application& x)
217 : {
218 17649 : return sort_list::is_element_at_application(x);
219 : }
220 :
221 : inline
222 17600 : bool is_set_intersection(const application& x)
223 : {
224 17600 : return sort_set::is_intersection_application(x);
225 : }
226 :
227 : inline
228 17529 : bool is_bag_intersection(const application& x)
229 : {
230 17529 : return sort_bag::is_intersection_application(x);
231 : }
232 :
233 : inline
234 19194 : bool is_concat(const application& x)
235 : {
236 19194 : return sort_list::is_concat_application(x);
237 : }
238 :
239 : inline
240 111 : bool is_cons_list(data_expression x)
241 : {
242 265 : while (sort_list::is_cons_application(x))
243 : {
244 154 : x = sort_list::right(x);
245 : }
246 111 : return sort_list::is_empty_function_symbol(x);
247 : }
248 :
249 : inline
250 2240 : bool is_snoc_list(data_expression x)
251 : {
252 4480 : while (sort_list::is_snoc_application(x))
253 : {
254 2240 : x = sort_list::left(x);
255 : }
256 2240 : return sort_list::is_empty_function_symbol(x);
257 : }
258 :
259 : inline
260 21494 : bool is_cons(const application& x)
261 : {
262 21494 : return sort_list::is_cons_application(x) && !is_cons_list(x);
263 : }
264 :
265 : inline
266 21424 : bool is_snoc(const application& x)
267 : {
268 21424 : return sort_list::is_snoc_application(x) && !is_snoc_list(x);
269 : }
270 :
271 : } // namespace detail
272 :
273 : int precedence(const data_expression& x);
274 :
275 : inline
276 34529 : int precedence(const application& x)
277 : {
278 : // N.B. this code should match printing of a creal
279 34529 : if (sort_real::is_creal_application(x))
280 : {
281 51 : const data_expression& numerator = sort_real::left(x);
282 51 : const data_expression& denominator = sort_real::right(x);
283 51 : if (sort_pos::is_c1_function_symbol(denominator))
284 : {
285 28 : return precedence(numerator);
286 : }
287 : else
288 : {
289 23 : return precedence(sort_real::divides(numerator, sort_int::pos2int(denominator)));
290 : }
291 : }
292 34478 : else if (detail::is_implies(x))
293 : {
294 75 : return 2;
295 : }
296 34403 : else if (detail::is_or(x))
297 : {
298 48 : return 3;
299 : }
300 34355 : else if (detail::is_and(x))
301 : {
302 1779 : return 4;
303 : }
304 59696 : else if (detail::is_equal_to(x) ||
305 27120 : detail::is_not_equal_to(x)
306 : )
307 : {
308 5582 : return 5;
309 : }
310 26994 : else if ( detail::is_less(x)
311 22094 : || detail::is_less_equal(x)
312 21827 : || detail::is_greater(x)
313 21754 : || detail::is_greater_equal(x)
314 49088 : || detail::is_in(x)
315 : )
316 : {
317 5500 : return 6;
318 : }
319 21494 : else if (detail::is_cons(x))
320 : {
321 70 : return 7;
322 : }
323 21424 : else if (detail::is_snoc(x))
324 : {
325 2230 : return 8;
326 : }
327 19194 : else if (detail::is_concat(x))
328 : {
329 25 : return 9;
330 : }
331 19169 : else if ( detail::is_plus(x)
332 18653 : || detail::is_minus(x)
333 18621 : || detail::is_set_union(x)
334 18569 : || detail::is_set_difference(x)
335 18537 : || detail::is_bag_join(x)
336 37822 : || detail::is_bag_difference(x)
337 : )
338 : {
339 632 : return 10;
340 : }
341 18537 : else if ( detail::is_div(x)
342 18516 : || detail::is_mod(x)
343 18470 : || detail::is_divmod(x)
344 37053 : || detail::is_divides(x)
345 : )
346 : {
347 171 : return 11;
348 : }
349 18366 : else if ( detail::is_times(x)
350 17649 : || detail::is_element_at(x)
351 17600 : || detail::is_set_intersection(x)
352 36015 : || detail::is_bag_intersection(x)
353 : )
354 : {
355 837 : return 12;
356 : }
357 17529 : else if (is_function_update_application(x) || is_function_update_stable_application(x))
358 : {
359 40 : return 13;
360 : }
361 : // TODO: add function application (there seems to be no recognizer for it)
362 17489 : return core::detail::max_precedence;
363 : }
364 :
365 5 : constexpr int precedence(const forall&) { return 1; }
366 1 : constexpr int precedence(const exists&) { return 1; }
367 152 : constexpr int precedence(const lambda&) { return 1; }
368 0 : constexpr int precedence(const set_comprehension&) { return core::detail::max_precedence; }
369 0 : constexpr int precedence(const bag_comprehension&) { return core::detail::max_precedence; }
370 0 : constexpr int precedence(const where_clause&) { return 0; }
371 49825 : inline int precedence(const data_expression& x)
372 : {
373 49825 : if (data::is_application(x)) { return precedence(atermpp::down_cast<application>(x)); }
374 33025 : else if (data::is_forall(x)) { return precedence(atermpp::down_cast<forall>(x)); }
375 33020 : else if (data::is_exists(x)) { return precedence(atermpp::down_cast<exists>(x)); }
376 33019 : else if (data::is_lambda(x)) { return precedence(atermpp::down_cast<lambda>(x)); }
377 32867 : else if (data::is_set_comprehension(x)) { return precedence(atermpp::down_cast<set_comprehension>(x)); }
378 32867 : else if (data::is_bag_comprehension(x)) { return precedence(atermpp::down_cast<bag_comprehension>(x)); }
379 32867 : else if (data::is_where_clause(x)) { return precedence(atermpp::down_cast<where_clause>(x)); }
380 32867 : return core::detail::max_precedence;
381 : }
382 :
383 : inline
384 70 : bool is_left_associative(const data_expression& x)
385 : {
386 70 : return !sort_bool::is_implies_application(x) && !sort_list::is_cons_application(x);
387 : }
388 :
389 : inline
390 80 : bool is_right_associative(const data_expression& x)
391 : {
392 80 : if (!is_application(x))
393 : {
394 0 : return false;
395 : }
396 80 : const auto& x_ = atermpp::down_cast<application>(x);
397 80 : return !detail::is_minus(x_) && !is_equal_to_application(x);
398 : }
399 :
400 : namespace detail
401 : {
402 :
403 : template <typename Derived>
404 : struct printer: public data::add_traverser_sort_expressions<core::detail::printer, Derived>
405 : {
406 : typedef data::add_traverser_sort_expressions<core::detail::printer, Derived> super;
407 :
408 : using super::enter;
409 : using super::leave;
410 : using super::apply;
411 : using super::derived;
412 : using super::print_expression;
413 : using super::print_unary_operand;
414 : using super::print_list;
415 :
416 4109 : void print_unary_data_operation(const application& x, const std::string& op)
417 : {
418 4109 : derived().print(op);
419 4109 : print_expression(x[0], precedence(x[0]) < precedence(x));
420 4109 : }
421 :
422 11283 : void print_binary_data_operation(const application& x, const data_expression& x1, const data_expression& x2, const std::string& op)
423 : {
424 11283 : auto p = precedence(x);
425 11283 : auto p1 = precedence(x1);
426 11283 : auto p2 = precedence(x2);
427 11283 : print_expression(x1, (p1 < p) || (p1 == p && !is_left_associative(x)));
428 11283 : derived().print(op);
429 11283 : print_expression(x2, (p2 < p) || (p2 == p && !is_right_associative(x)));
430 11283 : }
431 :
432 11240 : void print_binary_data_operation(const application& x, const std::string& op)
433 : {
434 11240 : const auto& x1 = x[0];
435 11240 : const auto& x2 = x[1];
436 11240 : print_binary_data_operation(x, x1, x2, op);
437 11240 : }
438 :
439 : // TODO: check if this test is precise enough
440 75 : bool is_one(const data_expression& x) const
441 : {
442 75 : return sort_pos::is_c1_function_symbol(x);
443 : }
444 :
445 9703 : bool is_infix_operation(const application& x) const
446 : {
447 9703 : if (x.size() != 2)
448 : {
449 8954 : return false;
450 : }
451 749 : core::identifier_string name;
452 749 : if (is_function_symbol(x.head()))
453 : {
454 439 : name = function_symbol(x.head()).name();
455 : }
456 310 : else if (is_untyped_identifier(x.head()))
457 : {
458 90 : name = untyped_identifier(x.head()).name();
459 : }
460 : else
461 : {
462 220 : return false;
463 : }
464 : return
465 1058 : (name == data::sort_bool::implies_name()) ||
466 1056 : (name == data::sort_bool::and_name()) ||
467 527 : (name == data::sort_bool::or_name()) ||
468 527 : data::detail::equal_symbol::is_symbol(name) ||
469 507 : data::detail::not_equal_symbol::is_symbol(name) ||
470 507 : data::detail::less_symbol::is_symbol(name) ||
471 507 : data::detail::less_equal_symbol::is_symbol(name) ||
472 505 : data::detail::greater_symbol::is_symbol(name) ||
473 1001 : data::detail::greater_equal_symbol::is_symbol(name) ||
474 999 : (name == data::sort_list::in_name()) ||
475 998 : (name == data::sort_list::cons_name()) ||
476 998 : (name == data::sort_list::snoc_name()) ||
477 984 : (name == data::sort_list::concat_name()) ||
478 932 : (name == data::sort_real::plus_name()) ||
479 894 : (name == data::sort_real::minus_name()) ||
480 894 : (name == data::sort_set::union_name()) ||
481 894 : (name == data::sort_fset::union_name()) ||
482 894 : (name == data::sort_set::difference_name()) ||
483 894 : (name == data::sort_fset::difference_name()) ||
484 894 : (name == data::sort_bag::union_name()) ||
485 894 : (name == data::sort_fbag::union_name()) ||
486 894 : (name == data::sort_bag::difference_name()) ||
487 894 : (name == data::sort_fbag::difference_name()) ||
488 894 : (name == data::sort_int::div_name()) ||
489 892 : (name == data::sort_int::mod_name()) ||
490 889 : (name == data::sort_real::divides_name()) ||
491 886 : (name == data::sort_int::times_name()) ||
492 884 : (name == data::sort_list::element_at_name()) ||
493 1500 : (name == data::sort_set::intersection_name()) ||
494 971 : (name == data::sort_bag::intersection_name());
495 749 : }
496 :
497 138 : core::identifier_string generate_identifier(const std::string& prefix, const data_expression& context) const
498 : {
499 138 : data::set_identifier_generator generator;
500 138 : std::set<variable> variables = data::find_all_variables(context);
501 498 : for (const variable& v: variables)
502 : {
503 360 : generator.add_identifier(v.name());
504 : }
505 276 : return generator(prefix);
506 138 : }
507 :
508 : template <typename Container>
509 18613 : void print_container(const Container& container,
510 : int container_precedence = -1,
511 : const std::string& separator = ", ",
512 : const std::string& open_bracket = "(",
513 : const std::string& close_bracket = ")"
514 : )
515 : {
516 49309 : for (auto i = container.begin(); i != container.end(); ++i)
517 : {
518 30696 : if (i != container.begin())
519 : {
520 12083 : derived().print(separator);
521 : }
522 30696 : bool print_brackets = (container.size() > 1) && (precedence(*i) < container_precedence);
523 30696 : if (print_brackets)
524 : {
525 152 : derived().print(open_bracket);
526 : }
527 30696 : derived().apply(*i);
528 30696 : if (print_brackets)
529 : {
530 152 : derived().print(close_bracket);
531 : }
532 : }
533 18613 : }
534 :
535 : template <typename Variable>
536 131 : void print_variable(const Variable& x, bool print_sort = false)
537 : {
538 131 : derived().apply(x);
539 131 : if (print_sort)
540 : {
541 131 : derived().print(": ");
542 131 : derived().apply(x.sort());
543 : }
544 131 : }
545 :
546 : struct get_sort_default
547 : {
548 : template <typename T>
549 2132 : sort_expression operator()(const T& t) const
550 : {
551 2132 : return t.sort();
552 : }
553 : };
554 :
555 : template <typename Container, typename SortAccessor>
556 3032 : void print_sorted_declarations(const Container& container,
557 : bool print_sorts = true,
558 : bool join_sorts = true,
559 : bool maximally_shared = false,
560 : const std::string& opener = "(",
561 : const std::string& closer = ")",
562 : const std::string& separator = ", ",
563 : SortAccessor get_sort = get_sort_default()
564 : )
565 : {
566 3032 : auto first = container.begin();
567 3032 : auto last = container.end();
568 3032 : if (first == last)
569 : {
570 1214 : return;
571 : }
572 :
573 1818 : derived().print(opener);
574 :
575 1818 : if (maximally_shared)
576 : {
577 : typedef typename Container::value_type T;
578 :
579 : // sort_map[s] will contain all elements t of container with t.sort() == s.
580 44 : std::map<sort_expression, std::vector<T> > sort_map;
581 :
582 : // sorts will contain all sort expressions s that appear as a key in sort_map,
583 : // in the order they are encountered in container
584 44 : std::vector<sort_expression> sorts;
585 :
586 283 : for (auto i = container.begin(); i != container.end(); ++i)
587 : {
588 239 : if (sort_map.find(i->sort()) == sort_map.end())
589 : {
590 66 : sorts.push_back(i->sort());
591 : }
592 239 : sort_map[i->sort()].push_back(*i);
593 : }
594 :
595 : // do the actual printing
596 110 : for (auto i = sorts.begin(); i != sorts.end(); ++i)
597 : {
598 66 : if (i != sorts.begin())
599 : {
600 22 : derived().print(separator);
601 : }
602 66 : const std::vector<T>& v = sort_map[*i];
603 66 : print_list(v, "", "", ",");
604 66 : derived().print(": ");
605 66 : derived().apply(*i);
606 : }
607 44 : }
608 : else
609 : {
610 3972 : while (first != last)
611 : {
612 2198 : if (first != container.begin())
613 : {
614 424 : derived().print(separator);
615 : }
616 :
617 2198 : if (print_sorts && join_sorts)
618 : {
619 : // determine a consecutive interval [first, i) with elements of the same sorts
620 2132 : auto i = first;
621 : do
622 : {
623 3258 : ++i;
624 : }
625 :
626 : // print the elements of the interval [first, i)
627 3258 : while (i != last && i->sort() == first->sort());
628 :
629 5390 : for (auto j = first; j != i; ++j)
630 : {
631 3258 : if (j != first)
632 : {
633 1126 : derived().print(",");
634 : }
635 3258 : derived().apply(*j);
636 : }
637 :
638 : // print the sort
639 2132 : if (print_sorts)
640 : {
641 2132 : derived().print(": ");
642 2132 : derived().apply(get_sort(*first));
643 : }
644 :
645 : // update first
646 2132 : first = i;
647 2132 : }
648 : else
649 : {
650 66 : derived().apply(*first);
651 :
652 : // print the sort
653 66 : if (print_sorts)
654 : {
655 0 : derived().print(": ");
656 0 : derived().apply(get_sort(*first));
657 : }
658 :
659 : // update first
660 66 : ++first;
661 : }
662 : }
663 : }
664 1818 : derived().print(closer);
665 : }
666 :
667 : template <typename Container>
668 2266 : void print_variables(const Container& container,
669 : bool print_sorts = true,
670 : bool join_sorts = true,
671 : bool maximally_shared = false,
672 : const std::string& opener = "(",
673 : const std::string& closer = ")",
674 : const std::string& separator = ", "
675 : )
676 : {
677 2266 : print_sorted_declarations(container, print_sorts, join_sorts, maximally_shared, opener, closer, separator, get_sort_default());
678 2266 : }
679 :
680 : template <typename Container>
681 95 : void print_assignments(const Container& container,
682 : bool print_lhs = true,
683 : const std::string& opener = "",
684 : const std::string& closer = "",
685 : const std::string& separator = ", ",
686 : const std::string& assignment_symbol = " = "
687 : )
688 : {
689 95 : if (container.empty())
690 : {
691 17 : return;
692 : }
693 78 : derived().print(opener);
694 253 : for (auto i = container.begin(); i != container.end(); ++i)
695 : {
696 175 : if (i != container.begin())
697 : {
698 97 : derived().print(separator);
699 : }
700 175 : if (print_lhs)
701 : {
702 175 : derived().apply(i->lhs());
703 175 : derived().print(assignment_symbol);
704 : }
705 175 : derived().apply(i->rhs());
706 : }
707 78 : derived().print(closer);
708 : }
709 :
710 : template <typename T>
711 677 : void print_condition(const T& x, const std::string& arrow = " -> ")
712 : {
713 677 : if (!sort_bool::is_true_function_symbol(x))
714 : {
715 131 : print_expression(x, true);
716 131 : derived().print(arrow);
717 : }
718 677 : }
719 :
720 : template <typename Container>
721 10112 : void print_sort_list(const Container& container,
722 : const std::string& opener = "(",
723 : const std::string& closer = ")",
724 : const std::string& separator = ", "
725 : )
726 : {
727 10112 : if (container.empty())
728 : {
729 0 : return;
730 : }
731 10112 : derived().print(opener);
732 29544 : for (auto i = container.begin(); i != container.end(); ++i)
733 : {
734 19432 : if (i != container.begin())
735 : {
736 9320 : derived().print(separator);
737 : }
738 19432 : bool print_brackets = is_function_sort(*i);
739 19432 : if (print_brackets)
740 : {
741 1007 : derived().print("(");
742 : }
743 19432 : derived().apply(*i);
744 19432 : if (print_brackets)
745 : {
746 1007 : derived().print(")");
747 : }
748 : }
749 10112 : derived().print(closer);
750 : }
751 :
752 57 : void print_list_enumeration(const application& x)
753 : {
754 57 : derived().print("[");
755 57 : print_container(x, precedence(x));
756 57 : derived().print("]");
757 57 : }
758 :
759 14 : void print_set_enumeration(const application& x)
760 : {
761 14 : derived().print("{ ");
762 14 : print_container(x, precedence(x));
763 14 : derived().print(" }");
764 14 : }
765 :
766 9 : void print_bag_enumeration(const application& x)
767 : {
768 9 : derived().print("{ ");
769 9 : application::const_iterator i = x.begin();
770 27 : while (i != x.end())
771 : {
772 18 : if (i != x.begin())
773 : {
774 9 : derived().print(", ");
775 : }
776 18 : derived().apply(*i++);
777 18 : derived().print(": ");
778 18 : derived().apply(*i++);
779 : }
780 9 : derived().print(" }");
781 9 : }
782 :
783 13 : void print_setbag_comprehension(const abstraction& x)
784 : {
785 13 : derived().print("{ ");
786 13 : print_variables(x.variables(), true, true, false, "", "", ", ");
787 13 : derived().print(" | ");
788 13 : derived().apply(x.body());
789 13 : derived().print(" }");
790 13 : }
791 :
792 7137 : bool is_abstraction_application(const application& x) const
793 : {
794 7137 : return is_abstraction(x.head());
795 : }
796 :
797 8760 : bool is_cons_list(data_expression x) const
798 : {
799 22515 : while (sort_list::is_cons_application(x))
800 : {
801 13755 : x = sort_list::right(x);
802 : }
803 8760 : return sort_list::is_empty_function_symbol(x);
804 : }
805 :
806 2234 : bool is_snoc_list(data_expression x) const
807 : {
808 4470 : while (sort_list::is_snoc_application(x))
809 : {
810 2236 : x = sort_list::left(x);
811 : }
812 2234 : return sort_list::is_empty_function_symbol(x);
813 : }
814 :
815 7486 : bool is_fset_cons_list(data_expression x)
816 : {
817 7853 : while (sort_fset::is_cons_application(x) || sort_fset::is_insert_application(x))
818 : {
819 367 : x = sort_fset::right(x);
820 : }
821 7486 : return sort_fset::is_empty_function_symbol(x);
822 : }
823 :
824 : /// \brief Returns true if x is a list composed of cons, insert and cinsert applications.
825 7260 : bool is_fbag_cons_list(data_expression x)
826 : {
827 7414 : while (sort_fbag::is_cons_application(x) || sort_fbag::is_insert_application(x) || sort_fbag::is_cinsert_application(x))
828 : {
829 154 : x = sort_fbag::arg3(x);
830 : }
831 7260 : return sort_fbag::is_empty_function_symbol(x);
832 : }
833 :
834 : bool is_numeric_expression(const application& x)
835 : {
836 : return sort_pos::is_pos(x.sort())
837 : || sort_nat::is_nat(x.sort())
838 : || sort_int::is_int(x.sort())
839 : || sort_real::is_real(x.sort());
840 : }
841 :
842 : bool is_standard_sort(const sort_expression& x)
843 : {
844 : return sort_pos::is_pos(x)
845 : || sort_bool::is_bool(x)
846 : || sort_nat::is_nat(x)
847 : || sort_int::is_int(x)
848 : || sort_real::is_real(x);
849 : }
850 :
851 86 : bool is_fset_true(const data_expression& x)
852 : {
853 86 : return sort_set::is_true_function_function_symbol(sort_set::left(x));
854 : }
855 :
856 85 : bool is_fset_false(const data_expression& x)
857 : {
858 85 : return sort_set::is_false_function_function_symbol(sort_set::left(x));
859 : }
860 :
861 65 : bool is_fset_lambda(const data_expression& x)
862 : {
863 65 : return is_lambda(sort_set::left(x)) && sort_fset::is_empty_function_symbol(sort_set::right(x));
864 : }
865 :
866 39 : bool is_fbag_zero(const data_expression& x)
867 : {
868 39 : return sort_bag::is_zero_function_function_symbol(sort_bag::left(x));
869 : }
870 :
871 24 : bool is_fbag_one(const data_expression& x)
872 : {
873 24 : return sort_bag::is_one_function_function_symbol(sort_bag::left(x));
874 : }
875 :
876 24 : bool is_fbag_lambda(const data_expression& x)
877 : {
878 24 : return is_lambda(sort_bag::left(x)) && sort_fbag::is_empty_function_symbol(sort_bag::right(x));
879 : }
880 :
881 8710 : void print_cons_list(data_expression x)
882 : {
883 8710 : data_expression_vector arguments;
884 22415 : while (sort_list::is_cons_application(x))
885 : {
886 13705 : arguments.push_back(sort_list::left(x));
887 13705 : x = sort_list::right(x);
888 : }
889 8710 : derived().print("[");
890 8710 : print_container(arguments, 6);
891 8710 : derived().print("]");
892 8710 : }
893 :
894 12 : void print_snoc_list(data_expression x)
895 : {
896 12 : data_expression_vector arguments;
897 26 : while (sort_list::is_snoc_application(x))
898 : {
899 14 : arguments.insert(arguments.begin(), sort_list::right(x));
900 14 : x = sort_list::left(x);
901 : }
902 12 : derived().print("[");
903 12 : print_container(arguments, 7);
904 12 : derived().print("]");
905 12 : }
906 :
907 151 : void print_fset_cons_list(data_expression x)
908 : {
909 151 : data_expression_vector arguments;
910 434 : while (sort_fset::is_cons_application(x) || sort_fset::is_insert_application(x))
911 : {
912 283 : arguments.push_back(sort_fset::left(x));
913 283 : x = sort_fset::right(x);
914 : }
915 151 : derived().print("{");
916 151 : print_container(arguments, 6);
917 151 : derived().print("}");
918 151 : }
919 :
920 15 : void print_fbag_zero(const data_expression& x)
921 : {
922 : // TODO: check if this is the correct way to handle this case
923 15 : data_expression y = sort_bag::right(x);
924 15 : if (sort_fbag::is_empty_function_symbol(y))
925 : {
926 4 : derived().print("{:}");
927 : }
928 11 : else if (data::is_variable(y))
929 : {
930 1 : derived().print("@bagfbag(");
931 1 : derived().apply(variable(y).name());
932 1 : derived().print(")");
933 : }
934 : else
935 : {
936 10 : derived().apply(y);
937 : }
938 15 : }
939 :
940 0 : void print_fbag_one(const data_expression& x)
941 : {
942 0 : sort_expression s = function_sort(sort_bag::left(x).sort()).domain().front(); // the sort of the bag elements
943 0 : core::identifier_string name = generate_identifier("x", x);
944 0 : variable var(name, s);
945 0 : data_expression body = number(sort_nat::nat(), "1");
946 0 : if (!sort_fbag::is_empty_function_symbol(sort_bag::right(x)))
947 : {
948 0 : body = sort_nat::swap_zero(body, sort_bag::count(s, var, sort_bag::bag_fbag(s, sort_bag::right(x))));
949 : }
950 0 : derived().print("{ ");
951 0 : print_variable(var, true);
952 0 : derived().print(" | ");
953 0 : derived().apply(body);
954 0 : derived().print(" }");
955 0 : }
956 :
957 7 : void print_fbag_lambda(const data_expression& x)
958 : {
959 14 : sort_expression s = function_sort(sort_bag::left(x).sort()).domain().front(); // the sort of the bag elements
960 14 : core::identifier_string name = generate_identifier("x", x);
961 7 : variable var(name, s);
962 7 : data::lambda left(sort_bag::left(x));
963 7 : data_expression body = left.body();
964 7 : if (!sort_fbag::is_empty_function_symbol(sort_bag::right(x)))
965 : {
966 0 : body = sort_nat::swap_zero(body, sort_bag::count(s, var, sort_bag::bag_fbag(s, sort_bag::right(x))));
967 : }
968 7 : derived().print("{ ");
969 7 : print_variables(left.variables(), true, true, false, "", "", ", ");
970 7 : derived().print(" | ");
971 7 : derived().apply(body);
972 7 : derived().print(" }");
973 7 : }
974 :
975 17 : void print_fbag_default(const data_expression& x)
976 : {
977 34 : sort_expression s = function_sort(sort_bag::left(x).sort()).domain().front();
978 34 : core::identifier_string name = generate_identifier("x", x);
979 17 : variable var(name, s);
980 17 : data_expression body = sort_bag::left(x)(var);
981 17 : if (!sort_fbag::is_empty_function_symbol(sort_bag::right(x)))
982 : {
983 16 : body = sort_nat::swap_zero(body, sort_bag::count(s, var, sort_bag::bag_fbag(s, sort_bag::right(x))));
984 : }
985 17 : derived().print("{ ");
986 17 : print_variable(var, true);
987 17 : derived().print(" | ");
988 17 : derived().apply(body);
989 17 : derived().print(" }");
990 17 : }
991 :
992 31 : void print_fbag_cons_list(data_expression x)
993 : {
994 31 : std::vector<std::pair<data_expression, data_expression> > arguments;
995 64 : while (sort_fbag::is_cons_application(x) || sort_fbag::is_insert_application(x) || sort_fbag::is_cinsert_application(x))
996 : {
997 33 : if (sort_fbag::is_cons_application(x))
998 : {
999 20 : arguments.emplace_back(sort_fbag::arg1(x), sort_fbag::arg2(x));
1000 20 : x = sort_fbag::arg3(x);
1001 : }
1002 13 : else if (sort_fbag::is_insert_application(x))
1003 : {
1004 1 : arguments.emplace_back(sort_fbag::arg1(x), sort_nat::cnat(sort_fbag::arg2(x)));
1005 1 : x = sort_fbag::arg3(x);
1006 : }
1007 : else // if (sort_fbag::is_fbagcinsert_application(x))
1008 : {
1009 12 : arguments.emplace_back(sort_fbag::arg1(x), sort_fbag::arg2(x));
1010 12 : x = sort_fbag::arg3(x);
1011 : }
1012 : }
1013 31 : print_list(arguments, "{", "}");
1014 31 : }
1015 :
1016 1 : void print_fset_true(const data_expression& x)
1017 : {
1018 1 : derived().print("!");
1019 1 : derived().apply(sort_set::right(x));
1020 1 : }
1021 :
1022 20 : void print_fset_false(const data_expression& x)
1023 : {
1024 20 : if (sort_fset::is_empty_function_symbol(sort_set::right(x)))
1025 : {
1026 7 : derived().print("{}");
1027 : }
1028 : else
1029 : {
1030 13 : derived().apply(sort_set::right(x));
1031 : }
1032 20 : }
1033 :
1034 7 : void print_fset_lambda(const data_expression& x)
1035 : {
1036 7 : data::lambda left(sort_set::left(x));
1037 7 : derived().print("{ ");
1038 7 : print_variables(left.variables(), true, true, false, "", "", ", ");
1039 7 : derived().print(" | ");
1040 7 : derived().apply(left.body());
1041 7 : derived().print(" }");
1042 7 : }
1043 :
1044 30 : void print_fset_set_operation(const data_expression& x, const std::string& op)
1045 : {
1046 30 : data_expression f = sort_set::arg1(x);
1047 30 : data_expression g = sort_set::arg2(x);
1048 :
1049 : // print lhs
1050 30 : if (sort_set::is_false_function_function_symbol(g))
1051 : {
1052 4 : derived().apply(sort_set::arg3(x));
1053 : }
1054 26 : else if (sort_set::is_true_function_function_symbol(g))
1055 : {
1056 0 : derived().print("!");
1057 0 : derived().apply(sort_set::arg3(x));
1058 : }
1059 26 : else if (is_function_sort(sort_set::arg1(x).sort()))
1060 : {
1061 26 : const sort_expression sort = sort_set::arg1(x).sort();
1062 26 : const sort_expression& s = atermpp::down_cast<function_sort>(sort).domain().front();
1063 52 : core::identifier_string name = generate_identifier("x", x);
1064 26 : variable var(name, s);
1065 52 : data_expression body = sort_bool::and_(sort_bool::not_(g(var)), sort_set::in(s, var, sort_set::arg3(x)));
1066 26 : derived().print("{ ");
1067 26 : print_variable(var, true);
1068 26 : derived().print(" | ");
1069 26 : derived().apply(body);
1070 26 : derived().print(" }");
1071 26 : }
1072 : else
1073 : {
1074 : // In this case the term is not well formed, for instance because it contains a "Rewritten@@term" function.
1075 : // We print the residue as an aterm.
1076 0 : derived().print(pp(atermpp::aterm(x)));
1077 0 : return;
1078 : }
1079 :
1080 : // print operator
1081 30 : derived().print(op);
1082 :
1083 : // print rhs
1084 30 : if (sort_set::is_false_function_function_symbol(f))
1085 : {
1086 2 : derived().apply(sort_set::arg4(x));
1087 : }
1088 28 : else if (sort_set::is_true_function_function_symbol(f))
1089 : {
1090 0 : derived().print("!");
1091 0 : derived().apply(sort_set::arg4(x));
1092 : }
1093 : else
1094 : {
1095 56 : sort_expression s = function_sort(sort_set::arg1(x).sort()).domain().front();
1096 56 : core::identifier_string name = generate_identifier("x", x);
1097 28 : variable var(name, s);
1098 56 : data_expression body = sort_bool::and_(sort_bool::not_(f(var)), sort_set::in(s, var, sort_set::arg4(x)));
1099 28 : derived().print("{ ");
1100 28 : print_variable(var, true);
1101 28 : derived().print(" | ");
1102 28 : derived().apply(body);
1103 28 : derived().print(" }");
1104 28 : }
1105 30 : }
1106 :
1107 58 : void print_fset_default(const data_expression& x)
1108 : {
1109 58 : data_expression right = sort_set::right(x);
1110 : // TODO: check if this is the correct way to handle this case
1111 58 : if (sort_fset::is_empty_function_symbol(right))
1112 : {
1113 2 : sort_expression s = function_sort(sort_set::left(x).sort()).domain().front();
1114 2 : core::identifier_string name = generate_identifier("x", x);
1115 1 : variable var(name, s);
1116 1 : data_expression body(sort_set::left(x)(var));
1117 1 : derived().print("{ ");
1118 1 : print_variable(var, true);
1119 1 : derived().print(" | ");
1120 1 : derived().apply(body);
1121 1 : derived().print(" }");
1122 1 : }
1123 : else
1124 : {
1125 114 : sort_expression s = function_sort(sort_set::left(x).sort()).domain().front();
1126 114 : core::identifier_string name = generate_identifier("x", x);
1127 57 : variable var(name, s);
1128 57 : data_expression lhs(sort_set::left(x)(var));
1129 114 : data_expression rhs(sort_set::in(s, var, sort_set::set_fset(s, right)));
1130 57 : data_expression body = not_equal_to(lhs, rhs);
1131 57 : derived().print("{ ");
1132 57 : print_variable(var, true);
1133 57 : derived().print(" | ");
1134 57 : derived().apply(body);
1135 57 : derived().print(" }");
1136 57 : }
1137 58 : }
1138 :
1139 : template <typename Abstraction>
1140 940 : void print_abstraction(const Abstraction& x, const std::string& op)
1141 : {
1142 940 : derived().enter(x);
1143 940 : derived().print(op + " ");
1144 940 : print_variables(x.variables(), true, true, false, "", "", ", ");
1145 940 : derived().print(". ");
1146 940 : derived().apply(x.body());
1147 940 : derived().leave(x);
1148 940 : }
1149 :
1150 9726 : void print_function_application(const application& x)
1151 : {
1152 : // Add special handling of list/set/bag enumeration types. This case applies to printing
1153 : // terms after parsing and before type checking.
1154 9726 : if (sort_list::is_list_enumeration_application(x))
1155 : {
1156 0 : print_list_enumeration(x);
1157 0 : return;
1158 : }
1159 9726 : else if (sort_set::is_set_enumeration_application(x))
1160 : {
1161 14 : print_set_enumeration(x);
1162 14 : return;
1163 : }
1164 9712 : else if (sort_bag::is_bag_enumeration_application(x))
1165 : {
1166 9 : print_bag_enumeration(x);
1167 9 : return;
1168 : }
1169 :
1170 9703 : if (is_infix_operation(x))
1171 : {
1172 87 : assert(detail::is_untyped(x));
1173 87 : auto i = x.begin();
1174 87 : data_expression left = *i++;
1175 87 : data_expression right = *i;
1176 87 : print_expression(left, false);
1177 87 : derived().print(" ");
1178 87 : derived().apply(x.head());
1179 87 : derived().print(" ");
1180 87 : print_expression(right, false);
1181 87 : return;
1182 87 : }
1183 :
1184 : // print the head
1185 9616 : bool print_parentheses = is_abstraction(x.head());
1186 9616 : if (print_parentheses)
1187 : {
1188 0 : derived().print("(");
1189 : }
1190 9616 : derived().apply(x.head());
1191 9616 : if (print_parentheses)
1192 : {
1193 0 : derived().print(")");
1194 : }
1195 :
1196 : // print the arguments
1197 9616 : print_parentheses = !x.empty();
1198 9616 : if (is_function_symbol(x.head()) && x.size() == 1)
1199 : {
1200 5519 : std::string name(function_symbol(x.head()).name());
1201 5519 : if (name == "!" || name == "#")
1202 : {
1203 0 : print_parentheses = precedence(*x.begin()) < core::detail::max_precedence;
1204 : }
1205 5519 : }
1206 9616 : if (print_parentheses)
1207 : {
1208 9616 : derived().print("(");
1209 : }
1210 9616 : print_container(x);
1211 9616 : if (print_parentheses)
1212 : {
1213 9616 : derived().print(")");
1214 : }
1215 : }
1216 :
1217 : // N.B. This is interpreted as the bag element 'x.first: x.second'
1218 33 : void apply(const std::pair<data_expression, data_expression>& x)
1219 : {
1220 33 : derived().apply(x.first);
1221 33 : derived().print(": ");
1222 33 : derived().apply(x.second);
1223 33 : }
1224 :
1225 : // TODO: this code should be generated!
1226 4656 : void apply(const data::container_type& x)
1227 : {
1228 4656 : derived().enter(x);
1229 4656 : if (data::is_list_container(x))
1230 : {
1231 1661 : derived().apply(data::list_container(atermpp::aterm_appl(x)));
1232 : }
1233 2995 : else if (data::is_set_container(x))
1234 : {
1235 558 : derived().apply(data::set_container(atermpp::aterm_appl(x)));
1236 : }
1237 2437 : else if (data::is_bag_container(x))
1238 : {
1239 324 : derived().apply(data::bag_container(atermpp::aterm_appl(x)));
1240 : }
1241 2113 : else if (data::is_fset_container(x))
1242 : {
1243 704 : derived().apply(data::fset_container(atermpp::aterm_appl(x)));
1244 : }
1245 1409 : else if (data::is_fbag_container(x))
1246 : {
1247 1409 : derived().apply(data::fbag_container(atermpp::aterm_appl(x)));
1248 : }
1249 4656 : derived().leave(x);
1250 4656 : }
1251 :
1252 32 : void apply(const data::assignment& x)
1253 : {
1254 32 : derived().enter(x);
1255 32 : derived().apply(x.lhs());
1256 32 : derived().print(" = ");
1257 32 : derived().apply(x.rhs());
1258 32 : derived().leave(x);
1259 32 : }
1260 :
1261 : // variable lists have their own notation
1262 28 : void apply(const data::variable_list& x)
1263 : {
1264 28 : derived().enter(x);
1265 28 : print_list(x, "", "", ", ", false);
1266 28 : derived().leave(x);
1267 28 : }
1268 :
1269 5 : void apply(const data::untyped_data_parameter& x)
1270 : {
1271 5 : derived().enter(x);
1272 5 : derived().apply(x.name());
1273 5 : print_list(x.arguments(), "(", ")", ", ");
1274 5 : derived().leave(x);
1275 5 : }
1276 :
1277 37 : void apply(const data::untyped_identifier_assignment& x)
1278 : {
1279 37 : derived().enter(x);
1280 37 : derived().apply(x.lhs());
1281 37 : derived().print("=");
1282 37 : derived().apply(x.rhs());
1283 37 : derived().leave(x);
1284 37 : }
1285 :
1286 0 : void apply(const data::untyped_set_or_bag_comprehension_binder& x)
1287 : {
1288 0 : derived().enter(x);
1289 0 : derived().leave(x);
1290 0 : }
1291 :
1292 0 : void apply(const data::set_comprehension_binder& x)
1293 : {
1294 0 : derived().enter(x);
1295 0 : derived().leave(x);
1296 0 : }
1297 :
1298 0 : void apply(const data::bag_comprehension_binder& x)
1299 : {
1300 0 : derived().enter(x);
1301 0 : derived().leave(x);
1302 0 : }
1303 :
1304 0 : void apply(const data::forall_binder& x)
1305 : {
1306 0 : derived().enter(x);
1307 0 : derived().leave(x);
1308 0 : }
1309 :
1310 0 : void apply(const data::exists_binder& x)
1311 : {
1312 0 : derived().enter(x);
1313 0 : derived().leave(x);
1314 0 : }
1315 :
1316 0 : void apply(const data::lambda_binder& x)
1317 : {
1318 0 : derived().enter(x);
1319 0 : derived().leave(x);
1320 0 : }
1321 :
1322 104 : void apply(const data::structured_sort_constructor_argument& x)
1323 : {
1324 104 : derived().enter(x);
1325 104 : if (x.name() != core::empty_identifier_string())
1326 : {
1327 35 : derived().apply(x.name());
1328 35 : derived().print(": ");
1329 : }
1330 104 : derived().apply(x.sort());
1331 104 : derived().leave(x);
1332 104 : }
1333 :
1334 207 : void apply(const data::structured_sort_constructor& x)
1335 : {
1336 207 : derived().enter(x);
1337 207 : derived().apply(x.name());
1338 207 : print_list(x.arguments(), "(", ")", ", ");
1339 207 : if (x.recogniser() != core::empty_identifier_string())
1340 : {
1341 28 : derived().print("?");
1342 28 : derived().apply(x.recogniser());
1343 : }
1344 207 : derived().leave(x);
1345 207 : }
1346 :
1347 110 : void apply(const data::alias& x)
1348 : {
1349 110 : derived().enter(x);
1350 110 : derived().apply(x.name());
1351 110 : derived().print(" = ");
1352 110 : derived().apply(x.reference());
1353 110 : derived().leave(x);
1354 110 : }
1355 :
1356 1661 : void apply(const data::list_container& x)
1357 : {
1358 1661 : derived().enter(x);
1359 1661 : derived().print("List");
1360 1661 : derived().leave(x);
1361 1661 : }
1362 :
1363 558 : void apply(const data::set_container& x)
1364 : {
1365 558 : derived().enter(x);
1366 558 : derived().print("Set");
1367 558 : derived().leave(x);
1368 558 : }
1369 :
1370 324 : void apply(const data::bag_container& x)
1371 : {
1372 324 : derived().enter(x);
1373 324 : derived().print("Bag");
1374 324 : derived().leave(x);
1375 324 : }
1376 :
1377 704 : void apply(const data::fset_container& x)
1378 : {
1379 704 : derived().enter(x);
1380 704 : derived().print("FSet");
1381 704 : derived().leave(x);
1382 704 : }
1383 :
1384 1409 : void apply(const data::fbag_container& x)
1385 : {
1386 1409 : derived().enter(x);
1387 1409 : derived().print("FBag");
1388 1409 : derived().leave(x);
1389 1409 : }
1390 :
1391 26172 : void apply(const data::basic_sort& x)
1392 : {
1393 26172 : derived().enter(x);
1394 26172 : derived().apply(x.name());
1395 26172 : derived().leave(x);
1396 26172 : }
1397 :
1398 4656 : void apply(const data::container_sort& x)
1399 : {
1400 4656 : derived().enter(x);
1401 4656 : derived().apply(x.container_name());
1402 4656 : derived().print("(");
1403 4656 : derived().apply(x.element_sort());
1404 4656 : derived().print(")");
1405 4656 : derived().leave(x);
1406 4656 : }
1407 :
1408 143 : void apply(const data::structured_sort& x)
1409 : {
1410 143 : derived().enter(x);
1411 143 : print_list(x.constructors(), "struct ", "", " | ");
1412 143 : derived().leave(x);
1413 143 : }
1414 :
1415 10112 : void apply(const data::function_sort& x)
1416 : {
1417 10112 : derived().enter(x);
1418 10112 : print_sort_list(x.domain(), "", " -> ", " # ");
1419 10112 : derived().apply(x.codomain());
1420 10112 : derived().leave(x);
1421 10112 : }
1422 :
1423 7944 : void apply(const data::untyped_sort& x)
1424 : {
1425 7944 : derived().enter(x);
1426 7944 : derived().print("untyped_sort");
1427 7944 : derived().leave(x);
1428 7944 : }
1429 :
1430 9 : void apply(const data::untyped_possible_sorts& x)
1431 : {
1432 9 : derived().enter(x);
1433 9 : derived().print("@untyped_possible_sorts[");
1434 9 : derived().apply(x.sorts());
1435 9 : derived().print("]");
1436 9 : derived().leave(x);
1437 9 : }
1438 :
1439 2209 : void apply(const data::untyped_sort_variable& x)
1440 : {
1441 2209 : derived().enter(x);
1442 2209 : derived().print("@s");
1443 2209 : derived().apply(x.value());
1444 2209 : derived().leave(x);
1445 2209 : }
1446 :
1447 3338 : void apply(const data::untyped_identifier& x)
1448 : {
1449 3338 : derived().enter(x);
1450 3338 : derived().apply(x.name());
1451 3338 : derived().leave(x);
1452 3338 : }
1453 :
1454 33646 : void apply(const data::variable& x)
1455 : {
1456 33646 : derived().enter(x);
1457 33646 : derived().apply(x.name());
1458 33646 : derived().leave(x);
1459 33646 : }
1460 :
1461 48833 : void apply(const data::function_symbol& x)
1462 : {
1463 48833 : derived().enter(x);
1464 48833 : if (sort_nat::is_c0_function_symbol(x))
1465 : {
1466 316 : derived().print("0");
1467 : }
1468 48517 : else if (sort_pos::is_c1_function_symbol(x))
1469 : {
1470 1752 : derived().print("1");
1471 : }
1472 46765 : else if (sort_fbag::is_empty_function_symbol(x))
1473 : {
1474 60 : derived().print("{:}");
1475 : }
1476 46705 : else if (sort_fset::is_empty_function_symbol(x))
1477 : {
1478 81 : derived().print("{}");
1479 : }
1480 : else
1481 : {
1482 46624 : derived().print(x.name());
1483 : }
1484 48833 : derived().leave(x);
1485 48833 : }
1486 :
1487 45056 : void apply(const data::application& x)
1488 : {
1489 45056 : derived().enter(x);
1490 :
1491 : //-------------------------------------------------------------------//
1492 : // bool
1493 : //-------------------------------------------------------------------//
1494 :
1495 45056 : if (sort_bool::is_not_application(x))
1496 : {
1497 4022 : print_unary_data_operation(x, "!");
1498 : }
1499 41034 : else if (sort_bool::is_and_application(x))
1500 : {
1501 977 : print_binary_data_operation(x, " && ");
1502 : }
1503 40057 : else if (sort_bool::is_or_application(x))
1504 : {
1505 38 : print_binary_data_operation(x, " || ");
1506 : }
1507 40019 : else if (sort_bool::is_implies_application(x))
1508 : {
1509 46 : print_binary_data_operation(x, " => ");
1510 : }
1511 :
1512 : //-------------------------------------------------------------------//
1513 : // data
1514 : //-------------------------------------------------------------------//
1515 :
1516 39973 : else if (data::is_equal_to_application(x))
1517 : {
1518 3681 : print_binary_data_operation(x, " == ");
1519 : }
1520 36292 : else if (data::is_not_equal_to_application(x))
1521 : {
1522 110 : print_binary_data_operation(x, " != ");
1523 : }
1524 36182 : else if (data::is_if_application(x))
1525 : {
1526 : // TODO: is this correct?
1527 2640 : print_function_application(x);
1528 : }
1529 33542 : else if (data::is_less_application(x))
1530 : {
1531 2572 : print_binary_data_operation(x, " < ");
1532 : }
1533 30970 : else if (data::is_less_equal_application(x))
1534 : {
1535 195 : print_binary_data_operation(x, " <= ");
1536 : }
1537 30775 : else if (data::is_greater_application(x))
1538 : {
1539 58 : print_binary_data_operation(x, " > ");
1540 : }
1541 30717 : else if (data::is_greater_equal_application(x))
1542 : {
1543 4 : print_binary_data_operation(x, " >= ");
1544 : }
1545 :
1546 : //-------------------------------------------------------------------//
1547 : // pos
1548 : //-------------------------------------------------------------------//
1549 :
1550 30713 : else if (sort_pos::is_cdub_application(x))
1551 : {
1552 4428 : if (data::sort_pos::is_positive_constant(x))
1553 : {
1554 4109 : derived().print(data::sort_pos::positive_constant_as_string(x));
1555 : }
1556 : else
1557 : {
1558 638 : std::vector<char> number = data::detail::string_to_vector_number("1");
1559 319 : derived().apply(detail::reconstruct_pos_mult(x, number));
1560 319 : }
1561 : }
1562 : // TODO: handle @pospred
1563 26285 : else if (sort_pos::is_plus_application(x))
1564 : {
1565 96 : print_binary_data_operation(x, " + ");
1566 : }
1567 26189 : else if (sort_pos::is_add_with_carry_application(x))
1568 : {
1569 116 : auto b = sort_pos::arg1(x);
1570 116 : auto x1 = sort_pos::arg2(x);
1571 116 : auto x2 = sort_pos::arg3(x);
1572 116 : if (b == data::sort_bool::true_())
1573 : {
1574 2 : derived().apply(sort_pos::succ(sort_pos::plus(x1, x2)));
1575 : }
1576 114 : else if (b == sort_bool::false_())
1577 : {
1578 24 : derived().apply(sort_pos::plus(x1, x2));
1579 : }
1580 : else
1581 : {
1582 90 : derived().apply(if_(b, x1, x2));
1583 : }
1584 116 : }
1585 26073 : else if (sort_pos::is_times_application(x))
1586 : {
1587 356 : print_binary_data_operation(x, " * ");
1588 : }
1589 : // TODO: handle @powerlog2
1590 :
1591 : //-------------------------------------------------------------------//
1592 : // natpair
1593 : //-------------------------------------------------------------------//
1594 :
1595 25717 : else if (sort_nat::is_first_application(x))
1596 : {
1597 : // TODO: verify if this is the correct way of dealing with first/divmod
1598 2 : const auto& y = atermpp::down_cast<application>(sort_nat::arg(x));
1599 2 : if (!sort_nat::is_divmod_application(y))
1600 : {
1601 1 : print_function_application(x);
1602 : }
1603 : else
1604 : {
1605 1 : print_binary_data_operation(y, " div ");
1606 : }
1607 : }
1608 25715 : else if (sort_nat::is_last_application(x))
1609 : {
1610 : // TODO: verify if this is the correct way of dealing with last/divmod
1611 2 : const auto& y = atermpp::down_cast<application>(sort_nat::arg(x));
1612 2 : if (!sort_nat::is_divmod_application(y))
1613 : {
1614 1 : print_function_application(x);
1615 : }
1616 : else
1617 : {
1618 1 : print_binary_data_operation(y, " mod ");
1619 : }
1620 : }
1621 :
1622 : //-------------------------------------------------------------------//
1623 : // nat
1624 : //-------------------------------------------------------------------//
1625 :
1626 25713 : else if (sort_nat::is_cnat_application(x))
1627 : {
1628 3213 : derived().apply(sort_nat::arg(x));
1629 : }
1630 22500 : else if (sort_nat::is_pos2nat_application(x))
1631 : {
1632 22 : derived().apply(*x.begin());
1633 : }
1634 : // TODO: handle @dub
1635 : // TODO: handle @dubsucc
1636 22478 : else if (sort_nat::is_plus_application(x))
1637 : {
1638 355 : print_binary_data_operation(x, " + ");
1639 : }
1640 : // TODO: handle @gtesubtb
1641 22123 : else if (sort_nat::is_times_application(x))
1642 : {
1643 21 : print_binary_data_operation(x, " * ");
1644 : }
1645 22102 : else if (sort_nat::is_div_application(x))
1646 : {
1647 4 : print_binary_data_operation(x, sort_nat::left(x), sort_nat::right(x), " div ");
1648 : }
1649 22098 : else if (sort_nat::is_mod_application(x))
1650 : {
1651 17 : print_binary_data_operation(x, sort_nat::left(x), sort_nat::right(x), " mod ");
1652 : }
1653 : // TODO: handle @monus
1654 : // TODO: handle @swap_zero*
1655 : // TODO: handle @sqrt_nat
1656 :
1657 : //-------------------------------------------------------------------//
1658 : // int
1659 : //-------------------------------------------------------------------//
1660 :
1661 22081 : else if (sort_int::is_cint_application(x))
1662 : {
1663 357 : derived().apply(sort_int::arg(x));
1664 : }
1665 21724 : else if (sort_int::is_cneg_application(x))
1666 : {
1667 46 : derived().apply(sort_int::negate(sort_int::arg(x)));
1668 : }
1669 21678 : else if (sort_int::is_nat2int_application(x))
1670 : {
1671 1 : derived().apply(*x.begin());
1672 : }
1673 21677 : else if (sort_int::is_pos2int_application(x))
1674 : {
1675 32 : derived().apply(*x.begin());
1676 : }
1677 21645 : else if (sort_int::is_negate_application(x))
1678 : {
1679 75 : print_unary_data_operation(x, "-");
1680 : }
1681 21570 : else if (sort_int::is_plus_application(x))
1682 : {
1683 12 : print_binary_data_operation(x, " + ");
1684 : }
1685 21558 : else if (sort_int::is_minus_application(x))
1686 : {
1687 16 : print_binary_data_operation(x, " - ");
1688 : }
1689 21542 : else if (sort_int::is_times_application(x))
1690 : {
1691 24 : print_binary_data_operation(x, " * ");
1692 : }
1693 21518 : else if (sort_int::is_div_application(x))
1694 : {
1695 10 : print_binary_data_operation(x, sort_int::left(x), sort_int::right(x), " div ");
1696 : }
1697 21508 : else if (sort_int::is_mod_application(x))
1698 : {
1699 12 : print_binary_data_operation(x, sort_int::left(x), sort_int::right(x), " mod ");
1700 : }
1701 :
1702 : //-------------------------------------------------------------------//
1703 : // real
1704 : //-------------------------------------------------------------------//
1705 :
1706 21496 : else if (sort_real::is_creal_application(x))
1707 : {
1708 75 : data_expression numerator = sort_real::left(x);
1709 75 : const data_expression& denominator = sort_real::right(x);
1710 75 : if (is_one(denominator))
1711 : {
1712 44 : derived().apply(numerator);
1713 : }
1714 : else
1715 : {
1716 31 : derived().apply(sort_real::divides(numerator, sort_int::pos2int(denominator)));
1717 : }
1718 75 : }
1719 21421 : else if (sort_real::is_pos2real_application(x))
1720 : {
1721 1 : derived().apply(*x.begin());
1722 : }
1723 21420 : else if (sort_real::is_nat2real_application(x))
1724 : {
1725 1 : derived().apply(*x.begin());
1726 : }
1727 21419 : else if (sort_real::is_int2real_application(x))
1728 : {
1729 10 : derived().apply(*x.begin());
1730 : }
1731 21409 : else if (sort_real::is_negate_application(x))
1732 : {
1733 5 : print_unary_data_operation(x, "-");
1734 : }
1735 21404 : else if (sort_real::is_plus_application(x))
1736 : {
1737 16 : print_binary_data_operation(x, " + ");
1738 : }
1739 21388 : else if (sort_real::is_minus_application(x))
1740 : {
1741 6 : print_binary_data_operation(x, " - ");
1742 : }
1743 21382 : else if (sort_real::is_times_application(x))
1744 : {
1745 6 : print_binary_data_operation(x, " * ");
1746 : }
1747 21376 : else if (sort_real::is_divides_application(x))
1748 : {
1749 67 : print_binary_data_operation(x, " / ");
1750 : }
1751 21309 : else if (sort_real::is_reduce_fraction_application(x))
1752 : {
1753 13 : derived().apply(sort_real::divides(sort_real::left(x),sort_real::right(x)));
1754 : }
1755 21296 : else if (sort_real::is_reduce_fraction_where_application(x))
1756 : {
1757 9 : derived().apply(sort_real::plus(sort_real::int2real(sort_real::arg2(x)), sort_real::divides(sort_real::arg3(x), sort_nat::pos2nat(sort_real::arg1(x)))));
1758 : }
1759 : // TODO: handle @redfrachlp
1760 :
1761 : //-------------------------------------------------------------------//
1762 : // list
1763 : //-------------------------------------------------------------------//
1764 :
1765 21287 : else if (sort_list::is_list_enumeration_application(x))
1766 : {
1767 57 : print_list_enumeration(x);
1768 : }
1769 21230 : else if (sort_list::is_cons_application(x))
1770 : {
1771 8760 : if (is_cons_list(x))
1772 : {
1773 8710 : print_cons_list(x);
1774 : }
1775 : else
1776 : {
1777 50 : print_binary_data_operation(x, " |> ");
1778 : }
1779 : }
1780 12470 : else if (sort_list::is_in_application(x))
1781 : {
1782 140 : print_binary_data_operation(x, " in ");
1783 : }
1784 12330 : else if (sort_list::is_count_application(x))
1785 : {
1786 2242 : derived().print("#");
1787 2242 : print_unary_operand(x, sort_list::arg(x));
1788 : }
1789 10088 : else if (sort_list::is_snoc_application(x))
1790 : {
1791 2234 : if (is_snoc_list(x))
1792 : {
1793 12 : print_snoc_list(x);
1794 : }
1795 : else
1796 : {
1797 2222 : print_binary_data_operation(x, " <| ");
1798 : }
1799 : }
1800 7854 : else if (sort_list::is_concat_application(x))
1801 : {
1802 19 : print_binary_data_operation(x, " ++ ");
1803 : }
1804 7835 : else if (sort_list::is_element_at_application(x))
1805 : {
1806 31 : print_binary_data_operation(x, " . ");
1807 : }
1808 :
1809 : //-------------------------------------------------------------------//
1810 : // set
1811 : //-------------------------------------------------------------------//
1812 :
1813 7804 : else if (sort_set::is_constructor_application(x))
1814 : {
1815 86 : if (is_fset_true(x))
1816 : {
1817 1 : print_fset_true(x);
1818 : }
1819 85 : else if (is_fset_false(x))
1820 : {
1821 20 : print_fset_false(x);
1822 : }
1823 65 : else if (is_fset_lambda(x))
1824 : {
1825 7 : print_fset_lambda(x);
1826 : }
1827 : else
1828 : {
1829 58 : print_fset_default(x);
1830 : }
1831 : }
1832 7718 : else if (sort_set::is_set_fset_application(x))
1833 : {
1834 74 : data_expression y = sort_set::arg(x);
1835 74 : if (sort_fset::is_empty_function_symbol(y))
1836 : {
1837 2 : derived().print("{}");
1838 : }
1839 72 : else if (data::is_variable(y))
1840 : {
1841 11 : derived().print("@setfset(");
1842 11 : derived().apply(variable(y).name());
1843 11 : derived().print(")");
1844 : }
1845 : else
1846 : {
1847 61 : derived().apply(y);
1848 : }
1849 74 : }
1850 7644 : else if (sort_set::is_set_comprehension_application(x))
1851 : {
1852 2 : sort_expression s = function_sort(sort_set::arg(x).sort()).domain().front();
1853 2 : core::identifier_string name = generate_identifier("x", x);
1854 1 : variable var(name, s);
1855 1 : data_expression body(sort_set::arg(x)(var));
1856 1 : derived().print("{ ");
1857 1 : print_variable(var, true);
1858 1 : derived().print(" | ");
1859 1 : derived().apply(body);
1860 1 : derived().print(" }");
1861 1 : }
1862 7643 : else if (sort_set::is_in_application(x))
1863 : {
1864 0 : print_binary_data_operation(x, " in ");
1865 : }
1866 7643 : else if (sort_set::is_complement_application(x))
1867 : {
1868 7 : print_unary_data_operation(x, "!");
1869 : }
1870 7636 : else if (sort_set::is_union_application(x))
1871 : {
1872 40 : print_binary_data_operation(x, " + ");
1873 : }
1874 7596 : else if (sort_set::is_intersection_application(x))
1875 : {
1876 52 : print_binary_data_operation(x, " * ");
1877 : }
1878 7544 : else if (sort_set::is_difference_application(x))
1879 : {
1880 28 : print_binary_data_operation(x, " - ");
1881 : }
1882 7516 : else if (sort_set::is_fset_union_application(x))
1883 : {
1884 15 : print_fset_set_operation(x, " + ");
1885 : }
1886 7501 : else if (sort_set::is_fset_intersection_application(x))
1887 : {
1888 15 : print_fset_set_operation(x, " * ");
1889 : }
1890 :
1891 : //-------------------------------------------------------------------//
1892 : // fset
1893 : //-------------------------------------------------------------------//
1894 :
1895 7486 : else if (is_fset_cons_list(x))
1896 : {
1897 151 : print_fset_cons_list(x);
1898 : }
1899 7335 : else if (sort_fset::is_in_application(x))
1900 : {
1901 0 : print_binary_data_operation(x, " in ");
1902 : }
1903 7335 : else if (sort_fset::is_difference_application(x))
1904 : {
1905 0 : derived().apply(sort_fset::left(x));
1906 0 : derived().print(" - ");
1907 0 : derived().apply(sort_fset::right(x));
1908 : }
1909 7335 : else if (sort_fset::is_union_application(x))
1910 : {
1911 0 : derived().apply(sort_fset::left(x));
1912 0 : derived().print(" + ");
1913 0 : derived().apply(sort_fset::right(x));
1914 : }
1915 7335 : else if (sort_fset::is_intersection_application(x))
1916 : {
1917 0 : derived().apply(sort_fset::left(x));
1918 0 : derived().print(" * ");
1919 0 : derived().apply(sort_fset::right(x));
1920 : }
1921 7335 : else if (sort_fset::is_count_application(x))
1922 : {
1923 0 : derived().print("#");
1924 0 : derived().apply(sort_fset::arg(x));
1925 : }
1926 :
1927 : //-------------------------------------------------------------------//
1928 : // bag
1929 : //-------------------------------------------------------------------//
1930 :
1931 7335 : else if (sort_bag::is_constructor_application(x))
1932 : {
1933 39 : if (is_fbag_zero(x))
1934 : {
1935 15 : print_fbag_zero(x);
1936 : }
1937 24 : else if (is_fbag_one(x))
1938 : {
1939 0 : print_fbag_one(x);
1940 : }
1941 24 : else if (is_fbag_lambda(x))
1942 : {
1943 7 : print_fbag_lambda(x);
1944 : }
1945 : else
1946 : {
1947 17 : print_fbag_default(x);
1948 : }
1949 : }
1950 7296 : else if (sort_bag::is_bag_fbag_application(x))
1951 : {
1952 35 : data_expression y = sort_bag::arg(x);
1953 35 : if (sort_fbag::is_empty_function_symbol(y))
1954 : {
1955 2 : derived().print("{:}");
1956 : }
1957 33 : else if (data::is_variable(y))
1958 : {
1959 13 : derived().print("@bagfbag(");
1960 13 : derived().apply(variable(y).name());
1961 13 : derived().print(")");
1962 : }
1963 : else
1964 : {
1965 20 : derived().apply(y);
1966 : }
1967 35 : }
1968 7261 : else if (sort_bag::is_bag_comprehension_application(x))
1969 : {
1970 2 : sort_expression s = function_sort(sort_bag::arg(x).sort()).domain().front();
1971 2 : core::identifier_string name = generate_identifier("x", x);
1972 1 : variable var(name, s);
1973 1 : data_expression body(sort_bag::arg(x)(var));
1974 1 : derived().print("{ ");
1975 1 : print_variable(var, true);
1976 1 : derived().print(" | ");
1977 1 : derived().apply(body);
1978 1 : derived().print(" }");
1979 1 : }
1980 7260 : else if (sort_bag::is_in_application(x))
1981 : {
1982 0 : print_binary_data_operation(x, " in ");
1983 : }
1984 7260 : else if (sort_bag::is_union_application(x))
1985 : {
1986 0 : print_binary_data_operation(x, " + ");
1987 : }
1988 7260 : else if (sort_bag::is_intersection_application(x))
1989 : {
1990 0 : print_binary_data_operation(x, " * ");
1991 : }
1992 7260 : else if (sort_bag::is_difference_application(x))
1993 : {
1994 0 : print_binary_data_operation(x, " - ");
1995 : }
1996 :
1997 : //-------------------------------------------------------------------//
1998 : // fbag
1999 : //-------------------------------------------------------------------//
2000 :
2001 : // cons / insert / cinsert
2002 7260 : else if (is_fbag_cons_list(x))
2003 : {
2004 31 : print_fbag_cons_list(x);
2005 : }
2006 7229 : else if (sort_fbag::is_in_application(x))
2007 : {
2008 0 : print_binary_data_operation(x, " in ");
2009 : }
2010 7229 : else if (sort_fbag::is_union_application(x))
2011 : {
2012 0 : print_binary_data_operation(x, " + ");
2013 : }
2014 7229 : else if (sort_fbag::is_intersection_application(x))
2015 : {
2016 0 : print_binary_data_operation(x, " * ");
2017 : }
2018 :
2019 7229 : else if (sort_fbag::is_difference_application(x))
2020 : {
2021 0 : print_binary_data_operation(x, " - ");
2022 : }
2023 7229 : else if (sort_fbag::is_count_all_application(x))
2024 : {
2025 0 : derived().print("#");
2026 0 : derived().apply(sort_fbag::arg(x));
2027 : }
2028 :
2029 : //-------------------------------------------------------------------//
2030 : // function update
2031 : //-------------------------------------------------------------------//
2032 7229 : else if (is_function_update_application(x) || is_function_update_stable_application(x))
2033 : {
2034 92 : data_expression x1 = data::arg1(x);
2035 92 : data_expression x2 = data::arg2(x);
2036 92 : data_expression x3 = data::arg3(x);
2037 92 : bool print_parentheses = is_abstraction(x1);
2038 92 : if (print_parentheses)
2039 : {
2040 14 : derived().print("(");
2041 : }
2042 92 : derived().apply(x1);
2043 92 : if (print_parentheses)
2044 : {
2045 14 : derived().print(")");
2046 : }
2047 92 : derived().print("[");
2048 92 : derived().apply(x2);
2049 92 : derived().print(" -> ");
2050 92 : derived().apply(x3);
2051 92 : derived().print("]");
2052 92 : }
2053 :
2054 : //-------------------------------------------------------------------//
2055 : // abstraction
2056 : //-------------------------------------------------------------------//
2057 7137 : else if (is_abstraction_application(x))
2058 : {
2059 53 : if (!x.empty()) {
2060 53 : derived().print("(");
2061 : }
2062 53 : derived().apply(x.head());
2063 53 : if (!x.empty())
2064 : {
2065 53 : derived().print(")(");
2066 : }
2067 53 : print_container(x);
2068 53 : if (!x.empty())
2069 : {
2070 53 : derived().print(")");
2071 : }
2072 : }
2073 :
2074 : //-------------------------------------------------------------------//
2075 : // function application
2076 : //-------------------------------------------------------------------//
2077 : else
2078 : {
2079 7084 : print_function_application(x);
2080 : }
2081 45056 : derived().leave(x);
2082 45056 : }
2083 :
2084 36 : void apply(const data::where_clause& x)
2085 : {
2086 36 : derived().enter(x);
2087 36 : derived().apply(x.body());
2088 36 : derived().print(" whr ");
2089 36 : const assignment_expression_list& declarations = x.declarations();
2090 105 : for (assignment_expression_list::const_iterator i = declarations.begin(); i != declarations.end(); ++i)
2091 : {
2092 69 : if (i != declarations.begin())
2093 : {
2094 33 : derived().print(", ");
2095 : }
2096 69 : derived().apply(*i);
2097 : }
2098 36 : derived().print(" end");
2099 36 : derived().leave(x);
2100 36 : }
2101 :
2102 122 : void apply(const data::forall& x)
2103 : {
2104 122 : print_abstraction(x, "forall");
2105 122 : }
2106 :
2107 16 : void apply(const data::exists& x)
2108 : {
2109 16 : print_abstraction(x, "exists");
2110 16 : }
2111 :
2112 780 : void apply(const data::lambda& x)
2113 : {
2114 780 : print_abstraction(x, "lambda");
2115 780 : }
2116 :
2117 571 : void apply(const data::data_equation& x)
2118 : {
2119 571 : derived().enter(x);
2120 571 : print_condition(x.condition());
2121 571 : derived().apply(x.lhs());
2122 571 : derived().print(" = ");
2123 571 : derived().apply(x.rhs());
2124 571 : derived().leave(x);
2125 571 : }
2126 :
2127 : // Adds variables v and function symbols f to variable_map and function_symbol_names respectively.
2128 112 : void update_mappings(const data_equation& eqn,
2129 : std::vector<variable>& variables,
2130 : std::map<core::identifier_string, variable>& variable_map,
2131 : std::set<core::identifier_string>& function_symbol_names
2132 : )
2133 : {
2134 489 : for (const function_symbol& f: data::find_function_symbols(eqn))
2135 : {
2136 377 : function_symbol_names.insert(f.name());
2137 : }
2138 1053 : for (const variable& v: eqn.variables())
2139 : {
2140 829 : std::pair<std::map<core::identifier_string, variable>::iterator, bool> k = variable_map.insert(std::make_pair(v.name(), v));
2141 829 : if (k.second) // new variable encountered
2142 : {
2143 163 : variables.push_back(v);
2144 : }
2145 : }
2146 112 : }
2147 :
2148 112 : bool has_conflict(const data_equation& eqn,
2149 : const std::map<core::identifier_string, variable>& variable_map
2150 : )
2151 : {
2152 1053 : for (const variable& v: eqn.variables())
2153 : {
2154 829 : auto j = variable_map.find(v.name());
2155 829 : if (j != variable_map.end() && v != j->second)
2156 : {
2157 0 : return true;
2158 : }
2159 : }
2160 112 : return false;
2161 : }
2162 :
2163 : /// \brief Searches in the range of equations [first, last) for the first equation
2164 : /// that conflicts with one of the previous equations. We say that equation e1 conflicts
2165 : /// with another equation e2 if their declared variables contain a variable with the same
2166 : /// name and a different sort, or if a declared variable in e1 has the same name as a
2167 : /// function symbol appearing in equation e2.
2168 : template <typename Iter>
2169 36 : Iter find_conflicting_equation(Iter first, Iter last, std::vector<variable>& variables)
2170 : {
2171 36 : std::map<core::identifier_string, variable> variable_map;
2172 36 : std::set<core::identifier_string> function_symbol_names;
2173 148 : for (Iter i = first; i != last; ++i)
2174 : {
2175 112 : if (has_conflict(*i, variable_map))
2176 : {
2177 0 : return i;
2178 : }
2179 : else
2180 : {
2181 112 : update_mappings(*i, variables, variable_map, function_symbol_names);
2182 : }
2183 : }
2184 36 : return last; // no conflict found
2185 36 : }
2186 :
2187 : template <typename AliasContainer, typename SortContainer>
2188 383 : void print_sort_declarations(const AliasContainer& aliases,
2189 : const SortContainer& sorts,
2190 : const std::string& opener = "(",
2191 : const std::string& closer = ")",
2192 : const std::string& separator = ", "
2193 : )
2194 : {
2195 383 : if (aliases.empty() && sorts.empty())
2196 : {
2197 282 : return;
2198 : }
2199 101 : bool first_element = true;
2200 101 : derived().print(opener);
2201 :
2202 : // print sorts
2203 165 : for (auto i = sorts.begin(); i != sorts.end(); ++i)
2204 : {
2205 64 : if (!first_element)
2206 : {
2207 27 : derived().print(separator);
2208 : }
2209 64 : derived().apply(*i);
2210 64 : first_element = false;
2211 : }
2212 :
2213 : // print aliases
2214 201 : for (auto i = aliases.begin(); i != aliases.end(); ++i)
2215 : {
2216 100 : if (!first_element)
2217 : {
2218 36 : derived().print(separator);
2219 : }
2220 100 : derived().apply(*i);
2221 100 : first_element = false;
2222 : }
2223 :
2224 101 : derived().print(closer);
2225 : }
2226 :
2227 : template <typename Container>
2228 383 : void print_equations(const Container& equations,
2229 : const data_specification& data_spec,
2230 : const std::string& opener = "(",
2231 : const std::string& closer = ")",
2232 : const std::string& separator = ", "
2233 : )
2234 : {
2235 383 : auto first = equations.begin();
2236 383 : auto last = equations.end();
2237 :
2238 383 : Container normalized_equations = equations;
2239 383 : data::normalize_sorts(normalized_equations, data_spec);
2240 :
2241 419 : while (first != last)
2242 : {
2243 36 : std::vector<variable> variables;
2244 36 : auto i = find_conflicting_equation(first, last, variables);
2245 36 : print_variables(variables, true, true, true, "var ", ";\n", ";\n ");
2246 :
2247 : // N.B. We print normalized equations instead of user defined equations.
2248 : // print_list(std::vector<data_equation>(first, i), opener, closer, separator);
2249 36 : auto first1 = normalized_equations.begin() + (first - equations.begin());
2250 36 : auto i1 = normalized_equations.begin() + (i - equations.begin());
2251 36 : print_list(std::vector<data_equation>(first1, i1), opener, closer, separator);
2252 :
2253 36 : first = i;
2254 : }
2255 383 : }
2256 :
2257 383 : void apply(const data::data_specification& x)
2258 : {
2259 383 : derived().enter(x);
2260 383 : print_sort_declarations(x.user_defined_aliases(), x.user_defined_sorts(), "sort ", ";\n\n", ";\n ");
2261 383 : print_sorted_declarations(x.user_defined_constructors(), true, true, false, "cons ",";\n\n", ";\n ", get_sort_default());
2262 383 : print_sorted_declarations(x.user_defined_mappings(), true, true, false, "map ",";\n\n", ";\n ", get_sort_default());
2263 383 : print_equations(x.user_defined_equations(), x, "eqn ", ";\n\n", ";\n ");
2264 383 : derived().leave(x);
2265 383 : }
2266 :
2267 : // Override, because there are set/bag/setbag comprehension classes that exist after parsing and before type checking.
2268 917 : void apply(const data::abstraction& x)
2269 : {
2270 917 : derived().enter(x);
2271 917 : if (data::is_forall(x))
2272 : {
2273 116 : derived().apply(atermpp::down_cast<data::forall>(x));
2274 : }
2275 801 : else if (data::is_exists(x))
2276 : {
2277 12 : derived().apply(atermpp::down_cast<data::exists>(x));
2278 : }
2279 789 : else if (data::is_lambda(x))
2280 : {
2281 776 : derived().apply(atermpp::down_cast<data::lambda>(x));
2282 : }
2283 13 : else if (data::is_set_comprehension(x))
2284 : {
2285 2 : print_setbag_comprehension(x);
2286 : }
2287 11 : else if (data::is_bag_comprehension(x))
2288 : {
2289 5 : print_setbag_comprehension(x);
2290 : }
2291 6 : else if (data::is_untyped_set_or_bag_comprehension(x))
2292 : {
2293 6 : print_setbag_comprehension(x);
2294 : }
2295 917 : derived().leave(x);
2296 917 : }
2297 : };
2298 :
2299 : } // namespace detail
2300 :
2301 : /// \brief Prints the object x to a stream.
2302 : struct stream_printer
2303 : {
2304 : template <typename T>
2305 31321 : void operator()(const T& x, std::ostream& out)
2306 : {
2307 31321 : core::detail::apply_printer<data::detail::printer> printer(out);
2308 31321 : printer.apply(x);
2309 31321 : }
2310 : };
2311 :
2312 : /// \brief Returns a string representation of the object x.
2313 : template <typename T>
2314 31321 : std::string pp(const T& x)
2315 : {
2316 31321 : std::ostringstream out;
2317 31321 : stream_printer()(x, out);
2318 62642 : return out.str();
2319 31321 : }
2320 :
2321 : } // namespace data
2322 :
2323 : } // namespace mcrl2
2324 :
2325 : #endif
|