/*
 * PDAToRHPDA.cpp
 *
 *  Created on: 23. 3. 2014
 *	  Author: Jan Travnicek
 */

#include "PDAToRHPDA.h"

#include <exception/AlibException.h>
#include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>
#include <automaton/PDA/RealTimeHeightDeterministicNPDA.h>
#include <automaton/PDA/DPDA.h>
#include <automaton/PDA/NPDA.h>

#include <alphabet/BottomOfTheStackSymbol.h>

#include <set>
#include <map>
#include <queue>

namespace automaton {

automaton::RealTimeHeightDeterministicDPDA PDAToRHPDA::convert( const automaton::RealTimeHeightDeterministicDPDA & pda ) {
	return pda;
}

auto PDAToRHPDARealTimeHeightDeterministicDPDA = PDAToRHPDA::RegistratorWrapper<automaton::RealTimeHeightDeterministicDPDA, automaton::RealTimeHeightDeterministicDPDA>(PDAToRHPDA::getInstance(), PDAToRHPDA::convert);

automaton::RealTimeHeightDeterministicNPDA PDAToRHPDA::convert( const automaton::RealTimeHeightDeterministicNPDA & pda ) {
	return pda;
}

auto PDAToRHPDARealTimeHeightDeterministicNPDA = PDAToRHPDA::RegistratorWrapper<automaton::RealTimeHeightDeterministicNPDA, automaton::RealTimeHeightDeterministicNPDA>(PDAToRHPDA::getInstance(), PDAToRHPDA::convert);

automaton::RealTimeHeightDeterministicDPDA PDAToRHPDA::convert( const automaton::DPDA & pda ) {
	automaton::State q0 = automaton::createUniqueState(automaton::State("q0"), pda.getStates());

	RealTimeHeightDeterministicDPDA res(q0, alphabet::Symbol { alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK } );

	res.setInputAlphabet(pda.getInputAlphabet());
	for(const auto& state : pda.getStates())
		res.addState(state);
	res.setFinalStates(pda.getFinalStates());
	std::set<alphabet::Symbol> stackSymbols = pda.getStackAlphabet();
	stackSymbols.insert( alphabet::Symbol { alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK } );
	res.setStackAlphabet(stackSymbols);

	res.addCallTransition(q0, pda.getInitialState(), pda.getInitialSymbol());

	std::string us("us");
	int i = 0;
	for(const auto& transition : pda.getTransitions()) {
		const auto& to = transition.second;
		if(std::get<2>(transition.first).size() == 0 && to.second.size() == 0)
			res.addLocalTransition(std::get<0>(transition.first), std::get<1>(transition.first), to.first);
		else if(std::get<2>(transition.first).size() == 1 && to.second.size() == 0)
			res.addReturnTransition(std::get<0>(transition.first), std::get<1>(transition.first), std::get<2>(transition.first)[0], to.first);
		else if(std::get<2>(transition.first).size() == 0 && to.second.size() == 1)
			res.addCallTransition(std::get<0>(transition.first), std::get<1>(transition.first), to.first, to.second[0]);
		else {
			int popPushIndex = 0;
			int popPushSymbols = std::get<2>(transition.first).size() + to.second.size();

			automaton::State lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(i)), res.getStates());
			std::for_each (std::get<2>(transition.first).rbegin(), std::get<2>(transition.first).rend(), [&](const alphabet::Symbol& pop) {
				automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : lastUS;
				if(popPushIndex != 0) lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(++i)), res.getStates());
				automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : lastUS;

				res.addState(fromState);
				res.addState(toState);

				if(popPushIndex == 0)
					res.addReturnTransition(fromState, std::get<1>(transition.first), pop, toState);
				else
					res.addReturnTransition(fromState, pop, toState);
				popPushIndex++;
			});
			for(const alphabet::Symbol& push : to.second) {
				automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : lastUS;
				if(popPushIndex != 0) lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(++i)), res.getStates());
				automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : lastUS;

				res.addState(fromState);
				res.addState(toState);

				if(popPushIndex == 0)
					res.addCallTransition(fromState, std::get<1>(transition.first), toState, push);
				else
					res.addCallTransition(fromState, toState, push);
				popPushIndex++;
			}
		}
	}
	
	return res;
}

