//
// 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 : Andrew Beach
// Last Modified On : Thr Jun 20 17:39:00 2019
// Update Count     : 8
//

#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 "AST/ForallSubstitutionTable.hpp"
#include "AST/Pass.hpp"
#include "AST/Type.hpp"
#include "Common/PassVisitor.h"
#include "Common/ScopedMap.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 {
	class RenamingData {
		int level = 0;
		int resetCount = 0;
		ScopedMap< std::string, std::string > nameMap;
	public:
		ast::ForallSubstitutionTable subs;

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

		void rename( TypeInstType * type ) {
			auto it = nameMap.find( type->name );
			if ( it != nameMap.end() ) {
				type->name = it->second;
			}
		}

		void openLevel( Type * type ) {
			if ( ! type->forall.empty() ) {
				nameMap.beginScope();
				// 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() );
					nameMap[ td->get_name() ] = newname;
					td->name = newname;
					// ditto for assertion names, the next level in
					level++;
				}
			}
		}

		void closeLevel( Type * type ) {
			if ( !type->forall.empty() ) {
				nameMap.endScope();
			}
		}

		const ast::TypeInstType * rename( const ast::TypeInstType * type ) {
			// re-linking of base type handled by WithForallSubstitutor

			// rename
			auto it = nameMap.find( type->name );
			if ( it != nameMap.end() ) {
				// unconditionally mutate because map will *always* have different name, 
				// if this mutates, will *always* have been mutated by ForallSubstitutor above
				ast::TypeInstType * mut = ast::mutate( type );
				mut->name = it->second;
	            type = mut;
			}

			return type;
		}

		template<typename NodeT>
		const NodeT * openLevel( const NodeT * type ) {
			if ( type->forall.empty() ) return type;
			
			nameMap.beginScope();

			// Load new names from this forall clause and perform renaming.
			NodeT * mutType = ast::mutate( type );
			assert( type == mutType && "mutated type must be unique from ForallSubstitutor" );
			for ( ast::ptr< ast::TypeDecl > & td : mutType->forall ) {
				std::ostringstream output;
				output << "_" << resetCount << "_" << level << "_" << td->name;
				std::string newname =  output.str();
				nameMap[ td->name ] = newname;
				++level;

				ast::TypeDecl * mutDecl = ast::mutate( td.get() );
				assert( td == mutDecl && "mutated decl must be unique from ForallSubstitutor" );
				mutDecl->name = newname;
				// assertion above means `td = mutDecl;` is unnecessary
			}
			// assertion above means `type = mutType;` is unnecessary

			return type;
		}

		void closeLevel( const ast::ParameterizedType * type ) {
			if ( type->forall.empty() ) return;
			
			nameMap.endScope();
		}
	};

	// Global State:
	RenamingData renaming;

	struct RenameVars_old {
		void previsit( TypeInstType * instType ) {
			renaming.openLevel( (Type*)instType );
			renaming.rename( instType );
		}
		void previsit( Type * type ) {
			renaming.openLevel( type );
		}
		void postvisit( Type * type ) {
			renaming.closeLevel( type );
		}
	};
	
	struct RenameVars_new /*: public ast::WithForallSubstitutor*/ {
		#warning when old RenameVars goes away, replace hack below with global pass inheriting from WithForallSubstitutor
		ast::ForallSubstitutionTable & subs = renaming.subs;

		const ast::FunctionType * previsit( const ast::FunctionType * type ) {
			return renaming.openLevel( type );
		}
		const ast::StructInstType * previsit( const ast::StructInstType * type ) {
			return renaming.openLevel( type );
		}
		const ast::UnionInstType * previsit( const ast::UnionInstType * type ) {
			return renaming.openLevel( type );
		}
		const ast::TraitInstType * previsit( const ast::TraitInstType * type ) {
			return renaming.openLevel( type );
		}
		const ast::TypeInstType * previsit( const ast::TypeInstType * type ) {
			return renaming.rename( renaming.openLevel( type ) );
		}
		void postvisit( const ast::ParameterizedType * type ) {
			renaming.closeLevel( type );
		}
	};

} // namespace

void renameTyVars( Type * t ) {
	PassVisitor<RenameVars_old> renamer;
	t->accept( renamer );
}

const ast::Type * renameTyVars( const ast::Type * t ) {
	ast::Pass<RenameVars_new> renamer;
	return t->accept( renamer );
}

void resetTyVarRenaming() {
	renaming.reset();
}

} // namespace ResolvExpr

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