OoasTools

/**

  *

  *                      OOAS Compiler

  *

  *       Copyright 2015, AIT Austrian Institute of Technology.

  * This code is based on the C# Version of the OOAS Compiler, which is

  * copyright 2015 by the Institute of Software Technology, Graz University

  * of Technology with portions copyright by the 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)

  *               Markus Demetz (AIT)

  *               Christoph Czurda (AIT)

  *

  */

package org.momut.ooas.visitors;

import java.util.ArrayList;

import org.momut.ooas.ast.IAst;

import org.momut.ooas.ast.expressions.AccessExpression;

import org.momut.ooas.ast.expressions.BinaryOperator;

import org.momut.ooas.ast.expressions.CallExpression;

import org.momut.ooas.ast.expressions.Expression;

import org.momut.ooas.ast.expressions.ExpressionKind;

import org.momut.ooas.ast.expressions.IdentifierExpression;

import org.momut.ooas.ast.expressions.ListConstructor;

import org.momut.ooas.ast.expressions.MapConstructor;

import org.momut.ooas.ast.expressions.ObjectConstructor;

import org.momut.ooas.ast.expressions.QValConstructor;

import org.momut.ooas.ast.expressions.SetConstructor;

import org.momut.ooas.ast.expressions.TernaryOperator;

import org.momut.ooas.ast.expressions.TupleConstructor;

import org.momut.ooas.ast.expressions.TupleMapAccessExpression;

import org.momut.ooas.ast.expressions.TypeExpression;

import org.momut.ooas.ast.expressions.UnaryOperator;

import org.momut.ooas.ast.expressions.UnresolvedIdentifierExpression;

import org.momut.ooas.ast.expressions.ValueExpression;

import org.momut.ooas.ast.expressions.MapConstructor.MapItem;

import org.momut.ooas.ast.identifiers.AttributeIdentifier;

import org.momut.ooas.ast.identifiers.EnumIdentifier;

import org.momut.ooas.ast.identifiers.ExpressionVariableIdentifier;

import org.momut.ooas.ast.identifiers.Identifier;

import org.momut.ooas.ast.identifiers.IdentifierKind;

import org.momut.ooas.ast.identifiers.LandmarkIdentifier;

import org.momut.ooas.ast.identifiers.MainModule;

import org.momut.ooas.ast.identifiers.MethodIdentifier;

import org.momut.ooas.ast.identifiers.NamedActionIdentifier;

import org.momut.ooas.ast.identifiers.NondetIdentifierList;

import org.momut.ooas.ast.identifiers.PrioIdentifierList;

import org.momut.ooas.ast.identifiers.SeqIdentifierList;

import org.momut.ooas.ast.identifiers.TypeIdentifier;

import org.momut.ooas.ast.statements.AbortStatement;

import org.momut.ooas.ast.statements.Assignment;

import org.momut.ooas.ast.statements.Call;

import org.momut.ooas.ast.statements.GuardedCommand;

import org.momut.ooas.ast.statements.KillStatement;

import org.momut.ooas.ast.statements.NondetBlock;

import org.momut.ooas.ast.statements.PrioBlock;

import org.momut.ooas.ast.statements.SeqBlock;

import org.momut.ooas.ast.statements.SkipStatement;

import org.momut.ooas.ast.statements.Statement;

import org.momut.ooas.ast.types.BoolType;

import org.momut.ooas.ast.types.CharType;

import org.momut.ooas.ast.types.EnumType;

import org.momut.ooas.ast.types.FloatType;

import org.momut.ooas.ast.types.FunctionType;

import org.momut.ooas.ast.types.IntType;

import org.momut.ooas.ast.types.ListType;

import org.momut.ooas.ast.types.MapType;

import org.momut.ooas.ast.types.NullType;

import org.momut.ooas.ast.types.OoActionSystemType;

import org.momut.ooas.ast.types.OpaqueType;

import org.momut.ooas.ast.types.QrType;

import org.momut.ooas.ast.types.TupleType;

