|
/**
|
|
*
|
|
* OOAS Compiler - C++ AST
|
|
*
|
|
* Copyright 2015, AIT Austrian Institute of Technology.
|
|
* All rights reserved.
|
|
*
|
|
* SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
|
|
*
|
|
* If you modify the file please update the list of contributors below to in-
|
|
* clude your name. Please also stick to the coding convention of using TABs
|
|
* to do the basic (block-level) indentation and spaces for anything after
|
|
* that. (Enable the display of special chars and it should be pretty obvious
|
|
* what this means.) Also, remove all trailing whitespace.
|
|
*
|
|
* Contributors:
|
|
* Willibald Krenn (AIT)
|
|
* Stephan Zimmerer (AIT)
|
|
* Christoph Czurda (AIT)
|
|
*
|
|
*/
|
|
|
|
|
|
|
|
|
|
#include "PrintVisitor.hpp"
|
|
#include <ast/identifiers/MainModule.hpp>
|
|
#include <ast/types/IntType.hpp>
|
|
#include <ast/identifiers/EnumIdentifier.hpp>
|
|
#include <ast/types/EnumType.hpp>
|
|
#include <ast/types/ListType.hpp>
|
|
#include <ast/types/TupleType.hpp>
|
|
#include <ast/types/ActionSystemType.hpp>
|
|
#include <ast/identifiers/AttributeIdentifier.hpp>
|
|
#include <ast/expressions/ValueExpression.hpp>
|
|
#include <ast/statements/Assignment.hpp>
|
|
#include <ast/expressions/AccessExpression.hpp>
|
|
#include <ast/expressions/TypeExpression.hpp>
|
|
#include <ast/expressions/BinaryOperator.hpp>
|
|
#include <ast/expressions/UnaryOperator.hpp>
|
|
#include <ast/expressions/CallExpression.hpp>
|
|
#include <ast/expressions/TupleMapAccessExpression.hpp>
|
|
#include <ast/expressions/TupleConstructor.hpp>
|
|
#include <ast/expressions/ListConstructor.hpp>
|
|
#include <ast/statements/NondetBlock.hpp>
|
|
#include <ast/statements/PrioBlock.hpp>
|
|
#include <ast/statements/SeqBlock.hpp>
|
|
#include <ast/statements/Call.hpp>
|
|
#include <ast/statements/GuardedCommand.hpp>
|
|
#include <ast/expressions/IdentifierExpression.hpp>
|
|
#include <ast/identifiers/IdentifierBlock.hpp>
|
|
#include <ast/statements/Skip.hpp>
|
|
#include <ast/expressions/TernaryOperator.hpp>
|
|
#include <ast/identifiers/NamedActionIdentifier.hpp>
|
|
#include <ast/identifiers/MethodIdentifier.hpp>
|
|
#include <ast/types/FunctionType.hpp>
|
|
#include <ast/identifiers/NamedActionIdentifier.hpp>
|
|
#include <ast/expressions/SetConstructor.hpp>
|
|
#include <ast/identifiers/ExpressionVariableIdentifier.hpp>
|
|
#include <ast/expressions/ObjectConstructor.hpp>
|
|
#include <ast/types/NullType.hpp>
|
|
#include <ast/types/PointerType.hpp>
|
|
#include <map>
|
|
#include <base/CdtFixes.hpp>
|
|
#include <cassert>
|
|
|
|
namespace Ast {
|
|
|
|
PrintVisitor::PrintVisitor(CallContext* context):
|
|
CompleteAstTraversalVisitor(context, false),
|
|
m_writeTypes (true),
|
|
m_output (),
|
|
m_currentTypeDef (nullptr)
|
|
{}
|
|
|
|
PrintVisitor::~PrintVisitor() {
|
|
}
|
|
|
|
template<typename T>
|
|
void PrintVisitor::printSubElementOrNull(T* anElem)
|
|
{
|
|
if (anElem == nullptr)
|
|
m_output.append("<null>");
|
|
else
|
|
anElem->accept(*this);
|
|
}
|
|
|
|
|
|
/*print the type identifier, or the type definition by calling the anAction delegate.*/
|
|
void PrintVisitor::printType(Type* atype, const std::function<void()>& anAction)
|
|
{
|
|
//m_context->logTrace(TRACE_EXECUTOR, "Start printing type: " + atype->toString());
|
|
|
|
if ( (atype->identifier() != nullptr)
|
|
&& (!atype->isAnonymousType())
|
|
&& (m_currentTypeDef != atype->identifier() || !m_writeTypes)) // ref equ.
|
|
{
|
|
bool write = m_writeTypes;
|
|
m_writeTypes = false;
|
|
atype->identifier()->accept(*this);
|
|
m_writeTypes = write;
|
|
}
|
|
else
|
|
anAction();
|
|
}
|
|
|
|
void PrintVisitor::visit(MainModule* mainModule)
|
|
{
|
|
int i = 0;
|
|
// write all types
|
|
m_writeTypes = true;
|
|
m_output.incIndent();
|
|
m_output.appendLine("types");
|
|
for (auto& type: *mainModule->symbolTable())
|
|
{
|
|
if (type.second->kind() != IdentifierKind::TypeIdentifier)
|
|
continue;
|
|
|
|
if (i != 0)
|
|
m_output.appendLine(";");
|
|
i++;
|
|
type.second->accept(*this);
|
|
}
|
|
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.incIndent();
|
|
m_output.incIndent();
|
|
m_output.appendLine("system");
|
|
m_writeTypes = false;
|
|
|
|
// write system description block
|
|
mainModule->systemDescription()->accept(*this);
|
|
|
|
if (mainModule->getMainFunction() != nullptr) {
|
|
m_output.appendLine("# Automatically generated main function:");
|
|
mainModule->getMainFunction()->accept(*this);
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(TypeIdentifier* typeIdentifier)
|
|
{
|
|
m_output.append(typeIdentifier->tokenText());
|
|
if (m_writeTypes)
|
|
{
|
|
m_currentTypeDef = typeIdentifier;
|
|
m_output.append(" = ");
|
|
printSubElementOrNull(typeIdentifier->type());
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(BoolType* )
|
|
{
|
|
m_output.append("bool");
|
|
}
|
|
|
|
|
|
//void PrintVisitor::visit(CharType* charType)
|
|
//{
|
|
// m_output.append("char");
|
|
//}
|
|
|
|
|
|
void PrintVisitor::visit(IntType* intType)
|
|
{
|
|
printType(intType, [&](){
|
|
m_output.append("int [");
|
|
m_output.append(intType->rangeLow());
|
|
m_output.append(" .. ");
|
|
m_output.append(intType->rangeHigh());
|
|
m_output.append("]");
|
|
});
|
|
}
|
|
|
|
// @Override
|
|
// public void visit(final FloatType floatType)
|
|
// {
|
|
// PrintType(floatType, new Action(){
|
|
// @Override
|
|
// public void doIt() {
|
|
// m_output.append("float [");
|
|
// m_output.append(Double.toString(floatType.low()));
|
|
// m_output.append(" .. ");
|
|
// m_output.append(Double.toString(floatType.high()));
|
|
// m_output.append("] /*");
|
|
// m_output.append(Double.toString(floatType.precision()));
|
|
// m_output.append("*/");
|
|
// }});
|
|
// }
|
|
|
|
|
|
void PrintVisitor::visit(EnumIdentifier* enumIdentifier)
|
|
{
|
|
m_output.append(enumIdentifier->tokenText());
|
|
if (enumIdentifier->haveValue())
|
|
m_output.append(" = " + std::to_string(enumIdentifier->value()));
|
|
}
|
|
|
|
template <typename T>
|
|
void PrintVisitor::printEnumeration(const T& arg)
|
|
{
|
|
int i = 0;
|
|
for (auto& sym: arg)
|
|
{
|
|
if (i != 0)
|
|
m_output.append(", ");
|
|
i++;
|
|
printSubElementOrNull(sym);
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(EnumType* enumType)
|
|
{
|
|
printType(enumType, [&]() {
|
|
m_output.append("{");
|
|
printEnumeration(enumType->listOfEnumSymbols());
|
|
m_output.append("}");
|
|
});
|
|
}
|
|
|
|
|
|
void PrintVisitor::visit(ListType* listType)
|
|
{
|
|
printType(listType, [&](){
|
|
m_output.append("list [");
|
|
m_output.append(listType->maxNumberOfElements());
|
|
m_output.append("] of ");
|
|
bool oldwrite = m_writeTypes;
|
|
m_writeTypes = false;
|
|
printSubElementOrNull(listType->innerType());
|
|
m_writeTypes = oldwrite;
|
|
});
|
|
}
|
|
|
|
//void PrintVisitor::visit(MapType* mapType)
|
|
//{
|
|
// printType(mapType, [this, mapType](){
|
|
// m_output.append("map [");
|
|
// m_output.append(mapType->maxNumberOfElements());
|
|
// m_output.append("] ");
|
|
// printSubElementOrNull(mapType->fromType());
|
|
// m_output.append(" to ");
|
|
// printSubElementOrNull(mapType->toType());
|
|
// });
|
|
//}
|
|
|
|
void PrintVisitor::visit(TupleType* tupleType)
|
|
{
|
|
printType(tupleType, [&](){
|
|
m_output.append("(");
|
|
bool oldwrite = m_writeTypes;
|
|
m_writeTypes = false;
|
|
printEnumeration(tupleType->innerTypes());
|
|
m_writeTypes = oldwrite;
|
|
m_output.append(")");
|
|
});
|
|
}
|
|
|
|
void PrintVisitor::visit(ActionSystemType* ooActionSystemType)
|
|
{
|
|
printType(ooActionSystemType, [&](){
|
|
if (ooActionSystemType->autoConstruction())
|
|
m_output.append("autocons ");
|
|
|
|
m_output.append("system ");
|
|
if (ooActionSystemType->baseType() != nullptr)
|
|
m_output.append(boost::format("(%s)") % ooActionSystemType->baseType()->identifier()->tokenText());
|
|
m_output.appendLine("");
|
|
|
|
m_output.incIndent();
|
|
m_output.appendLine("|[");
|
|
|
|
// get a list of interesting symbols
|
|
std::deque<AttributeIdentifier*> attrs;
|
|
std::deque<MethodIdentifier*> methods;
|
|
std::deque<NamedActionIdentifier*> namedActions;
|
|
|
|
for(auto& sym: *ooActionSystemType->symbols())
|
|
{
|
|
switch(sym.second->kind()) {
|
|
case IdentifierKind::AttributeIdentifier:
|
|
attrs.push_back((AttributeIdentifier*)sym.second);
|
|
break;
|
|
case IdentifierKind::MethodIdentifier:
|
|
methods.push_back((MethodIdentifier*)sym.second);
|
|
break;
|
|
case IdentifierKind::NamedActionIdentifier:
|
|
namedActions.push_back((NamedActionIdentifier*)sym.second);
|
|
break;
|
|
default:
|
|
// do nothing.
|
|
break;
|
|
}
|
|
}
|
|
|
|
int i = 0;
|
|
if (attrs.size() > 0)
|
|
{
|
|
// variables
|
|
m_output.incIndent();
|
|
m_output.appendLine("var");
|
|
for (AttributeIdentifier* attr : attrs)
|
|
{
|
|
if (i != 0)
|
|
m_output.appendLine(";");
|
|
i++;
|
|
printSubElementOrNull(attr);
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
}
|
|
bool writeTypesSave = m_writeTypes;
|
|
m_writeTypes = false;
|
|
|
|
i = 0;
|
|
if (methods.size() > 0)
|
|
{
|
|
m_output.incIndent();
|
|
m_output.appendLine("methods");
|
|
for (MethodIdentifier* method : methods)
|
|
{
|
|
if (i != 0)
|
|
m_output.appendLine(";");
|
|
i++;
|
|
printSubElementOrNull(method);
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
}
|
|
|
|
i = 0;
|
|
if (namedActions.size() > 0)
|
|
{
|
|
m_output.incIndent();
|
|
m_output.appendLine("actions");
|
|
for (NamedActionIdentifier* action: namedActions)
|
|
{
|
|
if (i != 0)
|
|
m_output.appendLine(";");
|
|
i++;
|
|
printSubElementOrNull(action);
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
}
|
|
|
|
if ((ooActionSystemType->doodBlock() != nullptr) &&
|
|
(ooActionSystemType->doodBlock()->statements().size() > 0))
|
|
{
|
|
m_output.incIndent();
|
|
m_output.appendLine("do");
|
|
printSubElementOrNull(ooActionSystemType->doodBlock());
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.appendLine("od");
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.append("]|");
|
|
m_writeTypes = writeTypesSave;
|
|
});
|
|
}
|
|
|
|
void PrintVisitor::visit(NullType* )
|
|
{
|
|
m_output.append("nil");
|
|
}
|
|
|
|
void PrintVisitor::visit(PointerType* )
|
|
{
|
|
m_output.append("<somePointer>");
|
|
}
|
|
|
|
|
|
void PrintVisitor::visit(AttributeIdentifier* attributeIdentifier)
|
|
{
|
|
if (attributeIdentifier->isStatic())
|
|
m_output.append("static ");
|
|
if (attributeIdentifier->isObservable())
|
|
m_output.append("obs ");
|
|
if (attributeIdentifier->isControllable())
|
|
m_output.append("ctr ");
|
|
|
|
m_output.append(attributeIdentifier->tokenText());
|
|
if (m_writeTypes)
|
|
{
|
|
m_output.append(": ");
|
|
assert(m_writeTypes == true); // if guards this
|
|
m_writeTypes = false;
|
|
printSubElementOrNull(attributeIdentifier->type());
|
|
m_writeTypes = true;
|
|
m_output.append(" = ");
|
|
printSubElementOrNull(attributeIdentifier->initializer());
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(BoolValueExpression* valueExpression){
|
|
m_output.append(std::to_string(valueExpression->value()));
|
|
}
|
|
|
|
void PrintVisitor::visit(IntValueExpression* valueExpression){
|
|
m_output.append(std::to_string(valueExpression->value()));
|
|
}
|
|
|
|
void PrintVisitor::visit(RefValueExpression* valueExpression){
|
|
if (valueExpression->value() != nullptr)
|
|
m_output.append((std::int64_t)valueExpression->value());
|
|
else
|
|
m_output.append("nil");
|
|
}
|
|
|
|
//void PrintVisitor::visit(AbortStatement* abortStatement)
|
|
//{
|
|
// m_output.append("abort");
|
|
//}
|
|
|
|
void PrintVisitor::visit(Assignment* assignment)
|
|
{
|
|
printEnumeration(assignment->places());
|
|
m_output.append(" := ");
|
|
printEnumeration(assignment->values());
|
|
if (assignment->nondetExpression() != nullptr)
|
|
{
|
|
m_output.incIndent();
|
|
m_output.appendLine("");
|
|
m_output.append("with ");
|
|
assignment->nondetExpression()->accept(*this);
|
|
|
|
if (assignment->symbols()->size() > 0)
|
|
{
|
|
m_output.append(" /* vars: ");
|
|
for (auto& localVar: *assignment->symbols())
|
|
{
|
|
localVar.second->accept(*this);
|
|
m_output.append(" ");
|
|
}
|
|
m_output.append("*/");
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
}
|
|
}
|
|
|
|
//void PrintVisitor::visit(KillStatement* killStatement)
|
|
//{
|
|
// m_output.append("kill (");
|
|
// printSubElementOrNull(killStatement->someOne);
|
|
// m_output.append(")");
|
|
//}
|
|
|
|
void PrintVisitor::visit(AccessExpression* accessExpression)
|
|
{
|
|
if (accessExpression->right() != nullptr)
|
|
{
|
|
m_output.append("(");
|
|
printSubElementOrNull(accessExpression->left());
|
|
m_output.append(").");
|
|
printSubElementOrNull(accessExpression->right());
|
|
} else {
|
|
m_output.append("(");
|
|
printSubElementOrNull(accessExpression->left());
|
|
m_output.append(")");
|
|
}
|
|
}
|
|
|
|
static std::map<ExpressionKind, const char*> opMap = {
|
|
{ ExpressionKind::conditional, "ternIf" },
|
|
{ ExpressionKind::domresby, "domresby"},
|
|
{ ExpressionKind::domresto, "domresto"},
|
|
{ ExpressionKind::rngresby, "rngresby"},
|
|
{ ExpressionKind::rngresto, "rngresto"},
|
|
{ ExpressionKind::munion, "munion"},
|
|
{ ExpressionKind::conc, "conc"},
|
|
{ ExpressionKind::diff, "diff"},
|
|
{ ExpressionKind::inter, "inter"},
|
|
{ ExpressionKind::elemin, "elemin"},
|
|
{ ExpressionKind::notelemin, "notelemin"},
|
|
{ ExpressionKind::subset, "subset"},
|
|
{ ExpressionKind::_union, "union"},
|
|
{ ExpressionKind::div, "div"},
|
|
{ ExpressionKind::greater, ">"},
|
|
{ ExpressionKind::greaterequal, ">="},
|
|
{ ExpressionKind::idiv, "idiv"},
|
|
{ ExpressionKind::less, "<"},
|
|
{ ExpressionKind::lessequal, "<="},
|
|
{ ExpressionKind::minus, "-"},
|
|
{ ExpressionKind::mod, "mod"},
|
|
{ ExpressionKind::pow, "pow"},
|
|
{ ExpressionKind::prod, "*"},
|
|
{ ExpressionKind::sum, "+"},
|
|
{ ExpressionKind::_and, "and"},
|
|
{ ExpressionKind::biimplies, "<=>"},
|
|
{ ExpressionKind::implies, "=>"},
|
|
{ ExpressionKind::_or, "or"},
|
|
{ ExpressionKind::equal, "="},
|
|
{ ExpressionKind::notequal, "<>"},
|
|
{ ExpressionKind::seqmod_mapoverride, "seqmod_mapoverride"},
|
|
{ ExpressionKind::dom, "dom"},
|
|
{ ExpressionKind::range, "range"},
|
|
{ ExpressionKind::merge, "merge"},
|
|
{ ExpressionKind::card, "card"},
|
|
{ ExpressionKind::dconc, "dconc"},
|
|
{ ExpressionKind::dinter, "dinter"},
|
|
{ ExpressionKind::dunion, "dunion"},
|
|
{ ExpressionKind::elems, "elems"},
|
|
{ ExpressionKind::head, "head"},
|
|
{ ExpressionKind::inds, "inds"},
|
|
{ ExpressionKind::len, "len"},
|
|
{ ExpressionKind::tail, "tail"},
|
|
{ ExpressionKind::unminus, "-"},
|
|
{ ExpressionKind::unplus, "+"},
|
|
{ ExpressionKind::_not, "not"},
|
|
{ ExpressionKind::abs, "abs"},
|
|
{ ExpressionKind::forall, "forall"},
|
|
{ ExpressionKind::exists, "exists"},
|
|
{ ExpressionKind::ListConstr, "listconstr"},
|
|
{ ExpressionKind::SetConstr, "setconstr"},
|
|
{ ExpressionKind::MapConstr, "mapconstr"},
|
|
{ ExpressionKind::TupleConstr, "tupleconstr"},
|
|
{ ExpressionKind::ObjectConstr, "objectconstr"},
|
|
{ ExpressionKind::QValConstr, "qvalconstr"},
|
|
{ ExpressionKind::Identifier, "identifier"},
|
|
{ ExpressionKind::UnresolvedIdentifier, "unresId"},
|
|
{ ExpressionKind::Type, "type"},
|
|
{ ExpressionKind::TupleMapAccess, "tuplemapaccess"},
|
|
{ ExpressionKind::Call, "call"},
|
|
{ ExpressionKind::Access, "."},
|
|
{ ExpressionKind::Primed, "'"},
|
|
{ ExpressionKind::Cast, "cast"},
|
|
{ ExpressionKind::foldLR, "foldLR"},
|
|
{ ExpressionKind::foldRL, "foldRL"},
|
|
{ ExpressionKind::Value_Integer, "value_int"},
|
|
{ ExpressionKind::Value_Bool, "value_bool"},
|
|
{ ExpressionKind::Value_Reference, "value_ref"}
|
|
};
|
|
|
|
|
|
void PrintVisitor::printOperator(Expression* expression)
|
|
{
|
|
ExpressionKind kind = expression->kind();
|
|
if (kind == ::Ast::ExpressionKind::Cast) {
|
|
m_output.append("(");
|
|
if (expression->type() != nullptr)
|
|
m_output.append(expression->type()->toString());
|
|
else
|
|
m_output.append("Cast??");
|
|
m_output.append(")");
|
|
} else if (opMap.count(kind) > 0) {
|
|
m_output.append(opMap[kind]);
|
|
} else {
|
|
m_context->logError("Internal error. Unknown operation: " + std::to_string((std::uint64_t)expression->kind()));
|
|
abort();
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(TypeExpression* typeExpression)
|
|
{
|
|
printSubElementOrNull(typeExpression->type());
|
|
}
|
|
|
|
void PrintVisitor::visit(BinaryOperator* binaryOperator)
|
|
{
|
|
m_output.incIndent();
|
|
m_output.appendLine("(");
|
|
printSubElementOrNull(binaryOperator->left());
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.appendLine(")");
|
|
|
|
printOperator(binaryOperator);
|
|
m_output.appendLine("");
|
|
|
|
m_output.incIndent();
|
|
m_output.appendLine("(");
|
|
printSubElementOrNull(binaryOperator->right());
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.appendLine(")");
|
|
}
|
|
|
|
void PrintVisitor::visit(UnaryOperator* unaryOperator)
|
|
{
|
|
printOperator(unaryOperator);
|
|
m_output.append("(");
|
|
printSubElementOrNull(unaryOperator->child());
|
|
m_output.append(")");
|
|
}
|
|
|
|
void PrintVisitor::visit(CallExpression* callExpression)
|
|
{
|
|
if (callExpression->child() != nullptr)
|
|
callExpression->child()->accept(*this);
|
|
if (callExpression->arguments().size() > 0)
|
|
{
|
|
m_output.append("(");
|
|
printEnumeration(callExpression->arguments());
|
|
m_output.append(")");
|
|
} else {
|
|
m_output.append("()");
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(TupleMapAccessExpression* tupleMapAccessExpression)
|
|
{
|
|
if (tupleMapAccessExpression->child() != nullptr)
|
|
tupleMapAccessExpression->child()->accept(*this);
|
|
m_output.append("[");
|
|
printSubElementOrNull(tupleMapAccessExpression->argument());
|
|
m_output.append("]");
|
|
}
|
|
|
|
void PrintVisitor::visit(TupleConstructor* tupleConstructor)
|
|
{
|
|
m_output.append(tupleConstructor->tupleType()->tokenText());
|
|
m_output.append("(");
|
|
printEnumeration(tupleConstructor->values());
|
|
m_output.append(")");
|
|
}
|
|
|
|
void PrintVisitor::visit(ListConstructor* listConstructor)
|
|
{
|
|
m_output.append("[");
|
|
printEnumeration(listConstructor->elements());
|
|
if (listConstructor->hasComprehension())
|
|
{
|
|
m_output.append("| var ");
|
|
int i = 0;
|
|
for (auto& element: *listConstructor->comprehensionVariables())
|
|
{
|
|
if (i != 0)
|
|
m_output.append("; ");
|
|
i++;
|
|
printSubElementOrNull(element.second);
|
|
}
|
|
m_output.appendLine(" &");
|
|
printSubElementOrNull(listConstructor->comprehension());
|
|
}
|
|
m_output.append("]");
|
|
}
|
|
|
|
void PrintVisitor::visit(NondetBlock* nondetBlock)
|
|
{
|
|
int i = 0;
|
|
if (m_makeParens)
|
|
{
|
|
m_output.incIndent();
|
|
m_output.appendLine("(");
|
|
}
|
|
for (auto& smt: nondetBlock->statements())
|
|
{
|
|
if (i != 0)
|
|
{
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.incIndent();
|
|
m_output.appendLine("[] ");
|
|
}
|
|
i++;
|
|
smt->accept(*this);
|
|
}
|
|
if (m_makeParens)
|
|
{
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.appendLine(")");
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(PrioBlock* prioBlock)
|
|
{
|
|
int i = 0;
|
|
if (m_makeParens)
|
|
{
|
|
m_output.incIndent();
|
|
m_output.appendLine("(");
|
|
}
|
|
for (auto& smt: prioBlock->statements())
|
|
{
|
|
if (i != 0)
|
|
{
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.incIndent();
|
|
m_output.appendLine("// ");
|
|
}
|
|
i++;
|
|
smt->accept(*this);
|
|
}
|
|
if (m_makeParens)
|
|
{
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.appendLine(")");
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(SeqBlock* seqBlock)
|
|
{
|
|
int i = 0;
|
|
bool old_makeparens = m_makeParens;
|
|
m_output.incIndent();
|
|
m_output.appendLine("(");
|
|
if (seqBlock->symbols() != nullptr && seqBlock->symbols()->size() > 0)
|
|
{
|
|
m_output.append("var ");
|
|
for (auto& id: *seqBlock->symbols())
|
|
{
|
|
m_output.append(id.second->tokenText());
|
|
m_output.append(": ");
|
|
printSubElementOrNull(id.second);
|
|
}
|
|
m_output.append(": ");
|
|
}
|
|
for (auto& smt: seqBlock->statements())
|
|
{
|
|
if (smt == nullptr)
|
|
continue;
|
|
if (i != 0)
|
|
{
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.incIndent();
|
|
m_output.appendLine("; ");
|
|
}
|
|
i++;
|
|
m_makeParens = true;
|
|
smt->accept(*this);
|
|
m_makeParens = old_makeparens;
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.appendLine(")");
|
|
}
|
|
|
|
void PrintVisitor::visit(Call* call)
|
|
{
|
|
call->callExpression()->accept(*this);
|
|
}
|
|
|
|
void PrintVisitor::visit(GuardedCommand* guardedCommand)
|
|
{
|
|
m_output.append("requires ");
|
|
printSubElementOrNull(guardedCommand->guard());
|
|
m_output.incIndent();
|
|
m_output.appendLine(" :");
|
|
|
|
if (guardedCommand->body() != nullptr)
|
|
guardedCommand->body()->accept(*this);
|
|
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.appendLine("end");
|
|
}
|
|
|
|
void PrintVisitor::visit(IdentifierExpression* identifierExpression)
|
|
{
|
|
m_output.append(identifierExpression->identifier()->tokenText());
|
|
}
|
|
|
|
void PrintVisitor::visit(NondetIdentifierBlock* nondetIdentifierList)
|
|
{
|
|
int i = 0;
|
|
for (auto& smt: nondetIdentifierList->identifiers())
|
|
{
|
|
if (i != 0)
|
|
{
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.incIndent();
|
|
m_output.appendLine("[] ");
|
|
}
|
|
i++;
|
|
smt->accept(*this);
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(PrioIdentifierBlock* prioIdentifierList)
|
|
{
|
|
int i = 0;
|
|
for (auto& smt: prioIdentifierList->identifiers())
|
|
{
|
|
if (i != 0)
|
|
{
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.incIndent();
|
|
m_output.appendLine("//");
|
|
}
|
|
i++;
|
|
smt->accept(*this);
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(SeqIdentifierBlock* seqIdentifierList)
|
|
{
|
|
int i = 0;
|
|
m_output.incIndent();
|
|
m_output.appendLine("(");
|
|
for (auto& smt: seqIdentifierList->identifiers())
|
|
{
|
|
if (i != 0)
|
|
m_output.appendLine("; ");
|
|
i++;
|
|
smt->accept(*this);
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.appendLine(")");
|
|
}
|
|
|
|
void PrintVisitor::visit(Skip* )
|
|
{
|
|
m_output.append("skip");
|
|
}
|
|
|
|
void PrintVisitor::visit(TernaryOperator* ternaryOperator)
|
|
{
|
|
switch(ternaryOperator->kind()) {
|
|
case ExpressionKind::conditional:
|
|
m_output.append("if");
|
|
printSubElementOrNull(ternaryOperator->left());
|
|
m_output.incIndent();
|
|
m_output.appendLine("then");
|
|
printSubElementOrNull(ternaryOperator->mid());
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.incIndent();
|
|
m_output.appendLine("else");
|
|
printSubElementOrNull(ternaryOperator->right());
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
m_output.append("end");
|
|
break;
|
|
case ExpressionKind::foldLR:
|
|
case ExpressionKind::foldRL:
|
|
printSubElementOrNull(ternaryOperator->left());
|
|
if (ternaryOperator->mid() != nullptr)
|
|
{
|
|
m_output.append(" :: (");
|
|
printSubElementOrNull(ternaryOperator->mid());
|
|
m_output.append(")");
|
|
}
|
|
if (ternaryOperator->kind() == ExpressionKind::foldLR)
|
|
m_output.append(" :>: (");
|
|
else
|
|
m_output.append(" :<: (");
|
|
printSubElementOrNull(ternaryOperator->right());
|
|
m_output.append(")");
|
|
break;
|
|
default:
|
|
m_context->logError("Internal error. Unknown ternary operator.");
|
|
abort();
|
|
break;
|
|
}
|
|
}
|
|
|
|
void PrintVisitor::visit(MethodIdentifier* methodIdentifier)
|
|
{
|
|
bool* safe = ((FunctionType*)methodIdentifier->type())->isMiracleSafe();
|
|
if ( safe == nullptr || *safe == false)
|
|
m_output.append("/*BASIC*/ ");
|
|
|
|
|
|
FunctionType* atype = (FunctionType*)methodIdentifier->type();
|
|
|
|
m_output.append(methodIdentifier->tokenText());
|
|
m_output.append("(");
|
|
int j = 0;
|
|
for (auto& x: methodIdentifier->parameter())
|
|
{
|
|
if (j != 0)
|
|
m_output.append(", ");
|
|
else
|
|
j++;
|
|
m_output.append(x->tokenText());
|
|
m_output.append(": ");
|
|
printSubElementOrNull(x->type());
|
|
}
|
|
m_output.append(")");
|
|
if (atype->returnType() != nullptr)
|
|
{
|
|
m_output.append(": ");
|
|
printSubElementOrNull(atype->returnType());
|
|
}
|
|
m_output.appendLine("");
|
|
|
|
m_output.incIndent();
|
|
m_output.appendLine("var");
|
|
int i = 0;
|
|
for (auto& sym: *methodIdentifier->symbolTable())
|
|
{
|
|
if (i != 0)
|
|
m_output.appendLine(";");
|
|
i++;
|
|
m_output.append(sym.second->tokenText());
|
|
m_output.append(": ");
|
|
printSubElementOrNull(sym.second->type());
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
|
|
printSubElementOrNull(methodIdentifier->body());
|
|
m_output.append("end");
|
|
}
|
|
|
|
void PrintVisitor::visit(NamedActionIdentifier* namedActionIdentifier)
|
|
{
|
|
bool* safe = ((FunctionType*)namedActionIdentifier->type())->isMiracleSafe();
|
|
if ( safe == nullptr || *safe == false)
|
|
m_output.append("/*BASIC*/ ");
|
|
|
|
m_output.append(namedActionIdentifier->tokenText());
|
|
m_output.append("(");
|
|
FunctionType* atype = (FunctionType*)namedActionIdentifier->type();
|
|
printEnumeration(atype->parameter());
|
|
m_output.append(")");
|
|
m_output.appendLine("");
|
|
|
|
m_output.incIndent();
|
|
m_output.appendLine("var");
|
|
int i = 0;
|
|
for (auto& sym: *namedActionIdentifier->symbolTable())
|
|
{
|
|
if (i != 0)
|
|
m_output.appendLine(";");
|
|
i++;
|
|
m_output.append(sym.second->tokenText());
|
|
m_output.append(": ");
|
|
printSubElementOrNull(sym.second->type());
|
|
}
|
|
m_output.decIndent();
|
|
m_output.appendLine("");
|
|
|
|
printSubElementOrNull(namedActionIdentifier->body());
|
|
m_output.append("end");
|
|
}
|
|
|
|
void PrintVisitor::visit(SetConstructor* setConstructor)
|
|
{
|
|
m_output.append("[");
|
|
printEnumeration(setConstructor->items());
|
|
if (setConstructor->hasComprehension())
|
|
{
|
|
m_output.append("| var ");
|
|
int i = 0;
|
|
for(auto& elem: *setConstructor->comprehensionVariables())
|
|
{
|
|
if (i != 0)
|
|
m_output.append("; ");
|
|
i++;
|
|
printSubElementOrNull(elem.second);
|
|
}
|
|
m_output.appendLine(" &");
|
|
printSubElementOrNull(setConstructor->comprehension());
|
|
}
|
|
m_output.append("]");
|
|
}
|
|
|
|
void PrintVisitor::visit(ExpressionVariableIdentifier* expressionVariableIdentifier)
|
|
{
|
|
m_output.append(expressionVariableIdentifier->tokenText());
|
|
m_output.append(": ");
|
|
printSubElementOrNull(expressionVariableIdentifier->type());
|
|
}
|
|
|
|
void PrintVisitor::visit(ObjectConstructor* objectConstructor)
|
|
{
|
|
m_output.append("new (");
|
|
printSubElementOrNull(objectConstructor->type());
|
|
m_output.append(")");
|
|
|
|
m_output.append(" //");
|
|
for (auto& i: objectConstructor->instances()) {
|
|
m_output.append(" (");
|
|
m_output.append(i->getName());
|
|
m_output.append(" parent: ");
|
|
m_output.append(i->getParentObject()->getName());
|
|
m_output.append(") ");
|
|
}
|
|
}
|
|
|
|
|
|
} /* namespace Ast */
|