class Illation_machine;
class Formulas;

class  Node{
	friend class Formulas;
	friend class Illation_machine;
public:
	Node();
	~Node(){ delete []formula;}
	Node(char *str,Node *link);
private:
	char *formula;
	Node *next;
};
Node::Node(char *str,Node *link){
	formula=new char[strlen(str)+1];
	mystrcpy(formula,str);
	next=link;
}

class Formulas{
	friend class Illation_machine;
public:
	Formulas(){ first=last=NULL;number=0; }
	Formulas(char *str);
	~Formulas();
	void Add(char *str);
	void Delete(Node *p);
	void copy(Formulas *f);
	bool Isin(char *str);
	void Toinfix(char *str);
	void print(CString &str);
	bool isoperator(char c){ return c=='!'||c=='*'||c=='+'||c=='>'||c=='=';}
private:
    Node *first,*last;
	int number;
};
Formulas::Formulas(char *str){
	first=last=new Node(str,NULL);
	number=1;
}
Formulas::~Formulas(){
	Node *p,*temp=first;
	while(temp!=NULL){
		p=temp;
		temp=temp->next;
		delete p;
	}
}
void Formulas::Add(char *str){
	if(first==NULL)
		first=last=new Node(str,NULL);
	else{
		last->next=new Node(str,NULL);
		last=last->next; 
	}
	number++;
}

void Formulas::Delete(Node *p){
		if(first!=NULL){
			if(p==first){
				first=first->next;
				delete p;
			}
			else{
				Node *temp=first,*pre;
				while(temp!=NULL&&temp!=p){
					pre=temp;
					temp=temp->next;
				}
				if(temp!=NULL){
					pre->next=temp->next;
					delete temp;
					if(temp==last)
						last=pre;
				}
			}
		}
		number--;
}

void Formulas::copy(Formulas *f){
	if(f->first!=NULL&&f->number!=0){
		last=first=new Node(f->first->formula,NULL);
		Node *temp=f->first->next;
		while(temp!=NULL){
			last->next=new Node(temp->formula,NULL);
			last=last->next;
			temp=temp->next;
		}
	}
	number=f->number;
}

bool Formulas::Isin(char *str){
	Node *temp=first;
	while(temp!=NULL){
		if(strcmp(str,temp->formula)==0)
			return true;
		temp=temp->next;
	}
	return false;
}

void Formulas::Toinfix(char *str){
	mystack<char *> st;
	for(int i=strlen(str)-1;i>=0;i--){
		if( ('a'<=str[i]&&str[i]<='z')||('A'<=str[i]&&str[i]<='Z') ){
			char *temp=new char[2];
			temp[0]=str[i];
			temp[1]='\0';
			st.push(temp);
		}
		else if(str[i]=='!'){
			int k=0;
			char *op=st.top(),*temp;
			st.pop();
			temp=new char[strlen(op)+4];
			temp[0]='!';
			if(strlen(op)!=1&&op[0]!='!')temp[++k]='(';
			mystrcpy(temp+k+1,op);
			if(strlen(op)!=1&&op[0]!='!')temp[strlen(op)+2]=')';
			temp[strlen(op)+2*k+1]='\0';
			st.push(temp);
			delete []op;
		}
		else if(isoperator(str[i])){
			int k1=0,k2=0;
			char *op1,*op2;
			op1=st.top(); st.pop();
			op2=st.top(); st.pop();
			char *temp=new char[strlen(op1)+strlen(op2)+6];
			if(strlen(op1)>2)temp[k1++]='(';
			mystrcpy(temp+k1,op1);
			if(strlen(op1)>2)temp[strlen(op1)+k1]=')';
			temp[strlen(op1)+k1*2]=str[i];

			if(strlen(op2)>2){temp[strlen(op1)+2*k1+1]='(';k2++;}
			mystrcpy(temp+strlen(op1)+2*k1+k2+1,op2);
			if(strlen(op2)>2)temp[strlen(op1)+strlen(op2)+2*k1+k2+1]=')';
			temp[strlen(op1)+strlen(op2)+2*k1+2*k2+1]='\0';
			st.push(temp);
			delete []op1;
			delete []op2;
		}
	}
	char *temp=st.top();st.pop();
	mystrcpy(str,temp);
	delete []temp;
}