import org.momut.ooas.ast.types.TypeKind;

import org.momut.ooas.ast.types.UlyssesType;

import org.momut.ooas.codegen.OoasCodeEmitter;

import org.momut.ooas.parser.ParserState;

import org.momut.ooas.utils.exceptions.NotImplementedException;

public class OoaPrintVisitor extends OoaCompleteAstTraversalVisitor

{

        private interface Action {

                void doIt();

        }

        protected boolean writeTypes;

        protected Identifier currentTypeDef;

        protected final OoasCodeEmitter output;

        private void PrintSubElementOrNull(IAst anElem)

        {

                if (anElem == null)

                        output.Append("<null>");

                else

                        anElem.Accept(this);

        }

        private void PrintEnumeration(Iterable<?> iarg)

        {

                int i = 0;

                @SuppressWarnings("unchecked")

                final

                Iterable<IAst> arg = (Iterable<IAst>) iarg;

                for (final IAst sym: arg)

                {

                        if (i != 0)

                                output.Append(", ");

                        i++;

                        PrintSubElementOrNull(sym);

                }

        }

        /*print the type identifier, or the type definition by calling the anAction delegate.*/

        private void PrintType(UlyssesType atype, Action anAction)

        {

                if (   (atype.identifier() != null)

                                && (!atype.isAnonymousType())

                                && (currentTypeDef != atype.identifier() || !writeTypes)) // ref equ.

                {

                        final boolean write = writeTypes;

                        writeTypes = false;

                        atype.identifier().Accept(this);

                        writeTypes = write;

                }

                else

                        anAction.doIt();

        }

        @Override

        public void visit(MainModule mainModule)

        {

                int i = 0;

                final boolean haveInstance = mainModule.instance() != null;

                /*print all types*/

                writeTypes = true;

                output.IncIndent();

                output.AppendLine("types");

                for (final Identifier type: mainModule.symbolTable().symbolList())

                {

                        if (type.kind() != IdentifierKind.TypeIdentifier)

                                continue;

                        if (i != 0)

                                output.AppendLine(";");

                        i++;

                        if (!haveInstance || ((TypeIdentifier)type).type().kind() != TypeKind.OoActionSystemType)

                                type.Accept(this);

                }

                if (haveInstance)

                        mainModule.instance().Accept(this);

                output.DecIndent();

                output.AppendLine("");

                output.IncIndent();

                output.IncIndent();

                output.AppendLine("system");

                writeTypes = false;

                if (!haveInstance)

                        mainModule.systemDescription().Accept(this);

                else

                        output.Append(mainModule.instance().identifier().tokenText());

        }

        @Override

        public void visit(TypeIdentifier typeIdentifier)

        {

                output.Append(typeIdentifier.tokenText());

                if (writeTypes)

                {

                        currentTypeDef = typeIdentifier;

                        output.Append(" = ");

                        PrintSubElementOrNull(typeIdentifier.type());

                }

        }

        /*write out type definitions*/

        @Override

        public void visit(BoolType boolType)

        {

                output.Append("bool");

        }

        @Override

        public void visit(CharType charType)

        {

                output.Append("char");

        }

        @Override

        public void visit(final IntType intType)

        {

                PrintType(intType, new Action(){

                        @Override

                        public void doIt() {

                                output.Append("int [");

                                output.Append(Integer.toString(intType.rangeLow()));

                                output.Append(" .. ");

                                output.Append(Integer.toString(intType.rangeHigh()));

                                output.Append("]");

                        }});

        }

        @Override

        public void visit(final FloatType floatType)

        {

                PrintType(floatType,  new Action(){

                        @Override

                        public void doIt() {

                                output.Append("float [");

                                output.Append(Double.toString(floatType.low()));

                                output.Append(" .. ");

                                output.Append(Double.toString(floatType.high()));

                                output.Append("] /*");

                                output.Append(Double.toString(floatType.precision()));

                                output.Append("*/");

                }});

        }

        @Override

        public void visit(EnumIdentifier enumIdentifier)

