1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
|
// This example shows how static polymorphism can in principle work
// in the implementation of the find functions in the mCRL2 Library.
// See also http://en.wikipedia.org/wiki/Template_metaprogramming#Static_polymorphism
#include <iostream>
struct where_clause {};
struct function_symbol {};
struct data_expression {};
struct abstraction: public data_expression {};
struct variable: public data_expression {};
struct application: public data_expression {};
struct identifier_string {};
struct lambda {};
struct forall {};
struct exists {};
struct data_expression_with_variables {};
struct assignment {};
struct data_equation {};
struct action_label {};
struct action {};
struct deadlock {};
struct multi_action {};
struct action_summand {};
struct deadlock_summand {};
struct process_initializer {};
struct linear_process {};
struct specification {};
template <typename Derived>
class data_traverser
{
protected:
template <typename Abstraction >
void visit(Abstraction const& a)
{
static_cast<Derived& >(*this).enter(static_cast<data_expression const&>(a));
static_cast<Derived& >(*this).enter(static_cast<abstraction const&>(a));
static_cast<Derived& >(*this).enter(a);
deadlock_summand s;
static_cast<Derived& >(*this)(s);
//(*this)(a.variables());
//static_cast<Derived& >(*this)(a.body());
static_cast<Derived&>(*this).leave(a);
static_cast<Derived&>(*this).leave(static_cast<abstraction const&>(a));
static_cast<Derived&>(*this).leave(static_cast<data_expression const&>(a));
}
public:
template <typename DataExpression >
void enter(DataExpression const&)
{}
template <typename DataExpression >
void leave(DataExpression const&)
{}
void operator()(identifier_string const& e)
{
static_cast<Derived&>(*this).enter(static_cast<identifier_string const&>(e));
static_cast<Derived&>(*this).leave(static_cast<identifier_string const&>(e));
}
void operator()(function_symbol const& e)
{
static_cast<Derived&>(*this).enter(static_cast<data_expression const&>(e));
static_cast<Derived&>(*this).enter(e);
//static_cast<Derived&>(*this)(e.name());
static_cast<Derived&>(*this).leave(e);
static_cast<Derived&>(*this).leave(static_cast<data_expression const&>(e));
}
void operator()(variable const& e)
{
static_cast<Derived&>(*this).enter(static_cast<data_expression const&>(e));
static_cast<Derived&>(*this).enter(e);
//static_cast<Derived&>(*this)(e.name());
static_cast<Derived&>(*this).leave(e);
static_cast<Derived&>(*this).leave(static_cast<data_expression const&>(e));
}
void operator()(lambda const& e)
{
visit(e);
}
void operator()(forall const& e)
{
visit(e);
}
void operator()(exists const& e)
{
visit(e);
}
void operator()(abstraction const& e)
{
//if (e.is_lambda())
//{
// static_cast<Derived&>(*this)(lambda(e));
//}
//else if (e.is_exists())
//{
// static_cast<Derived&>(*this)(exists(e));
//}
//else if (e.is_forall())
//{
// static_cast<Derived&>(*this)(forall(e));
//}
}
void operator()(application const& e)
{
static_cast<Derived&>(*this).enter(static_cast<data_expression const&>(e));
static_cast<Derived&>(*this).enter(e);
//static_cast<Derived&>(*this)(e.head());
//(*this)(e.arguments());
static_cast<Derived&>(*this).leave(e);
static_cast<Derived&>(*this).leave(static_cast<data_expression const&>(e));
}
void operator()(where_clause const& e)
{
static_cast<Derived&>(*this).enter(static_cast<data_expression const&>(e));
static_cast<Derived&>(*this).enter(e);
//(*this)(e.declarations());
//static_cast<Derived&>(*this)(e.body());
static_cast<Derived&>(*this).leave(e);
static_cast<Derived&>(*this).leave(static_cast<data_expression const&>(e));
}
// Default, no traversal of sort expressions
void operator()(data_expression_with_variables const& e)
{
static_cast<Derived&>(*this)(static_cast<data_expression const&>(e));
}
// Default, no traversal of sort expressions
void operator()(data_expression const& e)
{
std::cout << "data_traverser::operator()(data_expression const& e)" << std::endl;
static_cast<Derived&>(*this).enter(e);
action_summand a;
static_cast<Derived&>(*this)(a);
static_cast<Derived&>(*this).leave(e);
//if (e.is_application())
//{
// static_cast<Derived&>(*this)(application(e));
//}
//else if (e.is_where_clause())
//{
// static_cast<Derived&>(*this)(where_clause(e));
//}
//else if (e.is_abstraction())
//{
// static_cast<Derived&>(*this)(abstraction(e));
//}
//else if (e.is_variable())
//{
// static_cast<Derived&>(*this)(variable(e));
//}
//else if (e.is_function_symbol())
//{
// static_cast<Derived&>(*this)(function_symbol(e));
//}
}
void operator()(assignment const& a)
{
static_cast<Derived&>(*this).enter(a);
//static_cast<Derived&>(*this)(a.lhs());
//static_cast<Derived&>(*this)(a.rhs());
static_cast<Derived&>(*this).leave(a);
}
void operator()(data_equation const& e)
{
static_cast<Derived&>(*this).enter(e);
//static_cast<Derived&>(*this)(e.variables());
//static_cast<Derived&>(*this)(e.condition());
//static_cast<Derived&>(*this)(e.lhs());
//static_cast<Derived&>(*this)(e.rhs());
static_cast<Derived&>(*this).leave(e);
}
//template <typename Container>
//void operator()(Container const& container, typename atermpp::detail::enable_if_container<Container>::type* = 0)
//{
// for (typename Container::const_iterator i = container.begin(); i != container.end(); ++i)
// {
// static_cast<Derived&>(*this)(*i);
// }
//}
};
template <typename Derived>
class lps_traverser: public data_traverser<Derived>
{
public:
typedef data_traverser<Derived> super;
using super::operator();
/// \brief Traverses an action label
void operator()(const action_label& l)
{
static_cast<Derived&>(*this).enter(l);
//static_cast<Derived&>(*this)(l.name());
static_cast<Derived&>(*this).leave(l);
}
/// \brief Traverses an action
/// \param a An action
void operator()(const action& a)
{
static_cast<Derived&>(*this).enter(a);
//static_cast<Derived&>(*this)(a.label());
//static_cast<Derived&>(*this)(a.arguments());
static_cast<Derived&>(*this).leave(a);
}
/// \brief Traverses a deadlock
/// \param d A deadlock
void operator()(const deadlock& d)
{
static_cast<Derived&>(*this).enter(d);
//if (d.has_time()) {
// static_cast<Derived&>(*this)(d.time());
//}
static_cast<Derived&>(*this).leave(d);
}
/// \brief Traverses a multi-action
/// \param a A multi-action
void operator()(const multi_action& a)
{
static_cast<Derived&>(*this).enter(a);
//if (a.has_time()) {
// static_cast<Derived&>(*this)(a.time());
//}
//static_cast<Derived&>(*this)(a.actions());
static_cast<Derived&>(*this).leave(a);
}
/// \brief Traverses a summand
/// \param s A summand
void operator()(const action_summand& s)
{
static_cast<Derived&>(*this).enter(s);
//static_cast<Derived&>(*this)(s.summation_variables());
//static_cast<Derived&>(*this)(s.condition());
//static_cast<Derived&>(*this)(s.multi_action());
//static_cast<Derived&>(*this)(s.assignments());
static_cast<Derived&>(*this).leave(s);
}
/// \brief Traverses a summand
/// \param s A summand
void operator()(const deadlock_summand& s)
{
static_cast<Derived&>(*this).enter(s);
//static_cast<Derived&>(*this)(s.summation_variables());
//static_cast<Derived&>(*this)(s.condition());
//static_cast<Derived&>(*this)(s.deadlock());
static_cast<Derived&>(*this).leave(s);
}
/// \brief Traverses a process_initializer
/// \param s A process_initializer
void operator()(const process_initializer& i)
{
static_cast<Derived&>(*this).enter(i);
//static_cast<Derived&>(*this)(i.assignments());
static_cast<Derived&>(*this).leave(i);
}
/// \brief Traverses a linear_process
/// \param s A linear_process
void operator()(const linear_process& p)
{
static_cast<Derived&>(*this).enter(p);
//static_cast<Derived&>(*this)(p.process_parameters());
//static_cast<Derived&>(*this)(p.action_summands());
//static_cast<Derived&>(*this)(p.deadlock_summands());
static_cast<Derived&>(*this).leave(p);
}
/// \brief Traverses a linear process specification
/// \param spec A linear process specification
void operator()(const specification& spec)
{
static_cast<Derived&>(*this).enter(spec);
//static_cast<Derived&>(*this)(spec.process());
//static_cast<Derived&>(*this)(spec.global_variables());
//static_cast<Derived&>(*this)(spec.initial_process());
//static_cast<Derived&>(*this)(spec.action_labels());
static_cast<Derived&>(*this).leave(spec);
}
};
// This could be some kind of find algorithm.
template <template <class> class Traverser>
struct instantiate: public Traverser<instantiate<Traverser> >
{
typedef Traverser<instantiate<Traverser> > super;
using super::operator();
void enter(const data_expression&)
{}
void operator()(const action_summand&)
{
std::cout << "instantiate::operator()(const action_summand&)" << std::endl;
}
};
int main()
{
instantiate<lps_traverser> f;
data_expression e;
f(e);
return 0;
}
|
