import { AbstractVisitor, LiteralExpression, ValueType, AdditiveExpression, AndExpression, ArrayExpression, AssignDestination, AssignExpression, SendExpression, ConditionalExpression, OrExpression, EqualityExpression, RelationalExpression, MultiplicativeExpression, UnaryExpression, PostfixExpression, ReceiveExpression, ProcedureCall, ClassCall, IdentifierExpression, StatementWrapper, BreakStatement, StartExpression, ContinueStatement, StatementBlock, StatementExpression, SelectStatement, Case, IfStatement, WhileStatement, DoStatement, ForStatement, ForInit, ReturnStatement, PrimitiveStatement, ConditionStatement, PrintStatement, Program, MainAgent, ProcedureDeclaration, ProcedureParameter, Monitor, Struct, ConditionDeclaration, VariableDeclarations, VariableDeclarator, VariableInitializer, SimpleTypeNode, ArrayTypeNode, ChannelTypeNode, ClassTypeNode } from "@pseuco/lang"
import { TypeCheckCoordinator } from "./TypeCheckCoordinator";
import { Type } from "./types/Type";
import { ConcretePrimitiveType, PrimitiveType, PrimitiveTypes } from "./types/PrimitiveType";
import { ArrayType, UNKNOWN_SIZE } from "./types/ArrayType";
import { SystemTypes } from "./types/SystemType";
import { ChannelCapacity, ChannelType, UNKNOWN_CAPACITY } from "./types/ChannelType";
import { ProcedureType } from "./types/ProcedureType";
import { ClassType, ConcreteClassType } from "./types/ClassType";
import { TypeEnvironment } from "./environments/TypeEnvironment";
import { DeclarationType } from "./types/DeclarationType";
import { ReturnTypeCheckVisitor } from "./ReturnTypeCheckVisitor";
import { ClassReferenceCycleDetection } from "./ClassReferenceCycleDetection";

export class TypeCheckVisitor extends AbstractVisitor<Type> {
    constructor(readonly coordinator: TypeCheckCoordinator) {
        super();
    }

    // private findTypeErrorType(...types: Type[]): TypeErrorType | null {
    //     for (const type of types) {
    //         if (type instanceof TypeErrorType) {
    //             return type;
    //         }
    //     }
    //     return null;
    // }


    override visitLiteralExpression(node: LiteralExpression): Type {
        // e.g., true or 42 or "hello"

        // returns the (statically known) type of the literal
        const valueWrapper = node.valueWrapper;
        if (valueWrapper.type == ValueType.BOOL) {
            return PrimitiveTypes.bool; // new PrimitiveType(ConcretePrimitiveType.BOOL);
        } else if (valueWrapper.type == ValueType.INT) {
            return PrimitiveTypes.int; // new PrimitiveType(ConcretePrimitiveType.INT);
        } else if (valueWrapper.type == ValueType.STRING) {
            return PrimitiveTypes.string; // new PrimitiveType(ConcretePrimitiveType.STRING);
        } else {
            throw Error("Internal inconsistency.");
        }
    }

    override visitAdditiveExpression(node: AdditiveExpression): Type {
        // e.g., a + b
        const leftType = this.coordinator.typeForNode(node.left);
        const rightType = this.coordinator.typeForNode(node.right);
        
        if (node.operator == "+") {
            // a and b must be integers or strings
            const leftTypeIsOkay = leftType.isIntType || leftType.isStringType;
            const rightTypeIsOkay = rightType.isIntType || rightType.isStringType;

            if (!leftTypeIsOkay) {
                this.coordinator.submitAndThrowTypeError(node, `Left operand of "+" must be integer or string, but is "${leftType.toString()}".`);
            } else if (!rightTypeIsOkay) {
                this.coordinator.submitAndThrowTypeError(node, `Right operand of "+" must be integer or string, but is "${rightType.toString()}".`);
            } 
        } else {
            // Operator is "-"; a and b must be integers

            if (!leftType.isIntType) {
                this.coordinator.submitAndThrowTypeError(node, `Left operand of "-" must be integer, but is "${leftType.toString()}".`);
            } else if (!rightType.isIntType) {
                this.coordinator.submitAndThrowTypeError(node, `Right operand of "-" must be integer, but is "${rightType.toString()}".`);
            }
        }
        
        // If one of the two operands is of type string, then the whole expression is of type string; otherwise, it is of type integer
        if (leftType.isStringType || rightType.isStringType) {
            return PrimitiveTypes.string; // new PrimitiveType(ConcretePrimitiveType.STRING);
        } else {
            return PrimitiveTypes.int; // new PrimitiveType(ConcretePrimitiveType.INT);
        }
    }

    override visitMultiplicativeExpression(node: MultiplicativeExpression): Type {
        // e.g., x * y
        const leftType = this.coordinator.typeForNode(node.left);
        const rightType = this.coordinator.typeForNode(node.right);

        // Both operands must be of type integer; the result is of type integer
        if (!leftType.isIntType) {
            this.coordinator.submitAndThrowTypeError(node, `Left operand of "${node.operator}" must be integer, but is "${leftType.toString()}".`);
        } else if (!rightType.isIntType) {
            this.coordinator.submitAndThrowTypeError(node, `Right operand of "${node.operator}" must be integer, but is "${rightType.toString()}".`);
        } else {
            return PrimitiveTypes.int; // new PrimitiveType(ConcretePrimitiveType.INT);
        }
    }


