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
|
#include "PrintVisitor.hpp"
|
27
|
#include <ast/identifiers/MainModule.hpp>
|
28
|
#include <ast/types/IntType.hpp>
|
29
|
#include <ast/identifiers/EnumIdentifier.hpp>
|
30
|
#include <ast/types/EnumType.hpp>
|
31
|
#include <ast/types/ListType.hpp>
|
32
|
#include <ast/types/TupleType.hpp>
|
33
|
#include <ast/types/ActionSystemType.hpp>
|
34
|
#include <ast/identifiers/AttributeIdentifier.hpp>
|
35
|
#include <ast/expressions/ValueExpression.hpp>
|
36
|
#include <ast/statements/Assignment.hpp>
|
37
|
#include <ast/expressions/AccessExpression.hpp>
|
38
|
#include <ast/expressions/TypeExpression.hpp>
|
39
|
#include <ast/expressions/BinaryOperator.hpp>
|
40
|
#include <ast/expressions/UnaryOperator.hpp>
|
41
|
#include <ast/expressions/CallExpression.hpp>
|
42
|
#include <ast/expressions/TupleMapAccessExpression.hpp>
|
43
|
#include <ast/expressions/TupleConstructor.hpp>
|
44
|
#include <ast/expressions/ListConstructor.hpp>
|
45
|
#include <ast/statements/NondetBlock.hpp>
|
46
|
#include <ast/statements/PrioBlock.hpp>
|
47
|
#include <ast/statements/SeqBlock.hpp>
|
48
|
#include <ast/statements/Call.hpp>
|
49
|
#include <ast/statements/GuardedCommand.hpp>
|
50
|
#include <ast/expressions/IdentifierExpression.hpp>
|
51
|
#include <ast/identifiers/IdentifierBlock.hpp>
|
52
|
#include <ast/statements/Skip.hpp>
|
53
|
#include <ast/expressions/TernaryOperator.hpp>
|
54
|
#include <ast/identifiers/NamedActionIdentifier.hpp>
|
55
|
#include <ast/identifiers/MethodIdentifier.hpp>
|
56
|
#include <ast/types/FunctionType.hpp>
|
57
|
#include <ast/identifiers/NamedActionIdentifier.hpp>
|
58
|
#include <ast/expressions/SetConstructor.hpp>
|
59
|
#include <ast/identifiers/ExpressionVariableIdentifier.hpp>
|
60
|
#include <ast/expressions/ObjectConstructor.hpp>
|
61
|
#include <ast/types/NullType.hpp>
|
62
|
#include <ast/types/PointerType.hpp>
|
63
|
#include <map>
|
64
|
#include <base/CdtFixes.hpp>
|
65
|
#include <cassert>
|
66
|
|
67
|
namespace Ast {
|
68
|
|
69
|
PrintVisitor::PrintVisitor(CallContext* context):
|
70
|
CompleteAstTraversalVisitor(context, false),
|
71
|
m_writeTypes (true),
|
72
|
m_output (),
|
73
|
m_currentTypeDef (nullptr)
|
74
|
{}
|
75
|
|
76
|
PrintVisitor::~PrintVisitor() {
|
77
|
}
|
78
|
|
79
|
template<typename T>
|
80
|
void PrintVisitor::printSubElementOrNull(T* anElem)
|
81
|
{
|
82
|
if (anElem == nullptr)
|
83
|
m_output.append("<null>");
|
84
|
else
|
85
|
anElem->accept(*this);
|
86
|
}
|
87
|
|
88
|
|
89
|
|
90
|
void PrintVisitor::printType(Type* atype, const std::function<void()>& anAction)
|
91
|
{
|
92
|
|
93
|
|
94
|
if ( (atype->identifier() != nullptr)
|
95
|
&& (!atype->isAnonymousType())
|
96
|
&& (m_currentTypeDef != atype->identifier() || !m_writeTypes))
|
97
|
{
|
98
|
bool write = m_writeTypes;
|
99
|
m_writeTypes = false;
|
100
|
atype->identifier()->accept(*this);
|
101
|
m_writeTypes = write;
|
102
|
}
|
103
|
else
|
104
|
anAction();
|
105
|
}
|
106
|
|
107
|
void PrintVisitor::visit(MainModule* mainModule)
|
108
|
{
|
109
|
int i = 0;
|
110
|
|
111
|
m_writeTypes = true;
|
112
|
m_output.incIndent();
|
113
|
m_output.appendLine("types");
|
114
|
for (auto& type: *mainModule->symbolTable())
|
115
|
{
|
116
|
if (type.second->kind() != IdentifierKind::TypeIdentifier)
|
117
|
continue;
|
118
|
|
119
|
if (i != 0)
|
120
|
m_output.appendLine(";");
|
121
|
i++;
|
122
|
type.second->accept(*this);
|
123
|
}
|
124
|
|
125
|
m_output.decIndent();
|
126
|
m_output.appendLine("");
|
127
|
m_output.incIndent();
|
128
|
m_output.incIndent();
|
129
|
m_output.appendLine("system");
|
130
|
m_writeTypes = false;
|
131
|
|
132
|
|
133
|
mainModule->systemDescription()->accept(*this);
|
134
|
|
135
|
if (mainModule->getMainFunction() != nullptr) {
|
136
|
m_output.appendLine("# Automatically generated main function:");
|
137
|
mainModule->getMainFunction()->accept(*this);
|
138
|
}
|
139
|
}
|
140
|
|
141
|
void PrintVisitor::visit(TypeIdentifier* typeIdentifier)
|
142
|
{
|
143
|
m_output.append(typeIdentifier->tokenText());
|
144
|
if (m_writeTypes)
|
145
|
{
|
146
|
m_currentTypeDef = typeIdentifier;
|
147
|
m_output.append(" = ");
|
148
|
printSubElementOrNull(typeIdentifier->type());
|
149
|
}
|
150
|
}
|
151
|
|
152
|
void PrintVisitor::visit(BoolType* )
|
153
|
{
|
154
|
m_output.append("bool");
|
155
|
}
|
156
|
|
157
|
|
158
|
|
159
|
|
160
|
|
161
|
|
162
|
|
163
|
|
164
|
void PrintVisitor::visit(IntType* intType)
|
165
|
{
|
166
|
printType(intType, [&](){
|
167
|
m_output.append("int [");
|
168
|
m_output.append(intType->rangeLow());
|
169
|
m_output.append(" .. ");
|
170
|
m_output.append(intType->rangeHigh());
|
171
|
m_output.append("]");
|
172
|
});
|
173
|
}
|
174
|
|
175
|
|
176
|
|
177
|
|
178
|
|
179
|
|
180
|
|
181
|
|
182
|
|
183
|
|
184
|
|
185
|
|
186
|
|
187
|
|
188
|
|
189
|
|
190
|
|
191
|
|
192
|
void PrintVisitor::visit(EnumIdentifier* enumIdentifier)
|
193
|
{
|
194
|
m_output.append(enumIdentifier->tokenText());
|
195
|
if (enumIdentifier->haveValue())
|
196
|
m_output.append(" = " + std::to_string(enumIdentifier->value()));
|
197
|
}
|
198
|
|
199
|
template <typename T>
|
200
|
void PrintVisitor::printEnumeration(const T& arg)
|
201
|
{
|
202
|
int i = 0;
|
203
|
for (auto& sym: arg)
|
204
|
{
|
205
|
if (i != 0)
|
206
|
m_output.append(", ");
|
207
|
i++;
|
208
|
printSubElementOrNull(sym);
|
209
|
}
|
210
|
}
|
211
|
|
212
|
void PrintVisitor::visit(EnumType* enumType)
|
213
|
{
|
214
|
printType(enumType, [&]() {
|
215
|
m_output.append("{");
|
216
|
printEnumeration(enumType->listOfEnumSymbols());
|
217
|
m_output.append("}");
|
218
|
});
|
219
|
}
|
220
|
|
221
|
|
222
|
void PrintVisitor::visit(ListType* listType)
|
223
|
{
|
224
|
printType(listType, [&](){
|
225
|
m_output.append("list [");
|
226
|
m_output.append(listType->maxNumberOfElements());
|
227
|
m_output.append("] of ");
|
228
|
bool oldwrite = m_writeTypes;
|
229
|
m_writeTypes = false;
|
230
|
printSubElementOrNull(listType->innerType());
|
231
|
m_writeTypes = oldwrite;
|
232
|
});
|
233
|
}
|
234
|
|
235
|
|
236
|
|
237
|
|
238
|
|
239
|
|
240
|
|
241
|
|
242
|
|
243
|
|
244
|
|
245
|
|
246
|
|
247
|
void PrintVisitor::visit(TupleType* tupleType)
|
248
|
{
|
249
|
printType(tupleType, [&](){
|
250
|
m_output.append("(");
|
251
|
bool oldwrite = m_writeTypes;
|
252
|
m_writeTypes = false;
|
253
|
printEnumeration(tupleType->innerTypes());
|
254
|
m_writeTypes = oldwrite;
|
255
|
m_output.append(")");
|
256
|
});
|
257
|
}
|
258
|
|
259
|
void PrintVisitor::visit(ActionSystemType* ooActionSystemType)
|
260
|
{
|
261
|
printType(ooActionSystemType, [&](){
|
262
|
if (ooActionSystemType->autoConstruction())
|
263
|
m_output.append("autocons ");
|
264
|
|
265
|
m_output.append("system ");
|
266
|
if (ooActionSystemType->baseType() != nullptr)
|
267
|
m_output.append(boost::format("(%s)") % ooActionSystemType->baseType()->identifier()->tokenText());
|
268
|
m_output.appendLine("");
|
269
|
|
270
|
m_output.incIndent();
|
271
|
m_output.appendLine("|[");
|
272
|
|
273
|
|
274
|
std::deque<AttributeIdentifier*> attrs;
|
275
|
std::deque<MethodIdentifier*> methods;
|
276
|
std::deque<NamedActionIdentifier*> namedActions;
|
277
|
|
278
|
for(auto& sym: *ooActionSystemType->symbols())
|
279
|
{
|
280
|
switch(sym.second->kind()) {
|
281
|
case IdentifierKind::AttributeIdentifier:
|
282
|
attrs.push_back((AttributeIdentifier*)sym.second);
|
283
|
break;
|
284
|
case IdentifierKind::MethodIdentifier:
|
285
|
methods.push_back((MethodIdentifier*)sym.second);
|
286
|
break;
|
287
|
case IdentifierKind::NamedActionIdentifier:
|
288
|
namedActions.push_back((NamedActionIdentifier*)sym.second);
|
289
|
break;
|
290
|
default:
|
291
|
|
292
|
break;
|
293
|
}
|
294
|
}
|
295
|
|
296
|
int i = 0;
|
297
|
if (attrs.size() > 0)
|
298
|
{
|
299
|
|
300
|
m_output.incIndent();
|
301
|
m_output.appendLine("var");
|
302
|
for (AttributeIdentifier* attr : attrs)
|
303
|
{
|
304
|
if (i != 0)
|
305
|
m_output.appendLine(";");
|
306
|
i++;
|
307
|
printSubElementOrNull(attr);
|
308
|
}
|
309
|
m_output.decIndent();
|
310
|
m_output.appendLine("");
|
311
|
}
|
312
|
bool writeTypesSave = m_writeTypes;
|
313
|
m_writeTypes = false;
|
314
|
|
315
|
i = 0;
|
316
|
if (methods.size() > 0)
|
317
|
{
|
318
|
m_output.incIndent();
|
319
|
m_output.appendLine("methods");
|
320
|
for (MethodIdentifier* method : methods)
|
321
|
{
|
322
|
if (i != 0)
|
323
|
m_output.appendLine(";");
|
324
|
i++;
|
325
|
printSubElementOrNull(method);
|
326
|
}
|
327
|
m_output.decIndent();
|
328
|
m_output.appendLine("");
|
329
|
}
|
330
|
|
331
|
i = 0;
|
332
|
if (namedActions.size() > 0)
|
333
|
{
|
334
|
m_output.incIndent();
|
335
|
m_output.appendLine("actions");
|
336
|
for (NamedActionIdentifier* action: namedActions)
|
337
|
{
|
338
|
if (i != 0)
|
339
|
m_output.appendLine(";");
|
340
|
i++;
|
341
|
printSubElementOrNull(action);
|
342
|
}
|
343
|
m_output.decIndent();
|
344
|
m_output.appendLine("");
|
345
|
}
|
346
|
|
347
|
if ((ooActionSystemType->doodBlock() != nullptr) &&
|
348
|
(ooActionSystemType->doodBlock()->statements().size() > 0))
|
349
|
{
|
350
|
m_output.incIndent();
|
351
|
m_output.appendLine("do");
|
352
|
printSubElementOrNull(ooActionSystemType->doodBlock());
|
353
|
m_output.decIndent();
|
354
|
m_output.appendLine("");
|
355
|
m_output.appendLine("od");
|
356
|
}
|
357
|
m_output.decIndent();
|
358
|
m_output.appendLine("");
|
359
|
m_output.append("]|");
|
360
|
m_writeTypes = writeTypesSave;
|
361
|
});
|
362
|
}
|
363
|
|
364
|
void PrintVisitor::visit(NullType* )
|
365
|
{
|
366
|
m_output.append("nil");
|
367
|
}
|
368
|
|
369
|
void PrintVisitor::visit(PointerType* )
|
370
|
{
|
371
|
m_output.append("<somePointer>");
|
372
|
}
|
373
|
|
374
|
|
375
|
void PrintVisitor::visit(AttributeIdentifier* attributeIdentifier)
|
376
|
{
|
377
|
if (attributeIdentifier->isStatic())
|
378
|
m_output.append("static ");
|
379
|
if (attributeIdentifier->isObservable())
|
380
|
m_output.append("obs ");
|
381
|
if (attributeIdentifier->isControllable())
|
382
|
m_output.append("ctr ");
|
383
|
|
384
|
m_output.append(attributeIdentifier->tokenText());
|
385
|
if (m_writeTypes)
|
386
|
{
|
387
|
m_output.append(": ");
|
388
|
assert(m_writeTypes == true);
|
389
|
m_writeTypes = false;
|
390
|
printSubElementOrNull(attributeIdentifier->type());
|
391
|
m_writeTypes = true;
|
392
|
m_output.append(" = ");
|
393
|
printSubElementOrNull(attributeIdentifier->initializer());
|
394
|
}
|
395
|
}
|
396
|
|
397
|
void PrintVisitor::visit(BoolValueExpression* valueExpression){
|
398
|
m_output.append(std::to_string(valueExpression->value()));
|
399
|
}
|
400
|
|
401
|
void PrintVisitor::visit(IntValueExpression* valueExpression){
|
402
|
m_output.append(std::to_string(valueExpression->value()));
|
403
|
}
|
404
|
|
405
|
void PrintVisitor::visit(RefValueExpression* valueExpression){
|
406
|
if (valueExpression->value() != nullptr)
|
407
|
m_output.append((std::int64_t)valueExpression->value());
|
408
|
else
|
409
|
m_output.append("nil");
|
410
|
}
|
411
|
|
412
|
|
413
|
|
414
|
|
415
|
|
416
|
|
417
|
void PrintVisitor::visit(Assignment* assignment)
|
418
|
{
|
419
|
printEnumeration(assignment->places());
|
420
|
m_output.append(" := ");
|
421
|
printEnumeration(assignment->values());
|
422
|
if (assignment->nondetExpression() != nullptr)
|
423
|
{
|
424
|
m_output.incIndent();
|
425
|
m_output.appendLine("");
|
426
|
m_output.append("with ");
|
427
|
assignment->nondetExpression()->accept(*this);
|
428
|
|
429
|
if (assignment->symbols()->size() > 0)
|
430
|
{
|
431
|
m_output.append(" /* vars: ");
|
432
|
for (auto& localVar: *assignment->symbols())
|
433
|
{
|
434
|
localVar.second->accept(*this);
|
435
|
m_output.append(" ");
|
436
|
}
|
437
|
m_output.append("*/");
|
438
|
}
|
439
|
m_output.decIndent();
|
440
|
m_output.appendLine("");
|
441
|
}
|
442
|
}
|
443
|
|
444
|
|
445
|
|
446
|
|
447
|
|
448
|
|
449
|
|
450
|
|
451
|
void PrintVisitor::visit(AccessExpression* accessExpression)
|
452
|
{
|
453
|
if (accessExpression->right() != nullptr)
|
454
|
{
|
455
|
m_output.append("(");
|
456
|
printSubElementOrNull(accessExpression->left());
|
457
|
m_output.append(").");
|
458
|
printSubElementOrNull(accessExpression->right());
|
459
|
} else {
|
460
|
m_output.append("(");
|
461
|
printSubElementOrNull(accessExpression->left());
|
462
|
m_output.append(")");
|
463
|
}
|
464
|
}
|
465
|
|
466
|
static std::map<ExpressionKind, const char*> opMap = {
|
467
|
{ ExpressionKind::conditional, "ternIf" },
|
468
|
{ ExpressionKind::domresby, "domresby"},
|
469
|
{ ExpressionKind::domresto, "domresto"},
|
470
|
{ ExpressionKind::rngresby, "rngresby"},
|
471
|
{ ExpressionKind::rngresto, "rngresto"},
|
472
|
{ ExpressionKind::munion, "munion"},
|
473
|
{ ExpressionKind::conc, "conc"},
|
474
|
{ ExpressionKind::diff, "diff"},
|
475
|
{ ExpressionKind::inter, "inter"},
|
476
|
{ ExpressionKind::elemin, "elemin"},
|
477
|
{ ExpressionKind::notelemin, "notelemin"},
|
478
|
{ ExpressionKind::subset, "subset"},
|
479
|
{ ExpressionKind::_union, "union"},
|
480
|
{ ExpressionKind::div, "div"},
|
481
|
{ ExpressionKind::greater, ">"},
|
482
|
{ ExpressionKind::greaterequal, ">="},
|
483
|
{ ExpressionKind::idiv, "idiv"},
|
484
|
{ ExpressionKind::less, "<"},
|
485
|
{ ExpressionKind::lessequal, "<="},
|
486
|
{ ExpressionKind::minus, "-"},
|
487
|
{ ExpressionKind::mod, "mod"},
|
488
|
{ ExpressionKind::pow, "pow"},
|
489
|
{ ExpressionKind::prod, "*"},
|
490
|
{ ExpressionKind::sum, "+"},
|
491
|
{ ExpressionKind::_and, "and"},
|
492
|
{ ExpressionKind::biimplies, "<=>"},
|
493
|
{ ExpressionKind::implies, "=>"},
|
494
|
{ ExpressionKind::_or, "or"},
|
495
|
{ ExpressionKind::equal, "="},
|
496
|
{ ExpressionKind::notequal, "<>"},
|
497
|
{ ExpressionKind::seqmod_mapoverride, "seqmod_mapoverride"},
|
498
|
{ ExpressionKind::dom, "dom"},
|
499
|
{ ExpressionKind::range, "range"},
|
500
|
{ ExpressionKind::merge, "merge"},
|
501
|
{ ExpressionKind::card, "card"},
|
502
|
{ ExpressionKind::dconc, "dconc"},
|
503
|
{ ExpressionKind::dinter, "dinter"},
|
504
|
{ ExpressionKind::dunion, "dunion"},
|
505
|
{ ExpressionKind::elems, "elems"},
|
506
|
{ ExpressionKind::head, "head"},
|
507
|
{ ExpressionKind::inds, "inds"},
|
508
|
{ ExpressionKind::len, "len"},
|
509
|
{ ExpressionKind::tail, "tail"},
|
510
|
{ ExpressionKind::unminus, "-"},
|
511
|
{ ExpressionKind::unplus, "+"},
|
512
|
{ ExpressionKind::_not, "not"},
|
513
|
{ ExpressionKind::abs, "abs"},
|
514
|
{ ExpressionKind::forall, "forall"},
|
515
|
{ ExpressionKind::exists, "exists"},
|
516
|
{ ExpressionKind::ListConstr, "listconstr"},
|
517
|
{ ExpressionKind::SetConstr, "setconstr"},
|
518
|
{ ExpressionKind::MapConstr, "mapconstr"},
|
519
|
{ ExpressionKind::TupleConstr, "tupleconstr"},
|
520
|
{ ExpressionKind::ObjectConstr, "objectconstr"},
|
521
|
{ ExpressionKind::QValConstr, "qvalconstr"},
|
522
|
{ ExpressionKind::Identifier, "identifier"},
|
523
|
{ ExpressionKind::UnresolvedIdentifier, "unresId"},
|
524
|
{ ExpressionKind::Type, "type"},
|
525
|
{ ExpressionKind::TupleMapAccess, "tuplemapaccess"},
|
526
|
{ ExpressionKind::Call, "call"},
|
527
|
{ ExpressionKind::Access, "."},
|
528
|
{ ExpressionKind::Primed, "'"},
|
529
|
{ ExpressionKind::Cast, "cast"},
|
530
|
{ ExpressionKind::foldLR, "foldLR"},
|
531
|
{ ExpressionKind::foldRL, "foldRL"},
|
532
|
{ ExpressionKind::Value_Integer, "value_int"},
|
533
|
{ ExpressionKind::Value_Bool, "value_bool"},
|
534
|
{ ExpressionKind::Value_Reference, "value_ref"}
|
535
|
};
|
536
|
|
537
|
|
538
|
void PrintVisitor::printOperator(Expression* expression)
|
539
|
{
|
540
|
ExpressionKind kind = expression->kind();
|
541
|
if (kind == ::Ast::ExpressionKind::Cast) {
|
542
|
m_output.append("(");
|
543
|
if (expression->type() != nullptr)
|
544
|
m_output.append(expression->type()->toString());
|
545
|
else
|
546
|
m_output.append("Cast??");
|
547
|
m_output.append(")");
|
548
|
} else if (opMap.count(kind) > 0) {
|
549
|
m_output.append(opMap[kind]);
|
550
|
} else {
|
551
|
m_context->logError("Internal error. Unknown operation: " + std::to_string((std::uint64_t)expression->kind()));
|
552
|
abort();
|
553
|
}
|
554
|
}
|
555
|
|
556
|
void PrintVisitor::visit(TypeExpression* typeExpression)
|
557
|
{
|
558
|
printSubElementOrNull(typeExpression->type());
|
559
|
}
|
560
|
|
561
|
void PrintVisitor::visit(BinaryOperator* binaryOperator)
|
562
|
{
|
563
|
m_output.incIndent();
|
564
|
m_output.appendLine("(");
|
565
|
printSubElementOrNull(binaryOperator->left());
|
566
|
m_output.decIndent();
|
567
|
m_output.appendLine("");
|
568
|
m_output.appendLine(")");
|
569
|
|
570
|
printOperator(binaryOperator);
|
571
|
m_output.appendLine("");
|
572
|
|
573
|
m_output.incIndent();
|
574
|
m_output.appendLine("(");
|
575
|
printSubElementOrNull(binaryOperator->right());
|
576
|
m_output.decIndent();
|
577
|
m_output.appendLine("");
|
578
|
m_output.appendLine(")");
|
579
|
}
|
580
|
|
581
|
void PrintVisitor::visit(UnaryOperator* unaryOperator)
|
582
|
{
|
583
|
printOperator(unaryOperator);
|
584
|
m_output.append("(");
|
585
|
printSubElementOrNull(unaryOperator->child());
|
586
|
m_output.append(")");
|
587
|
}
|
588
|
|
589
|
void PrintVisitor::visit(CallExpression* callExpression)
|
590
|
{
|
591
|
if (callExpression->child() != nullptr)
|
592
|
callExpression->child()->accept(*this);
|
593
|
if (callExpression->arguments().size() > 0)
|
594
|
{
|
595
|
m_output.append("(");
|
596
|
printEnumeration(callExpression->arguments());
|
597
|
m_output.append(")");
|
598
|
} else {
|
599
|
m_output.append("()");
|
600
|
}
|
601
|
}
|
602
|
|
603
|
void PrintVisitor::visit(TupleMapAccessExpression* tupleMapAccessExpression)
|
604
|
{
|
605
|
if (tupleMapAccessExpression->child() != nullptr)
|
606
|
tupleMapAccessExpression->child()->accept(*this);
|
607
|
m_output.append("[");
|
608
|
printSubElementOrNull(tupleMapAccessExpression->argument());
|
609
|
m_output.append("]");
|
610
|
}
|
611
|
|
612
|
void PrintVisitor::visit(TupleConstructor* tupleConstructor)
|
613
|
{
|
614
|
m_output.append(tupleConstructor->tupleType()->tokenText());
|
615
|
m_output.append("(");
|
616
|
printEnumeration(tupleConstructor->values());
|
617
|
m_output.append(")");
|
618
|
}
|
619
|
|
620
|
void PrintVisitor::visit(ListConstructor* listConstructor)
|
621
|
{
|
622
|
m_output.append("[");
|
623
|
printEnumeration(listConstructor->elements());
|
624
|
if (listConstructor->hasComprehension())
|
625
|
{
|
626
|
m_output.append("| var ");
|
627
|
int i = 0;
|
628
|
for (auto& element: *listConstructor->comprehensionVariables())
|
629
|
{
|
630
|
if (i != 0)
|
631
|
m_output.append("; ");
|
632
|
i++;
|
633
|
printSubElementOrNull(element.second);
|
634
|
}
|
635
|
m_output.appendLine(" &");
|
636
|
printSubElementOrNull(listConstructor->comprehension());
|
637
|
}
|
638
|
m_output.append("]");
|
639
|
}
|
640
|
|
641
|
void PrintVisitor::visit(NondetBlock* nondetBlock)
|
642
|
{
|
643
|
int i = 0;
|
644
|
if (m_makeParens)
|
645
|
{
|
646
|
m_output.incIndent();
|
647
|
m_output.appendLine("(");
|
648
|
}
|
649
|
for (auto& smt: nondetBlock->statements())
|
650
|
{
|
651
|
if (i != 0)
|
652
|
{
|
653
|
m_output.decIndent();
|
654
|
m_output.appendLine("");
|
655
|
m_output.incIndent();
|
656
|
m_output.appendLine("[] ");
|
657
|
}
|
658
|
i++;
|
659
|
smt->accept(*this);
|
660
|
}
|
661
|
if (m_makeParens)
|
662
|
{
|
663
|
m_output.decIndent();
|
664
|
m_output.appendLine("");
|
665
|
m_output.appendLine(")");
|
666
|
}
|
667
|
}
|
668
|
|
669
|
void PrintVisitor::visit(PrioBlock* prioBlock)
|
670
|
{
|
671
|
int i = 0;
|
672
|
if (m_makeParens)
|
673
|
{
|
674
|
m_output.incIndent();
|
675
|
m_output.appendLine("(");
|
676
|
}
|
677
|
for (auto& smt: prioBlock->statements())
|
678
|
{
|
679
|
if (i != 0)
|
680
|
{
|
681
|
m_output.decIndent();
|
682
|
m_output.appendLine("");
|
683
|
m_output.incIndent();
|
684
|
m_output.appendLine("// ");
|
685
|
}
|
686
|
i++;
|
687
|
smt->accept(*this);
|
688
|
}
|
689
|
if (m_makeParens)
|
690
|
{
|
691
|
m_output.decIndent();
|
692
|
m_output.appendLine("");
|
693
|
m_output.appendLine(")");
|
694
|
}
|
695
|
}
|
696
|
|
697
|
void PrintVisitor::visit(SeqBlock* seqBlock)
|
698
|
{
|
699
|
int i = 0;
|
700
|
bool old_makeparens = m_makeParens;
|
701
|
m_output.incIndent();
|
702
|
m_output.appendLine("(");
|
703
|
if (seqBlock->symbols() != nullptr && seqBlock->symbols()->size() > 0)
|
704
|
{
|
705
|
m_output.append("var ");
|
706
|
for (auto& id: *seqBlock->symbols())
|
707
|
{
|
708
|
m_output.append(id.second->tokenText());
|
709
|
m_output.append(": ");
|
710
|
printSubElementOrNull(id.second);
|
711
|
}
|
712
|
m_output.append(": ");
|
713
|
}
|
714
|
for (auto& smt: seqBlock->statements())
|
715
|
{
|
716
|
if (smt == nullptr)
|
717
|
continue;
|
718
|
if (i != 0)
|
719
|
{
|
720
|
m_output.decIndent();
|
721
|
m_output.appendLine("");
|
722
|
m_output.incIndent();
|
723
|
m_output.appendLine("; ");
|
724
|
}
|
725
|
i++;
|
726
|
m_makeParens = true;
|
727
|
smt->accept(*this);
|
728
|
m_makeParens = old_makeparens;
|
729
|
}
|
730
|
m_output.decIndent();
|
731
|
m_output.appendLine("");
|
732
|
m_output.appendLine(")");
|
733
|
}
|
734
|
|
735
|
void PrintVisitor::visit(Call* call)
|
736
|
{
|
737
|
call->callExpression()->accept(*this);
|
738
|
}
|
739
|
|
740
|
void PrintVisitor::visit(GuardedCommand* guardedCommand)
|
741
|
{
|
742
|
m_output.append("requires ");
|
743
|
printSubElementOrNull(guardedCommand->guard());
|
744
|
m_output.incIndent();
|
745
|
m_output.appendLine(" :");
|
746
|
|
747
|
if (guardedCommand->body() != nullptr)
|
748
|
guardedCommand->body()->accept(*this);
|
749
|
|
750
|
m_output.decIndent();
|
751
|
m_output.appendLine("");
|
752
|
m_output.appendLine("end");
|
753
|
}
|
754
|
|
755
|
void PrintVisitor::visit(IdentifierExpression* identifierExpression)
|
756
|
{
|
757
|
m_output.append(identifierExpression->identifier()->tokenText());
|
758
|
}
|
759
|
|
760
|
void PrintVisitor::visit(NondetIdentifierBlock* nondetIdentifierList)
|
761
|
{
|
762
|
int i = 0;
|
763
|
for (auto& smt: nondetIdentifierList->identifiers())
|
764
|
{
|
765
|
if (i != 0)
|
766
|
{
|
767
|
m_output.decIndent();
|
768
|
m_output.appendLine("");
|
769
|
m_output.incIndent();
|
770
|
m_output.appendLine("[] ");
|
771
|
}
|
772
|
i++;
|
773
|
smt->accept(*this);
|
774
|
}
|
775
|
}
|
776
|
|
777
|
void PrintVisitor::visit(PrioIdentifierBlock* prioIdentifierList)
|
778
|
{
|
779
|
int i = 0;
|
780
|
for (auto& smt: prioIdentifierList->identifiers())
|
781
|
{
|
782
|
if (i != 0)
|
783
|
{
|
784
|
m_output.decIndent();
|
785
|
m_output.appendLine("");
|
786
|
m_output.incIndent();
|
787
|
m_output.appendLine("//");
|
788
|
}
|
789
|
i++;
|
790
|
smt->accept(*this);
|
791
|
}
|
792
|
}
|
793
|
|
794
|
void PrintVisitor::visit(SeqIdentifierBlock* seqIdentifierList)
|
795
|
{
|
796
|
int i = 0;
|
797
|
m_output.incIndent();
|
798
|
m_output.appendLine("(");
|
799
|
for (auto& smt: seqIdentifierList->identifiers())
|
800
|
{
|
801
|
if (i != 0)
|
802
|
m_output.appendLine("; ");
|
803
|
i++;
|
804
|
smt->accept(*this);
|
805
|
}
|
806
|
m_output.decIndent();
|
807
|
m_output.appendLine("");
|
808
|
m_output.appendLine(")");
|
809
|
}
|
810
|
|
811
|
void PrintVisitor::visit(Skip* )
|
812
|
{
|
813
|
m_output.append("skip");
|
814
|
}
|
815
|
|
816
|
void PrintVisitor::visit(TernaryOperator* ternaryOperator)
|
817
|
{
|
818
|
switch(ternaryOperator->kind()) {
|
819
|
case ExpressionKind::conditional:
|
820
|
m_output.append("if");
|
821
|
printSubElementOrNull(ternaryOperator->left());
|
822
|
m_output.incIndent();
|
823
|
m_output.appendLine("then");
|
824
|
printSubElementOrNull(ternaryOperator->mid());
|
825
|
m_output.decIndent();
|
826
|
m_output.appendLine("");
|
827
|
m_output.incIndent();
|
828
|
m_output.appendLine("else");
|
829
|
printSubElementOrNull(ternaryOperator->right());
|
830
|
m_output.decIndent();
|
831
|
m_output.appendLine("");
|
832
|
m_output.append("end");
|
833
|
break;
|
834
|
case ExpressionKind::foldLR:
|
835
|
case ExpressionKind::foldRL:
|
836
|
printSubElementOrNull(ternaryOperator->left());
|
837
|
if (ternaryOperator->mid() != nullptr)
|
838
|
{
|
839
|
m_output.append(" :: (");
|
840
|
printSubElementOrNull(ternaryOperator->mid());
|
841
|
m_output.append(")");
|
842
|
}
|
843
|
if (ternaryOperator->kind() == ExpressionKind::foldLR)
|
844
|
m_output.append(" :>: (");
|
845
|
else
|
846
|
m_output.append(" :<: (");
|
847
|
printSubElementOrNull(ternaryOperator->right());
|
848
|
m_output.append(")");
|
849
|
break;
|
850
|
default:
|
851
|
m_context->logError("Internal error. Unknown ternary operator.");
|
852
|
abort();
|
853
|
break;
|
854
|
}
|
855
|
}
|
856
|
|
857
|
void PrintVisitor::visit(MethodIdentifier* methodIdentifier)
|
858
|
{
|
859
|
bool* safe = ((FunctionType*)methodIdentifier->type())->isMiracleSafe();
|
860
|
if ( safe == nullptr || *safe == false)
|
861
|
m_output.append("/*BASIC*/ ");
|
862
|
|
863
|
|
864
|
FunctionType* atype = (FunctionType*)methodIdentifier->type();
|
865
|
|
866
|
m_output.append(methodIdentifier->tokenText());
|
867
|
m_output.append("(");
|
868
|
int j = 0;
|
869
|
for (auto& x: methodIdentifier->parameter())
|
870
|
{
|
871
|
if (j != 0)
|
872
|
m_output.append(", ");
|
873
|
else
|
874
|
j++;
|
875
|
m_output.append(x->tokenText());
|
876
|
m_output.append(": ");
|
877
|
printSubElementOrNull(x->type());
|
878
|
}
|
879
|
m_output.append(")");
|
880
|
if (atype->returnType() != nullptr)
|
881
|
{
|
882
|
m_output.append(": ");
|
883
|
printSubElementOrNull(atype->returnType());
|
884
|
}
|
885
|
m_output.appendLine("");
|
886
|
|
887
|
m_output.incIndent();
|
888
|
m_output.appendLine("var");
|
889
|
int i = 0;
|
890
|
for (auto& sym: *methodIdentifier->symbolTable())
|
891
|
{
|
892
|
if (i != 0)
|
893
|
m_output.appendLine(";");
|
894
|
i++;
|
895
|
m_output.append(sym.second->tokenText());
|
896
|
m_output.append(": ");
|
897
|
printSubElementOrNull(sym.second->type());
|
898
|
}
|
899
|
m_output.decIndent();
|
900
|
m_output.appendLine("");
|
901
|
|
902
|
printSubElementOrNull(methodIdentifier->body());
|
903
|
m_output.append("end");
|
904
|
}
|
905
|
|
906
|
void PrintVisitor::visit(NamedActionIdentifier* namedActionIdentifier)
|
907
|
{
|
908
|
bool* safe = ((FunctionType*)namedActionIdentifier->type())->isMiracleSafe();
|
909
|
if ( safe == nullptr || *safe == false)
|
910
|
m_output.append("/*BASIC*/ ");
|
911
|
|
912
|
m_output.append(namedActionIdentifier->tokenText());
|
913
|
m_output.append("(");
|
914
|
FunctionType* atype = (FunctionType*)namedActionIdentifier->type();
|
915
|
printEnumeration(atype->parameter());
|
916
|
m_output.append(")");
|
917
|
m_output.appendLine("");
|
918
|
|
919
|
m_output.incIndent();
|
920
|
m_output.appendLine("var");
|
921
|
int i = 0;
|
922
|
for (auto& sym: *namedActionIdentifier->symbolTable())
|
923
|
{
|
924
|
if (i != 0)
|
925
|
m_output.appendLine(";");
|
926
|
i++;
|
927
|
m_output.append(sym.second->tokenText());
|
928
|
m_output.append(": ");
|
929
|
printSubElementOrNull(sym.second->type());
|
930
|
}
|
931
|
m_output.decIndent();
|
932
|
m_output.appendLine("");
|
933
|
|
934
|
printSubElementOrNull(namedActionIdentifier->body());
|
935
|
m_output.append("end");
|
936
|
}
|
937
|
|
938
|
void PrintVisitor::visit(SetConstructor* setConstructor)
|
939
|
{
|
940
|
m_output.append("[");
|
941
|
printEnumeration(setConstructor->items());
|
942
|
if (setConstructor->hasComprehension())
|
943
|
{
|
944
|
m_output.append("| var ");
|
945
|
int i = 0;
|
946
|
for(auto& elem: *setConstructor->comprehensionVariables())
|
947
|
{
|
948
|
if (i != 0)
|
949
|
m_output.append("; ");
|
950
|
i++;
|
951
|
printSubElementOrNull(elem.second);
|
952
|
}
|
953
|
m_output.appendLine(" &");
|
954
|
printSubElementOrNull(setConstructor->comprehension());
|
955
|
}
|
956
|
m_output.append("]");
|
957
|
}
|
958
|
|
959
|
void PrintVisitor::visit(ExpressionVariableIdentifier* expressionVariableIdentifier)
|
960
|
{
|
961
|
m_output.append(expressionVariableIdentifier->tokenText());
|
962
|
m_output.append(": ");
|
963
|
printSubElementOrNull(expressionVariableIdentifier->type());
|
964
|
}
|
965
|
|
966
|
void PrintVisitor::visit(ObjectConstructor* objectConstructor)
|
967
|
{
|
968
|
m_output.append("new (");
|
969
|
printSubElementOrNull(objectConstructor->type());
|
970
|
m_output.append(")");
|
971
|
|
972
|
m_output.append(" //");
|
973
|
for (auto& i: objectConstructor->instances()) {
|
974
|
m_output.append(" (");
|
975
|
m_output.append(i->getName());
|
976
|
m_output.append(" parent: ");
|
977
|
m_output.append(i->getParentObject()->getName());
|
978
|
m_output.append(") ");
|
979
|
}
|
980
|
}
|
981
|
|
982
|
|
983
|
}
|