        {

                output.Append(enumIdentifier.tokenText());

                if (enumIdentifier.HaveValue())

                        output.Append(String.format(" = %s", enumIdentifier.Value()));

        }

        @Override

        public void visit(final EnumType enumType)

        {

                PrintType(enumType, new Action(){

                        @Override

                        public void doIt() {

                                output.Append("{");

                                PrintEnumeration(enumType.listOfEnumSymbols());

                                output.Append("}");

                        }});

        }

        @Override

        public void visit(final ListType listType)

        {

                PrintType(listType, new Action(){

                        @Override

                        public void doIt() {

                                output.Append("list [");

                                output.Append(listType.maxNumberOfElements());

                                output.Append("] of ");

                                PrintSubElementOrNull(listType.innerType());

                        }});

        }

        @Override

        public void visit(final MapType mapType)

        {

                PrintType(mapType, new Action(){

                        @Override

                        public void doIt() {

                                output.Append("map [");

                                output.Append(mapType.maxNumberOfElements());

                                output.Append("] ");

                                PrintSubElementOrNull(mapType.fromType());

                                output.Append(" to ");

                                PrintSubElementOrNull(mapType.toType());

                        }});

        }

        @Override

        public void visit(final TupleType tupleType)

        {

                PrintType(tupleType, new Action(){

                        @Override

                        public void doIt() {

                                output.Append("(");

                                PrintEnumeration(tupleType.innerTypes());

                                output.Append(")");

                        }});

        }

        @Override

        public void visit(OpaqueType opaqueType)

        {

                PrintSubElementOrNull(opaqueType.resolvedType());

                output.Append(" /*opagque*/");

        }

        @Override

        public void visit(final QrType qrType)

        {

                PrintType(qrType, new Action(){

                        @Override

                        public void doIt() {

                                output.Append("qspace of [");

                                PrintEnumeration(qrType.landmarks());

                                output.Append("]");

                        }});

        }

        @Override

        public void visit(LandmarkIdentifier landmarkIdentifier)

        {

                output.Append(landmarkIdentifier.tokenText());

        }

        @Override

        public void visit(final OoActionSystemType ooActionSystemType)

        {

                PrintType(ooActionSystemType, new Action(){

                        @Override

                        public void doIt() {

                                if (ooActionSystemType.autoConstruction())

                                        output.Append("autocons ");

                                output.Append("system ");

                                if (ooActionSystemType.baseType() != null)

                                        output.Append(String.format("(%s)", ooActionSystemType.baseType().identifier().tokenText()));

                                output.AppendLine("");

                                output.IncIndent();

                                output.AppendLine("|[");

                                // get a list of interesting symbols

                                final ArrayList<AttributeIdentifier> attrs = new ArrayList<AttributeIdentifier>();

                                final ArrayList<MethodIdentifier> methods = new ArrayList<MethodIdentifier>();

                                final ArrayList<NamedActionIdentifier> namedActions = new ArrayList<NamedActionIdentifier>();

                                for(final Identifier sym: ooActionSystemType.symbols().symbolList())

                                {

                                        if (sym.kind() == IdentifierKind.AttributeIdentifier)

                                                attrs.add((AttributeIdentifier)sym);

                                        else if (sym.kind() == IdentifierKind.MethodIdentifier)

                                                methods.add((MethodIdentifier)sym);

                                        else if (sym.kind() == IdentifierKind.NamedActionIdentifier)

                                                namedActions.add((NamedActionIdentifier)sym);

                                }

                                int i = 0;

                                if (attrs.size() > 0)

                                {

                                        // variables

                                        output.IncIndent();

                                        output.AppendLine("var");

                                        for (final AttributeIdentifier attr : attrs)

                                        {

                                                if (i != 0)

                                                        output.AppendLine(";");

                                                i++;

                                                PrintSubElementOrNull(attr);

                                        }

                                        output.DecIndent();

                                        output.AppendLine("");

                                }

                                final boolean writeTypesSave = writeTypes;

                                writeTypes = false;

                                i = 0;

                                if (methods.size() > 0)

                                {

                                        output.IncIndent();

                                        output.AppendLine("methods");

                                        for (final MethodIdentifier method : methods)

                                        {

                                                if (i != 0)

                                                        output.AppendLine(";");

                                                i++;

                                                PrintSubElementOrNull(method);

                                        }

                                        output.DecIndent();

                                        output.AppendLine("");

                                }

                                i = 0;

                                if (namedActions.size() > 0)

                                {

                                        output.IncIndent();

                                        output.AppendLine("actions");

                                        for (final NamedActionIdentifier action: namedActions)

                                        {

                                                if (i != 0)

                                                        output.AppendLine(";");

                                                i++;

                                                PrintSubElementOrNull(action);

                                        }

                                        output.DecIndent();

                                        output.AppendLine("");

                                }

                                if ((ooActionSystemType.doOdBlock() != null) &&

                                    (ooActionSystemType.doOdBlock().statements().size() > 0))

                                {

                                        output.IncIndent();

                                        output.AppendLine("do");

                                        PrintSubElementOrNull(ooActionSystemType.doOdBlock());

                                        output.DecIndent();

                                        output.AppendLine("");

                                        output.AppendLine("od");

                                }

                                output.DecIndent();

                                output.AppendLine("");

                                output.Append("]|");

                                writeTypes = writeTypesSave;

                        }});

        }

