#include <iostream>
#include <string>
#include <vector>
#include <map>
#include <queue>
#include <cassert>
#include "tree.h"

using namespace std;


struct Axiom{
	Tree from,to;
};

ostream& operator<<(ostream &os,const Axiom &ax){
	return os<<ax.from<<" -> "<<ax.to;
}

void parseAxiom(vector<Axiom> &dst,const string &expr){
	size_t idx=expr.find('=');
	bool twoway=true;
	if(idx==string::npos){
		idx=expr.find('>');
		assert(idx!=string::npos);
		twoway=false;
	}
	assert(expr.find('=',idx+1)==string::npos);
	assert(expr.find('>',idx+1)==string::npos);
	string from=expr.substr(0,idx),to=expr.substr(idx+1);
	dst.push_back({Tree(from),Tree(to)});
	if(twoway)dst.push_back({Tree(to),Tree(from)});
}

vector<Axiom> importAxioms(const vector<string> &list){
	vector<Axiom> axioms;
	for(const string &str : list){
		parseAxiom(axioms,str);
	}
	return axioms;
}

using Heuristic = int (*)(const Tree&);

int heuristic_nleaves(const Tree &tree){return tree.nleaves();}
int heuristic_height(const Tree &tree){return tree.height();}

template <Heuristic F>
struct AscendingCompare{
	bool operator()(const Tree &a,const Tree &b) const {
		return F(a)>F(b);
	}
};

template <Heuristic F>
vector<Tree>* deduceEq(const vector<Axiom> &axioms,const Tree &startTree,const Tree &target){
	priority_queue<Tree,vector<Tree>,AscendingCompare<F>> pqu;
	map<Tree,Tree,TreeCompare> parentMap;
	pqu.push(startTree);
	Tree current;
	while(true){
		if(pqu.size()==0)return nullptr;
		current=pqu.top();
		pqu.pop();
		// cerr<<"current = "<<current;
		// {
		// 	auto it=parentMap.find(current);
		// 	if(it!=parentMap.end())cerr<<"   parent = "<<it->second<<endl;
		// 	else cerr<<endl;
		// }
		if(current.matches(target))break;
		for(const Axiom &ax : axioms){
			vector<Tree> nexts=current.replace(ax.from,ax.to);
			// cerr<<" ax = "<<ax<<endl;
			// cerr<<"   nexts.size() = "<<nexts.size()<<endl;
			for(const Tree &t : nexts){
				auto it=parentMap.find(t);
				if(it==parentMap.end()&&t.compare(startTree)!=0){
					parentMap.emplace(t,current);
					pqu.push(t);
					// cerr<<" Pushing "<<t<<endl;
				} else {
					// cerr<<" Skipping "<<t<<" because already seen"<<endl;
				}
			}
		}
	}
	vector<Tree> *v=new vector<Tree>();
	Tree *t=&current;
	while(true){
		// cerr<<"*t = "<<*t<<endl;
		v->push_back(*t);
		auto it=parentMap.find(*t);
		if(it==parentMap.end())break;
		t=&it->second;
	}
	return v;
}


void test_func(){
	Tree from("([2]*([2]*1))"),to("10");
	Tree subj("(([1]*1)*[1])");

	/*unordered_set<Variable> temps=to.collectTemporaries();
	for(Variable v : temps){
		cout<<v<<endl;
	}*/

	vector<Tree> res=subj.replace(from,to);
	for(const Tree &t : res){
		cout<<t<<endl;
	}
}

int main(){
	/*test_func();
	return 0;*/

	const vector<Axiom> axioms=importAxioms({
		// "([1]*[2])>([2]*[1])",  // Commutativity
		// "(([1]*[2])*[3])=([1]*([2]*[3]))",  // Associativity

		// "([1]*([1]*[2]))=[1]",  // Onno's 1=2 axioms
		// "(([2]*[1])*[1])=[1]",

		// "[1]=([1]*[1])",
		// "(([1]*[2])*[3])=(([2]*[3])*[1])",

		// "[1]=[2]",

		"[1]=([1]*([1]*([1]*[2])))",  // Daan's 1=2 axioms
		"(([2]*[1])*[1])=[1]",
	});
	const Tree t_from("1"),t_to("2");

	for(const Axiom &ax : axioms)cout<<ax<<endl;
	cout<<endl;

	vector<Tree> *res=deduceEq<heuristic_nleaves>(axioms,t_from,t_to);
	if(res==nullptr){
		cout<<"No deduction"<<endl;
	} else {
		cout<<"Deduction:"<<endl;
		for(int i=res->size()-1;i>=0;i--){
			cout<<res->at(i)<<endl;
		}
	}
}