LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - print.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 1092 1174 93.0 %
Date: 2024-03-08 02:52:28 Functions: 327 955 34.2 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14