        @Override

        public void visit(NullType nullType)

        {

                output.Append("nil");

        }

        @Override

        public void visit(AttributeIdentifier attributeIdentifier)

        {

                if (attributeIdentifier.isStatic())

                        output.Append("static ");

                if (attributeIdentifier.isObservable())

                        output.Append("obs ");

                if (attributeIdentifier.isControllable())

                        output.Append("ctr ");

                output.Append(attributeIdentifier.tokenText());

                if (writeTypes)

                {

                        output.Append(": ");

                        PrintSubElementOrNull(attributeIdentifier.type());

                        output.Append(" = ");

                        PrintSubElementOrNull(attributeIdentifier.initializer());

                }

        }

        @Override

        public <T>void visit(ValueExpression<T> valueExpression)

        {

                if (valueExpression.value() != null)

                        output.Append(valueExpression.value().toString());

                else

                        output.Append("nil");

        }

        @Override

        public void visit(AbortStatement abortStatement)

        {

                output.Append("abort");

        }

        @Override

        public void visit(Assignment assignment)

        {

                PrintEnumeration(assignment.places());

                output.Append(" := ");

                PrintEnumeration(assignment.values());

                if (assignment.nondetExpression() != null)

                {

                        output.IncIndent();

                        output.AppendLine("");

                        output.Append("with ");

                        assignment.nondetExpression().Accept(this);

                        if (assignment.symbols().symbolList().size() > 0)

                        {

                                output.Append(" /* vars: ");

                                for (final Identifier localVar: assignment.symbols().symbolList())

                                {

                                        localVar.Accept(this);

                                        output.Append(" ");

                                }

                                output.Append("*/");

                        }

                        output.DecIndent();

                        output.AppendLine("");

                }

        }

        @Override

        public void visit(KillStatement killStatement)

        {

                output.Append("kill (");

                PrintSubElementOrNull(killStatement.someOne);

                output.Append(")");

        }

        @Override

        public void visit(AccessExpression accessExpression)

        {

                if (accessExpression.right() != null)

                {

                        output.Append("(");

                        PrintSubElementOrNull(accessExpression.left());

                        output.Append(").");

                        PrintSubElementOrNull(accessExpression.right());

                }

                else

                {

                        output.Append("(");

                        PrintSubElementOrNull(accessExpression.left());

                        output.Append(")");

                }

        }

        private void PrintOperator(Expression expression)

