//
// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
//
// The contents of this file are covered under the licence agreement in the
// file "LICENCE" distributed with Cforall.
//
// RenameVars.cc --
//
// Author           : Richard C. Bilson
// Created On       : Sun May 17 12:05:18 2015
// Last Modified By : Peter A. Buhr
// Last Modified On : Tue Apr 30 17:07:57 2019
// Update Count     : 7
//

#include <ext/alloc_traits.h>      // for __alloc_traits<>::value_type
#include <memory>                  // for allocator_traits<>::value_type
#include <sstream>                 // for operator<<, basic_ostream, ostring...
#include <utility>                 // for pair

#include "Common/PassVisitor.h"
#include "Common/SemanticError.h"  // for SemanticError
#include "RenameVars.h"
#include "SynTree/Declaration.h"   // for DeclarationWithType, TypeDecl, Dec...
#include "SynTree/Expression.h"    // for Expression
#include "SynTree/Type.h"          // for Type, TypeInstType, TraitInstType
#include "SynTree/Visitor.h"       // for acceptAll, maybeAccept

namespace ResolvExpr {
	namespace {
		struct RenameVars {
			RenameVars();
			void reset();

			void previsit( TypeInstType * instType );
			void previsit( Type * );
			void postvisit( Type * );

		  private:
			int level, resetCount;
			std::list< std::unordered_map< std::string, std::string > > mapStack;
		};

		PassVisitor<RenameVars> global_renamer;
	} // namespace

	void renameTyVars( Type * t ) {
		t->accept( global_renamer );
	}

	void resetTyVarRenaming() {
		global_renamer.pass.reset();
	}

	namespace {
		RenameVars::RenameVars() : level( 0 ), resetCount( 0 ) {
			mapStack.push_front( std::unordered_map< std::string, std::string >() );
		}

		void RenameVars::reset() {
			level = 0;
			resetCount++;
		}

		void RenameVars::previsit( TypeInstType * instType ) {
			previsit( (Type *)instType );
			std::unordered_map< std::string, std::string >::const_iterator i = mapStack.front().find( instType->name );
			if ( i != mapStack.front().end() ) {
				instType->name = i->second;
			} // if
		}

		void RenameVars::previsit( Type * type ) {
			if ( ! type->forall.empty() ) {
				// copies current name mapping into new mapping
				mapStack.push_front( mapStack.front() );
				// renames all "forall" type names to `_${level}_${name}'
				for ( auto td : type->forall ) {
					std::ostringstream output;
					output << "_" << resetCount << "_" << level << "_" << td->name;
					std::string newname( output.str() );
					mapStack.front()[ td->get_name() ] = newname;
					td->name = newname;
					// ditto for assertion names, the next level in
					level++;
					// acceptAll( td->assertions, *this );
				} // for
			} // if
		}

		void RenameVars::postvisit( Type * type ) {
			// clears name mapping added by typeBefore()
			if ( ! type->forall.empty() ) {
				mapStack.pop_front();
			} // if
		}
	} // namespace
} // namespace ResolvExpr

// Local Variables: //
// tab-width: 4 //
// mode: c++ //
// compile-command: "make install" //
// End: //