aspect TypeCheck{

	/**
	 * synthesized attribute isJPITypeDecl() indicates
	 * if the TypeDecl is a JPITypeDecl or not.
	 */
	syn lazy boolean TypeDecl.isJPITypeDecl() = false;
	eq JPITypeDecl.isJPITypeDecl() = true;
	
	syn lazy boolean JPITypeDecl.hasException(String name){
  		for(int i = 0; i < getNumException(); i++){
  			if(((TypeAccess)getException(i)).name().equals(name)){
  				return true;
  			}
	    }
	    return false;	
	}

	public void JPITypeDecl.typeCheck(){
		TypeAccess jpiSuperAccess = (TypeAccess)getSuperTypeName();
		JPITypeDecl jpiSuperDecl;
		
		/***
		 * 0) check exceptions
		 * 1) check if SuperAcces is $RootJPI$
		 * 2) check that the type of SuperAccess is JPITypeDecl.
		 * 3) check the return types.
		 * 4) check the exception accesses.
		 * 5) check the arguments types.
		 */
		
	    TypeDecl exceptionType = typeThrowable();
	    for(int i = 0; i < getNumException(); i++) {
	      TypeDecl typeDecl = getException(i).type();
	      if(!typeDecl.instanceOf(exceptionType))
	        error("Typecheck: jpi type declaration throws non throwable type " + typeDecl.fullName());
	    }
		
		if (jpiSuperAccess.getID().equals("$RootJPI$")){
			return;
		}
		
		if (!jpiSuperAccess.type().isJPITypeDecl()){
			error("TypeCheck: "+jpiSuperAccess.getID()+" must be a JPI not a "+jpiSuperAccess.type().typeName());
			return;
		}
		
		TypeDecl jpiTypeDecl = ((JPITypeAccess)jpiSuperAccess).decl(getParentParameterTypeList());
		if (jpiTypeDecl.isUnknown()){
			error("TypeCheck: There is not a JPI declaration with the same signature.");
			return;
		}
		jpiSuperDecl = (JPITypeDecl)jpiTypeDecl;
				
		if(!getTypeAccess().type().equals(jpiSuperDecl.getTypeAccess().type())){
			error("TypeCheck: Return type must be equals");
		}
		
		if(jpiSuperDecl.getNumException() > getNumException()){
			error("TypeCheck: " +typeName()+" must at least defines the same exceptions of its parent.");
		}
		for(Access exceptionAccess: jpiSuperDecl.getExceptionList()){
			if (!hasException(((TypeAccess)exceptionAccess).name())){
				error("TypeCheck: "+((TypeAccess)exceptionAccess).name() +" must be declared in "+typeName());
			}
		}
				
		if(getNumSuperArgumentName() != jpiSuperDecl.getNumParameter()){
			error("TypeCheck: Arguments quantity must match in the extends clause.");
		}
		else {
			for(int i=0; i<getNumSuperArgumentName(); i++){
				SimpleSet childParameter = lookupVariable(getSuperArgumentName(i).variableName());
				ParameterDeclaration parentParameter = jpiSuperDecl.getParameter(i);
				if (childParameter.isEmpty()){
					error("TypeCheck: "+getSuperArgumentName(i).variableName()+" doesn't exist as formal parameter of "+typeName()+" JPI.");
					continue;
				}
				//HINT:getSootType is added in this check because TypeVariables.
				if (!((ParameterDeclaration)childParameter).getTypeAccess().type().getSootType().equals(parentParameter.getTypeAccess().type().getSootType())){
					error("TypeCheck: Argument types must be equals.");
				}				
			}
		}	
	}	
	
	public void ExhibitBodyDecl.typeCheck(){
	  	TypeAccess jpiAccess = (TypeAccess)getJPIName();
	  	JPITypeDecl jpiDecl;
	  
		if (!((JPITypeAccess)jpiAccess).decl(this.getParameterTypeList()).isJPITypeDecl()){
			error("TypeCheck: "+jpiAccess.getID()+" must be a valid JPI type definition");// not a "+jpiAccess.type().typeName());
			return;
		}
		
		jpiDecl = (JPITypeDecl) ((JPITypeAccess)jpiAccess).decl(this.getParameterTypeList());
		doTypeChecking(jpiDecl);

		if (!(getPointcut() instanceof GlobalExpr)){
			for(ParameterDeclaration parameter: getParameterList()){
				int bindings = getPointcut().binds(parameter.name());
				if(bindings == 0){
					error("TypeCheck: Exhibits must bind its formal argument "+parameter.name());
				}
				else if(bindings > 1){
					error("TypeCheck: Exhibits binds formal argument "+parameter.name() + " multiple times.");
				}
			}
		}			
		PointcutExpr pe = getPointcut();
		if (!pe.isInvPCD())
			warning("TypeCheck: Use argsInv, thisInv, respectively targetInv instead.");
		pe.checkInterfaceTypeInvPCD();
	}
	
	public void ExhibitBodyDecl.doTypeChecking(JPITypeDecl jpiDecl){
		if(!getReturnType().type().equals(jpiDecl.getTypeAccess().type())){
			error("TypeCheck: Exhibit return type: "+getReturnType().type().name()+" instead "+jpiDecl.getTypeAccess().type().name());
		}
		
		if(getNumParameter() != jpiDecl.getNumParameter()){
			error("TypeCheck: Exhibit clause must declare the same quantity of arguments that its JPI");
		}
		else{
			ParameterDeclaration exhibitParameter;
			ParameterDeclaration jpiParameter;
			for(int i=0; i<jpiDecl.getNumParameter(); i++){
				exhibitParameter = getParameter(i);
				jpiParameter = jpiDecl.getParameter(i);
				if(!exhibitParameter.type().equals(jpiParameter.type())){
					error("TypeCheck: Exhibit parameter "+exhibitParameter.getID()+" must be the type of "+jpiParameter.type().name()+" instead "+exhibitParameter.type().name());
				}
			}
		}	
	}
	
	refine TypeCheckCJP public void CJPAdviceDecl.typeCheck() {
		super.typeCheck();
		TypeAccess jpiAccess = (TypeAccess)getName();
		
		if (!((JPITypeAccess)jpiAccess).decl(this.getAdviceSpec().getParameterTypeList()).isJPITypeDecl()){
			error("TypeChecking: "+jpiAccess.getID()+" is not a valid type for JPITypeDeclaration");
			return;
		} 
		doTypeChecking((JoinpointTypeDecl)((JPITypeAccess)jpiAccess).decl(this.getAdviceSpec().getParameterTypeList()));				
	}	
	
	refine AspectErrorCheck public void AspectDecl.typeCheck() {
		AspectErrorCheck.AspectDecl.typeCheck();
		CJPAdviceDecl cjpAdvice;
  		int CJPAdviceCounter=0, FinalCJPAdviceCounter=0;
  		for(BodyDecl bd : getBodyDeclList()){
	  		if(bd.isCJPAdviceDecl()){
			  	cjpAdvice = (CJPAdviceDecl)bd;
			  	if (cjpAdvice.isFinal()){
			  		if (CJPAdviceCounter != FinalCJPAdviceCounter){
			  			cjpAdvice.error("TypeCheck: final advice "+cjpAdvice.getAdviceSpec().kind()+" " + cjpAdvice.getName().typeName() +" has to be defined before all non-final pieces of advice");
			  		}
			  		FinalCJPAdviceCounter++;
			  	}
			  	CJPAdviceCounter++;
	  		}
  		}
	}
}