        {

                switch (expression.kind())

                {

                case abs:    // T_ABS:

                        output.Append("abs");

                        break;

                case card:   // T_CARD:

                        output.Append("card");

                        break;

                case dom:    // T_DOM:

                        output.Append("dom");

                        break;

                case range:  // T_RNG:

                        output.Append("range");

                        break;

                case merge:  // T_MERGE:

                        output.Append("merge");

                        break;

                case len:    // T_LEN:

                        output.Append("len");

                        break;

                case elems:  // T_ELEMS:

                        output.Append("elems");

                        break;

                case head:   // T_HEAD:

                        output.Append("head");

                        break;

                case tail:   // T_TAIL:

                        output.Append("tail");

                        break;

                case conc:   // T_CONC:

                        output.Append("conc");

                        break;

                case inds:   // T_INDS:

                        output.Append("inds");

                        break;

                case dinter: // T_DINTER:

                        output.Append("dinter");

                        break;

                case dunion: // T_DUNION:

                        output.Append("dunion");

                        break;

                case domresby:   // T_DOMRESBY:

                        output.Append("domresby");

                        break;

                case domresto:   // T_DOMRESTO:

                        output.Append("domresto");

                        break;

                case rngresby:   // T_RNGRESBY:

                        output.Append("rngresby");

                        break;

                case rngresto:   // T_RNGRESTO:

                        output.Append("rngresto");

                        break;

                case div:    // T_DIV:

                        output.Append("div");

                        break;

                case idiv:   // T_IDIV:

                        output.Append("idiv");

                        break;

                case mod:    // T_MOD:

                        output.Append("mod");

                        break;

                case prod:   // T_PROD:

                        output.Append("*");

                        break;

                case inter:  // T_INTER:

                        output.Append("inter");

                        break;

                case sum:    // T_SUM:

                        output.Append("+");

                        break;

                case minus:  // T_MINUS:

                        output.Append("-");

                        break;

                case union:  // T_UNION:

                        output.Append("union");

                        break;

                case diff:   // T_DIFF:

                        output.Append("diff");

                        break;

                case munion: // T_MUNION:

                        output.Append("munion");

                        break;

                case seqmod_mapoverride: // T_SEQMOD_MAPOVERRIDE:

                        output.Append("seqmod_mapoverride");

                        break;

                case less:

                        output.Append("<");

                        break;

                case lessequal:

                        output.Append("<=");

                        break;

                case greater:

                        output.Append(">");

                        break;

                case greaterequal:

                        output.Append(">=");

                        break;

                case equal:

                        output.Append("=");

                        break;

                case notequal:

                        output.Append("<>");

                        break;

                case subset:

                        output.Append("subset");

                        break;

                case elemin:

                        output.Append("in");

                        break;

                case notelemin:

                        output.Append("not in");

                        break;

                case and:    // T_AND:

                        output.Append("and");

                        break;

                case or:     // T_OR:

                        output.Append("or");

                        break;

                case implies:    // T_IMPLIES:

                        output.Append("=>");

                        break;

                case biimplies:  // T_BIIMPLIES:

                        output.Append("<=>");

                        break;

                case Primed:

                        output.Append("'");

                        break;

                case Cast:

                        output.Append("(");

                        if (expression.type() != null)

                                output.Append(expression.type().toString());

                        else

                                output.Append("Cast??");

                        output.Append(")");

                        break;

                default:

                        output.Append(expression.kind().toString()); //Enum.GetName(typeof(ExpressionKind), expression.kind));

                        break;

                }

        }

        @Override

        public void visit(TypeExpression typeExpression)

        {

                PrintSubElementOrNull(typeExpression.type());

        }

        @Override

        public void visit(BinaryOperator binaryOperator)

        {

                output.IncIndent();

                output.AppendLine("(");

                PrintSubElementOrNull(binaryOperator.left());

                output.DecIndent();

                output.AppendLine("");

                output.AppendLine(")");

                PrintOperator(binaryOperator); output.AppendLine("");

                output.IncIndent();

                output.AppendLine("(");

                PrintSubElementOrNull(binaryOperator.right());

                output.DecIndent();

                output.AppendLine("");

                output.AppendLine(")");

        }

        @Override