    override visitUnaryExpression(node: UnaryExpression): Type {
        // e.g., !e or -e
        
        const subType = this.coordinator.typeForNode(node.valueExpression);

        // Operator "!" requires a Boolean subexpression and returns a Boolean value
        if (node.operator == "!") {
            if (!subType.isBoolType) {
                this.coordinator.submitAndThrowTypeError(node, `Boolean negation can be applied only to Boolean values, but not to values of type "${subType.toString()}".`);
            } else {
                return subType;
            }
        } 
        // Operators "+" and "-" require an integer subexpression and return an integer value
        else {
            if (!subType.isIntType) {
                this.coordinator.submitAndThrowTypeError(node, `Unary operator "${node.operator}" can be applied only to integer values, but not to values of type "${subType.toString()}".`);
            } else {
                return subType;
            }
        }
    }


    override visitPostfixExpression(node: PostfixExpression): Type {
        // e.g., x++

        const subType = this.coordinator.typeForNode(node.assignDestination);

        // The postfix operator requires an integer subexpression and returns an integer value
        if (!subType.isIntType) {
            this.coordinator.submitAndThrowTypeError(node, `Postfix operator "${node.operator}" can be applied only to integer values, but not to values of type "${subType.toString()}".`);
        } else {
            return subType;
        }
    }


    override visitAndExpression(node: AndExpression): Type {
        // e.g., a && b
        const leftType = this.coordinator.typeForNode(node.left);
        const rightType = this.coordinator.typeForNode(node.right);

        // a and b must be of type Bool; then the result is of type Bool
        if (leftType.isBoolType && rightType.isBoolType) {
            return new PrimitiveType(ConcretePrimitiveType.BOOL);
        } else {
            this.coordinator.submitAndThrowTypeError(node, `Operator '&&' expects boolean operands, but found "${leftType.toString()}" and "${rightType.toString()}".`);
        }
    }

    override visitOrExpression(node: OrExpression): Type {
        // e.g., a && b

        const leftType = this.coordinator.typeForNode(node.left);
        const rightType = this.coordinator.typeForNode(node.right);
        
        // a and b must be of type Bool; then the result is of type Bool
        if (leftType.isBoolType && rightType.isBoolType) {
            return PrimitiveTypes.bool; // new PrimitiveType(ConcretePrimitiveType.BOOL);
        } else {
            this.coordinator.submitAndThrowTypeError(node, `Operator '||' expects boolean operands, but found "${leftType.toString()}" and "${rightType.toString()}".`);
        }
    }

    override visitArrayExpression(node: ArrayExpression): Type {
        // e.g., a[x]

        const instanceType = this.coordinator.typeForNode(node.instanceExpression);
        const indexType = this.coordinator.typeForNode(node.indexExpression);

        // The type of `x` must be integer
        if (!indexType.isIntType) {
            this.coordinator.submitAndThrowTypeError(node.indexExpression, `Array index must be of type integer, but is of type "${indexType.toString()}".`);
        }

        // `a` must be an array type; the type of this expression if the inner type of the array
        if (instanceType instanceof ArrayType) {
            return instanceType.elementsType;
        } else {
            this.coordinator.submitAndThrowTypeError(node,`"Expected an array, but found a value of type "${instanceType.toString()}".`);
        }
    }

    override visitAssignDestination(node: AssignDestination): Type {
        // assign destinations are very restricted expressions that are either an identifier or an identifier followed by array accesses. Thus, we must retrieve the type of the identifier from the current environment:
        const env = this.coordinator.environmentForNode(node);
        const identifierDecl = env.getDeclarationForVariableIdentifier(node.identifier);
        if (identifierDecl == undefined) {
            this.coordinator.submitAndThrowTypeError(node, `${node.identifier} is not defined.`);
        }

        var destType = (this.coordinator.typeForNode(identifierDecl) as DeclarationType).declaredType;
        // If the assign destination is inside an array, check the array access:
        for(var arrayIndex = 0; arrayIndex < node.arrayIndexExpressions.length; arrayIndex++) {
            // Reason of failure 1: the type on which the array access happens is not an array:
            if (!(destType instanceof ArrayType)) {
                this.coordinator.submitAndThrowTypeError(node, `Array index notation used on non-array. "${node.identifier}" is of type ${destType.toString()}`);
            }

            // Reason of failure 2: the index is not an integer:
            const indexType = this.coordinator.typeForNode(node.arrayIndexExpressions[arrayIndex]);
            if (!indexType.isIntType) {
                this.coordinator.submitAndThrowTypeError(node, `Array index must be of type integer, but is of type "${indexType.toString()}".`);
            }

            // Future Work: Try to statically determine the accessed index and check if this is within array bounds

            // Replace the destType with the inner type of the array type
            destType = destType.elementsType;
        }

        // Return the most inner type
        return destType;
    }

