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.codegen.ast;

import java.util.HashSet;

import java.util.IdentityHashMap;

import org.momut.ooas.ast.IAst;

import org.momut.ooas.ast.IAstVisitor;

import org.momut.ooas.ast.IScope;

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.ExistsQuantifier;

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

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

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

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

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.Quantifier;

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.identifiers.AttributeIdentifier;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.AnyType;

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.OoActionSystemInstance;

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

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

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

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

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

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

import org.momut.ooas.parser.ParserState;

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

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

public class OoaAstEmitter<T> implements IAstVisitor {

        final IAstDuplicator<T> m_copier;

        final ParserState m_state;

        protected HashSet<Object> m_visited = new HashSet<Object>();

        final IdentityHashMap<Identifier,T> m_convertedIdentifiers;

        final IdentityHashMap<Type,T> m_convertedTypes;

        final IdentityHashMap<Expression,T> m_convertedExpressions;

        final IdentityHashMap<Statement,T> m_convertedStatements;

        final IdentityHashMap<IScope,T> m_convertedScopes;

        final IdentityHashMap<OoActionSystemInstance, T> m_convertedInstances;

        public OoaAstEmitter(ParserState aState, IAstDuplicator<T> copier) {

                m_copier = copier;

                m_state = aState;

                m_convertedIdentifiers = new IdentityHashMap<>();

                m_convertedTypes = new IdentityHashMap<>();

                m_convertedExpressions = new IdentityHashMap<>();

                m_convertedStatements = new IdentityHashMap<>();

                m_convertedScopes = new IdentityHashMap<>();

                m_convertedInstances = new IdentityHashMap<>();

        }

        @Override

        public String returnVisitorName() {

                return this.getClass().getName();

        }

        @Override

        public void done() {

        }

        protected final void VisitSub(IAst subElement, IAst parent)

        {

                if (subElement == null || m_visited.contains(subElement))

                        return;

                m_visited.add(subElement);

                subElement.Accept(this);

        }

        /**

         * Tells the underlying IAstDuplicator to create an

         * identifier T. Also checks for duplicate instantiations

         * @param id Identifier to map

         * @return some opaque T

         */

        private final T createIdentifier(Identifier id) {

                IdentifierKind kind = id.kind();

                if (id instanceof MainModule)

                        kind = IdentifierKind.MainModule;

                final int subOrd =  (id instanceof IdentifierList)

                                ? ((IdentifierList)id).listType().integerValue

                                : 0;

                final T result = m_copier.createIdentifier(kind, subOrd);

                if (m_convertedIdentifiers.put(id, result) != null)

                        throw new OoasCompilerRuntimeException("Identifier %s already has been copied.", id.toString());

                if (id instanceof IScope) {

                        if (m_convertedScopes.put((IScope)id, m_copier.castToIScope(result)) != null)

                                throw new OoasCompilerRuntimeException("Scope %s already has been copied.", id.toString());

                }

                return result;

        }

        private final T createType(Type type) {

                TypeKind kind = type.kind();

                if (type instanceof ValuedEnumType)

                        kind = TypeKind.ValuedEnumeratedType;

                final T result = m_copier.createType(kind);

                if (m_convertedTypes.put(type, result) != null)

                        throw new OoasCompilerRuntimeException("Type %s already has been copied.", type.toString());

                if (type instanceof IScope) {

                        if (m_convertedScopes.put((IScope)type, m_copier.castToIScope(result)) != null)

                                throw new OoasCompilerRuntimeException("Scope %s already has been copied.", type.toString());

                }

                return result;

        }

        private final T createExpression(Expression expression) {

                final int subOrd =  (expression instanceof LeafExpression)

                                ? ((LeafExpression)expression).valueType().integerValue

                                : 0;

                final T result = m_copier.createExpression(expression.kind(), subOrd);

                if (m_convertedExpressions.put(expression, result) != null)

                        throw new OoasCompilerRuntimeException("Expression %s already has been copied.", expression.toString());

                if (expression instanceof IScope) {

                        if (m_convertedScopes.put((IScope)expression, m_copier.castToIScope(result)) != null)

                                throw new OoasCompilerRuntimeException("Scope %s already has been copied.", expression.toString());

                }

                return result;

        }

        private final T createStatement(Statement statement) {

                final T result = m_copier.createStatement(statement.kind());

                if (m_convertedStatements.put(statement, result) != null)

                        throw new OoasCompilerRuntimeException("Statement %s already has been copied.", statement.toString());

                if (statement instanceof IScope) {

                        if (m_convertedScopes.put((IScope)statement, m_copier.castToIScope(result)) != null)

                                throw new OoasCompilerRuntimeException("Scope %s already has been copied.", statement.toString());

                }

                return result;

        }

        @Override

        public void visit(EnumIdentifier enumIdentifier)

