aspect GlobaJPI{

	syn boolean JPITypeDecl.hasGlobalPointcut() = false;
	eq GlobalJPITypeDecl.hasGlobalPointcut() = true;
	eq GenericGlobalJPITypeDecl.hasGlobalPointcut() = true;
	
	syn PointcutExpr JPITypeDecl.getPointcut(){throw new InternalCompilerError("Trying to get a pointcut expression");}

    eq GlobalJPITypeDecl.getPointcut().bindsInCurrentCflow(String name) =
        getPointcut().binds(name) > 0;

    eq GenericGlobalJPITypeDecl.getPointcut().bindsInCurrentCflow(String name) =
        getPointcut().binds(name) > 0;

	eq GlobalJPITypeDecl.getPointcut().nameType() = NameType.TYPE_NAME;

	eq GenericGlobalJPITypeDecl.getPointcut().nameType() = NameType.TYPE_NAME;
	
	eq GlobalJPITypeDecl.getParameter(int i).nameType() = NameType.TYPE_NAME;	
	eq GlobalJPITypeDecl.getParameter(int index).isMethodParameter() = false;
  	eq GlobalJPITypeDecl.getParameter(int index).isConstructorParameter() = false;
  	eq GlobalJPITypeDecl.getParameter(int index).isExceptionHandlerParameter() = false;
  	eq GlobalJPITypeDecl.getParameter(int index).isPointcutVariable() = true;

	eq GenericGlobalJPITypeDecl.getParameter(int i).nameType() = NameType.TYPE_NAME;	
	eq GenericGlobalJPITypeDecl.getParameter(int index).isMethodParameter() = false;
  	eq GenericGlobalJPITypeDecl.getParameter(int index).isConstructorParameter() = false;
  	eq GenericGlobalJPITypeDecl.getParameter(int index).isExceptionHandlerParameter() = false;
  	eq GenericGlobalJPITypeDecl.getParameter(int index).isPointcutVariable() = true;

    syn SimpleSet GlobalJPITypeDecl.localLookupVariable(String name) {
    	for(ParameterDeclaration formalParameter : getParameterList()){
    		if(formalParameter.name().equals(name)){
                return SimpleSet.emptySet.add(formalParameter);    			
    		}
    	}
        return SimpleSet.emptySet;
    }

	eq GlobalJPITypeDecl.getPointcut().lookupVariable(String name){
        return localLookupVariable(name);
	}

    syn SimpleSet GenericGlobalJPITypeDecl.localLookupVariable(String name) {
    	for(ParameterDeclaration formalParameter : getParameterList()){
    		if(formalParameter.name().equals(name)){
                return SimpleSet.emptySet.add(formalParameter);    			
    		}
    	}
        return SimpleSet.emptySet;
    }

	eq GenericGlobalJPITypeDecl.getPointcut().lookupVariable(String name){
        return localLookupVariable(name);
	}

	public void GlobalJPITypeDecl.typeCheck(){
		super.typeCheck();
		for(ParameterDeclaration parameter: getParameterList()){
			int bindings = getPointcut().binds(parameter.name());
			if(bindings == 0){
				error("TypeCheck: global jpi must bind its formal argument "+parameter.name());
			}
			else if(bindings > 1){
				error("TypeCheck: global jpi 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 GenericGlobalJPITypeDecl.typeCheck(){
		super.typeCheck();
		for(ParameterDeclaration parameter: getParameterList()){
			int bindings = getPointcut().binds(parameter.name());
			if(bindings == 0){
				error("TypeCheck: generic global jpi must bind its formal argument "+parameter.name());
			}
			else if(bindings > 1){
				error("TypeCheck: generic global jpi binds formal argument "+parameter.name() + " multiple times.");
			}
		}
		
		PointcutExpr pe = getPointcut();
		if (!pe.isInvPCD())
			warning("TypeCheck: generic global jpi pointcut expression should not contain PCD such as Args, This, or Target.");			
	}
	
	refine CodeGen eq CJPPointcutExpr.pointcut(){
		Pointcut pointcutSynthesized = CodeGen.CJPPointcutExpr.pointcut();
		Pointcut globalPointcut, scopedPointcut, withinPointcut = null;
		JPITypeDecl jpiTypeDecl = (JPITypeDecl)getJPIAccess().type();		

		if (jpiTypeDecl.hasGlobalPointcut()){
			globalPointcut = jpiTypeDecl.getPointcut().pointcut();
			withinPointcut = OrPointcut.construct(
				abc.ja.jpi.utils.PointcutCombination.makeWithinPointcut(getAllSealedClasses()),
				//makeScope avoid matching over classes/aspects wich redifine the given jpi decl.
				abc.ja.jpi.utils.PointcutCombination.makeScope(jpiTypeDecl, getAllExhibitDecls(), false),
				pos()
			);
			scopedPointcut = NotPointcut.construct(withinPointcut, pos());
			pointcutSynthesized = OrPointcut.construct(
				AndPointcut.construct(globalPointcut, scopedPointcut, pos()),
				pointcutSynthesized,
				pos()
			);
	  	}
	  	return pointcutSynthesized;
	}
	
		
	syn lazy boolean ExhibitBodyDecl.bindGlobalJPI(){
		return ((JPITypeDecl)((JPITypeAccess)getJPIName()).decl(getParameterTypeList())).hasGlobalPointcut();
	}
	    
	syn lazy Pointcut GlobalExpr.pointcut(){
		ExhibitBodyDecl type = hostExhibitBodyDecl();
		JPITypeDecl jpiDecl = ((JPITypeDecl)((JPITypeAccess)type.getJPIName()).decl(type.getParameterTypeList()));
		PointcutExpr pc = null;
		try {
			pc = jpiDecl.getPointcut().clone();
		} catch (CloneNotSupportedException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		if (jpiDecl instanceof GenericGlobalJPITypeDecl)
			abc.ja.jpi.utils.PointcutCombination.replaceTypeVariableForTypeBound(pc, jpiDecl);
		return pc.pointcut();
	}

	inh ExhibitBodyDecl GlobalExpr.hostExhibitBodyDecl();
	eq Program.getCompilationUnit().hostExhibitBodyDecl() = null;

	eq ExhibitBodyDecl.getChild().hostExhibitBodyDecl(){
		return this;
	}
	
	/*
	* register dummy advice decl to perform typechecking
	*/
	public void GlobalJPITypeDecl.jimplify1phase2() {
		if (jpiWithoutAdvice.contains(this)){
	  		registerDummyAdviceDecl();
	  		jpiWithoutAdvice.remove(this);
	  	}
	}

	public void GenericGlobalJPITypeDecl.jimplify1phase2() {
		if (jpiWithoutAdvice.contains(this)){
	  		registerDummyAdviceDecl();
	  		jpiWithoutAdvice.remove(this);
	  	}
	}
	
	public void GlobalJPITypeDecl.registerDummyAdviceDecl(){
	  	adviceParameterList = getParameterList();
	  	Pointcut synthesizedPointcut = abc.ja.jpi.utils.PointcutCombination.synthesizedPointcutsFromJPIWithoutAdviceDecl(getExhibitDecls(), adviceParameterList, pos());
		Pointcut globalPointcut, scopePointcut = null;	
		if (hasGlobalPointcut()){
			scopePointcut = NotPointcut.construct(abc.ja.jpi.utils.PointcutCombination.makeScope(this, getAllExhibitDecls(), false), pos());
			synthesizedPointcut = OrPointcut.construct(AndPointcut.construct(getPointcut().pointcut(), scopePointcut, pos()), synthesizedPointcut, pos());
	  	}  	
	  	doRegisterDummyAdviceDecl(synthesizedPointcut);
	}  	

	public void GenericGlobalJPITypeDecl.registerDummyAdviceDecl(){
	  	adviceParameterList = getParameterList();
	  	Pointcut synthesizedPointcut = abc.ja.jpi.utils.PointcutCombination.synthesizedPointcutsFromJPIWithoutAdviceDecl(getExhibitDecls(), adviceParameterList, pos());
		Pointcut globalPointcut, scopePointcut = null;	
		if (hasGlobalPointcut()){
			scopePointcut = NotPointcut.construct(abc.ja.jpi.utils.PointcutCombination.makeScope(this, getAllExhibitDecls(), false), pos());
			synthesizedPointcut = OrPointcut.construct(AndPointcut.construct(getPointcut().pointcut(), scopePointcut, pos()), synthesizedPointcut, pos());
	  	}  	
	  	doRegisterDummyAdviceDecl(synthesizedPointcut);
	}  	


	inh lazy Collection<ExhibitBodyDecl> JPITypeDecl.getAllExhibitDecls();	

	public String JPITypeDecl.positionInfo() {
      return "JPITypeDecl " + typeName()
          +" ("+pos().file()
          +", line "+pos().line()+")";
  	}  
	
    syn lazy boolean PointcutExpr.hasGlobal() = false;
    
    eq BinaryPointcutExpr.hasGlobal(){
    	return getLhs().hasGlobal() || getRhs().hasGlobal();
    }
    
    eq GlobalExpr.hasGlobal(){
    	return true;
    }
    
    refine TypeCheck public void ExhibitBodyDecl.doTypeChecking(JPITypeDecl jpiDecl){
    	TypeCheck.ExhibitBodyDecl.doTypeChecking(jpiDecl);
		if (getPointcut().hasGlobal() && !jpiDecl.hasGlobalPointcut())
			error("TypeCheck: global() pointcut expression must be used in a exhibit clause which binds a global jpi definition.");			    	
    }

    refine GenericsJPI public void GenericExhibitBodyDecl.doTypeChecking(JPITypeDecl jpiDecl){
    	GenericsJPI.ExhibitBodyDecl.doTypeChecking(jpiDecl);
		if (getPointcut().hasGlobal() && !jpiDecl.hasGlobalPointcut())
			error("TypeCheck: global() pointcut expression must be used in a exhibit clause which binds a global jpi definition.");			    	
    }


	/***
	 * controlled global quantification
	 **/
 
 	inh lazy Collection<ClassDecl> CJPPointcutExpr.getAllSealedClasses();	
	eq Program.getCompilationUnit().getAllSealedClasses(){
		HashSet<ClassDecl> set = new HashSet<ClassDecl>();
		ClassDecl classDecl;
		TypeAccess jpiAccess;
		for(CompilationUnit cu : getCompilationUnits()){
			for(TypeDecl typeDecl : cu.getTypeDecls()){		
				if (!typeDecl.isClassDecl()){ //aspect is considered as a class
					continue;
				}
				classDecl = (ClassDecl)typeDecl;
				if (classDecl.isSealed()) {
					set.add(classDecl);
				}
				//getAllSealedClasses(classDecl.getBodyDeclList(),set);
			}
		}
		return set;	
	}

	/*private void Program.getAllSealedClasses(List<BodyDecl> bodyDeclList, HashSet<ExhibitBodyDecl> set) {
		for(BodyDecl bodyDecl : bodyDeclList){
			if (bodyDecl.isMemberClassDecl()){
				getAllSealedClasses(((MemberClassDecl)bodyDecl).getClassDecl().getBodyDeclList(),set);
				continue;
			}
			if (!bodyDecl.isExhibit()){
				continue;
			}
			set.add((ExhibitBodyDecl)bodyDecl);
		}
	}*/
	
	public boolean ClassDecl.isSealed() {
		for (Modifier modifier : getModifiers().getModifierList()) {
			if (modifier.getID().equals("sealed")) {
				return true;
			}
			if (modifier.getID().equals("open")) {
				return false;
			}
		}		
		return ((abc.ja.jpi.AbcExtension)abc.main.Main.v().getAbcExtension()).cgq.equals("sealed");
	}
    
}