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/traverser.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_TRAVERSER_H
      13             : #define MCRL2_DATA_TRAVERSER_H
      14             : 
      15             : #include "mcrl2/core/traverser.h"
      16             : #include "mcrl2/data/alias.h"
      17             : #include "mcrl2/data/bag_comprehension.h"
      18             : #include "mcrl2/data/exists.h"
      19             : #include "mcrl2/data/forall.h"
      20             : #include "mcrl2/data/lambda.h"
      21             : #include "mcrl2/data/set_comprehension.h"
      22             : #include "mcrl2/data/structured_sort.h"
      23             : #include "mcrl2/data/untyped_data_parameter.h"
      24             : #include "mcrl2/data/untyped_possible_sorts.h"
      25             : #include "mcrl2/data/untyped_set_or_bag_comprehension.h"
      26             : #include "mcrl2/data/untyped_sort_variable.h"
      27             : #include "mcrl2/data/where_clause.h"
      28             : 
      29             : namespace mcrl2
      30             : {
      31             : 
      32             : namespace data
      33             : {
      34             : 
      35             : // Adds sort expression traversal to a traverser
      36             : //--- start generated add_traverser_sort_expressions code ---//
      37             : template <template <class> class Traverser, class Derived>
      38             : struct add_traverser_sort_expressions: public Traverser<Derived>
      39             : {
      40             :   typedef Traverser<Derived> super;
      41             :   using super::enter;
      42             :   using super::leave;
      43             :   using super::apply;
      44             : 
      45       94770 :   void apply(const data::variable& x)
      46             :   {
      47       94770 :     static_cast<Derived&>(*this).enter(x);
      48       94770 :     static_cast<Derived&>(*this).apply(x.sort());
      49       94770 :     static_cast<Derived&>(*this).leave(x);
      50       94770 :   }
      51             : 
      52      175420 :   void apply(const data::function_symbol& x)
      53             :   {
      54      175420 :     static_cast<Derived&>(*this).enter(x);
      55      175420 :     static_cast<Derived&>(*this).apply(x.sort());
      56      175420 :     static_cast<Derived&>(*this).leave(x);
      57      175420 :   }
      58             : 
      59       96528 :   void apply(const data::application& x)
      60             :   {
      61       96528 :     static_cast<Derived&>(*this).enter(x);
      62       96528 :     static_cast<Derived&>(*this).apply(x.head());
      63      374435 :     for (const data_expression& t: x) { static_cast<Derived&>(*this).apply(t); }
      64       96528 :     static_cast<Derived&>(*this).leave(x);
      65       96528 :   }
      66             : 
      67          46 :   void apply(const data::where_clause& x)
      68             :   {
      69          46 :     static_cast<Derived&>(*this).enter(x);
      70          46 :     static_cast<Derived&>(*this).apply(x.body());
      71          46 :     static_cast<Derived&>(*this).apply(x.declarations());
      72          46 :     static_cast<Derived&>(*this).leave(x);
      73          46 :   }
      74             : 
      75        4458 :   void apply(const data::untyped_identifier& x)
      76             :   {
      77        4458 :     static_cast<Derived&>(*this).enter(x);
      78             :     // skip
      79        4458 :     static_cast<Derived&>(*this).leave(x);
      80        4458 :   }
      81             : 
      82       10021 :   void apply(const data::assignment& x)
      83             :   {
      84       10021 :     static_cast<Derived&>(*this).enter(x);
      85       10021 :     static_cast<Derived&>(*this).apply(x.lhs());
      86       10021 :     static_cast<Derived&>(*this).apply(x.rhs());
      87       10021 :     static_cast<Derived&>(*this).leave(x);
      88       10021 :   }
      89             : 
      90          22 :   void apply(const data::untyped_identifier_assignment& x)
      91             :   {
      92          22 :     static_cast<Derived&>(*this).enter(x);
      93          22 :     static_cast<Derived&>(*this).apply(x.rhs());
      94          22 :     static_cast<Derived&>(*this).leave(x);
      95          22 :   }
      96             : 
      97     1079435 :   void apply(const data::basic_sort& x)
      98             :   {
      99     1079435 :     static_cast<Derived&>(*this).enter(x);
     100             :     // skip
     101     1079435 :     static_cast<Derived&>(*this).leave(x);
     102     1079435 :   }
     103             : 
     104       35124 :   void apply(const data::container_sort& x)
     105             :   {
     106       35124 :     static_cast<Derived&>(*this).enter(x);
     107       35124 :     static_cast<Derived&>(*this).apply(x.element_sort());
     108       35124 :     static_cast<Derived&>(*this).leave(x);
     109       35124 :   }
     110             : 
     111         311 :   void apply(const data::structured_sort& x)
     112             :   {
     113         311 :     static_cast<Derived&>(*this).enter(x);
     114         311 :     static_cast<Derived&>(*this).apply(x.constructors());
     115         311 :     static_cast<Derived&>(*this).leave(x);
     116         311 :   }
     117             : 
     118      330348 :   void apply(const data::function_sort& x)
     119             :   {
     120      330348 :     static_cast<Derived&>(*this).enter(x);
     121      330348 :     static_cast<Derived&>(*this).apply(x.domain());
     122      330348 :     static_cast<Derived&>(*this).apply(x.codomain());
     123      330348 :     static_cast<Derived&>(*this).leave(x);
     124      330348 :   }
     125             : 
     126         588 :   void apply(const data::untyped_sort& x)
     127             :   {
     128         588 :     static_cast<Derived&>(*this).enter(x);
     129             :     // skip
     130         588 :     static_cast<Derived&>(*this).leave(x);
     131         588 :   }
     132             : 
     133           0 :   void apply(const data::untyped_possible_sorts& x)
     134             :   {
     135           0 :     static_cast<Derived&>(*this).enter(x);
     136           0 :     static_cast<Derived&>(*this).apply(x.sorts());
     137           0 :     static_cast<Derived&>(*this).leave(x);
     138           0 :   }
     139             : 
     140           0 :   void apply(const data::untyped_sort_variable& x)
     141             :   {
     142           0 :     static_cast<Derived&>(*this).enter(x);
     143             :     // skip
     144           0 :     static_cast<Derived&>(*this).leave(x);
     145           0 :   }
     146             : 
     147          13 :   void apply(const data::forall& x)
     148             :   {
     149          13 :     static_cast<Derived&>(*this).enter(x);
     150          13 :     static_cast<Derived&>(*this).apply(x.variables());
     151          13 :     static_cast<Derived&>(*this).apply(x.body());
     152          13 :     static_cast<Derived&>(*this).leave(x);
     153          13 :   }
     154             : 
     155          27 :   void apply(const data::exists& x)
     156             :   {
     157          27 :     static_cast<Derived&>(*this).enter(x);
     158          27 :     static_cast<Derived&>(*this).apply(x.variables());
     159          27 :     static_cast<Derived&>(*this).apply(x.body());
     160          27 :     static_cast<Derived&>(*this).leave(x);
     161          27 :   }
     162             : 
     163         138 :   void apply(const data::lambda& x)
     164             :   {
     165         138 :     static_cast<Derived&>(*this).enter(x);
     166         138 :     static_cast<Derived&>(*this).apply(x.variables());
     167         138 :     static_cast<Derived&>(*this).apply(x.body());
     168         138 :     static_cast<Derived&>(*this).leave(x);
     169         138 :   }
     170             : 
     171           6 :   void apply(const data::set_comprehension& x)
     172             :   {
     173           6 :     static_cast<Derived&>(*this).enter(x);
     174           6 :     static_cast<Derived&>(*this).apply(x.variables());
     175           6 :     static_cast<Derived&>(*this).apply(x.body());
     176           6 :     static_cast<Derived&>(*this).leave(x);
     177           6 :   }
     178             : 
     179           0 :   void apply(const data::bag_comprehension& x)
     180             :   {
     181           0 :     static_cast<Derived&>(*this).enter(x);
     182           0 :     static_cast<Derived&>(*this).apply(x.variables());
     183           0 :     static_cast<Derived&>(*this).apply(x.body());
     184           0 :     static_cast<Derived&>(*this).leave(x);
     185           0 :   }
     186             : 
     187           7 :   void apply(const data::untyped_set_or_bag_comprehension& x)
     188             :   {
     189           7 :     static_cast<Derived&>(*this).enter(x);
     190           7 :     static_cast<Derived&>(*this).apply(x.variables());
     191           7 :     static_cast<Derived&>(*this).apply(x.body());
     192           7 :     static_cast<Derived&>(*this).leave(x);
     193           7 :   }
     194             : 
     195         308 :   void apply(const data::structured_sort_constructor_argument& x)
     196             :   {
     197         308 :     static_cast<Derived&>(*this).enter(x);
     198         308 :     static_cast<Derived&>(*this).apply(x.sort());
     199         308 :     static_cast<Derived&>(*this).leave(x);
     200         308 :   }
     201             : 
     202         622 :   void apply(const data::structured_sort_constructor& x)
     203             :   {
     204         622 :     static_cast<Derived&>(*this).enter(x);
     205         622 :     static_cast<Derived&>(*this).apply(x.arguments());
     206         622 :     static_cast<Derived&>(*this).leave(x);
     207         622 :   }
     208             : 
     209             :   void apply(const data::alias& x)
     210             :   {
     211             :     static_cast<Derived&>(*this).enter(x);
     212             :     static_cast<Derived&>(*this).apply(x.reference());
     213             :     static_cast<Derived&>(*this).leave(x);
     214             :   }
     215             : 
     216        2220 :   void apply(const data::data_equation& x)
     217             :   {
     218        2220 :     static_cast<Derived&>(*this).enter(x);
     219        2220 :     static_cast<Derived&>(*this).apply(x.variables());
     220        2220 :     static_cast<Derived&>(*this).apply(x.condition());
     221        2220 :     static_cast<Derived&>(*this).apply(x.lhs());
     222        2220 :     static_cast<Derived&>(*this).apply(x.rhs());
     223        2220 :     static_cast<Derived&>(*this).leave(x);
     224        2220 :   }
     225             : 
     226           0 :   void apply(const data::untyped_data_parameter& x)
     227             :   {
     228           0 :     static_cast<Derived&>(*this).enter(x);
     229           0 :     static_cast<Derived&>(*this).apply(x.arguments());
     230           0 :     static_cast<Derived&>(*this).leave(x);
     231           0 :   }
     232             : 
     233      447981 :   void apply(const data::data_expression& x)
     234             :   {
     235      447981 :     static_cast<Derived&>(*this).enter(x);
     236      447981 :     if (data::is_abstraction(x))
     237             :     {
     238        1108 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::abstraction>(x));
     239             :     }
     240      446873 :     else if (data::is_variable(x))
     241             :     {
     242       75281 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     243             :     }
     244      371592 :     else if (data::is_function_symbol(x))
     245             :     {
     246      222130 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_symbol>(x));
     247             :     }
     248      149462 :     else if (data::is_application(x))
     249             :     {
     250      141292 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::application>(x));
     251             :     }
     252        8170 :     else if (data::is_where_clause(x))
     253             :     {
     254          82 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::where_clause>(x));
     255             :     }
     256        8088 :     else if (data::is_untyped_identifier(x))
     257             :     {
     258        8088 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier>(x));
     259             :     }
     260      447981 :     static_cast<Derived&>(*this).leave(x);
     261      447981 :   }
     262             : 
     263         115 :   void apply(const data::assignment_expression& x)
     264             :   {
     265         115 :     static_cast<Derived&>(*this).enter(x);
     266         115 :     if (data::is_assignment(x))
     267             :     {
     268          56 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::assignment>(x));
     269             :     }
     270          59 :     else if (data::is_untyped_identifier_assignment(x))
     271             :     {
     272          59 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier_assignment>(x));
     273             :     }
     274         115 :     static_cast<Derived&>(*this).leave(x);
     275         115 :   }
     276             : 
     277     1494962 :   void apply(const data::sort_expression& x)
     278             :   {
     279     1494962 :     static_cast<Derived&>(*this).enter(x);
     280     1494962 :     if (data::is_basic_sort(x))
     281             :     {
     282     1105423 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::basic_sort>(x));
     283             :     }
     284      389539 :     else if (data::is_container_sort(x))
     285             :     {
     286       39774 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::container_sort>(x));
     287             :     }
     288      349765 :     else if (data::is_structured_sort(x))
     289             :     {
     290         454 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::structured_sort>(x));
     291             :     }
     292      349311 :     else if (data::is_function_sort(x))
     293             :     {
     294      340102 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_sort>(x));
     295             :     }
     296        9209 :     else if (data::is_untyped_sort(x))
     297             :     {
     298        8548 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_sort>(x));
     299             :     }
     300         661 :     else if (data::is_untyped_possible_sorts(x))
     301             :     {
     302           9 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_possible_sorts>(x));
     303             :     }
     304         652 :     else if (data::is_untyped_sort_variable(x))
     305             :     {
     306         652 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_sort_variable>(x));
     307             :     }
     308     1494962 :     static_cast<Derived&>(*this).leave(x);
     309     1494962 :   }
     310             : 
     311         191 :   void apply(const data::abstraction& x)
     312             :   {
     313         191 :     static_cast<Derived&>(*this).enter(x);
     314         191 :     if (data::is_forall(x))
     315             :     {
     316          13 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::forall>(x));
     317             :     }
     318         178 :     else if (data::is_exists(x))
     319             :     {
     320          27 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::exists>(x));
     321             :     }
     322         151 :     else if (data::is_lambda(x))
     323             :     {
     324         138 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::lambda>(x));
     325             :     }
     326          13 :     else if (data::is_set_comprehension(x))
     327             :     {
     328           6 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::set_comprehension>(x));
     329             :     }
     330           7 :     else if (data::is_bag_comprehension(x))
     331             :     {
     332           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::bag_comprehension>(x));
     333             :     }
     334           7 :     else if (data::is_untyped_set_or_bag_comprehension(x))
     335             :     {
     336           7 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
     337             :     }
     338         191 :     static_cast<Derived&>(*this).leave(x);
     339         191 :   }
     340             : 
     341             : };
     342             : 
     343             : /// \\brief Traverser class
     344             : template <typename Derived>
     345             : struct sort_expression_traverser: public add_traverser_sort_expressions<core::traverser, Derived>
     346             : {
     347             : };
     348             : //--- end generated add_traverser_sort_expressions code ---//
     349             : 
     350             : //--- start generated add_traverser_data_expressions code ---//
     351             : template <template <class> class Traverser, class Derived>
     352             : struct add_traverser_data_expressions: public Traverser<Derived>
     353             : {
     354             :   typedef Traverser<Derived> super;
     355             :   using super::enter;
     356             :   using super::leave;
     357             :   using super::apply;
     358             : 
     359       37893 :   void apply(const data::variable& x)
     360             :   {
     361       37893 :     static_cast<Derived&>(*this).enter(x);
     362             :     // skip
     363       37893 :     static_cast<Derived&>(*this).leave(x);
     364       37893 :   }
     365             : 
     366     3942549 :   void apply(const data::function_symbol& x)
     367             :   {
     368     3942549 :     static_cast<Derived&>(*this).enter(x);
     369             :     // skip
     370     3942549 :     static_cast<Derived&>(*this).leave(x);
     371     3942549 :   }
     372             : 
     373     1616029 :   void apply(const data::application& x)
     374             :   {
     375     1616029 :     static_cast<Derived&>(*this).enter(x);
     376     1616029 :     static_cast<Derived&>(*this).apply(x.head());
     377     5972416 :     for (const data_expression& t: x) { static_cast<Derived&>(*this).apply(t); }
     378     1616029 :     static_cast<Derived&>(*this).leave(x);
     379     1616029 :   }
     380             : 
     381           1 :   void apply(const data::where_clause& x)
     382             :   {
     383           1 :     static_cast<Derived&>(*this).enter(x);
     384           1 :     static_cast<Derived&>(*this).apply(x.body());
     385           1 :     static_cast<Derived&>(*this).apply(x.declarations());
     386           1 :     static_cast<Derived&>(*this).leave(x);
     387           1 :   }
     388             : 
     389          30 :   void apply(const data::untyped_identifier& x)
     390             :   {
     391          30 :     static_cast<Derived&>(*this).enter(x);
     392             :     // skip
     393          30 :     static_cast<Derived&>(*this).leave(x);
     394          30 :   }
     395             : 
     396      112226 :   void apply(const data::assignment& x)
     397             :   {
     398      112226 :     static_cast<Derived&>(*this).enter(x);
     399      112226 :     static_cast<Derived&>(*this).apply(x.rhs());
     400      112226 :     static_cast<Derived&>(*this).leave(x);
     401      112226 :   }
     402             : 
     403           1 :   void apply(const data::untyped_identifier_assignment& x)
     404             :   {
     405           1 :     static_cast<Derived&>(*this).enter(x);
     406           1 :     static_cast<Derived&>(*this).apply(x.rhs());
     407           1 :     static_cast<Derived&>(*this).leave(x);
     408           1 :   }
     409             : 
     410         195 :   void apply(const data::forall& x)
     411             :   {
     412         195 :     static_cast<Derived&>(*this).enter(x);
     413         195 :     static_cast<Derived&>(*this).apply(x.body());
     414         195 :     static_cast<Derived&>(*this).leave(x);
     415         195 :   }
     416             : 
     417          18 :   void apply(const data::exists& x)
     418             :   {
     419          18 :     static_cast<Derived&>(*this).enter(x);
     420          18 :     static_cast<Derived&>(*this).apply(x.body());
     421          18 :     static_cast<Derived&>(*this).leave(x);
     422          18 :   }
     423             : 
     424        1505 :   void apply(const data::lambda& x)
     425             :   {
     426        1505 :     static_cast<Derived&>(*this).enter(x);
     427        1505 :     static_cast<Derived&>(*this).apply(x.body());
     428        1505 :     static_cast<Derived&>(*this).leave(x);
     429        1505 :   }
     430             : 
     431           0 :   void apply(const data::set_comprehension& x)
     432             :   {
     433           0 :     static_cast<Derived&>(*this).enter(x);
     434           0 :     static_cast<Derived&>(*this).apply(x.body());
     435           0 :     static_cast<Derived&>(*this).leave(x);
     436           0 :   }
     437             : 
     438           0 :   void apply(const data::bag_comprehension& x)
     439             :   {
     440           0 :     static_cast<Derived&>(*this).enter(x);
     441           0 :     static_cast<Derived&>(*this).apply(x.body());
     442           0 :     static_cast<Derived&>(*this).leave(x);
     443           0 :   }
     444             : 
     445           1 :   void apply(const data::untyped_set_or_bag_comprehension& x)
     446             :   {
     447           1 :     static_cast<Derived&>(*this).enter(x);
     448           1 :     static_cast<Derived&>(*this).apply(x.body());
     449           1 :     static_cast<Derived&>(*this).leave(x);
     450           1 :   }
     451             : 
     452         112 :   void apply(const data::data_equation& x)
     453             :   {
     454         112 :     static_cast<Derived&>(*this).enter(x);
     455         112 :     static_cast<Derived&>(*this).apply(x.condition());
     456         112 :     static_cast<Derived&>(*this).apply(x.lhs());
     457         112 :     static_cast<Derived&>(*this).apply(x.rhs());
     458         112 :     static_cast<Derived&>(*this).leave(x);
     459         112 :   }
     460             : 
     461           0 :   void apply(const data::untyped_data_parameter& x)
     462             :   {
     463           0 :     static_cast<Derived&>(*this).enter(x);
     464           0 :     static_cast<Derived&>(*this).apply(x.arguments());
     465           0 :     static_cast<Derived&>(*this).leave(x);
     466           0 :   }
     467             : 
     468     7895907 :   void apply(const data::data_expression& x)
     469             :   {
     470     7895907 :     static_cast<Derived&>(*this).enter(x);
     471     7895907 :     if (data::is_abstraction(x))
     472             :     {
     473        1719 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::abstraction>(x));
     474             :     }
     475     7894188 :     else if (data::is_variable(x))
     476             :     {
     477     2203511 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     478             :     }
     479     5690677 :     else if (data::is_function_symbol(x))
     480             :     {
     481     3980869 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_symbol>(x));
     482             :     }
     483     1709808 :     else if (data::is_application(x))
     484             :     {
     485     1709727 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::application>(x));
     486             :     }
     487          81 :     else if (data::is_where_clause(x))
     488             :     {
     489          51 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::where_clause>(x));
     490             :     }
     491          30 :     else if (data::is_untyped_identifier(x))
     492             :     {
     493          30 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier>(x));
     494             :     }
     495     7895907 :     static_cast<Derived&>(*this).leave(x);
     496     7895907 :   }
     497             : 
     498          51 :   void apply(const data::assignment_expression& x)
     499             :   {
     500          51 :     static_cast<Derived&>(*this).enter(x);
     501          51 :     if (data::is_assignment(x))
     502             :     {
     503          50 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::assignment>(x));
     504             :     }
     505           1 :     else if (data::is_untyped_identifier_assignment(x))
     506             :     {
     507           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier_assignment>(x));
     508             :     }
     509          51 :     static_cast<Derived&>(*this).leave(x);
     510          51 :   }
     511             : 
     512        1719 :   void apply(const data::abstraction& x)
     513             :   {
     514        1719 :     static_cast<Derived&>(*this).enter(x);
     515        1719 :     if (data::is_forall(x))
     516             :     {
     517         195 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::forall>(x));
     518             :     }
     519        1524 :     else if (data::is_exists(x))
     520             :     {
     521          18 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::exists>(x));
     522             :     }
     523        1506 :     else if (data::is_lambda(x))
     524             :     {
     525        1505 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::lambda>(x));
     526             :     }
     527           1 :     else if (data::is_set_comprehension(x))
     528             :     {
     529           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::set_comprehension>(x));
     530             :     }
     531           1 :     else if (data::is_bag_comprehension(x))
     532             :     {
     533           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::bag_comprehension>(x));
     534             :     }
     535           1 :     else if (data::is_untyped_set_or_bag_comprehension(x))
     536             :     {
     537           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
     538             :     }
     539        1719 :     static_cast<Derived&>(*this).leave(x);
     540        1719 :   }
     541             : 
     542             : };
     543             : 
     544             : /// \\brief Traverser class
     545             : template <typename Derived>
     546             : struct data_expression_traverser: public add_traverser_data_expressions<core::traverser, Derived>
     547             : {
     548             : };
     549             : //--- end generated add_traverser_data_expressions code ---//
     550             : 
     551             : //--- start generated add_traverser_variables code ---//
     552             : template <template <class> class Traverser, class Derived>
     553             : struct add_traverser_variables: public Traverser<Derived>
     554             : {
     555             :   typedef Traverser<Derived> super;
     556             :   using super::enter;
     557             :   using super::leave;
     558             :   using super::apply;
     559             : 
     560             :   void apply(const data::variable& x)
     561             :   {
     562             :     static_cast<Derived&>(*this).enter(x);
     563             :     // skip
     564             :     static_cast<Derived&>(*this).leave(x);
     565             :   }
     566             : 
     567     2290569 :   void apply(const data::function_symbol& x)
     568             :   {
     569     2290569 :     static_cast<Derived&>(*this).enter(x);
     570             :     // skip
     571     2290569 :     static_cast<Derived&>(*this).leave(x);
     572     2290569 :   }
     573             : 
     574     1752434 :   void apply(const data::application& x)
     575             :   {
     576     1752434 :     static_cast<Derived&>(*this).enter(x);
     577     1752434 :     static_cast<Derived&>(*this).apply(x.head());
     578     6635371 :     for (const data_expression& t: x) { static_cast<Derived&>(*this).apply(t); }
     579     1752434 :     static_cast<Derived&>(*this).leave(x);
     580     1752434 :   }
     581             : 
     582           9 :   void apply(const data::where_clause& x)
     583             :   {
     584           9 :     static_cast<Derived&>(*this).enter(x);
     585           9 :     static_cast<Derived&>(*this).apply(x.body());
     586           9 :     static_cast<Derived&>(*this).apply(x.declarations());
     587           9 :     static_cast<Derived&>(*this).leave(x);
     588           9 :   }
     589             : 
     590           0 :   void apply(const data::untyped_identifier& x)
     591             :   {
     592           0 :     static_cast<Derived&>(*this).enter(x);
     593             :     // skip
     594           0 :     static_cast<Derived&>(*this).leave(x);
     595           0 :   }
     596             : 
     597        1389 :   void apply(const data::assignment& x)
     598             :   {
     599        1389 :     static_cast<Derived&>(*this).enter(x);
     600        1389 :     static_cast<Derived&>(*this).apply(x.lhs());
     601        1389 :     static_cast<Derived&>(*this).apply(x.rhs());
     602        1389 :     static_cast<Derived&>(*this).leave(x);
     603        1389 :   }
     604             : 
     605           0 :   void apply(const data::untyped_identifier_assignment& x)
     606             :   {
     607           0 :     static_cast<Derived&>(*this).enter(x);
     608           0 :     static_cast<Derived&>(*this).apply(x.rhs());
     609           0 :     static_cast<Derived&>(*this).leave(x);
     610           0 :   }
     611             : 
     612        4912 :   void apply(const data::forall& x)
     613             :   {
     614        4912 :     static_cast<Derived&>(*this).enter(x);
     615        4912 :     static_cast<Derived&>(*this).apply(x.variables());
     616        4912 :     static_cast<Derived&>(*this).apply(x.body());
     617        4912 :     static_cast<Derived&>(*this).leave(x);
     618        4912 :   }
     619             : 
     620           6 :   void apply(const data::exists& x)
     621             :   {
     622           6 :     static_cast<Derived&>(*this).enter(x);
     623           6 :     static_cast<Derived&>(*this).apply(x.variables());
     624           6 :     static_cast<Derived&>(*this).apply(x.body());
     625           6 :     static_cast<Derived&>(*this).leave(x);
     626           6 :   }
     627             : 
     628         146 :   void apply(const data::lambda& x)
     629             :   {
     630         146 :     static_cast<Derived&>(*this).enter(x);
     631         146 :     static_cast<Derived&>(*this).apply(x.variables());
     632         146 :     static_cast<Derived&>(*this).apply(x.body());
     633         146 :     static_cast<Derived&>(*this).leave(x);
     634         146 :   }
     635             : 
     636           0 :   void apply(const data::set_comprehension& x)
     637             :   {
     638           0 :     static_cast<Derived&>(*this).enter(x);
     639           0 :     static_cast<Derived&>(*this).apply(x.variables());
     640           0 :     static_cast<Derived&>(*this).apply(x.body());
     641           0 :     static_cast<Derived&>(*this).leave(x);
     642           0 :   }
     643             : 
     644           0 :   void apply(const data::bag_comprehension& x)
     645             :   {
     646           0 :     static_cast<Derived&>(*this).enter(x);
     647           0 :     static_cast<Derived&>(*this).apply(x.variables());
     648           0 :     static_cast<Derived&>(*this).apply(x.body());
     649           0 :     static_cast<Derived&>(*this).leave(x);
     650           0 :   }
     651             : 
     652           0 :   void apply(const data::untyped_set_or_bag_comprehension& x)
     653             :   {
     654           0 :     static_cast<Derived&>(*this).enter(x);
     655           0 :     static_cast<Derived&>(*this).apply(x.variables());
     656           0 :     static_cast<Derived&>(*this).apply(x.body());
     657           0 :     static_cast<Derived&>(*this).leave(x);
     658           0 :   }
     659             : 
     660             :   void apply(const data::data_equation& x)
     661             :   {
     662             :     static_cast<Derived&>(*this).enter(x);
     663             :     static_cast<Derived&>(*this).apply(x.variables());
     664             :     static_cast<Derived&>(*this).apply(x.condition());
     665             :     static_cast<Derived&>(*this).apply(x.lhs());
     666             :     static_cast<Derived&>(*this).apply(x.rhs());
     667             :     static_cast<Derived&>(*this).leave(x);
     668             :   }
     669             : 
     670           0 :   void apply(const data::untyped_data_parameter& x)
     671             :   {
     672           0 :     static_cast<Derived&>(*this).enter(x);
     673           0 :     static_cast<Derived&>(*this).apply(x.arguments());
     674           0 :     static_cast<Derived&>(*this).leave(x);
     675           0 :   }
     676             : 
     677     6062497 :   void apply(const data::data_expression& x)
     678             :   {
     679     6062497 :     static_cast<Derived&>(*this).enter(x);
     680     6062497 :     if (data::is_abstraction(x))
     681             :     {
     682        5064 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::abstraction>(x));
     683             :     }
     684     6057433 :     else if (data::is_variable(x))
     685             :     {
     686     2014421 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     687             :     }
     688     4043012 :     else if (data::is_function_symbol(x))
     689             :     {
     690     2290569 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_symbol>(x));
     691             :     }
     692     1752443 :     else if (data::is_application(x))
     693             :     {
     694     1752434 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::application>(x));
     695             :     }
     696           9 :     else if (data::is_where_clause(x))
     697             :     {
     698           9 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::where_clause>(x));
     699             :     }
     700           0 :     else if (data::is_untyped_identifier(x))
     701             :     {
     702           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier>(x));
     703             :     }
     704     6062497 :     static_cast<Derived&>(*this).leave(x);
     705     6062497 :   }
     706             : 
     707           9 :   void apply(const data::assignment_expression& x)
     708             :   {
     709           9 :     static_cast<Derived&>(*this).enter(x);
     710           9 :     if (data::is_assignment(x))
     711             :     {
     712           9 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::assignment>(x));
     713             :     }
     714           0 :     else if (data::is_untyped_identifier_assignment(x))
     715             :     {
     716           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier_assignment>(x));
     717             :     }
     718           9 :     static_cast<Derived&>(*this).leave(x);
     719           9 :   }
     720             : 
     721        5064 :   void apply(const data::abstraction& x)
     722             :   {
     723        5064 :     static_cast<Derived&>(*this).enter(x);
     724        5064 :     if (data::is_forall(x))
     725             :     {
     726        4912 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::forall>(x));
     727             :     }
     728         152 :     else if (data::is_exists(x))
     729             :     {
     730           6 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::exists>(x));
     731             :     }
     732         146 :     else if (data::is_lambda(x))
     733             :     {
     734         146 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::lambda>(x));
     735             :     }
     736           0 :     else if (data::is_set_comprehension(x))
     737             :     {
     738           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::set_comprehension>(x));
     739             :     }
     740           0 :     else if (data::is_bag_comprehension(x))
     741             :     {
     742           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::bag_comprehension>(x));
     743             :     }
     744           0 :     else if (data::is_untyped_set_or_bag_comprehension(x))
     745             :     {
     746           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
     747             :     }
     748        5064 :     static_cast<Derived&>(*this).leave(x);
     749        5064 :   }
     750             : 
     751             : };
     752             : 
     753             : /// \\brief Traverser class
     754             : template <typename Derived>
     755             : struct variable_traverser: public add_traverser_variables<core::traverser, Derived>
     756             : {
     757             : };
     758             : //--- end generated add_traverser_variables code ---//
     759             : 
     760             : //--- start generated add_traverser_identifier_strings code ---//
     761             : template <template <class> class Traverser, class Derived>
     762             : struct add_traverser_identifier_strings: public Traverser<Derived>
     763             : {
     764             :   typedef Traverser<Derived> super;
     765             :   using super::enter;
     766             :   using super::leave;
     767             :   using super::apply;
     768             : 
     769     1747657 :   void apply(const data::variable& x)
     770             :   {
     771     1747657 :     static_cast<Derived&>(*this).enter(x);
     772     1747657 :     static_cast<Derived&>(*this).apply(x.name());
     773     1747657 :     static_cast<Derived&>(*this).apply(x.sort());
     774     1747657 :     static_cast<Derived&>(*this).leave(x);
     775     1747657 :   }
     776             : 
     777     1909603 :   void apply(const data::function_symbol& x)
     778             :   {
     779     1909603 :     static_cast<Derived&>(*this).enter(x);
     780     1909603 :     static_cast<Derived&>(*this).apply(x.name());
     781     1909603 :     static_cast<Derived&>(*this).apply(x.sort());
     782     1909603 :     static_cast<Derived&>(*this).leave(x);
     783     1909603 :   }
     784             : 
     785     1125949 :   void apply(const data::application& x)
     786             :   {
     787     1125949 :     static_cast<Derived&>(*this).enter(x);
     788     1125949 :     static_cast<Derived&>(*this).apply(x.head());
     789     4225436 :     for (const data_expression& t: x) { static_cast<Derived&>(*this).apply(t); }
     790     1125949 :     static_cast<Derived&>(*this).leave(x);
     791     1125949 :   }
     792             : 
     793          21 :   void apply(const data::where_clause& x)
     794             :   {
     795          21 :     static_cast<Derived&>(*this).enter(x);
     796          21 :     static_cast<Derived&>(*this).apply(x.body());
     797          21 :     static_cast<Derived&>(*this).apply(x.declarations());
     798          21 :     static_cast<Derived&>(*this).leave(x);
     799          21 :   }
     800             : 
     801           0 :   void apply(const data::untyped_identifier& x)
     802             :   {
     803           0 :     static_cast<Derived&>(*this).enter(x);
     804           0 :     static_cast<Derived&>(*this).apply(x.name());
     805           0 :     static_cast<Derived&>(*this).leave(x);
     806           0 :   }
     807             : 
     808       15351 :   void apply(const data::assignment& x)
     809             :   {
     810       15351 :     static_cast<Derived&>(*this).enter(x);
     811       15351 :     static_cast<Derived&>(*this).apply(x.lhs());
     812       15351 :     static_cast<Derived&>(*this).apply(x.rhs());
     813       15351 :     static_cast<Derived&>(*this).leave(x);
     814       15351 :   }
     815             : 
     816           0 :   void apply(const data::untyped_identifier_assignment& x)
     817             :   {
     818           0 :     static_cast<Derived&>(*this).enter(x);
     819           0 :     static_cast<Derived&>(*this).apply(x.lhs());
     820           0 :     static_cast<Derived&>(*this).apply(x.rhs());
     821           0 :     static_cast<Derived&>(*this).leave(x);
     822           0 :   }
     823             : 
     824     6226103 :   void apply(const data::basic_sort& x)
     825             :   {
     826     6226103 :     static_cast<Derived&>(*this).enter(x);
     827     6226103 :     static_cast<Derived&>(*this).apply(x.name());
     828     6226103 :     static_cast<Derived&>(*this).leave(x);
     829     6226103 :   }
     830             : 
     831       98514 :   void apply(const data::container_sort& x)
     832             :   {
     833       98514 :     static_cast<Derived&>(*this).enter(x);
     834       98514 :     static_cast<Derived&>(*this).apply(x.element_sort());
     835       98514 :     static_cast<Derived&>(*this).leave(x);
     836       98514 :   }
     837             : 
     838         863 :   void apply(const data::structured_sort& x)
     839             :   {
     840         863 :     static_cast<Derived&>(*this).enter(x);
     841         863 :     static_cast<Derived&>(*this).apply(x.constructors());
     842         863 :     static_cast<Derived&>(*this).leave(x);
     843         863 :   }
     844             : 
     845     1488298 :   void apply(const data::function_sort& x)
     846             :   {
     847     1488298 :     static_cast<Derived&>(*this).enter(x);
     848     1488298 :     static_cast<Derived&>(*this).apply(x.domain());
     849     1488298 :     static_cast<Derived&>(*this).apply(x.codomain());
     850     1488298 :     static_cast<Derived&>(*this).leave(x);
     851     1488298 :   }
     852             : 
     853           0 :   void apply(const data::untyped_sort& x)
     854             :   {
     855           0 :     static_cast<Derived&>(*this).enter(x);
     856             :     // skip
     857           0 :     static_cast<Derived&>(*this).leave(x);
     858           0 :   }
     859             : 
     860           0 :   void apply(const data::untyped_possible_sorts& x)
     861             :   {
     862           0 :     static_cast<Derived&>(*this).enter(x);
     863           0 :     static_cast<Derived&>(*this).apply(x.sorts());
     864           0 :     static_cast<Derived&>(*this).leave(x);
     865           0 :   }
     866             : 
     867           0 :   void apply(const data::untyped_sort_variable& x)
     868             :   {
     869           0 :     static_cast<Derived&>(*this).enter(x);
     870             :     // skip
     871           0 :     static_cast<Derived&>(*this).leave(x);
     872           0 :   }
     873             : 
     874        1727 :   void apply(const data::forall& x)
     875             :   {
     876        1727 :     static_cast<Derived&>(*this).enter(x);
     877        1727 :     static_cast<Derived&>(*this).apply(x.variables());
     878        1727 :     static_cast<Derived&>(*this).apply(x.body());
     879        1727 :     static_cast<Derived&>(*this).leave(x);
     880        1727 :   }
     881             : 
     882           0 :   void apply(const data::exists& x)
     883             :   {
     884           0 :     static_cast<Derived&>(*this).enter(x);
     885           0 :     static_cast<Derived&>(*this).apply(x.variables());
     886           0 :     static_cast<Derived&>(*this).apply(x.body());
     887           0 :     static_cast<Derived&>(*this).leave(x);
     888           0 :   }
     889             : 
     890          54 :   void apply(const data::lambda& x)
     891             :   {
     892          54 :     static_cast<Derived&>(*this).enter(x);
     893          54 :     static_cast<Derived&>(*this).apply(x.variables());
     894          54 :     static_cast<Derived&>(*this).apply(x.body());
     895          54 :     static_cast<Derived&>(*this).leave(x);
     896          54 :   }
     897             : 
     898           0 :   void apply(const data::set_comprehension& x)
     899             :   {
     900           0 :     static_cast<Derived&>(*this).enter(x);
     901           0 :     static_cast<Derived&>(*this).apply(x.variables());
     902           0 :     static_cast<Derived&>(*this).apply(x.body());
     903           0 :     static_cast<Derived&>(*this).leave(x);
     904           0 :   }
     905             : 
     906           0 :   void apply(const data::bag_comprehension& x)
     907             :   {
     908           0 :     static_cast<Derived&>(*this).enter(x);
     909           0 :     static_cast<Derived&>(*this).apply(x.variables());
     910           0 :     static_cast<Derived&>(*this).apply(x.body());
     911           0 :     static_cast<Derived&>(*this).leave(x);
     912           0 :   }
     913             : 
     914           0 :   void apply(const data::untyped_set_or_bag_comprehension& x)
     915             :   {
     916           0 :     static_cast<Derived&>(*this).enter(x);
     917           0 :     static_cast<Derived&>(*this).apply(x.variables());
     918           0 :     static_cast<Derived&>(*this).apply(x.body());
     919           0 :     static_cast<Derived&>(*this).leave(x);
     920           0 :   }
     921             : 
     922          62 :   void apply(const data::structured_sort_constructor_argument& x)
     923             :   {
     924          62 :     static_cast<Derived&>(*this).enter(x);
     925          62 :     static_cast<Derived&>(*this).apply(x.name());
     926          62 :     static_cast<Derived&>(*this).apply(x.sort());
     927          62 :     static_cast<Derived&>(*this).leave(x);
     928          62 :   }
     929             : 
     930        1674 :   void apply(const data::structured_sort_constructor& x)
     931             :   {
     932        1674 :     static_cast<Derived&>(*this).enter(x);
     933        1674 :     static_cast<Derived&>(*this).apply(x.name());
     934        1674 :     static_cast<Derived&>(*this).apply(x.arguments());
     935        1674 :     static_cast<Derived&>(*this).apply(x.recogniser());
     936        1674 :     static_cast<Derived&>(*this).leave(x);
     937        1674 :   }
     938             : 
     939         258 :   void apply(const data::alias& x)
     940             :   {
     941         258 :     static_cast<Derived&>(*this).enter(x);
     942         258 :     static_cast<Derived&>(*this).apply(x.name());
     943         258 :     static_cast<Derived&>(*this).apply(x.reference());
     944         258 :     static_cast<Derived&>(*this).leave(x);
     945         258 :   }
     946             : 
     947      308305 :   void apply(const data::data_equation& x)
     948             :   {
     949      308305 :     static_cast<Derived&>(*this).enter(x);
     950      308305 :     static_cast<Derived&>(*this).apply(x.variables());
     951      308305 :     static_cast<Derived&>(*this).apply(x.condition());
     952      308305 :     static_cast<Derived&>(*this).apply(x.lhs());
     953      308305 :     static_cast<Derived&>(*this).apply(x.rhs());
     954      308305 :     static_cast<Derived&>(*this).leave(x);
     955      308305 :   }
     956             : 
     957           0 :   void apply(const data::untyped_data_parameter& x)
     958             :   {
     959           0 :     static_cast<Derived&>(*this).enter(x);
     960           0 :     static_cast<Derived&>(*this).apply(x.name());
     961           0 :     static_cast<Derived&>(*this).apply(x.arguments());
     962           0 :     static_cast<Derived&>(*this).leave(x);
     963           0 :   }
     964             : 
     965     4066622 :   void apply(const data::data_expression& x)
     966             :   {
     967     4066622 :     static_cast<Derived&>(*this).enter(x);
     968     4066622 :     if (data::is_abstraction(x))
     969             :     {
     970        1781 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::abstraction>(x));
     971             :     }
     972     4064841 :     else if (data::is_variable(x))
     973             :     {
     974     1176929 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     975             :     }
     976     2887912 :     else if (data::is_function_symbol(x))
     977             :     {
     978     1761942 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_symbol>(x));
     979             :     }
     980     1125970 :     else if (data::is_application(x))
     981             :     {
     982     1125949 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::application>(x));
     983             :     }
     984          21 :     else if (data::is_where_clause(x))
     985             :     {
     986          21 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::where_clause>(x));
     987             :     }
     988           0 :     else if (data::is_untyped_identifier(x))
     989             :     {
     990           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier>(x));
     991             :     }
     992     4066622 :     static_cast<Derived&>(*this).leave(x);
     993     4066622 :   }
     994             : 
     995          22 :   void apply(const data::assignment_expression& x)
     996             :   {
     997          22 :     static_cast<Derived&>(*this).enter(x);
     998          22 :     if (data::is_assignment(x))
     999             :     {
    1000          22 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::assignment>(x));
    1001             :     }
    1002           0 :     else if (data::is_untyped_identifier_assignment(x))
    1003             :     {
    1004           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_identifier_assignment>(x));
    1005             :     }
    1006          22 :     static_cast<Derived&>(*this).leave(x);
    1007          22 :   }
    1008             : 
    1009     7813520 :   void apply(const data::sort_expression& x)
    1010             :   {
    1011     7813520 :     static_cast<Derived&>(*this).enter(x);
    1012     7813520 :     if (data::is_basic_sort(x))
    1013             :     {
    1014     6225845 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::basic_sort>(x));
    1015             :     }
    1016     1587675 :     else if (data::is_container_sort(x))
    1017             :     {
    1018       98514 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::container_sort>(x));
    1019             :     }
    1020     1489161 :     else if (data::is_structured_sort(x))
    1021             :     {
    1022         863 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::structured_sort>(x));
    1023             :     }
    1024     1488298 :     else if (data::is_function_sort(x))
    1025             :     {
    1026     1488298 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::function_sort>(x));
    1027             :     }
    1028           0 :     else if (data::is_untyped_sort(x))
    1029             :     {
    1030           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_sort>(x));
    1031             :     }
    1032           0 :     else if (data::is_untyped_possible_sorts(x))
    1033             :     {
    1034           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_possible_sorts>(x));
    1035             :     }
    1036           0 :     else if (data::is_untyped_sort_variable(x))
    1037             :     {
    1038           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_sort_variable>(x));
    1039             :     }
    1040     7813520 :     static_cast<Derived&>(*this).leave(x);
    1041     7813520 :   }
    1042             : 
    1043        1781 :   void apply(const data::abstraction& x)
    1044             :   {
    1045        1781 :     static_cast<Derived&>(*this).enter(x);
    1046        1781 :     if (data::is_forall(x))
    1047             :     {
    1048        1727 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::forall>(x));
    1049             :     }
    1050          54 :     else if (data::is_exists(x))
    1051             :     {
    1052           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::exists>(x));
    1053             :     }
    1054          54 :     else if (data::is_lambda(x))
    1055             :     {
    1056          54 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::lambda>(x));
    1057             :     }
    1058           0 :     else if (data::is_set_comprehension(x))
    1059             :     {
    1060           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::set_comprehension>(x));
    1061             :     }
    1062           0 :     else if (data::is_bag_comprehension(x))
    1063             :     {
    1064           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::bag_comprehension>(x));
    1065             :     }
    1066           0 :     else if (data::is_untyped_set_or_bag_comprehension(x))
    1067             :     {
    1068           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
    1069             :     }
    1070        1781 :     static_cast<Derived&>(*this).leave(x);
    1071        1781 :   }
    1072             : 
    1073             : };
    1074             : 
    1075             : /// \\brief Traverser class
    1076             : template <typename Derived>
    1077             : struct identifier_string_traverser: public add_traverser_identifier_strings<core::traverser, Derived>
    1078             : {
    1079             : };
    1080             : //--- end generated add_traverser_identifier_strings code ---//
    1081             : 
    1082             : } // namespace data
    1083             : 
    1084             : } // namespace mcrl2
    1085             : 
    1086             : #endif // MCRL2_DATA_TRAVERSER_H