/*
Research Project:   Graphical Database for Category Theory
                    J. Bradbury, Dr. R. Rosebrugh, I. Rutherford
                    M. Graves, J. Tweedle
                    Mount Allison University 2001
                    Updated: May 8th, 2003
File:               MakeConfluent.java
Description:	      This file contains the algorithms to make a given
						category confluent.  It is used by the MakeConfluentFrame
						class.
*/


public class MakeConfluent
{

	private Category cat;
	private String newRelations;   //Array to store relations that needed to be
	                               //added to current category in order to make it confluent.
	private String output;

	public MakeConfluent(Category newCat)
	{
		cat = newCat;
		newRelations = "";
		output = "";
	}

	public int overlap(int path1[], int path2[])
	/*
	Parameters:
	    path1, path2: arrays of integers representing two paths of arrows.
	Purpose:
	    To determine if there is an overlap between the two paths and to
	    return its length; if there is no overlap, returns -1.
	Design:
	    Compare the beginning of path1 to the end of path2.  If they are
	    the same, return the size of the overlap; otherwise return -1.
	*/
	{
		int i, k;
		//the length of the smaller of path1 and path2
		int size =0;
		//temporary variables to store portions of path1 and path2
		int temp1[] = new int [cat.ini.getMAXWORD()];
		int temp2[] = new int [cat.ini.getMAXWORD()];

		if(cat.path_len(path1) > cat.path_len(path2))
		{
			size = cat.path_len(path2);
		}
		else
		{
			size = cat.path_len(path1);
		}
		for(i=0;i<size;i++)
		{
			temp1 = cat.copy_path(path1);
			temp1[size-i] = -1;
			for(k=0;k<size-i;k++)
			{
				int indexof = cat.path_len(path2) - size + k +i;
				temp2[k] = path2[indexof];
			}
			temp2[k] = -1;
			if(cat.equals(temp1,temp2))
			{
				return(size-i);
			}
		}
		return(-1);
	}

	public void add_relation(int w1[], int w2[])
	/*
	Parameters:
	    w1,w2:  arrays of integers representing paths which are the left and
	                    right sides of a relation to be added to the category.
	    A:      pointer to the current category.
	Purpose:
	    To add the relation w1 = w2 to the set of relations in the category *A.
	Design:
	    The number of relations in the category is incremented.  Whichever of
	    w1 and w2 has the greater order is stored as the left side of the new
	    relation, and the other as the right side.
	*/
	{
		Relation r = new Relation();

		cat.num_relations++;

		if (cat.greater(w1,w2))
		{
			r.lhs = cat.copy_path(w1);
			r.rhs = cat.copy_path(w2);
		}
		else
		{
			r.lhs = cat.copy_path(w2);
			r.rhs = cat.copy_path(w1);
		}
		cat.relations[cat.num_relations-1] = r;

		int i = 0;
		while (cat.relations[cat.num_relations-1].lhs[i] != -1)
		{
			i++;
		}
		i = 0;
		while (cat.relations[cat.num_relations-1].rhs[i] != -1)
		{
			i++;
		}

		//Display	on the screen relation that is being added to category
		output += "\nThe relation " + cat.path_to_string(cat.relations[cat.num_relations-1].lhs) 
				 + " = " + cat.path_to_string(cat.relations[cat.num_relations-1].rhs) + " will be added to the set of relations.";

		//Add relatiom to graphical dispaly of category
		newRelations += ", " + cat.path_to_string(cat.relations[cat.num_relations-1].lhs) + " = " + cat.path_to_string(cat.relations[cat.num_relations-1].rhs);
	}

