/*
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:               Iso.java
Description:        This class contains the algorithms to perform the
                    isomorphism test on a given category.  It is used only by
                    the IsoFrame class.
*/


public class Iso
{
	private Category cat;
	private String output;

	private int maxpaths;
	private boolean includeid;
	private boolean endopassed;

	public Iso(Category category_)
	{
		cat = category_;
		output = "";
		maxpaths = 50;
		includeid = true;
		endopassed = false;
	}

	public void checkzero(String path1, String path2)
	{
		// both paths are specified, so this function simply has to
		// verify both paths, make sure they have matching domains and
		// codomains, then check if they're inverses
		int p1[], p2[];
		String str1 = path1;
		String str2 = path2;
		if (!cat.check_string(str1))
		{
			output += "Invalid first path.";
			return;
		}
		if (!cat.check_string(str2))
		{
			output += "Invalid second path.";
			return;
		}
		p1 = cat.string_to_path(str1);
		p2 = cat.string_to_path(str2);
		if (cat.path_len(p1) == 0 || !cat.check_path(p1))
		{
			output += "Invalid first path.";
			return;
		}
		if (cat.path_len(p2) == 0 || !cat.check_path(p2))
		{
			output += "Invalid second path.";
			return;
		}
		if (cat.arr[p1[0]][1] != cat.arr[p2[cat.path_len(p2)-1]][0])
		{
			output += "The codomain of first path must equal the domain of the second path.\n\n";
			return;
		}
		if (cat.arr[p2[0]][1] != cat.arr[p1[cat.path_len(p1)-1]][0])
		{
			output += "The domain of first path must equal the codomain of the second path.\n\n";
			return;
		}
		
		// check if the two paths are mutually inverse
		if (cat.path_len(cat.reduce(cat.append_path(p1, p2))) == 0 &&
				cat.path_len(cat.reduce(cat.append_path(p2, p1))) == 0)
		{
			output += str1 + " and " + str2 + " are mutually inverse!\n\n";
		}
		else
		{
			output += str1 + " and " + str2 + " are not mutually inverse.\n\n";
		}
	}

	public void checkone(String path1)
	{
		int i;
		int path[];
		int temp[] = new int[cat.ini.getMAXWORD()];
		int obj1, obj2, numisos = 0, numpaths;
		HomTree paths = new HomTree();
		HomTree tree = new HomTree();
		String str = path1;

		if (!cat.check_string(str))
		{
			output += "Invalid path.";
			return;
		}
		path = cat.string_to_path(str);
		if (cat.path_len(path) == 0 || !cat.check_path(path))
		{
			output += "Invalid path.";
			return;
		}
		obj1 = cat.arr[path[0]][1];
		obj2 = cat.arr[path[cat.path_len(path)-1]][0];
		temp[0] = -1;

		// get all paths from obj1 to obj2 and then check them all
		numpaths = get_all_paths(temp, paths, obj1, obj2, cat.ini.getMaxLoop(), 0, tree);

		// go through each path and see if it is an inverse
		temp = paths.getFirstPath();
		for (i=0; i<numpaths; i++)
		{
			// if temp is an inverse to path, then their two compositions (one
			// with temp first and one with path first) will be identity arrows
			if (cat.path_len(cat.reduce(cat.append_path(path, temp))) == 0 &&
					cat.path_len(cat.reduce(cat.append_path(temp, path))) == 0)
			{
				output += str + " has inverse " + cat.path_to_string(temp) + ".\n\n";
				numisos++;
			}
			temp = paths.getNextPath();
		}
		if (numisos == 0)
			output += str + " has no inverse.\n\n";
	}

	public void checkboth(String choice1Item, String choice2Item)
	{
		int i, j, numisos = 0;
		HomTree paths = new HomTree();
		HomTree inversepaths = new HomTree();
		String str1 = choice1Item;
		String str2 = choice2Item;
		String str3;

		// if the second choice is to check all objects, then switch the two strings
		if (str2.equals("Check all objects"))
		{
			str3 = str1;
			str1 = str2;
			str2 = str3;
		}

		if (str1.equals("Check all objects"))
		{
			if (str2.equals("Check all objects"))
			{
				this.setIncludeId(false);
				// do a double loop to check all objects in the category against all others
				for (i=0; i<cat.num_objects; i++)
				{
					for (j=i; j<cat.num_objects; j++)
					{
						paths = new HomTree();
						inversepaths = new HomTree();
						numisos += is_iso(i, j, paths, inversepaths);
					}
				}
				if (numisos == 0)
					output += "There are no nontrivial isomorphisms in this category.\n\n";
				else
					output += Integer.toString(numisos) + " pairs of mutually inverse paths found.\n\n";
			}
			else
			{
				// loop through each object to see if it is isomorphic to object str2
				includeid = false;
				j = cat.object_number(str2);
				for (i=0; i<cat.num_objects; i++)
				{
					paths = new HomTree();
					inversepaths = new HomTree();
					numisos += is_iso(i, j, paths, inversepaths);
				}
				if (numisos == 0)
					output += "There are no objects isomorphic to " + str2 + ".\n\n";
				else
					output += Integer.toString(numisos) + " pairs of mutually inverse paths found.\n\n";
			}
		}
		else
		{
			// check if objects str1 and str2 are isomorphic
			i = cat.object_number(str1);
			j = cat.object_number(str2);
			numisos = is_iso(i, j, paths, inversepaths);
			if (numisos == 0)
				output += "Objects " + str1 + " and " + str2 + " are not isomorphic.\n\n";
			else
				output += Integer.toString(numisos) + " isomorphisms found.\n\n";
		}
	}