    override visitAssignExpression(node: AssignExpression): Type {
        // e.g., e[i] = v

        // Type of e[i]:
        const destType = this.coordinator.typeForNode(node.assignDestination);

        // Type of v:
        const valueType = this.coordinator.typeForNode(node.valueExpression);

        
        if (node.operator == "=") {
            // If valueType is not assignable to destType, try to give a helpful error message
            if (!valueType.isAssignableTo(destType)) {
                if (destType.equals(valueType)) {
                    this.coordinator.submitAndThrowTypeError(node, `Identifiers of type "${destType.toString()}" cannot be re-assigned.`);
                } else {
                    // The array hint is implemented to detect by automatic testers that the problem is a mismatch of array size
                    const arrayHint = (destType instanceof ArrayType && valueType instanceof ArrayType) ? "Arrays" : "Values";
                    this.coordinator.submitAndThrowTypeError(node, `${arrayHint} of type "${valueType.toString()}" cannot be assigned to type "${destType.toString()}".`);
                }
            }
        }
        // Add a special check if operator is not '=', but '+=', etc.
        else {
            if (node.operator == "+=") {
                if (!destType.isStringType && !destType.isIntType || !valueType.isStringType && !valueType.isIntType) {
                    this.coordinator.submitAndThrowTypeError(node, `Operator "+=" can only be applied to strings or integers, but not to ${destType.toString()} and ${valueType.toString()}.`);
                }
            } else {
                if (!destType.isIntType || !destType.equals(valueType)) {
                    this.coordinator.submitAndThrowTypeError(node, `Operator "${node.operator}" can only be applied to integers, but not to ${destType.toString()} and ${valueType.toString()}.`);
                }
            }
        }

        // return PrimitiveTypes.void;
        return destType;
    }


    override visitSendExpression(node: SendExpression): Type {
        // e.g., c <! v

        // Type of c:
        const channelType = this.coordinator.typeForNode(node.channelExpression);
        // Type of v:
        const valueType = this.coordinator.typeForNode(node.valueExpression);

        // c must be a channel type (intchan, boolchan, or stringchan):
        if (!(channelType instanceof ChannelType)) {
            this.coordinator.submitAndThrowTypeError(node, `Channel must be of a channel type, but is of type ${channelType.toString()}".`);
        } 
        // The type of v must match the type that c can send:
        else if (!channelType.elementsType.equals(valueType)) {
            this.coordinator.submitAndThrowTypeError(node, `Values of type "${valueType.toString()}" cannot be sent over channels of type ${channelType.toString()}".`);
        }

        return valueType;
    }


    override visitReceiveExpression(node: ReceiveExpression): Type {
        // e.g., <? c

        const channelType = this.coordinator.typeForNode(node.channelExpression);

        // c must be a channel type (intchan, boolchan, or stringchan):
        if (!(channelType instanceof ChannelType)) {
            this.coordinator.submitAndThrowTypeError(node, `Channel must be of a channel type, but is of type ${channelType.toString()}".`);
        } else {
            // The result is of the type of values that c receives:
            return channelType.elementsType;
        }
    }


    override visitConditionalExpression(node: ConditionalExpression): Type {
        // e.g., (e1) ? e2 : e3

        const predicateType = this.coordinator.typeForNode(node.predicate);
        const consequenceType = this.coordinator.typeForNode(node.consequence);
        const alternativeType = this.coordinator.typeForNode(node.alternative);

        // Type of e1 must be bool
        if (!predicateType.isBoolType) {
            this.coordinator.submitAndThrowTypeError(node, `Condition of a conditional expression must be of type Bool, but is of type "${predicateType}".`);
        } // The types of e2 and e3 must be identical
        else if(!consequenceType.equals(alternativeType)) {
            this.coordinator.submitAndThrowTypeError(node, `The types of the two alternatives of a conditional expression must equal, but were "${consequenceType}" and "${alternativeType}".`); 
        } // When using the `case` construct, channel expressions must not occur in one of the alternatives of the conditional expression
        else if (node.insideCaseStatement() && (node.consequence.usedSendOrReceiveOperators() > 0 || node.alternative.usedSendOrReceiveOperators() > 0)) {
            this.coordinator.submitAndThrowTypeError(node, `When using the "case" construct, channel expressions must not occur in one of the alternatives of an conditional expression.`);
        } else {
            // The type of the expression is the type of the two alternatives
            return consequenceType;
        }
    }


    override visitEqualityExpression(node: EqualityExpression): Type {
        // e.g., a == b

        const leftType = this.coordinator.typeForNode(node.left);
        const rightType = this.coordinator.typeForNode(node.right);

        // Condition objects cannot be compared
        if (leftType.isConditionType || rightType.isConditionType) {
            this.coordinator.submitAndThrowTypeError(node, "Condition objects cannot be compared.");
        } 
        // Other types can be compared, if a and b have the same type -- but non-primitive types are compared by reference, not by value!
        else if (!leftType.equals(rightType)) {
            this.coordinator.submitAndThrowTypeError(node, `Equality can only be checked for values of the same type, but not for "${leftType.toString()}" and "${rightType.toString()}".`);
        } 
        // The result type of a comparison is Boolean
        else {
            return PrimitiveTypes.bool; // new PrimitiveType(ConcretePrimitiveType.BOOL);
        }
    }


