//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package parser.visitor;

import parser.ast.*;
import prism.PrismLangException;

/**
 * Rename (according to RenamedModule definition), return result.
 */
public class Rename extends ASTTraverseModify
{
	private RenamedModule rm;
	
	public Rename(RenamedModule rm)
	{
		this.rm = rm;
	}
	
	public void visitPost(ModulesFile e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException("ModulesFile should never be renamed");
	}
	
	public void visitPost(PropertiesFile e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException("PropertiesFile should never be renamed");
	}
	
	public void visitPost(Declaration e) throws PrismLangException
	{
		// Get new name for variable
		String s = rm.getNewName(e.getName());
		// No new name is an error
		if (s != null) {
			e.setName(s);
		} else {
			throw new PrismLangException("Definition of module \"" + rm.getName() + "\" must rename variable \"" + e.getName() + "\"", rm);
		}
	}
	
	public void visitPost(parser.ast.Module e) throws PrismLangException
	{
		// New name for module is specied in RenamedModule
		e.setName(rm.getName());
	}
	
	public void visitPost(Command e) throws PrismLangException
	{
		// Rename synchronising action of command
		String s = rm.getNewName(e.getSynch());
		if (s != null) e.setSynch(s);
	}
	
	public void visitPost(Update e) throws PrismLangException
	{
		int i, n;
		String s;
		// Rename variables in update
		n = e.getNumElements();
		for (i = 0; i < n; i++) {
			s = rm.getNewName(e.getVar(i));
			if (s != null) e.setVar(i, new ExpressionIdent(s));
		}
	}

	public void visitPost(ExpressionTemporal e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException("Temporal operators should never be renamed");
	}

	public void visitPost(ExpressionFunc e) throws PrismLangException
	{
		// Rename function name (if necessary)
		String s = rm.getNewName(e.getName());
		if (s != null) e.setName(s);
	}

	public void visitPost(ExpressionIdent e) throws PrismLangException
	{
		// Rename identifier (if necessary)
		String s = rm.getNewName(e.getName());
		if (s != null) e.setName(s);
	}

	public void visitPost(ExpressionProb e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException("P operator should never be renamed");
	}

	public void visitPost(ExpressionReward e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException("R operator should never be renamed");
	}

	public void visitPost(ExpressionSS e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException("S operator should never be renamed");
	}

	public void visitPost(ExpressionExists e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException("E operator should never be renamed");
	}

	public void visitPost(ExpressionForAll e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException("A operator should never be renamed");
	}

	public void visitPost(ExpressionStrategy e) throws PrismLangException
	{
		// This renaming is only designed to be applied
		// at the level of an individual module (and below)
		throw new PrismLangException(e.getOperatorString() + " operator should never be renamed");
	}
}