	public boolean reduce_overlap(Relation rel1, Relation rel2, int olap_size)
	/*
	Parameters:
	    rel1, rel2:     two relations from the current category whose left sides
	                    have an overlap.
	    olap_size:      the size of the overlap between rel1 and rel2.
	    A:              pointer to the current category.
	Purpose:
	    To check to see that rel1 and rel2 satisfy the Overlap rule of the
	    Knuth-Bendix algorithm and if not, to add a relation to the set
	    of relations in the category.  Returns a boolean indicating whether
	    or not a relation was added.
	Design:
	    Construct r1 and r2 as described below in the variable declarations.
	    If w1 and w2 (the reduced forms of r1 and r2) are not equal, then
	    add the relation w1 = w2 to the category.
	*/
	{
		//arrows in left side of rel1 BEFORE the overlap, plus right side of rel2
		int r1[] = new int [cat.ini.getMAXWORD()];
		// right side of rel1, plus arrows in left side of rel2 AFTER the overlap
		int r2[] = new int [cat.ini.getMAXWORD()];
		//reduced forms of r1 and r2
		int w1[] = new int [cat.ini.getMAXWORD()];
		int w2[] = new int [cat.ini.getMAXWORD()];
		//temporary variable to store path
		int temp[] = new int[cat.ini.getMAXWORD()];

		//textArea1.append("Entering reduce_overlap()\n");
		//Copy the rhs of rel1 into r2
		r2 = cat.copy_path(rel1.rhs);
		//Copy subpath of rel2 (ie. arrows after overlap) into temp array
		temp = copy_sub(temp, rel2.lhs, olap_size, cat.path_len(rel2.lhs)-olap_size);
		//Append temp array to r2
		r2 = cat.append_path(temp, r2);

		//Copy subpath of rel1(ie. arrows before the overlap) into r1
		r1 = copy_sub(r1, rel1.lhs, 0, cat.path_len(rel1.lhs) - olap_size);
		//Append the rhs of rel2 to r1
		r1 = cat.append_path(rel2.rhs, r1);

		//textArea1.append("Reducing r1 to w1\n");
		//textArea1.append("r1 = ");
//		if (r1[0] == -2)
//		{
//		  textArea1.append(" 1 \n");
//		}
//		else
//		{
		int i=0;
//			System.out.println(cat.path_to_string(r1));
		while (r1[i] != -1 && r1[i] != -2)
		{
//			System.out.println(r1[i]);
//				textArea1.append(" " + r1[i] + " ");
			i++;
		}
//			textArea1.append("\n");
//		}

		//Reduce r1 and r2 into w1 and w2
		w1 = cat.reduce(r1);
		//textArea1.append("Reducing r2 to w2\n");
		w2 = cat.reduce(r2);

		//textArea1.append("Comparing w1 and w2 for equality\n");

		//If the reduced forms of r1 and r2 are not equal,
		//add relation w1 = w2 to category
		if (!(cat.equals(w1,w2)))
		{
			add_relation(w1,w2);
		//	textArea1.append("Leaving reduce_overlap() [Relations added]\n");
			return(true);
		}
		//textArea1.append("Leaving reduce_overlap() [No relations added]\n");
		return(false);
	}

	public boolean reduce_subpath(Relation rel1, Relation rel2, int location)
	/*
	Parameters:
	    rel1, rel2:     two relations from the current category where the left
	                    side of rel2 is a subpath of the left side of rel1.
	    location:       the location of rel2 inside rel1.
	    A:              pointer to the current category.
	Purpose:
	    To check to see that rel1 and rel2 satisfy the Subpath rule of the
	    Knuth-Bendix algorithm and if not, to add a relation to the set of
	    relations in the category.  Returns a boolean indicating whether
	    or not a relation was added.
	Design:
	    Construct r1 and r2 as described below in the variable declarations.
	    If w1 and w2 (the reduced forms of r1 and r2) are not equal, then
	    add the relation w1 = w2 to the category.
	*/
	{
		//right side of rel1
		int r1[] = new int [cat.ini.getMAXWORD()];
		//left side of rel1 with left side of rel2
		//(substring) replaced by right side of rel2
		int r2[] = new int [cat.ini.getMAXWORD()];
		//reduced forms of r1 and r2
		int w1[] = new int [cat.ini.getMAXWORD()];
		int w2[] = new int [cat.ini.getMAXWORD()];
		//temporary variable to store path
		int temp[] = new int [cat.ini.getMAXWORD()];

		//Copy rhs of rel1 into r1
		r1 = cat.copy_path(rel1.rhs);

		//Copy subpath of lhs of rel1 into r2
		r2 = copy_sub(r2,rel1.lhs,0,location);

		//Append rhs of rel2 to r2
		r2 = cat.append_path(rel2.rhs, r2);
		//Copy a subpath of lhs of re11 into temp
		temp = copy_sub(temp,rel1.lhs,location+cat.path_len(rel2.lhs),cat.path_len(rel1.lhs)-(location+cat.path_len(rel2.lhs)));
		//Append temp to r2
		r2 = cat.append_path(temp, r2);

		//Reduce r1 and r2 into w1 and w2
		w1 = cat.reduce(r1);
		w2 = cat.reduce(r2);

		//If the reduced forms of r1 and r2 are not equal,
		//add relation w1 = w2 to category
		if (!cat.equals(w1,w2))
		{
			add_relation(w1,w2);
			return(true);
		}
		return(false);
	}