void Formulas::print(CString &str){
	Node *temp=first;
	while(temp!=NULL){
		if(strlen(temp->formula)==1){
			str+=temp->formula;
			if(temp!=last)str+=",";
		}
		else{
			char *form=new char[strlen(temp->formula)*3];
			mystrcpy(form,temp->formula);
			Toinfix(form);
			str+=form;
			if(temp!=last)str+=",";
			delete form;
		}
		temp=temp->next;
	}
}
//第二部分，推理機類

class Illation_machine{
public:
	Illation_machine(){ formula=NULL; }
	Illation_machine(char *str);
	~Illation_machine(){ delete []formula; }
	int Illation(myqueue<CString> &poof_procedure);
private:
	int Illation(Formulas *pre,Formulas *post,int &line,myqueue<CString> &poof_procedure);
	bool Detect(Formulas *f,char &operat,char *op1,char *op2);
	bool isoperator(char c){ return c=='!'||c=='*'||c=='+'||c=='>'||c=='=';}
	int order(char c){				//字符的秩
		if(c=='!')
			return 0;
		else if(isoperator(c))
			return 1;
		else
			return -1;
	}
	char *formula;
};

Illation_machine::Illation_machine(char *str){//在此構造函數中將str轉為前綴存于formula中
	mystack<char> temp,operat;
	for(int i=strlen(str)-1;i>=0;i--){
		if( ('a'<=str[i]&&str[i]<='z')||('A'<=str[i]&&str[i]<='Z') )
			temp.push(str[i]);
		else{
			if(str[i]=='('){
				char c;
				while( ( c=operat.top() )!=')' ){ temp.push(c); operat.pop(); }
				operat.pop(); 
			}
			else if(str[i]=='!')
				temp.push(str[i]);
			else
				operat.push(str[i]);
		}
	}
	while(operat.IsEmpty ()==false){
		temp.push(operat.top());
		operat.pop();
	}
	formula=new char[strlen(str)+1];
	int j=0;
	while(temp.IsEmpty ()==false){
		formula[j++]=temp.top();
		temp.pop();
	}
	formula[j]='\0';
}


bool Illation_machine::Detect(Formulas *f,char &operat,char *op1,char *op2){

	if(f->number==0) return false;
	Node *temp=f->first;
	while(temp!=NULL){
		if(isoperator(temp->formula[0])){
			int n=strlen(temp->formula);
			operat=temp->formula[0];
			if(temp->formula[0]=='!'){
				mystrncpy(op1,(temp->formula)+1,n-1);
				op1[n-1]='\0';
			}
			else{
				int count=1,s=1,start=1;
				while(count<n){
					s+=order(temp->formula[count]);
					if(s==0){
						s=1;
						if(start==1){
							mystrncpy(op1,temp->formula+start,count-start+1);
							op1[count-start+1]='\0';
						}
						else{
							mystrncpy(op2,temp->formula+start,count-start+1);
							op2[count-start+1]='\0';
						}
					start=count+1;
					}
					count++;
				}
			}
			f->Delete(temp); 
			break;
		}
		temp=temp->next; 
	}
	if(temp!=NULL)
		return true;
	else
		return false;
}

int Illation_machine::Illation(myqueue<CString> &poof_procedure){
	Formulas *pre,*post;
	pre=new Formulas;
	post=new Formulas(formula);
	int line=1;
	int f=Illation(pre,post,line,poof_procedure);
	delete pre;
	delete post;
	return f;
}