        {

                final T id = createIdentifier(enumIdentifier);

                // create all referenced subs

                VisitSub(enumIdentifier.definingScope(), enumIdentifier);

                VisitSub(enumIdentifier.type(), enumIdentifier);

                // create the identifier and initialize it.

                m_copier.initEnumIdentifier(

                                id,

                                enumIdentifier.line(),

                                enumIdentifier.column(),

                                enumIdentifier.tokenText(),

                                m_convertedScopes.get(enumIdentifier.definingScope()),

                                m_convertedTypes.get(enumIdentifier.type()),

                                enumIdentifier.HaveValue(),

                                enumIdentifier.Value());

        }

        @Override

        public void visit(ConstantIdentifier constantIdentifier)

        {

                final T constId = createIdentifier(constantIdentifier);

                // make sure all the sub elements are created.

                VisitSub(constantIdentifier.definingScope(), constantIdentifier);

                VisitSub(constantIdentifier.type(), constantIdentifier);

                VisitSub(constantIdentifier.Value(), constantIdentifier);

                // create the identifier and initialize it.

                m_copier.initConstantIdentifier(

                                constId,

                                constantIdentifier.line(),

                                constantIdentifier.column(),

                                constantIdentifier.tokenText(),

                                m_convertedScopes.get(constantIdentifier.definingScope()),

                                m_convertedTypes.get(constantIdentifier.type()),

                                m_convertedExpressions.get(constantIdentifier.Value()));

        }

        @Override

        public void visit(AttributeIdentifier attributeIdentifier)

        {

                final T id = createIdentifier(attributeIdentifier);

                // make sure all the sub elements are created.

                VisitSub(attributeIdentifier.definingScope(), attributeIdentifier);

                VisitSub(attributeIdentifier.type(), attributeIdentifier);

                VisitSub(attributeIdentifier.initializer(), attributeIdentifier);

                // create the identifier and initialize it.

                m_copier.initAttributeIdentifier(

                                id,

                                attributeIdentifier.line(),

                                attributeIdentifier.column(),

                                attributeIdentifier.tokenText(),

                                m_convertedScopes.get(attributeIdentifier.definingScope()),

                                m_convertedTypes.get(attributeIdentifier.type()),

                                m_convertedExpressions.get(attributeIdentifier.initializer()),

                                attributeIdentifier.isStatic(),

                                attributeIdentifier.isControllable(),

                                attributeIdentifier.isObservable());

        }

        @Override

        public void visit(ExpressionVariableIdentifier expressionVariableIdentifier)

        {

                final T id = createIdentifier(expressionVariableIdentifier);

                // make sure all the sub elements are created.

                VisitSub(expressionVariableIdentifier.definingScope(), expressionVariableIdentifier);

                VisitSub(expressionVariableIdentifier.type(), expressionVariableIdentifier);

                // create the identifier and initialize it.

                m_copier.initExprVarIdentifier(

                                id,

                                expressionVariableIdentifier.line(),

                                expressionVariableIdentifier.column(),

                                expressionVariableIdentifier.tokenText(),

                                m_convertedScopes.get(expressionVariableIdentifier.definingScope()),

                                m_convertedTypes.get(expressionVariableIdentifier.type()),

                                expressionVariableIdentifier.initialized());

        }

        @Override

        public void visit(ParameterIdentifier parameterIdentifier)

        {

                final T id = createIdentifier(parameterIdentifier);

                // create sub elements.

                VisitSub(parameterIdentifier.definingScope(), parameterIdentifier);

                VisitSub(parameterIdentifier.type(), parameterIdentifier);

                // create the identifier and initialize it.

                m_copier.initParamIdentifier(

                                id,

                                parameterIdentifier.line(),

                                parameterIdentifier.column(),

                                parameterIdentifier.tokenText(),

                                m_convertedScopes.get(parameterIdentifier.definingScope()),

                                m_convertedTypes.get(parameterIdentifier.type()));

        }

        @Override

        public void visit(LocalVariableIdentifier localVariableIdentifier)

        {

                final T id = createIdentifier(localVariableIdentifier);

                // create sub elements.

                VisitSub(localVariableIdentifier.definingScope(), localVariableIdentifier);

                VisitSub(localVariableIdentifier.type(), localVariableIdentifier);

                // create the identifier and initialize it.

                m_copier.initLocalVarIdentifier(

                                id,

                                localVariableIdentifier.line(),

                                localVariableIdentifier.column(),

                                localVariableIdentifier.tokenText(),

                                m_convertedScopes.get(localVariableIdentifier.definingScope()),

                                m_convertedTypes.get(localVariableIdentifier.type()));

}

        @Override

        public void visit(TypeIdentifier typeIdentifier)

        {

                final T id = createIdentifier(typeIdentifier);

                // create sub elements.

                VisitSub(typeIdentifier.definingScope(), typeIdentifier);

                VisitSub(typeIdentifier.type(), typeIdentifier);

                // create the identifier and initialize it.

                m_copier.initTypeIdentifier(

                                id,

                                typeIdentifier.line(),

                                typeIdentifier.column(),

                                typeIdentifier.tokenText(),

                                m_convertedScopes.get(typeIdentifier.definingScope()),

                                m_convertedTypes.get(typeIdentifier.type()),

                                typeIdentifier.prefix);

        }