    override visitRelationalExpression(node: RelationalExpression): Type {
        // e.g., a < b

        const leftType = this.coordinator.typeForNode(node.left);
        const rightType = this.coordinator.typeForNode(node.right);

        // a and b must be integers
        if (!leftType.isIntType) {
            this.coordinator.submitAndThrowTypeError(node, `Only integers can be compared, but left operand of relational expression is of type "${leftType.toString()}".`);
        } else if (!rightType.isIntType) {
            this.coordinator.submitAndThrowTypeError(node, `Only integers can be compared, but right operand of relational expression is of type "${rightType.toString()}".`);
        } 
        // The result type of a comparison is Boolean
        else {
            return PrimitiveTypes.bool; // new PrimitiveType(ConcretePrimitiveType.BOOL);
        }
    }


    private checkProcedureCall(node: ProcedureCall, env: TypeEnvironment, classType: ClassType | null): Type {
        // This method can handle both regular procedure calls and calls of procedures defined in monitors or structs

        // Procedure call must not happen on the top level of a pseuCo program; effectively, this means that procedure calls may only happen from within procedure (or agent) declarations
        if (!node.insideProcedure()) {
            this.coordinator.submitAndThrowTypeError(node, "Procedures can only be called by agents, i.e., the call must be located inside a procedure declaration or the mainAgent");
        }

        // Get the procedure declaration
        const procedureDecl = env.getDeclarationForProcedureIdentifier(node.procedureName);
        if (procedureDecl == undefined) {
            const scope = (classType == null) ? "scope" : classType.toString();
            this.coordinator.submitAndThrowTypeError(node, `Procedure "${node.procedureName}" not defined in ${scope}.`);
        }
        const procedureDeclType = this.coordinator.typeForNode(procedureDecl) as DeclarationType;
        const procedureType = procedureDeclType.declaredType as ProcedureType;

        // Check that number of arguments match
        const numberOfExpectedArguments = procedureType.argumentTypes.length;
        const numberOfPassedArguments =  node.argumentExpressions.length;
        const procedureName = (classType == null) ? node.procedureName : `${node.procedureName} in ${classType.toString()}`;  // For error messages
        if (numberOfExpectedArguments != numberOfPassedArguments) {
            this.coordinator.submitAndThrowTypeError(node, `Procedure ${procedureName} expects ${numberOfExpectedArguments} arguments, but is called with ${numberOfPassedArguments} arguments.`);
        }

        // Check that the type of each argument is correct
        for(var i = 0; i < procedureType.argumentTypes.length; i++) {
            const expectedType = procedureType.argumentTypes[i];
            const passedType = this.coordinator.typeForNode(node.argumentExpressions[i]);
            if (!passedType.isAssignableTo(expectedType)) {
                // The array hint is implemented to detect by automatic testers that the problem is a mismatch of array size
                const arrayHint = (expectedType instanceof ArrayType && passedType instanceof ArrayType) ? "array " : "";
                this.coordinator.submitAndThrowTypeError(node, `Argument ${i+1} of procedure ${procedureName} expects value of ${arrayHint}type "${expectedType.toString()}", but got value of type "${passedType.toString()}".`);
            }
        }

        // The resulting type is the return type of the procedure
        return procedureType.returnType;
    }

    override visitProcedureCall(node: ProcedureCall): Type {
        // e.g., f(x, y)

        return this.checkProcedureCall(node, this.coordinator.environmentForNode(node), null);
    }


    override visitClassCall(node: ClassCall): Type {
        // e.g., m.f(x, y)

        // Retrieve information about the monitor/struct
        const classType = this.coordinator.typeForNode(node.instanceExpression);
        if (!(classType instanceof ClassType)) {
            this.coordinator.submitAndThrowTypeError(node, `Expected a struct or monitor instance, but found a value of type "${classType.toString()}".`);
        }
        const classDecl = this.coordinator.environmentForNode(node).getDeclarationForClassIdentifier(classType.className)!; // Declaration must exist, because we just added it

        // Retrieve type information for called class procedure
        if (classDecl.declarations.length == 0) {
            // Empty class, thus, the procedure cannot exist
            this.coordinator.submitAndThrowTypeError(node, `Procedure "${node.callExpression.procedureName}" is not defined in empty ${classType.concreteClassTypeName}.`);
        } else {
            const classSubEnvironment = this.coordinator.environmentForNode(classDecl.declarations[0]);
            return this.checkProcedureCall(node.callExpression, classSubEnvironment, classType);
        }
    }