	public int is_iso(int obj1, int obj2, HomTree paths, HomTree inversepaths)
	/*
		Parameters:
			obj1, obj2	 - the objects to be checked for an isomorphism
			paths				- an array which will store all paths from obj1 to obj2
			inversepaths - an array that will store all paths from obj2 to obj1
			maxpaths		 - the max number of paths to be stored
		Purpose:
			Checks for an isomorphism between two objects
		Design:
			Returns true is an isomorphism is found, and prints a message to the user
			Otherwise, returns false and prints nothing
	*/
	{
		int i, j;
		int numpaths1, numpaths2;
		int path[] = new int[cat.ini.getMAXWORD()];
		int objects[] = new int[cat.num_objects];
		int p1[] = new int[cat.ini.getMAXWORD()];
		int p2[] = new int[cat.ini.getMAXWORD()];
		HomTree tree = new HomTree();

		// get all paths from obj1 to obj2, and then from obj2 to obj1
		path[0] = -1;
		for (i=0; i<cat.num_objects; i++)
			objects[i] = 0;
		numpaths1 = get_all_paths(path, paths, obj1, obj2, cat.ini.getMaxLoop(), 0, tree);
		path[0] = -1;
		for (i=0; i<cat.num_objects; i++)
			objects[i] = 0;
		tree = new HomTree();
		numpaths2 = get_all_paths(path, inversepaths, obj2, obj1, cat.ini.getMaxLoop(), 0, tree);
		tree = new HomTree();

		// check all paths (obj1 to obj2) against all paths (obj2 to obj1)
		// and see if any pair forms an isomorphism
		int ret = 0;
		p1 = paths.getFirstPath();
		for (i=0; i<numpaths1; i++)
		{
			p2 = inversepaths.getFirstPath();
			for (j=0; j<numpaths2; j++)
			{
				// if the two paths are inverses, then their compositions will
				// reduce to the identity
				path = cat.reduce(cat.append_path(p1, p2));
				if (cat.path_len(path) == 0)
				{
					path = cat.reduce(cat.append_path(p2, p1));
					if (cat.path_len(path) == 0)
					{
						if (tree.addPath(p1))
						{
							if (tree.prev.tree == null) tree.prev.tree = new HomTree();
							if (tree.prev.tree.addPath(p2))
							{
								if (this.getIncludeId() || cat.path_len(p1) != 0 || cat.path_len(p2) != 0)
								{
									output += cat.path_to_string(p1) + " and " + cat.path_to_string(p2) + " are mutually inverse.\n";
									ret++;
								}
							}
						}
					}
				}
				p2 = inversepaths.getNextPath();
			}
			p1 = paths.getNextPath();
		}
		return ret;
	}

	public int get_all_paths(int path[], HomTree paths, int obj1, int obj2, int maxloop, int numpathssofar, HomTree tree)
	/*
		Parameters:
			path[]				- integer array containing the path followed so far
			objects[]		 - integer array containing a list of all the objects visited along the path
			paths[][]		 - integer array containing a list of paths found
			obj1 and obj2 - the two objects to check for an isomorphism
			maxloop			 - max endomorphism limit
		Purpose:
			gets all paths from obj1 to obj2
		Design:
			returns the number of paths found
	*/
	{
		int i, j, pathlen;
		int endo = 0;
		int numnewpaths = 0;
		int numpaths = numpathssofar;

		if (path[0] == -1 && obj1 == obj2)
		{
			path[0] = -2;
			path[1] = -1;
			paths.addPath(path);
			numpaths++;
			numnewpaths++;
		}

		path = cat.reduce(path);
		pathlen = cat.path_len(path);
		if (path[0] == -2)
			path[0] = -1;

		for (i=0; i<pathlen; i++)
		{
			if (cat.arr[path[i]][0] == cat.arr[path[pathlen-1]][1])
			{
				endo++;
			}
		}

		// check to see if we've passed the endomorphism limit
		if (endo >= maxloop)
		{
			this.setEndoPassed(true);
		}
		else if (pathlen < cat.ini.getMAXWORD()-1 && (!tree.containsPath(path) || pathlen == 0))
		{
			// now check all paths from here, recursively
			if (pathlen != 0) tree.addPath(path);
			int arrows[] = new int[cat.num_arrows];
			for (i = cat.all_arr(obj1, arrows)-1; i>=0; i--)
			{
				// add the new arrow to the path, and the new object to the object list
				for (j=pathlen; j>=0; j--)
					path[j+1] = path[j];
				path[0] = arrows[i];

				numpaths = get_all_paths(path, paths, cat.arr[arrows[i]][1], obj2, maxloop, numpaths, tree);

				// now remove the arrow and object from the path and object list
				for (j=0; j<=pathlen; j++)
					path[j] = path[j+1];
			}

			// if we're at the second object, then add the path to the list, unless
			// it's already in there
			if (pathlen > 0 && cat.arr[path[0]][1] == obj2)
			{
				if (paths.addPath(path))
				{
					numpaths++;
					numnewpaths++;
				}
			}
		}
		return numpaths;
	}

		public String getOutput()
			{
				return output;
			}
		
		public void setOutput(String newOutput)
			{
				output = newOutput;
			}
		
		public boolean getIncludeId()
			{
				return includeid;
			}
		
		public void setIncludeId(boolean newIncludeId)
			{
				includeid = newIncludeId;
			}
		
		public boolean getEndoPassed()
			{
				return endopassed;
			}
		public void setEndoPassed(boolean newEndoPassed)
			{
				endopassed = newEndoPassed;
			}
}