        public void visit(UnaryOperator unaryOperator)

        {

                PrintOperator(unaryOperator);

                output.Append("(");

                PrintSubElementOrNull(unaryOperator.child());

                output.Append(")");

        }

        @Override

        public void visit(UnresolvedIdentifierExpression unresolvedIdentifierExpression)

        {

                output.Append(unresolvedIdentifierExpression.tokenText());

        }

        @Override

        public void visit(CallExpression callExpression)

        {

                if (callExpression.child() != null)

                        callExpression.child().Accept(this);

                if ((callExpression.arguments() != null) && (callExpression.arguments().size() > 0))

                {

                        output.Append("(");

                        PrintEnumeration(callExpression.arguments());

                        output.Append(")");

                }

                else

                {

                        output.Append("()");

                }

        }

        @Override

        public void visit(TupleMapAccessExpression tupleMapAccessExpression)

        {

                if (tupleMapAccessExpression.child() != null)

                        tupleMapAccessExpression.child().Accept(this);

                output.Append("[");

                PrintSubElementOrNull(tupleMapAccessExpression.argument());

                output.Append("]");

        }

        @Override

        public void visit(TupleConstructor tupleConstructor)

        {

                output.Append(tupleConstructor.tupleType().tokenText());

                output.Append("(");

                PrintEnumeration(tupleConstructor.values());

                output.Append(")");

        }

        @Override

        public void visit(ListConstructor listConstructor)

        {

                output.Append("[");

                PrintEnumeration(listConstructor.elements());

                if (listConstructor.hasComprehension())

                {

                        output.Append("| var ");

                        int i = 0;

                        for (final Identifier element: listConstructor.comprehensionVariables().symbolList())

                        {

                                if (i != 0)

                                        output.Append("; ");

                                i++;

                                PrintSubElementOrNull(element);

                        }

                        output.AppendLine(" &");

                        PrintSubElementOrNull(listConstructor.comprehension());

                }

                output.Append("]");

        }

        @Override

        public void visit(QValConstructor qValConstructor)

        {

                output.Append("qval(");

                PrintSubElementOrNull(qValConstructor.value()[0]);

                if (qValConstructor.value().length == 2)

                {

                        output.Append(" .. ");

                        PrintSubElementOrNull(qValConstructor.value()[1]);

                }

                output.Append(",");

                output.Append(qValConstructor.valueDeriv().toString());

                output.Append(")");

        }

        private boolean make_parens = false;

        @Override

        public void visit(NondetBlock nondetBlock)

        {

                int i = 0;

                if (make_parens)

                {

                        output.IncIndent();

                        output.AppendLine("(");

                }

                for (final Statement smt: nondetBlock.statements())

                {

                        if (i != 0)

                        {

                                output.DecIndent();

                                output.AppendLine("");

                                output.IncIndent();

                                output.AppendLine("[] ");

                        }

                        i++;

                        smt.Accept(this);

                }

                if (make_parens)

                {

                        output.DecIndent();

                        output.AppendLine("");

                        output.AppendLine(")");

                }

        }

        @Override

        public void visit(PrioBlock prioBlock)

        {

                int i = 0;

                if (make_parens)

                {

                        output.IncIndent();

                        output.AppendLine("(");

                }

                for (final Statement smt: prioBlock.statements())

                {

                        if (i != 0)

                        {

                                output.DecIndent();

                                output.AppendLine("");

                                output.IncIndent();

                                output.AppendLine("// ");

                        }

                        i++;

                        smt.Accept(this);

                }

                if (make_parens)

                {

                        output.DecIndent();

                        output.AppendLine("");

                        output.AppendLine(")");

                }

        }

        @Override

        public void visit(SeqBlock seqBlock)