	public void make_confluent()
	/*
	Parameter:
	    cat:      pointer to the current category
	Purpose:
	    To check all pairs of relations in the category for the Overlap and
	    Subpath rules and to add relations to make the set of relations confluent.
	Design:
	    Using a double for loop, compare all pairs of relations.  Check for
	    any overlaps between the left sides of the two relations, and call
	    function reduce_overlap to add any relations necessary to make the
	    set of relations confluent.  Then, check if the left side of one
	    relation is a subpath of the other left side, and call function
	    reduce_subpath to add any necessary relations to the category.
	*/
	{
		//set to true when all overlaps and subpaths have been checked,
		//and the set of relations is confluent
		boolean done;
		//set to true when all overlaps have been checked
		boolean finished;

		int i,j;
		//size of an overlap between two paths
		int size;
		//location of one path inside another
		int loc;
		//position in one path to begin searching for another path as a substring
		int position;
		//temporary variables to store paths
		int temp1[] = new int [cat.ini.getMAXWORD()];
		int temp2[] = new int [cat.ini.getMAXWORD()];

		//Initialize done to fale
		done = false;
		//While not done...
		while(!done)
		{
			done = true;
			//For all of the relations in category cat
			for(i=0;i<cat.num_relations;i++)
			{
				//For all other relations in category cat
				for(j=0;j<cat.num_relations;j++)
				{
					//If an overlap between the lhs of the two relations exists...
					if((size = overlap(cat.relations[j].lhs,cat.relations[i].lhs)) != -1)
					{
//System.out.println("overlap");
						//Set finished to false
						finished = false;
						while(!finished)
						{
							Relation t1 = cat.relations[i];
							Relation t2 = cat.relations[j];
							//If a relation was added to the category
							//due to overlap, set done to false
							if(reduce_overlap(t1,t2,size))
							{
								done = false;
							}
							//If size of overlap is 1 then set finished
							//to equal true
							if(size == 1)
							{
								finished = true;
							}
							//If size of overlap is greater than 1
							else
							{
								size--;
								//Into temp1 copy a subpath of lhs of current relation (ie. copy
								//the last size arrows in path
								temp1 = copy_sub(temp1,cat.relations[i].lhs,(cat.path_len(cat.relations[i].lhs) - size),size);
								//Into temp2 copy the first size arrows of lhs of current relation
								temp2 = copy_sub(temp2,cat.relations[j].lhs,0,size);

								//If temp1 equals temp2 let finished by true
								if(!cat.equals(temp1,temp2))
								{
									finished = true;
								}
							}
						}
					}
					//Set position to be zero
					position = 0;
					//Starting at position searc for lhs of relation j inside lhs of relation
					//i until search returns a match
					while((loc = cat.search(cat.relations[i].lhs,cat.relations[j].lhs,position)) != -1)
					{
						//Set position to be loc + 1
						position = loc + 1;
						//Call reduce subpath on relations i and j
						//and set done to false if true
						if(reduce_subpath(cat.relations[j],cat.relations[i],loc))
						{
							done = false;
						}
					}
				}
			}
		}
		if (output.equals(""))
			output = "No relations need to be added to the category. The set of reductions is now confluent.";
	}



	public int[] copy_sub(int dest[], int source[], int start, int length)
	/*
	Parameters:
	    dest:   a substring of source is copied into dest
	    source: a substring of source is copied into dest
	    start:  the position in source at which the substring starts
	    length: the length of the substring
	Purpose:
	    To copy a substring of one array into another array
	Design:
	      Makes dest equal a substring of source
	*/
	{
		int i;

		//Starting at position start in source, copy length
		//arrows from dest
		for(i=0;i<length;i++)
		{
			dest[i] = source[start+i];
		}
		//End the path of arrows with a -1
		dest[i] = -1;
		return(dest);
	}

	public String getNewRelations()
	{
		return newRelations;
	}
	
	public void setNewRelations(String newNewRelations)
	{
		newRelations = newNewRelations;
	}
	
	public String getOutput()
	{
		return output;
	}
	
	public void setOutput(String newOutput)
	{
		output = newOutput;
	}
}