        @Override

        public void visit(SelfTypeIdentifier aself)

        {

                final T id = createIdentifier(aself);

                // create sub elements.

                VisitSub(aself.definingScope(), aself);

                VisitSub(aself.type(), aself);

                // create the identifier and initialize it. (selftypeid extends typeid..)

                m_copier.initSelfIdentifier(

                                id,

                                aself.line(),

                                aself.column(),

                                aself.tokenText(),

                                m_convertedScopes.get(aself.definingScope()),

                                m_convertedTypes.get(aself.type()),

                                aself.prefix);

        }

        @Override

        public void visit(MethodIdentifier methodIdentifier)

        {

                final T id = createIdentifier(methodIdentifier);

                // create sub elements.

                VisitSub(methodIdentifier.definingScope(), methodIdentifier);

                VisitSub(methodIdentifier.type(), methodIdentifier);

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

                        VisitSub(sym, methodIdentifier);

                for (final ParameterIdentifier par: methodIdentifier.parameter())

                        VisitSub(par, methodIdentifier);

                VisitSub(methodIdentifier.body(), methodIdentifier);

                // create the identifier and initialize it.

                final T symbolTable = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symbolTable, m_convertedIdentifiers.get(sym));

                final T parameterList = m_copier.createParameterList();

                for (final ParameterIdentifier par: methodIdentifier.parameter())

                        m_copier.addParameterIdentifierToList(parameterList, m_convertedIdentifiers.get(par));

