Project

General

Profile

root / trunk / compiler / cppAst / ast / PrintVisitor.cpp @ 7

1
/**
2
  *
3
  *                  OOAS Compiler - C++ AST
4
  *
5
  * Copyright 2015, AIT Austrian Institute of Technology.
6
  * All rights reserved.
7
  *
8
  * SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
9
  *
10
  * If you modify the file please update the list of contributors below to in-
11
  * clude your name. Please also stick to the coding convention of using TABs
12
  * to do the basic (block-level) indentation and spaces for anything after
13
  * that. (Enable the display of special chars and it should be pretty obvious
14
  * what this means.) Also, remove all trailing whitespace.
15
  *
16
  * Contributors:
17
  *               Willibald Krenn (AIT)
18
  *               Stephan Zimmerer (AIT)
19
  *               Christoph Czurda (AIT)
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
/*print the type identifier, or the type definition by calling the anAction delegate.*/
90
void PrintVisitor::printType(Type* atype, const std::function<void()>& anAction)
91
{
92
        //m_context->logTrace(TRACE_EXECUTOR, "Start printing type: " + atype->toString());
93

    
94
        if (   (atype->identifier() != nullptr)
95
            && (!atype->isAnonymousType())
96
            && (m_currentTypeDef != atype->identifier() || !m_writeTypes)) // ref equ.
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
        // write all types
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
        // write system description block
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
//void PrintVisitor::visit(CharType* charType)
159
//{
160
//        m_output.append("char");
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
//        @Override
176
//        public void visit(final FloatType floatType)
177
//        {
178
//                PrintType(floatType,  new Action(){
179
//                        @Override
180
//                        public void doIt() {
181
//                                m_output.append("float [");
182
//                                m_output.append(Double.toString(floatType.low()));
183
//                                m_output.append(" .. ");
184
//                                m_output.append(Double.toString(floatType.high()));
185
//                                m_output.append("] /*");
186
//                                m_output.append(Double.toString(floatType.precision()));
187
//                                m_output.append("*/");
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
//void PrintVisitor::visit(MapType* mapType)
236
//{
237
//        printType(mapType, [this, mapType](){
238
//                m_output.append("map [");
239
//                m_output.append(mapType->maxNumberOfElements());
240
//                m_output.append("] ");
241
//                printSubElementOrNull(mapType->fromType());
242
//                m_output.append(" to ");
243
//                printSubElementOrNull(mapType->toType());
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
                // get a list of interesting symbols
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
                                // do nothing.
292
                                break;
293
                        }
294
                }
295

    
296
                int i = 0;
297
                if (attrs.size() > 0)
298
                {
299
                        // variables
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); // if guards this
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
//void PrintVisitor::visit(AbortStatement* abortStatement)
413
//{
414
//        m_output.append("abort");
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
//void PrintVisitor::visit(KillStatement* killStatement)
445
//{
446
//        m_output.append("kill (");
447
//        printSubElementOrNull(killStatement->someOne);
448
//        m_output.append(")");
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
} /* namespace Ast */