        {

                int i = 0;

                final boolean old_makeparens = make_parens;

                output.IncIndent();

                output.AppendLine("(");

                if (seqBlock.symbols().symbolList().size() > 0)

                {

                        output.Append("var ");

                        for (final Identifier id: seqBlock.symbols().symbolList())

                        {

                                output.Append(id.tokenText());

                                output.Append(": ");

                                PrintSubElementOrNull(id);

                        }

                        output.Append(": ");

                }

                for (final Statement smt: seqBlock.statements())

                {

                        if (smt == null)

                                continue;

                        if (i != 0)

                        {

                                output.DecIndent();

                                output.AppendLine("");

                                output.IncIndent();

                                output.AppendLine("; ");

                        }

                        i++;

                        make_parens = true;

                        smt.Accept(this);

                        make_parens = old_makeparens;

                }

                output.DecIndent();

                output.AppendLine("");

                output.AppendLine(")");

        }

        @Override

        public void visit(Call call)

        {

                call.callExpression().Accept(this);

        }

        @Override

        public void visit(GuardedCommand guardedCommand)

        {

                output.Append("requires ");

                PrintSubElementOrNull(guardedCommand.guard());

                output.IncIndent();

                output.AppendLine(" :");

                guardedCommand.body().Accept(this);

                output.DecIndent();

                output.AppendLine("");

                output.AppendLine("end");

        }

        @Override

        public void visit(IdentifierExpression identifierExpression)

        {

                output.Append(identifierExpression.identifier().tokenText());

        }

        @Override

        public void visit(NondetIdentifierList nondetIdentifierList)

        {

                int i = 0;

                for (final Identifier smt: nondetIdentifierList.identifiers())

                {

                        if (i != 0)

                        {

                                output.DecIndent();

                                output.AppendLine("");

                                output.IncIndent();

                                output.AppendLine("[] ");

                        }

                        i++;

                        smt.Accept(this);

                }

        }

        @Override

        public void visit(PrioIdentifierList prioIdentifierList)

        {

                int i = 0;

                for (final Identifier smt: prioIdentifierList.identifiers())

                {

                        if (i != 0)

                        {

                                output.DecIndent();

                                output.AppendLine("");

                                output.IncIndent();

                                output.AppendLine("//");

                        }

                        i++;

                        smt.Accept(this);

                }

        }

        @Override

        public void visit(SeqIdentifierList seqIdentifierList)

        {

                int i = 0;

                output.IncIndent();

                output.AppendLine("(");

                for (final Identifier smt: seqIdentifierList.identifiers())

                {

                        if (i != 0)

                        {

                                output.AppendLine("; ");

                        }

                        i++;

                        smt.Accept(this);

                }

                output.DecIndent();

                output.AppendLine("");

                output.AppendLine(")");

        }

        @Override

        public void visit(SkipStatement skipStatement)

        {

                output.Append("skip");

        }

        @Override

        public void visit(TernaryOperator ternaryOperator)

        {

                if (ternaryOperator.kind() == ExpressionKind.conditional)

                {

                        output.Append("if");

                        PrintSubElementOrNull(ternaryOperator.left());

                        output.IncIndent();

                        output.AppendLine("then");

                        PrintSubElementOrNull(ternaryOperator.mid());

                        output.DecIndent();

                        output.AppendLine("");

                        output.IncIndent();

                        output.AppendLine("else");

                        PrintSubElementOrNull(ternaryOperator.right());

                        output.DecIndent();

                        output.AppendLine("");

                        output.Append("end");

                }

                else if (ternaryOperator.kind() == ExpressionKind.foldLR ||

                                ternaryOperator.kind() == ExpressionKind.foldRL)

                {

                        PrintSubElementOrNull(ternaryOperator.left());

                        if (ternaryOperator.mid() != null)

                        {

                                output.Append(" :: (");

                                PrintSubElementOrNull(ternaryOperator.mid());

                                output.Append(")");

                        }

                        if (ternaryOperator.kind() == ExpressionKind.foldLR)

                                output.Append(" :>: (");

                        else

                                output.Append(" :<: (");

                        PrintSubElementOrNull(ternaryOperator.right());

                        output.Append(")");

                }

                else

                        throw new NotImplementedException();

        }

        @Override

        public void visit(MethodIdentifier methodIdentifier)