    override visitStartExpression(node: StartExpression): Type {
        // e.g., start(f(x,y))

        // As procedure calls, agents must be started by other existing agents; effectively, this means that procedure calls may only happen from within procedure (or agent) declarations
        if (!node.insideProcedure()) {
            this.coordinator.submitAndThrowTypeError(node, "New agents can only be started by existing agents, i.e., start expressions must be located inside a procedure declaration or the mainAgent");
        }

        // Re-use the existing procedure call checks
        const call = node.callExpression;
        if (call instanceof ProcedureCall) {
            this.visitProcedureCall(call);
        } else {
            this.visitClassCall(call);
        }
        
        // The result of the start expression is always of type `agent`
        return SystemTypes.agent;
    }


    override visitIdentifierExpression(node: IdentifierExpression): Type {
        // e.g., x

        // Lookup identifier's name in the environment
        const env = this.coordinator.environmentForNode(node);
        const decl = env.getDeclarationForVariableIdentifier(node.identifier);
        if (decl == undefined) {
            // The identifier has not been declared in current scope
            this.coordinator.submitAndThrowTypeError(node, `Variable ${node.identifier} is undefined.`);
        }

        // Obtain the type of the declaration to extract the identifier's type
        const declType = this.coordinator.typeForNode(decl) as DeclarationType;
        return declType.declaredType;
    }


    
















    // STATEMENTS

    override visitStatementWrapper(node: StatementWrapper): Type {
        // An invisible node that wraps statements or represents the empty statement

        // Continue type checking in subnode if `node` is not the empty statement
        if (node.statement != null) {
            this.coordinator.typeForNode(node.statement);
        }

        // The result of statements is always void
        return PrimitiveTypes.void;
    }

