/* the names of fresh variables are guaranteed not to clash
 * with the names of other variables */
aspect FreshVariables {
	interface FreshVariable extends Variable { 
		String pickFreshName();
	}
	FreshParameter implements FreshVariable;
	FreshLocalVariable implements FreshVariable;
	FreshField implements FreshVariable;
	
	public FreshParameter.FreshParameter(Access type, String name) {
		this(new Modifiers(new List()), type, name);
	}
	
	public FreshLocalVariable.FreshLocalVariable(Access type, String name) {
		this(new Modifiers(new List()), type, name, new Opt<Expr>());
	}
	
	public boolean FreshVariable.canIntroduceLocal(String name) {
		return true;
	}
	
	public String FreshVariable.name() {
		return "#fresh#" + super.name();
	}
	
	eq FreshVariable.refreshVariable() = this;
	
	public static LanguageExtension ASTNode.FRESH_VARIABLES = new LanguageExtension("fresh variables") {
		public void eliminateOn(ASTNode n) {
			n.eliminateFreshVariables();
			n.flushCaches();
		}
	};
	
	public void ASTNode.eliminateFreshVariables() {
		for(int i=0;i<getNumChild();++i) {
			ASTNode ch = getChild(i);
			if(ch != null)
				ch.eliminateFreshVariables();
		}
	}
	
	public void FreshParameter.eliminateFreshVariables() {
		String new_name = pickFreshName();
		ParameterDeclaration pd = new ParameterDeclaration(getModifiers(), getTypeAccess(), new_name);
		for(VarAccess va : uses()) {
			assert va.isLocked();
			va.lock(pd);
		}
		replaceWith(pd);
		pd.eliminateFreshVariables();
	}
	
	public void FreshLocalVariable.eliminateFreshVariables() {
		String new_name = pickFreshName();
		VariableDeclaration vd = new VariableDeclaration(getModifiers(), getTypeAccess(), new_name, getInitOpt());
		for(VarAccess va : uses()) {
			assert va.isLocked();
			va.lock(vd);
		}
		replaceWith(vd);
		vd.eliminateFreshVariables();
	}
	
	public void FreshField.eliminateFreshVariables() {
		String new_name = pickFreshName();
		FieldDeclaration fd = new FieldDeclaration(getModifiers(), getTypeAccess(), new_name, getInitOpt());
		for(VarAccess va : uses()) {
			assert va.isLocked();
			va.lock(fd);
		}
		replaceWith(fd);
		fd.eliminateFreshVariables();
	}
	
	public String FreshField.pickFreshName() {
		String fresh_name = getID();
		if(!hostType().localFields(fresh_name).isEmpty()) {
			for(int i=0;;++i) {
				fresh_name = getID()+i;
				if(hostType().localFields(fresh_name).isEmpty())
					break;
			}
		}
		return fresh_name;
	}
	
	public String FreshParameter.pickFreshName() {
		String fresh_name = getID();
		Collection<Declaration> decls = hostBodyDecl().allDecls();
		if(conflicts(fresh_name, decls)) {
			for(int i=0;;++i) {
				fresh_name = getID()+i;
				if(!conflicts(fresh_name, decls))
					break;
			}
		}
		return fresh_name;
	}
	
	// duplicate of the preceding method
	public String FreshLocalVariable.pickFreshName() {
		String fresh_name = getID();
		Collection<Declaration> decls = hostBodyDecl().allDecls();
		if(conflicts(fresh_name, decls)) {
			for(int i=0;;++i) {
				fresh_name = getID()+i;
				if(!conflicts(fresh_name, decls))
					break;
			}
		}
		return fresh_name;
	}
	
	// check whether the name conflicts with any of the decls
	public boolean FreshVariable.conflicts(String name, Collection<Declaration> decls) {
		for(Declaration decl : decls)
			if(decl != this && !(decl instanceof MethodDecl) && decl.name().equals(name))
				return true;
		return false;
	}
	
	// collect all declarations made or referenced in a subtree
	public Collection<Declaration> ASTNode.allDecls() {
		HashSet<Declaration> res = new HashSet<Declaration>();
		collectAllDecls(res);
		return res;
	}
	
	public void ASTNode.collectAllDecls(Collection<Declaration> res) {
		for(int i=0;i<getNumChild();++i)
			getChild(i).collectAllDecls(res);
	}
	
	public void Declaration.collectAllDecls(Collection<Declaration> res) {
		res.add(this);
		super.collectAllDecls(res);
	}
	
	// this shouldn't really be necessary, but JastAdd doesn't propagate through
	// more than one interface
	public void Variable.collectAllDecls(Collection<Declaration> res) {
		res.add(this);
		super.collectAllDecls(res);
	}
	
	public void PackageAccess.collectAllDecls(Collection<Declaration> res) {
		res.add(lookupPackage(getTopLevelPackage()));
		super.collectAllDecls(res);
	}
	
	public void TypeAccess.collectAllDecls(Collection<Declaration> res) {
		if(!getPackage().equals(""))
			res.add(lookupPackage(getTopLevelPackage()));
		res.add(decl());
		super.collectAllDecls(res);
	}
	
	public void VarAccess.collectAllDecls(Collection<Declaration> res) {
		res.add(decl());
		super.collectAllDecls(res);
	}
	
	public void MethodAccess.collectAllDecls(Collection<Declaration> res) {
		res.add(decl());
		super.collectAllDecls(res);
	}

	// replace all declarations in this subtree by their fresh counterparts
	public void ASTNode.freshenAllDeclarations() {
		freshenDeclaration();
		for(int i=0;i<getNumChild();++i) {
			ASTNode child = getChild(i);
			if(child != null)
				child.freshenAllDeclarations();
		}
	}
	public void TypeDecl.freshenAllLocalDeclarations() { }

	public void ASTNode.freshenDeclaration() { }
	public void ParameterDeclaration.freshenDeclaration() {
		Collection<VarAccess> uses = allUses();
		FreshParameter fp = new FreshParameter(getModifiers(), getTypeAccess(), getID());
		for(VarAccess va : uses)
			va.lock(fp);
		replaceWith(fp);
	}
	public void VariableDeclaration.freshenDeclaration() {
		Collection<VarAccess> uses = allUses();
		FreshLocalVariable fv = new FreshLocalVariable(getModifiers(), getTypeAccess(), getID(), getInitOpt());
		for(VarAccess va : uses)
			va.lock(fv);
		replaceWith(fv);
	}

	public FreshLocalVariable ParameterDeclaration.asFreshVariableDeclaration() {
		Collection<VarAccess> uses = allUses();
		FreshLocalVariable fv = new FreshLocalVariable(getModifiers(), getTypeAccess(), getID(), new Opt());
		for(VarAccess va : uses)
			va.lock(fv);
		return fv;
	}
}