        {

                final Boolean safe = ((FunctionType)methodIdentifier.type()).isMiracleSafe();

                if ( safe == null || safe == false)

                        output.Append("/*BASIC*/ ");

                final FunctionType atype = (FunctionType)methodIdentifier.type();

                output.Append(methodIdentifier.tokenText());

                output.Append("(");

                int j = 0;

                for (final Identifier x: methodIdentifier.parameter())

                {

                        if (j != 0)

                                output.Append(", ");

                        else

                                j++;

                        output.Append(x.tokenText());

                        output.Append(": ");

                        PrintSubElementOrNull(x.type());

                }

                output.Append(")");

                if (atype.returnType() != null)

                {

                        output.Append(": ");

                        PrintSubElementOrNull(atype.returnType());

                }

                output.AppendLine("");

                output.IncIndent();

                output.AppendLine("var");

                int i = 0;

                for (final Identifier sym: methodIdentifier.symbolTable().symbolList())

                {

                        if (i != 0)

                                output.AppendLine(";");

                        i++;

                        output.Append(sym.tokenText()); output.Append(": "); PrintSubElementOrNull(sym.type());

                }

                output.DecIndent();

                output.AppendLine("");

                PrintSubElementOrNull(methodIdentifier.body());

                output.Append("end");

        }

        @Override

        public void visit(NamedActionIdentifier namedActionIdentifier)

        {

                final Boolean safe = ((FunctionType)namedActionIdentifier.type()).isMiracleSafe();

                if ( safe == null || safe == false)

                        output.Append("/*BASIC*/ ");

                output.Append(namedActionIdentifier.tokenText());

                output.Append("(");

                final FunctionType atype = (FunctionType)namedActionIdentifier.type();

                PrintEnumeration(atype.parameter());

                output.Append(")");

                output.AppendLine("");

                output.IncIndent();

                output.AppendLine("var");

                int i = 0;

                for (final Identifier sym: namedActionIdentifier.symbolTable().symbolList())

                {

                        if (i != 0)

                                output.AppendLine(";");

                        i++;

                        output.Append(sym.tokenText()); output.Append(": "); PrintSubElementOrNull(sym.type());

                }

                output.DecIndent();

                output.AppendLine("");

                PrintSubElementOrNull(namedActionIdentifier.body());

                output.Append("end");

        }

        @Override

        public void visit(MapConstructor mapConstructor)

        {

                output.Append("{");

                int i = 0;

                for (final MapItem x: mapConstructor.items())

                {

                        if (i != 0)

                                output.Append(", ");

                        i++;

                        PrintSubElementOrNull(x.key);

                        output.Append(" -> ");

                        PrintSubElementOrNull(x.value);

                }

                output.Append("}");

        }

        @Override

        public void visit(SetConstructor setConstructor)

        {

                output.Append("[");

                PrintEnumeration(setConstructor.items());

                if (setConstructor.hasComprehension())

                {

                        output.Append("| var ");

                        int i = 0;

                        for(final Identifier elem: setConstructor.comprehensionVariables().symbolList())

                        {

                                if (i != 0)

                                        output.Append("; ");

                                i++;

                                PrintSubElementOrNull(elem);

                        }

                        output.AppendLine(" &");

                        PrintSubElementOrNull(setConstructor.comprehension());

                }

                output.Append("]");

        }

        @Override

        public void visit(ExpressionVariableIdentifier expressionVariableIdentifier)

        {

                output.Append(expressionVariableIdentifier.tokenText()); output.Append(": ");

                PrintSubElementOrNull(expressionVariableIdentifier.type());

        }

        @Override

        public void visit(ObjectConstructor objectConstructor)

        {

                output.Append("new (");

                PrintSubElementOrNull(objectConstructor.type());

                output.Append(")");

        }

        @Override

        public String toString()

        {

                return output.toString();

        }

        public OoaPrintVisitor(ParserState aState)

        {

                super(aState);

                writeTypes = true;

                output = new OoasCodeEmitter();

        }

}