auto PDAToRHPDADPDA = PDAToRHPDA::RegistratorWrapper<automaton::RealTimeHeightDeterministicDPDA, automaton::DPDA>(PDAToRHPDA::getInstance(), PDAToRHPDA::convert);

automaton::RealTimeHeightDeterministicNPDA PDAToRHPDA::convert( const automaton::NPDA & pda ) {
	RealTimeHeightDeterministicNPDA res(alphabet::Symbol { alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK } );

	res.setInputAlphabet(pda.getInputAlphabet());
	res.setStates(pda.getStates());
	res.setFinalStates(pda.getFinalStates());
	std::set<alphabet::Symbol> stackSymbols = pda.getStackAlphabet();
	stackSymbols.insert( alphabet::Symbol { alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK } );
	res.setStackAlphabet(stackSymbols);

	automaton::State q0 = automaton::createUniqueState(automaton::State("q0"), res.getStates());
	res.addState(q0);
	res.addInitialState(q0);

	res.addCallTransition(q0, pda.getInitialState(), pda.getInitialSymbol());

	std::string us("us");
	int i = 0;
	for(const auto& transition : pda.getTransitions()) {
		for(const auto& to : transition.second) {
			if(std::get<2>(transition.first).size() == 0 && to.second.size() == 0)
				res.addLocalTransition(std::get<0>(transition.first), std::get<1>(transition.first), to.first);
			else if(std::get<2>(transition.first).size() == 1 && to.second.size() == 0)
				res.addReturnTransition(std::get<0>(transition.first), std::get<1>(transition.first), std::get<2>(transition.first)[0], to.first);
			else if(std::get<2>(transition.first).size() == 0 && to.second.size() == 1)
				res.addCallTransition(std::get<0>(transition.first), std::get<1>(transition.first), to.first, to.second[0]);
			else {
				int popPushIndex = 0;
				int popPushSymbols = std::get<2>(transition.first).size() + to.second.size();

				automaton::State lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(i)), res.getStates());
				std::for_each (std::get<2>(transition.first).rbegin(), std::get<2>(transition.first).rend(), [&](const alphabet::Symbol& pop) {
					automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : lastUS;
					if(popPushIndex != 0) lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(++i)), res.getStates());
					automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : lastUS;

					res.addState(fromState);
					res.addState(toState);

					if(popPushIndex == 0)
						res.addReturnTransition(fromState, std::get<1>(transition.first), pop, toState);
					else
						res.addReturnTransition(fromState, pop, toState);
					popPushIndex++;
				});
				for(const alphabet::Symbol& push : to.second) {
					automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : lastUS;
					if(popPushIndex != 0) lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(++i)), res.getStates());
					automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : lastUS;

					res.addState(fromState);
					res.addState(toState);

					if(popPushIndex == 0)
						res.addCallTransition(fromState, std::get<1>(transition.first), toState, push);
					else
						res.addCallTransition(fromState, toState, push);
					popPushIndex++;
				}
			}
		}
	}
	
	return res;
}

auto PDAToRHPDANPDA = PDAToRHPDA::RegistratorWrapper<automaton::RealTimeHeightDeterministicNPDA, automaton::NPDA>(PDAToRHPDA::getInstance(), PDAToRHPDA::convert);

automaton::Automaton PDAToRHPDA::convert(const Automaton& automaton) {
	return getInstance().dispatch(automaton.getData());
}

}

namespace alib {

auto RealTimeHeightDeterministicDPDAFromDPDA = castApi::CastRegister<automaton::RealTimeHeightDeterministicDPDA, automaton::DPDA>(automaton::PDAToRHPDA::convert);
auto RealTimeHeightDeterministicNPDAFromNPDA = castApi::CastRegister<automaton::RealTimeHeightDeterministicNPDA, automaton::NPDA>(automaton::PDAToRHPDA::convert);

}