    override visitBreakStatement(node: BreakStatement): Type {
        // break

        // break must occur only inside of loops
        if (!node.insideLoop()) {
            this.coordinator.submitAndThrowTypeError(node, "break statements cannot occur outside of a loop.");
        }

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitContinueStatement(node: ContinueStatement): Type {
        // continue

        // continue must occur only inside of loops
        if (!node.insideLoop()) {
            this.coordinator.submitAndThrowTypeError(node, "continue statements cannot occur outside of a loop.");
        }

        // The result of statements is always void
        return PrimitiveTypes.void;
    }

    
    override visitStatementBlock(node: StatementBlock): Type {
        // A set of statements, typically enclosed in curly braces; 
        // e.g., {
        //     println("abc");
        //     x = x + 1;   
        // }

        // Check all captured sub-statements
        node.blockStatements.map(subnode => this.coordinator.typeForNode(subnode));
        // TODO: Previous type checker was collecting error messages

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitStatementExpression(node: StatementExpression): Type {
        // An expression that is used on a statement level; e.g., <? c;

        // Check the expression
        this.coordinator.typeForNode(node.expression);

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitSelectStatement(node: SelectStatement): Type {
        // The select-case-statement

        // Check all sub-statements
        node.cases.map(subnode => this.coordinator.typeForNode(subnode));

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitCase(node: Case): Type {
        // The case of a select statement, e.g., case (<? c): stmt

        // Check that case conditions are well defined
        if (node.condition != null) {
            this.coordinator.typeForNode(node.condition);

            if (node.condition.usedSendOrReceiveOperators() != 1) {
                this.coordinator.submitTypeWarning(node, "You are using two or more send or receive operations in a case condition. Be aware that a non-top-level send or receive operation can cause a deadlock, even if this case is not chosen or if there is a default case!", "Use only one send or receive operation per case");
            }
        }

        // Check body
        this.coordinator.typeForNode(node.statement);

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitIfStatement(node: IfStatement): Type {
        // e.g., if (p) { s1 } else { s2 }

        // Predicate b must be of type bool
        const predicateType = this.coordinator.typeForNode(node.predicate);
        if (!predicateType.isBoolType) {
            this.coordinator.submitAndThrowTypeError(node, `Condition of an if statement must be of type Bool, but is of type "${predicateType}".`);
        }

        // Consequence and alternative must have the same type
        const consequenceType = this.coordinator.typeForNode(node.consequence);
        if (node.alternative != null) {
            const alternativeType = this.coordinator.typeForNode(node.alternative);
            if (!alternativeType.equals(consequenceType)) {
                this.coordinator.submitAndThrowTypeError(node, `The types of the two alternatives of an if-statement must equal, but were "${consequenceType}" and "${alternativeType}".`);
            }
        }

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitWhileStatement(node: WhileStatement): Type {
        // e.g., while(p) { println("Hello"); }

        // The predicate must be a boolean value
        const predicateType = this.coordinator.typeForNode(node.predicate);
        if (!predicateType.isBoolType) {
            this.coordinator.submitAndThrowTypeError(node, `Condition of a while statement must be of type Bool, but is of type "${predicateType}".`);
        }

        // Check types of loop body
        this.coordinator.typeForNode(node.loopBody);

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitDoStatement(node: DoStatement): Type {
        // e.g., do { println("Hello"); } while (p)

        // The predicate must be a boolean value
        const predicateType = this.coordinator.typeForNode(node.predicate);
        if (!predicateType.isBoolType) {
            this.coordinator.submitAndThrowTypeError(node, `Condition of a while statement must be of type Bool, but is of type "${predicateType}".`);
        }

        // Check types of loop body
        this.coordinator.typeForNode(node.loopBody);

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitForStatement(node: ForStatement): Type {
        // e.g., for (;;) { println("Hi"); }

        // The predicate must be a boolean value
        if (node.predicate != null) {
            const predicateType = this.coordinator.typeForNode(node.predicate);
            if (!predicateType.isBoolType) {
                this.coordinator.submitAndThrowTypeError(node, `Condition of a while statement must be of type Bool, but is of type "${predicateType}".`);
            }
        }

        // Check types of the initialisation and the update component of the loop header
        if (node.loopInit != null) {
            this.coordinator.typeForNode(node.loopInit);
        }
        node.loopUpdates.forEach(stmt => this.coordinator.typeForNode(stmt));

        // Check types of loop body
        this.coordinator.typeForNode(node.loopBody);

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitForInit(node: ForInit): Type {
        // the first component of the for-loop header

        // Check all declarations
        node.variableInitialisations.forEach(decl => this.coordinator.typeForNode(decl));

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitReturnStatement(node: ReturnStatement): Type {
        // e.g., return 42

        // Check return expression if it exists
        if (node.expression != null) {
            this.coordinator.typeForNode(node.expression);
        }

        if (!node.insideProcedure()) {
            this.coordinator.submitAndThrowTypeError(node, "return statements cannot occur outside of a procedure.");
        }

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitPrimitiveStatement(node: PrimitiveStatement): Type {
        // e.g., lock(l) or join(a), ...

        // Type checking depends on which concrete primitive is used
        const expType = this.coordinator.typeForNode(node.expression);
        if (node.primitive == "lock" || node.primitive == "unlock") {
            if (!expType.isLockType) {
                this.coordinator.submitAndThrowTypeError(node, `Lock and unlock primitives can only be applied to lock objects, but was applied to object of type ${expType.toString()}.`);
            }
        }
        if (node.primitive == "join" && !expType.isAgentType) {
            this.coordinator.submitAndThrowTypeError(node, `Join primitive can only be applied to agent objects, but was applied to object of type ${expType.toString()}.`);
        }
        if (node.primitive == "assert" && !expType.isBoolType) {
            this.coordinator.submitAndThrowTypeError(node, `Assert primitive can only be applied to Boolean values, but was applied to value of type ${expType.toString()}.`);
        }

        // The result of statements is always void
        return PrimitiveTypes.void;
    }

    
    override visitConditionStatement(node: ConditionStatement): Type {
        // e.g., signal(c) or waitForCondition(c) or signalAll()

        // Statement must occur only in monitors
        if (!node.insideMonitor()) {
            this.coordinator.submitAndThrowTypeError(node, `Primitive ${node.modifier} can only be used within monitor procedures.`);
        }

        if (node.identifier != null) {
            const cDecl = this.coordinator.environmentForNode(node).getDeclarationForConditionIdentifier(node.identifier);
            if (cDecl == undefined) {
                this.coordinator.submitAndThrowTypeError(node, `Condition ${node.identifier} was not found in scope.`);
            }
        } else if (node.modifier == "waitForCondition") {
            // waitForCondition needs a condition object, while for signal and signalAll this is optional
            this.coordinator.submitAndThrowTypeError(node, `Primitive ${node.modifier} must be applied to condition object, but none was given.`);
        }

        // The result of statements is always void
        return PrimitiveTypes.void;
    }


    override visitPrintStatement(node: PrintStatement): Type {
        node.argumentExpressions.forEach( exp => {
            const expType = this.coordinator.typeForNode(exp);
            if (!expType.isIntType && !expType.isStringType) {
                this.coordinator.submitAndThrowTypeError(node, `Arguments to println must be of type string or integer, but was ${expType.toString()}.`);
            }
        });

        // The result of statements is always void
        return PrimitiveTypes.void;
    }
























    // Declarations, etc.

    override visitProgram(node: Program): Type {
        // The root of the AST

        // Assumes that the environment visitor did already process the AST

        // Every program must have at least one child node, namely the mainAgent
        if (node.declarations.length == 0) {
            this.coordinator.submitAndThrowTypeError(node, `Every pseuCo program must have a mainAgent.`);
        }

        // The program itself has assigned the root environment; to get the classes environment, we must retrieve the environment of the program's children
        const innerEnvironment = this.coordinator.environmentForNode(node.declarations[0]);

        // There must be a main agent in the program
        const mainAgentDecl = innerEnvironment.getDeclarationForMainAgent();
        if (mainAgentDecl == undefined) {
            this.coordinator.submitAndThrowTypeError(node, `Every pseuCo program must have a mainAgent.`);
        }

        // Continue type checking in the child nodes
        node.declarations.forEach(decl => this.coordinator.typeForNode(decl));

        // Check that there are no cyclic class references
        const cycleChecker = new ClassReferenceCycleDetection(this.coordinator, innerEnvironment.getAllClassDeclarators());
        const cycleWitness = cycleChecker.findCycles();
        if (cycleWitness != null) {
            const witnessDescription = cycleWitness.join(" -> ");
            this.coordinator.submitAndThrowTypeError(node, `There are cyclic dependencies among the monitors and structs. For example, ${witnessDescription}.`);
        }

        // TODO: Collect errors instead of immediate abortion

        // The program does not have a type
        return PrimitiveTypes.void;
    }


    override visitMainAgent(node: MainAgent): Type {
        // mainAgent { ... }

        //Continue the type checking in the child node
        this.coordinator.typeForNode(node.body);

        // `mainAgent` declares a new agent
        return new DeclarationType(SystemTypes.agent);
    }


    override visitProcedureDeclaration(node: ProcedureDeclaration): Type {
        // e.g. int f(int x) { return x+1; }

        // Check return type
        const returnType = this.coordinator.typeForNode(node.resultTypeNode) as DeclarationType;

        // Check parameters
        const parameterTypes = node.parameters.map(p => this.coordinator.typeForNode(p)) as DeclarationType[];

        // Construct the type of the procedure using the types of the arguments and the return type
        const procedureType = new DeclarationType(new ProcedureType(parameterTypes.map(dt => dt.declaredType), returnType.declaredType));

        // Tell the coordinator about the type; this is necessary for recursive procedures
        this.coordinator.presubmitTypeForProcedureDeclaration(node, procedureType);

        // Check body
        this.coordinator.typeForNode(node.body);

        // Check return statements and that for every possible control flow a value is always returned (for non-void return types)
        const exhaustiveReturns = node.body.accept(new ReturnTypeCheckVisitor(this.coordinator, returnType.declaredType));
        if (!returnType.declaredType.isVoidType && !exhaustiveReturns) {
            this.coordinator.submitAndThrowTypeError(node, `Procedure ${node.name} has a non-void return type, but a value is not always returned.`);
        }

        // The type of this declaration is a declaration type that encapsulates the above procedure type
        return procedureType;
    }


    override visitProcedureParameter(node: ProcedureParameter): Type {
        // e.g., int x

        // Evaluate the type node
        const typeType = this.coordinator.typeForNode(node.typeNode) as DeclarationType;

        // The type of the parameter is the declared type (that remains wrapped in the DeclarationType object)
        return typeType;
    }


    override visitMonitor(node: Monitor): Type {
        // e.g., monitor M { ... }

        // Forward type checking to child nodes
        node.declarations.forEach(decl => this.coordinator.typeForNode(decl));

        // Construct monitor type
        const monitorType = new ClassType(node.name, ConcreteClassType.MONITOR);

        // Wrap in a declaration type
        return new DeclarationType(monitorType);
    }


    override visitStruct(node: Struct): Type {
        // e.g., struct M { ... }

        // Forward type checking to child nodes
        node.declarations.forEach(decl => this.coordinator.typeForNode(decl));

        // Construct struct type
        const structType = new ClassType(node.name, ConcreteClassType.STRUCT);

        // Wrap in a declaration type
        return new DeclarationType(structType);
    }


    override visitConditionDeclaration(node: ConditionDeclaration): Type {
        // e.g., condition with (x > 0)

        // Condition declarations must occur only in monitors
        if(!node.insideMonitor()) {
            this.coordinator.submitAndThrowTypeError(node, `Conditions can only be defined in monitor declarations.`);
        }

        // Check that the condition is a boolean
        const predicateType = this.coordinator.typeForNode(node.expression);
        if (!predicateType.isBoolType) {
            this.coordinator.submitAndThrowTypeError(node, `The predicate for a condition object must be of type Bool, but is of type ${predicateType.toString()}.`);
        }

        // Return the type of this declaration
        return new DeclarationType(SystemTypes.condition);
    }


    override visitVariableDeclarations(node: VariableDeclarations): Type {
        // e.g., int x = 5, y;

        // First evaluate the type node
        this.coordinator.typeForNode(node.typeNode) as DeclarationType;
        // If the type is channel with unknown capacity, we can infer that capacity is 0. Since it is declared here, we assume that its constructor will create a channel without buffer.
        // if (type.declaredType instanceof ChannelType && type.declaredType.capacity == UNKNOWN_CAPACITY) {
        //     const updatedType = new ChannelType(type.declaredType.elementsType, 0);
        //     type = new DeclarationType(updatedType);

        // }

        // Continue the type check in the declarators
        node.declarators.forEach(decl => this.coordinator.typeForNode(decl));

        // The actual declarations happen in the declarator, so we return void here
        return PrimitiveTypes.void;
    }


    override visitVariableDeclarator(node: VariableDeclarator): Type {
        // e.g., x = 5

        // To determine the type of this declaration, we need the the VariableDeclarations object that defines the type
        const declarationsNode = node.parent as VariableDeclarations;

        // Retrieving the type of the type node will not cause infinite recursion; the node has already been completely processed by `declarationsNode` (while the processing of `declarationsNode` is still ongoing)
        const declType = this.coordinator.typeForNode(declarationsNode.typeNode) as DeclarationType;

        // The variable initialiser must be type checked, if provided
        if (node.initializer) {
            const initType = this.coordinator.typeForNode(node.initializer);
            if (!initType.isAssignableTo(declType.declaredType)) {
                this.coordinator.submitAndThrowTypeError(node, `${node.name} is defined to be of type ${declType.declaredType.toString()}, but the value it is initialised with is of type ${initType.toString()}.`);
            }
        }

        // We declare a variable of type declType.declaredType, so we return declType
        return declType;
    }


    override visitVariableInitializer(node: VariableInitializer): Type {
        // e.g., 42+1 or {1,2,3,}

        // Case 1: Simple expression:
        if (node.expression != null) {
            return this.coordinator.typeForNode(node.expression);
        } 
        // Case 2: Array initialisation
        else if (node.arrayInitializers != null && node.arrayInitializers.length > 0) {
            // Compute the type of the first array element
            const firstType = this.coordinator.typeForNode(node.arrayInitializers[0]);
            // Check that all aray elements have the same type as the first one
            const firstOneDeviating = node.arrayInitializers.findIndex((initialiser => !this.coordinator.typeForNode(initialiser).equals(firstType)))
            if (firstOneDeviating != -1) {
                const deviatingType = this.coordinator.typeForNode(node.arrayInitializers[firstOneDeviating]);
                this.coordinator.submitAndThrowTypeError(node, `Array initialiser is composed of two different types: index 0 has type ${firstType.toString()} and index ${firstOneDeviating} has type ${deviatingType.toString()}.`);
            }

            const arrayType = new ArrayType(firstType, node.arrayInitializers.length, node.isUncompletedArray);
            return arrayType;
        } else {
            throw Error("Invalid AST. Please contact the pseuCo.com developers.");
        }
    }













    // Type Nodes

    override visitSimpleTypeNode(node: SimpleTypeNode): Type {
        // "void" | "bool" | "int" | "string" | "lock" | "agent"

        if (node.typeName == "agent") {
            return new DeclarationType(SystemTypes.agent);
        } else if (node.typeName == "bool") {
            return new DeclarationType(PrimitiveTypes.bool);
        } else if (node.typeName == "int") {
            return new DeclarationType(PrimitiveTypes.int);
        } else if (node.typeName == "lock") {
            return new DeclarationType(SystemTypes.lock);
        } else if (node.typeName == "string") {
            return new DeclarationType(PrimitiveTypes.string);
        } else if (node.typeName == "void") {
            return new DeclarationType(PrimitiveTypes.void);
        } else {
            throw Error("Internal error."); // TypeScript could not detect automatically that this is unreachable for well-typed programs
        }
    }


    override visitArrayTypeNode(node: ArrayTypeNode): Type {
        // e.g., int[4]

        // Construct array type from the baseType and the capacity (capacity might be unknown for procedure parameter declarations)
        const baseType = this.coordinator.typeForNode(node.baseTypeNode) as DeclarationType;
        const capacity = (node.size == undefined) ? UNKNOWN_SIZE : node.size;

        return new DeclarationType(new ArrayType(baseType.declaredType, capacity));
    }


    override visitChannelTypeNode(node: ChannelTypeNode): Type {
        // e.g., intchan5

        // Get the base type of the channel
        var baseType: PrimitiveType;
        if (node.channelTypeName == "boolchan") {
            baseType = PrimitiveTypes.bool;
        } else if (node.channelTypeName == "intchan") {
            baseType = PrimitiveTypes.int;
        } else {
            baseType = PrimitiveTypes.string;
        }

        // Get its capacity
        // If no capacity is specified, it is 0 if used in a VariableDeclarations node and it is unknown when used as a procedure parameter
        let channelCapacity: ChannelCapacity = node.capacity ?? UNKNOWN_CAPACITY;
        // The VariableDeclarations node may be several parents up (e.g., when having an array of channels)
        if (channelCapacity == UNKNOWN_CAPACITY) {
            let parent = node.parent;
            while(parent) {
                if (parent instanceof VariableDeclarations) {
                    channelCapacity = 0;
                    break;
                } else {
                    parent = parent.parent;
                }
            }
        }
        

        // Construct a channel type from the information above and wrap into a declaration type
        return new DeclarationType(new ChannelType(baseType, channelCapacity));
    }



    override visitClassTypeNode(node: ClassTypeNode): Type {
        // e.g., M

        // Try to finde the class declaration in the environment
        const classDecl = this.coordinator.environmentForNode(node).getDeclarationForClassIdentifier(node.className);
        if (classDecl == undefined) {
            this.coordinator.submitAndThrowTypeError(node, `Type "${node.className}" does not exist. In particular, no monitor or struct with such a name exists.`);
        }

        // Distinguish between struct and monitor by checking of which class `classDecl` is
        if (classDecl instanceof Monitor) {
            // Return monitor type object wrapped as a declaration type
            return new DeclarationType(new ClassType(node.className, ConcreteClassType.MONITOR));
        } else {
            // Return struct type object wrapped as a declaration type
            return new DeclarationType(new ClassType(node.className, ConcreteClassType.STRUCT));
        }
    }









    // FUTURE: Error besser sammeln, .....

}