int Illation_machine::Illation(Formulas *pre,Formulas *post,int &line,myqueue<CString> &poof_procedure){
	char operat;
	char op1[100],op2[100],reason[8];
	Formulas pre1,post1,pre2,post2;
	int reason1,reason2,f1=1,f2=1;
	pre1.copy(pre);
	post1.copy(post);
	if(Detect(pre,operat,op1,op2)){
		pre2.copy(pre);
		post2.copy(post);
		switch(operat){
			case '!':post->Add(op1);
				     f1=Illation(pre,post,line,poof_procedure);
					 mystrcpy(reason,"!├");
					 break;
			case '*':pre->Add(op1);
					 pre->Add(op2);
					 f1=Illation(pre,post,line,poof_procedure);
					 mystrcpy(reason,"*├");
					 break;
			case '+':pre->Add(op1);
					 f1=Illation(pre,post,line,poof_procedure);
					 reason1=line-1;
					 pre2.Add(op2);
					 f2=Illation(&pre2,&post2,line,poof_procedure);
					 reason2=line-1;
					 mystrcpy(reason,"+├");
					 break;
			case '>':post->Add(op1);
					 f1=Illation(pre,post,line,poof_procedure);
					 reason1=line-1;
					 pre2.Add(op2);
					 f2=Illation(&pre2,&post2,line,poof_procedure);
					 reason2=line-1;
					 mystrcpy(reason,">├");
					 break;
			case '=':;pre->Add(op1);
					pre->Add(op2);
					f1=Illation(pre,post,line,poof_procedure);
					reason1=line-1;
					post2.Add(op1);
					post2.Add(op2);
					f2=Illation(&pre2,&post2,line,poof_procedure);
					reason2=line-1;
					mystrcpy(reason,"=├");
					break;
		}
		CString temp;
		temp.Format(_T("(%d)    "),line++);
		pre1.print(temp);
		temp+="├";
		post1.print(temp);
		temp+="              是由(";
		if(operat=='!'||operat=='*'){
			CString t;
			t.Format(_T("%d"),line-2);
			temp+=t;
			temp+=")實施";
			temp+=reason;
			temp+="規則得到";
		}
		else{
			CString t;
			t.Format(_T("%d"),reason1);
			temp+=t;
			t.Empty();
			t.Format(_T("%d"),reason2);
			temp+="),(";
			temp+=t;
			temp+=")實施";
			temp+=reason;
			temp+="規則得到";
		}
		poof_procedure.push(temp);
	}
	else if(Detect(post,operat,op1,op2)){
		pre2.copy(pre);
		post2.copy(post);
		switch(operat){
			case '!':pre->Add(op1);
				     f1=Illation(pre,post,line,poof_procedure);
					 mystrcpy(reason,"├!");
					 break;
			case '*':post->Add(op1);
					 f1=Illation(pre,post,line,poof_procedure);
					 reason1=line-1;
					 post2.Add(op2);
					 f2=Illation(&pre2,&post2,line,poof_procedure);	
					 reason2=line-1;
					 mystrcpy(reason,"├*");
					 break;
			case '+':post->Add(op1);
					 post->Add(op2);
					 f1=Illation(pre,post,line,poof_procedure);
					 mystrcpy(reason,"├+");
					 break;
			case '>':pre->Add(op1);
					 post->Add(op2);
					 f1=Illation(pre,post,line,poof_procedure);
					 mystrcpy(reason,"├>");
					 break;
			case '=': pre->Add(op1);
					  post->Add(op2);
					  f1=Illation(pre,post,line,poof_procedure);
					  reason1=line-1;
					  pre2.Add(op2);
					  post2.Add(op1);
					  f2=Illation(&pre2,&post2,line,poof_procedure);
					  reason2=line-1;
					  mystrcpy(reason,"├=");
					  break;
		}
		CString temp;
		temp.Format(_T("(%d)    "),line++);
		pre1.print(temp);
		temp+="├";
		post1.print(temp);
		temp+="              是由(";
		if(operat=='!'||operat=='+'||operat=='>'){
			CString t;
			t.Format(_T("%d"),line-2);
			temp+=t;
			temp+=")實施";
			temp+=reason;
			temp+="規則得到";
		}
		else{
			CString t;
			t.Format(_T("%d"),reason1);
			temp+=t;
			t.Empty();
			t.Format(_T("%d"),reason2);
			temp+="),(";
			temp+=t;
			temp+=")實施";
			temp+=reason;
			temp+="規則得到";
		}
		poof_procedure.push(temp);
	}
	else{
		Node *temp=pre->first;
		while(temp!=NULL){
			if(post->Isin(temp->formula)){
			CString temp;
			temp.Format(_T("(%d)    "),line++);
			pre1.print(temp);
			temp+="├";
			post1.print(temp);
			temp+="              定理";
			poof_procedure.push(temp);
			break;
			}
			temp=temp->next;
		}
		if(temp==NULL)f1=0;
	}
	return f1*f2;
}