                m_copier.initMethodIdentifier(

                                id,

                                methodIdentifier.line(),

                                methodIdentifier.column(),

                                methodIdentifier.tokenText(),

                                m_convertedScopes.get(methodIdentifier.definingScope()),

                                m_convertedTypes.get(methodIdentifier.type()),

                                methodIdentifier.prefix,

                                parameterList,

                                symbolTable,

                                m_convertedStatements.get(methodIdentifier.body()));

        }

        @Override

        public void visit(NamedActionIdentifier namedActionIdentifier)

        {

                final T id = createIdentifier(namedActionIdentifier);

                // create sub elements.

                VisitSub(namedActionIdentifier.definingScope(), namedActionIdentifier);

                VisitSub(namedActionIdentifier.type(), namedActionIdentifier);

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

                        VisitSub(sym, namedActionIdentifier);

                for (final ParameterIdentifier par: namedActionIdentifier.parameter())

                        VisitSub(par, namedActionIdentifier);

                VisitSub(namedActionIdentifier.body(), namedActionIdentifier);

                // create the identifier and initialize it.

                final T symbolTable = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symbolTable, m_convertedIdentifiers.get(sym));

                final T parameterList = m_copier.createParameterList();

                for (final ParameterIdentifier par: namedActionIdentifier.parameter())

                        m_copier.addParameterIdentifierToList(parameterList, m_convertedIdentifiers.get(par));

                m_copier.initMethodIdentifier(

                                id,

                                namedActionIdentifier.line(),

                                namedActionIdentifier.column(),

                                namedActionIdentifier.tokenText(),

                                m_convertedScopes.get(namedActionIdentifier.definingScope()),

                                m_convertedTypes.get(namedActionIdentifier.type()),

                                namedActionIdentifier.prefix,

                                parameterList,

                                symbolTable,

                                m_convertedStatements.get(namedActionIdentifier.body()));

        }

        @Override

        public void visit(Module module)

        {

                final T id = createIdentifier(module);

                VisitSub(module.definingScope(), module);

                VisitSub(module.type(), module);

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

                        VisitSub(sym, module);

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(sym));

                m_copier.initModule(

                                id,

                                module.line(),

                                module.column(),

                                module.tokenText(),

                                m_convertedScopes.get(module.definingScope()),

                                m_convertedTypes.get(module.type()),

                                module.prefix,

                                symTab);

        }

        /**

         * Emit the main module. Notice that even though we run the

         * Instantiation Visitor, we DO NOT emit the flattened AS here

         * but the normal classes etc. That said, we include the information

         * about the instantiated objects (how many etc..)

         */

        @Override

        public void visit(MainModule mainModule)

        {

                m_visited.add(mainModule);

                final T id = createIdentifier(mainModule);

                VisitSub(mainModule.definingScope(), mainModule);

                VisitSub(mainModule.type(), mainModule);

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

                        VisitSub(sym, mainModule);

                VisitSub(mainModule.systemDescription(), mainModule);

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(sym));

                m_copier.initMainModule(

                                id,

                                mainModule.line(),

                                mainModule.column(),

                                mainModule.tokenText(),

                                m_convertedScopes.get(mainModule.definingScope()),

                                m_convertedTypes.get(mainModule.type()),

                                mainModule.prefix,

                                symTab,

                                m_convertedIdentifiers.get(mainModule.systemDescription()));

                m_copier.setMainModule(mainModule, id);

        }

        @Override

        public void visit(NondetIdentifierList nondetIdentifierList)

        {

                final T idList = createIdentifier(nondetIdentifierList);

//                VisitSub(nondetIdentifierList.definingScope(), nondetIdentifierList);

//                VisitSub(nondetIdentifierList.type(), nondetIdentifierList);

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

                        VisitSub(id, nondetIdentifierList);

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

                        m_copier.addIdentifierToBlock(idList, m_convertedIdentifiers.get(id));

        }

        @Override

        public void visit(SeqIdentifierList seqIdentifierList)

        {

                final T idList = createIdentifier(seqIdentifierList);

//                VisitSub(nondetIdentifierList.definingScope(), nondetIdentifierList);

//                VisitSub(nondetIdentifierList.type(), nondetIdentifierList);

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

                        VisitSub(id, seqIdentifierList);

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

                        m_copier.addIdentifierToBlock(idList, m_convertedIdentifiers.get(id));

        }

        @Override

        public void visit(PrioIdentifierList prioIdentifierList)

        {

                final T idList = createIdentifier(prioIdentifierList);

//                VisitSub(nondetIdentifierList.definingScope(), nondetIdentifierList);

//                VisitSub(nondetIdentifierList.type(), nondetIdentifierList);

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

                        VisitSub(id, prioIdentifierList);

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

                        m_copier.addIdentifierToBlock(idList, m_convertedIdentifiers.get(id));

        }

        @Override

        public void visit(UnspecIdentifierList unspecIdentifierList)

        {

                final T idList = createIdentifier(unspecIdentifierList);

//                VisitSub(nondetIdentifierList.definingScope(), nondetIdentifierList);

//                VisitSub(nondetIdentifierList.type(), nondetIdentifierList);

                for (final Identifier id: unspecIdentifierList.identifiers())

                        VisitSub(id, unspecIdentifierList);

                for (final Identifier id: unspecIdentifierList.identifiers())

                        m_copier.addIdentifierToBlock(idList, m_convertedIdentifiers.get(id));

        }

        @Override

        public void visit(IntType intType)

        {

                final T type = createType(intType);

                final Identifier id = intType.identifier();

                VisitSub(id, intType);

                m_copier.initIntType(

                                type,

                                m_convertedIdentifiers.get(id),

                                intType.isAnonymousType(),

                                intType.rangeLow(),

                                intType.rangeHigh());

        }

        @Override

        public void visit(BoolType boolType)

        {

                final T type = createType(boolType);

                final Identifier id = boolType.identifier();

                VisitSub(id, boolType);

                m_copier.initBoolType(

                                type,

                                m_convertedIdentifiers.get(id),

                                boolType.isAnonymousType());

        }

        @Override

        public void visit(EnumType enumType)

        {

                final T type = createType(enumType);

                final Identifier id = enumType.identifier();

                VisitSub(id, enumType);

                for (final Identifier sym: enumType.listOfEnumSymbols())

                        VisitSub(sym, enumType);

                // initialize

                final T symTab = m_copier.createSymbolTable();

                for (final Identifier sym: enumType.listOfEnumSymbols())

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(sym));

                // FIXME: fix the visitor to have a separate method for ValuedEnumTypes..

                if (enumType instanceof ValuedEnumType) {

                        final ValuedEnumType t = (ValuedEnumType) enumType;

                        VisitSub(t.getIntType(), t);

                        m_copier.initValuedEnumType(

                                        type,

                                        m_convertedIdentifiers.get(id),

                                        enumType.isAnonymousType(),

                                        symTab,

                                        m_convertedTypes.get(t.getIntType()));

                } else

                        m_copier.initEnumType(

                                type,

                                m_convertedIdentifiers.get(id),

                                enumType.isAnonymousType(),

                                symTab);

        }

        @Override

        public void visit(ListType listType)

        {

                final T type = createType(listType);

                final Identifier id = listType.identifier();

                VisitSub(id, listType);

                VisitSub(listType.innerType(), listType);

                m_copier.initListType(

                                type,

                                m_convertedIdentifiers.get(id),

                                listType.isAnonymousType(),

                                m_convertedTypes.get(listType.innerType()),

                                listType.maxNumberOfElements());

        }

        @Override

        public void visit(TupleType tupleType)

        {

                final T type = createType(tupleType);

                final Identifier id = tupleType.identifier();

                VisitSub(id, tupleType);

                for (final Type t: tupleType.innerTypes())

                        VisitSub(t, tupleType);

                final T list = m_copier.createTypeList();

                for (final Type t: tupleType.innerTypes())

                        m_copier.addTypeToList(list, m_convertedTypes.get(t));

                m_copier.initTupleType(

                                type,

                                m_convertedIdentifiers.get(id),

                                tupleType.isAnonymousType(),

                                list);

        }

        @Override

        public void visit(FunctionType functionType)

        {

                final T type = createType(functionType);

                final Identifier id = functionType.identifier();

                VisitSub(id, functionType);

                for (final Type a: functionType.parameter())

                        VisitSub(a, functionType);

                VisitSub(functionType.returnType(), functionType);

                final T list = m_copier.createTypeList();

                for (final Type t: functionType.parameter())

                        m_copier.addTypeToList(list, m_convertedTypes.get(t));

                m_copier.initFunctionType(

                                type,

                                m_convertedIdentifiers.get(id),

                                functionType.isAnonymousType(),

                                list,

                                m_convertedTypes.get(functionType.returnType()),

                                functionType.functionType().integerValue,

                                functionType.isPureFunction());

                        // we ignore the isMiracleSafe property here.

        }

        private void convertActionSystemInstance(OoActionSystemInstance i, IAst ooActionSystemType) {

                if (i == null || m_convertedInstances.containsKey(i))

                        return;

                final T instance = m_copier.createActionSystemInstance();

                m_convertedInstances.put(i, instance);

                VisitSub(i.Type, ooActionSystemType);

                convertActionSystemInstance(i.ParentObject, ooActionSystemType);

                m_copier.initActionSystemInstance(

                                instance,

                                m_convertedTypes.get(i.Type),

                                i.Name,

                                i.numberOfCreatedObjects,

                                m_convertedInstances.get(i.ParentObject));

        }

        @Override

        public void visit(OoActionSystemType ooActionSystemType)

        {

                final T type = createType(ooActionSystemType);

                final Identifier id = ooActionSystemType.identifier();

                VisitSub(id, ooActionSystemType);

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

                        VisitSub(s, ooActionSystemType);

                VisitSub(ooActionSystemType.doOdBlock(), ooActionSystemType);

                VisitSub(ooActionSystemType.baseType(), ooActionSystemType);

                for (final OoActionSystemInstance i: ooActionSystemType.objects())

                        convertActionSystemInstance(i, ooActionSystemType);

                for (final OoActionSystemInstance i: ooActionSystemType.derivedObjects())

                        convertActionSystemInstance(i, ooActionSystemType);

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(s));

                final T objectsList = m_copier.createActionSystemInstanceList();

                for (final OoActionSystemInstance i: ooActionSystemType.objects())

                        m_copier.addActionSystemInstanceToList(objectsList, m_convertedInstances.get(i));

                final T derivedObjectsList = m_copier.createActionSystemInstanceList();

                for (final OoActionSystemInstance i: ooActionSystemType.derivedObjects())

                        m_copier.addActionSystemInstanceToList(objectsList, m_convertedInstances.get(i));

                m_copier.initActionSystemType(

                                type,

                                m_convertedIdentifiers.get(id),

                                ooActionSystemType.isAnonymousType(),

                                m_convertedTypes.get(ooActionSystemType.baseType()),

                                m_convertedScopes.get(ooActionSystemType.GetParentScope()),

                                m_convertedStatements.get(ooActionSystemType.doOdBlock()),

                                symTab,

                                objectsList,

                                derivedObjectsList,

                                ooActionSystemType.autoConstruction(),

                                ooActionSystemType.isInSystemDescription());

        }

        @Override

        public void visit(NullType nullType)

        {

                final T type = createType(nullType);

                final Identifier id = nullType.identifier();

                VisitSub(id, nullType);

                m_copier.initNullType(

                                type,

                                m_convertedIdentifiers.get(id),

                                nullType.isAnonymousType());

        }

        // Statements..

        @Override

        public void visit(SkipStatement skipStatement)

        {

                m_copier.initSkipStatement(

                                createStatement(skipStatement),

                                skipStatement.line(),

                                skipStatement.pos());

        }

        @Override

        public void visit(BreakStatement breakStatement)

        {

                m_copier.initBreakStatement(

                                createStatement(breakStatement),

                                breakStatement.line(),

                                breakStatement.pos());

        }

        @Override

        public void visit(AbortStatement abortStatement)

        {

                m_copier.initAbortStatement(

                                createStatement(abortStatement),

                                abortStatement.line(),

                                abortStatement.pos());

        }

        @Override

        public void visit(NondetBlock nondetBlock)

        {

                final T stmt = createStatement(nondetBlock);

                // make sure all elements are allocated

                VisitSub(nondetBlock.GetParentScope(), nondetBlock);

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

                        VisitSub(id, nondetBlock);

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

                        VisitSub(stmnt, nondetBlock);

                // assemble data and initialize the block

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(id));

                final T stmtList = m_copier.createStatementList();

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

                        m_copier.addStatementToList(stmtList, m_convertedStatements.get(stmnt));

                m_copier.initNondetBlock(

                                stmt,

                                nondetBlock.line(),

                                nondetBlock.pos(),

                                symTab,

                                stmtList,

                                m_convertedScopes.get(nondetBlock.GetParentScope()));

        }

        @Override

        public void visit(SeqBlock seqBlock)

        {

                final T stmt = createStatement(seqBlock);

                // make sure all elements are allocated

                VisitSub(seqBlock.GetParentScope(), seqBlock);

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

                        VisitSub(id, seqBlock);

                if (seqBlock.filter() != null)

                        VisitSub(seqBlock.filter(), seqBlock);

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

                        VisitSub(stmnt, seqBlock);

                // assemble data and initialize the block

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(id));

                final T stmtList = m_copier.createStatementList();

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

                        m_copier.addStatementToList(stmtList, m_convertedStatements.get(stmnt));

                m_copier.initSeqBlock(

                                stmt,

                                seqBlock.line(),

                                seqBlock.pos(),

                                symTab,

                                stmtList,

                                m_convertedScopes.get(seqBlock.GetParentScope()),

                                m_convertedExpressions.get(seqBlock.filter()));

        }

        @Override

        public void visit(PrioBlock prioBlock)

        {

                final T stmt = createStatement(prioBlock);

                // make sure all elements are allocated

                VisitSub(prioBlock.GetParentScope(), prioBlock);

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

                        VisitSub(id, prioBlock);

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

                        VisitSub(stmnt, prioBlock);

                // assemble data and initialize the block

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(id));

                final T stmtList = m_copier.createStatementList();

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

                        m_copier.addStatementToList(stmtList, m_convertedStatements.get(stmnt));

                m_copier.initPrioBlock(

                                stmt,

                                prioBlock.line(),

                                prioBlock.pos(),

                                symTab,

                                stmtList,

                                m_convertedScopes.get(prioBlock.GetParentScope()));

        }

        @Override

        public void visit(GuardedCommand guardedCommand)

        {

                final T stmt = createStatement(guardedCommand);

                // make sure all elements are allocated

                VisitSub(guardedCommand.GetParentScope(), guardedCommand);

                VisitSub(guardedCommand.guard(), guardedCommand);

                VisitSub(guardedCommand.body(), guardedCommand);

                m_copier.initGuardedCommand(

                                stmt,

                                guardedCommand.line(),

                                guardedCommand.pos(),

                                m_convertedScopes.get(guardedCommand.GetParentScope()),

                                m_convertedExpressions.get(guardedCommand.guard()),

                                m_convertedStatements.get(guardedCommand.body()));

        }

        @Override

        public void visit(Assignment assignment)

        {

                final T stmt = createStatement(assignment);

                // make sure all elements are allocated

                VisitSub(assignment.GetParentScope(), assignment);

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

                        VisitSub(id, assignment);

                for (final Expression vexp: assignment.places())

                        VisitSub(vexp, assignment);

                for (final Expression expr: assignment.values())

                        VisitSub(expr, assignment);

                VisitSub(assignment.nondetExpression(), assignment);

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(id));

                final T places = m_copier.createExpressionList();

                for (final Expression vexp: assignment.places())

                        m_copier.addExpressionToList(places,m_convertedExpressions.get(vexp));

                final T values = m_copier.createExpressionList();

                for (final Expression expr: assignment.values())

                        m_copier.addExpressionToList(values,m_convertedExpressions.get(expr));

                m_copier.initAssignment(

                                stmt,

                                assignment.line(),

                                assignment.pos(),

                                m_convertedScopes.get(assignment.GetParentScope()),

                                m_convertedExpressions.get(assignment.nondetExpression()),

                                places,

                                values,

                                symTab);

        }

        @Override

        public void visit(Call call)

        {

                final T stmt = createStatement(call);

                // make sure all elements are allocated

                VisitSub(call.callExpression(), call);

                m_copier.initCall(

                                stmt,

                                call.line(),

                                call.pos(),

                                m_convertedExpressions.get(call.callExpression()));

        }

        // Expressions

        private final class ExprData {

                public final T typeRef;

                public final T callTargetsIdentifierListRef;

                public final T symbTabRef;

                public final int line;

                public final int pos;

                public ExprData(T type, T callTgts, T symbTabRef, int line, int pos) {

                        typeRef = type;

                        callTargetsIdentifierListRef = callTgts;

                        this.symbTabRef = symbTabRef;

                        this.line = line;

                        this.pos = pos;

                }

        }

        private ExprData visitBasicExpression(Expression e) {

                final T list = m_copier.createIdentifierList();

                final T symTab = m_copier.createSymbolTable();

                VisitSub(e.type(), e);

                for (final FunctionIdentifier i: e.callTargets())

                        VisitSub(i, e);

                if (e.freeVariables() != null) {

                        for (final Identifier id: e.freeVariables().symbolList())

                                VisitSub(id, e);

                        for (final Identifier id: e.freeVariables().symbolList())

                                m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(id));

                }

                for (final FunctionIdentifier i: e.callTargets())

                        m_copier.addIdentifierToList(list, m_convertedIdentifiers.get(i));

                return new ExprData(m_convertedTypes.get(e.type()), list, symTab,

                                e.line(), e.pos());

        }

        @Override

        public void visit(TypeExpression typeExpression)

        {

                final T expr = createExpression(typeExpression);

                final ExprData d = visitBasicExpression(typeExpression);

                m_copier.initTypeExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef);

        }

        @Override

        public void visit(IdentifierExpression identifierExpression)

        {

                final T expr = createExpression(identifierExpression);

                final ExprData d = visitBasicExpression(identifierExpression);

                VisitSub(identifierExpression.identifier(), identifierExpression);

                m_copier.initIdentifierExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                m_convertedIdentifiers.get(identifierExpression.identifier()),

                                identifierExpression.isSelf());

        }

        @Override

        public void visit(UnaryOperator unaryOperator)

        {

                final T expr = createExpression(unaryOperator);

                final ExprData d = visitBasicExpression(unaryOperator);

                VisitSub(unaryOperator.child(), unaryOperator);

                m_copier.initUnaryExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                m_convertedExpressions.get(unaryOperator.child()));

        }

        @Override

        public void visit(BinaryOperator binaryOperator)

        {

                final T expr = createExpression(binaryOperator);

                final ExprData d = visitBasicExpression(binaryOperator);

                VisitSub(binaryOperator.left(), binaryOperator);

                VisitSub(binaryOperator.right(), binaryOperator);

                m_copier.initBinaryExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                m_convertedExpressions.get(binaryOperator.left()),

                                m_convertedExpressions.get(binaryOperator.right()));

        }

        @Override

        public void visit(TernaryOperator ternaryOperator)

        {

                final T expr = createExpression(ternaryOperator);

                final ExprData d = visitBasicExpression(ternaryOperator);

                VisitSub(ternaryOperator.left(), ternaryOperator);

                VisitSub(ternaryOperator.mid(), ternaryOperator);

                VisitSub(ternaryOperator.right(), ternaryOperator);

                VisitSub(ternaryOperator.definingScope(), ternaryOperator);

                m_copier.initTernaryExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                m_convertedExpressions.get(ternaryOperator.left()),

                                m_convertedExpressions.get(ternaryOperator.mid()),

                                m_convertedExpressions.get(ternaryOperator.right()),

                                m_convertedScopes.get(ternaryOperator.definingScope()));

        }

        @Override

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

        {

                final T expr = createExpression(valueExpression);

                final ExprData d = visitBasicExpression(valueExpression);

                switch (valueExpression.valueType()) {

                case integer:

                        @SuppressWarnings("unchecked")

                        final int value = ((ValueExpression<Integer>) valueExpression).value();

                        m_copier.initIntValueExpression(

                                        expr,

                                        d.line,

                                        d.pos,

                                        d.typeRef,

                                        d.callTargetsIdentifierListRef,

                                        d.symbTabRef,

                                        value);

                        break;

                case bool:

                        @SuppressWarnings("unchecked")

                        final boolean bvalue = ((ValueExpression<Boolean>) valueExpression).value();

                        m_copier.initBoolValueExpression(

                                        expr,

                                        d.line,

                                        d.pos,

                                        d.typeRef,

                                        d.callTargetsIdentifierListRef,

                                        d.symbTabRef,

                                        bvalue);

                        break;

                case reference:

                        @SuppressWarnings("unchecked")

                        final Object ovalue = ((ValueExpression<Object>) valueExpression).value();

                        if (ovalue != null)

                                throw new NotImplementedException();

                        m_copier.initNullValueExpression(

                                        expr,

                                        d.line,

                                        d.pos,

                                        d.typeRef,

                                        d.callTargetsIdentifierListRef,

                                        d.symbTabRef);

                        break;

                case qval:

                case real:

                case chr:

                        throw new NotImplementedException();

                case identifier:

                case complex:

                case type:

                case unset:

                default:

                        throw new IllegalArgumentException();

                }

        }

        @Override

        public void visit(ListConstructor listConstructor)

        {

                final T expr = createExpression(listConstructor);

                final ExprData d = visitBasicExpression(listConstructor);

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

                        VisitSub(lvar, listConstructor);

                for (final Expression elems: listConstructor.elements())

                        VisitSub(elems, listConstructor);

                VisitSub(listConstructor.comprehension(), listConstructor);

                VisitSub(listConstructor.GetParentScope(), listConstructor);

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(lvar));

                final T exprList = m_copier.createExpressionList();

                for (final Expression elems: listConstructor.elements())

                        m_copier.addExpressionToList(exprList, m_convertedExpressions.get(elems));

                m_copier.initListConstructor(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                exprList,

                                symTab,

                                m_convertedScopes.get(listConstructor.GetParentScope()),

                                m_convertedExpressions.get(listConstructor.comprehension()),

                                listConstructor.hasComprehension());

        }

        @Override

        public void visit(SetConstructor setConstructor)

        {

                final T expr = createExpression(setConstructor);

                final ExprData d = visitBasicExpression(setConstructor);

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

                        VisitSub(svar, setConstructor);

                for (final Expression elems: setConstructor.items())

                        VisitSub(elems, setConstructor);

                VisitSub(setConstructor.comprehension(), setConstructor);

                VisitSub(setConstructor.GetParentScope(), setConstructor);

                final T symTab = m_copier.createSymbolTable();

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

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(lvar));

                final T exprList = m_copier.createExpressionList();

                for (final Expression elems: setConstructor.items())

                        m_copier.addExpressionToList(exprList, m_convertedExpressions.get(elems));

                m_copier.initSetConstructor(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                exprList,

                                symTab,

                                m_convertedScopes.get(setConstructor.GetParentScope()),

                                m_convertedExpressions.get(setConstructor.comprehension()),

                                setConstructor.hasComprehension());

        }

        @Override

        public void visit(TupleConstructor tupleConstructor)

        {

                final T expr = createExpression(tupleConstructor);

                final ExprData d = visitBasicExpression(tupleConstructor);

                for (final Expression elem: tupleConstructor.values())

                        VisitSub(elem, tupleConstructor);

                VisitSub(tupleConstructor.tupleType(), tupleConstructor);

                final T exprList = m_copier.createExpressionList();

                for (final Expression elems: tupleConstructor.values())

                        m_copier.addExpressionToList(exprList, m_convertedExpressions.get(elems));

                m_copier.initTupleConstructor(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                exprList,

                                m_convertedIdentifiers.get(tupleConstructor.tupleType()),

                                tupleConstructor.isMatcher());

        }

        @Override

        public void visit(AccessExpression accessExpression)

        {

                final T expr = createExpression(accessExpression);

                final ExprData d = visitBasicExpression(accessExpression);

                VisitSub(accessExpression.left(), accessExpression);

                VisitSub(accessExpression.right(), accessExpression);

                m_copier.initAccessExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                m_convertedExpressions.get(accessExpression.left()),

                                m_convertedExpressions.get(accessExpression.right()));

        }

        @Override

        public void visit(TupleMapAccessExpression tupleMapAccessExpression)

        {

                final T expr = createExpression(tupleMapAccessExpression);

                final ExprData d = visitBasicExpression(tupleMapAccessExpression);

                VisitSub(tupleMapAccessExpression.argument(), tupleMapAccessExpression);

                VisitSub(tupleMapAccessExpression.child(), tupleMapAccessExpression);

                m_copier.initTupleMapAccessExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                m_convertedExpressions.get(tupleMapAccessExpression.child()),

                                m_convertedExpressions.get(tupleMapAccessExpression.argument()));

        }

        @Override

        public void visit(CallExpression callExpression)

        {

                final T expr = createExpression(callExpression);

                final ExprData d = visitBasicExpression(callExpression);

                VisitSub(callExpression.child(), callExpression);

                VisitSub(callExpression.scope(), callExpression);

                final T exprList = m_copier.createExpressionList();

                if (callExpression.arguments() != null) {

                        for (final Expression arg: callExpression.arguments())

                                VisitSub(arg, callExpression);

                        for (final Expression elems: callExpression.arguments())

                                m_copier.addExpressionToList(exprList, m_convertedExpressions.get(elems));

                }

                m_copier.initCallExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                m_convertedExpressions.get(callExpression.child()),

                                exprList,

                                m_convertedScopes.get(callExpression.scope()));

        }

        private void visitQuantifierExpression(Quantifier quantifier)

        {

                final T expr = createExpression(quantifier);

                final ExprData d = visitBasicExpression(quantifier);

                for (final Identifier lvar: quantifier.symbols().symbolList())

                        VisitSub(lvar, quantifier);

                VisitSub(quantifier.child(), quantifier);

                VisitSub(quantifier.GetParentScope(), quantifier);

                final T symTab = m_copier.createSymbolTable();

                for (final Identifier lvar: quantifier.symbols().symbolList())

                        m_copier.addIdentifierToSymbolTable(symTab, m_convertedIdentifiers.get(lvar));

                m_copier.initQuantifierExpression(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                m_convertedExpressions.get(quantifier.child()),

                                symTab,

                                m_convertedScopes.get(quantifier.GetParentScope()));

        }

        @Override

        public void visit(ForallQuantifier quantifier)

        {

                visitQuantifierExpression(quantifier);

        }

        @Override

        public void visit(ExistsQuantifier quantifier)

        {

                visitQuantifierExpression(quantifier);

        }

        @Override

        public void visit(ObjectConstructor objectConstructor)

        {

                final T expr = createExpression(objectConstructor);

                final ExprData d = visitBasicExpression(objectConstructor);

                for (final OoActionSystemInstance i: objectConstructor.instances())

                        convertActionSystemInstance(i, objectConstructor);

                final T instanceList = m_copier.createActionSystemInstanceList();

                for (final OoActionSystemInstance i: objectConstructor.instances())

                        m_copier.addActionSystemInstanceToList(instanceList, m_convertedInstances.get(i));

                m_copier.initObjectConstructor(

                                expr,

                                d.line,

                                d.pos,

                                d.typeRef,

                                d.callTargetsIdentifierListRef,

                                d.symbTabRef,

                                instanceList,

                                objectConstructor.currentInstance(),

                                objectConstructor.givenObjectName());

        }

        /*

         * UNSUPPORTED METHODS BELOW

         */

        @Override

        public void visit(KillStatement killStatement)

        {

                // no support for kill right now..

                throw new NotImplementedException();

        }