/*
Research Project:   Graphical Database for Category Theory
                    J. Bradbury, Dr. R. Rosebrugh, I. Rutherford
                    Mount Allison University 2001
File:               CoequalizerFrame.java
Description:        This class implements a frame which allows the user to run
                    the category tool "Coequalizer" on the current category.
*/


import java.awt.*;
import java.awt.event.*;
import borland.jbcl.layout.*;
import borland.jbcl.control.*;

public class CoequalizerFrame extends Frame
{
  Panel panel1 = new Panel();
  XYLayout xYLayout1 = new XYLayout();
  Button coequalizer_button = new Button();
  Button close_button = new Button();
  TextArea viewbox = new TextArea("", 10, 10, TextArea.SCROLLBARS_VERTICAL_ONLY);
  TextField alphaPath = new TextField();
  TextField betaPath = new TextField();
  Label alphaLabel = new Label();
  Label betaLabel = new Label();
  MainWindow ed;
  Category cat = new Category();
  Label coequalizerLabel = new Label();
  TextField coequalizerPath = new TextField();
  CheckboxControl search_checkbox = new CheckboxControl();
  ChoiceControl coequalizerChoice = new ChoiceControl();
  int numcoequalizers = 0;
  boolean supress_output = false;
  boolean endopassed = false;

  public CoequalizerFrame(MainWindow edit)
  {
    ed = edit;
    cat = ed.cat.makeDual();
    ed.enableMenus(false);
    try
    {
      jbInit();
    }
    catch (Exception e)
    {
      e.printStackTrace();
    }
    add(panel1);
    pack();
  }

  public boolean handleEvent(Event e)
  {
    if (e.id == Event.WINDOW_DESTROY || e.key == Event.ENTER)
    {
      ed.enableMenus(true);
      hide();            //hide frame
      dispose();         //free resources
      return true;
    }
    return super.handleEvent(e);
  }

  private void jbInit() throws Exception
  {
    this.setBackground(Color.lightGray);
    this.setSize(new Dimension(453, 203));
    this.setTitle("GDCT: Coequalizer");
    panel1.setBackground(Color.lightGray);
    xYLayout1.setWidth(453);
    xYLayout1.setHeight(222);
    coequalizer_button.setLabel("Coequalizer?");
    coequalizer_button.addActionListener(new java.awt.event.ActionListener() {
      public void actionPerformed(ActionEvent e) {
        coequalizer_button_actionPerformed(e);
      }
    });
    close_button.setLabel("Close");
    alphaLabel.setText("First path:");
    betaLabel.setText("Second path:");
    coequalizerLabel.setText("Coequalizer path:");
    coequalizerChoice.addItem("Check all objects");
    for (int i = 0; i < cat.numobj; i++)
      coequalizerChoice.addItem(cat.obj[i]);
    coequalizerChoice.select(1);
    search_checkbox.setLabel("Check All Paths");
    search_checkbox.addItemListener(new java.awt.event.ItemListener()
    {
      public void itemStateChanged(ItemEvent e)
      {
        search_checkbox_itemStateChanged(e);
      }
    });
    viewbox.setEditable(false);
    viewbox.setBackground(Color.white);
    close_button.addActionListener(new java.awt.event.ActionListener() {
      public void actionPerformed(ActionEvent e) {
        close_button_actionPerformed(e);
      }
    });
    panel1.setLayout(xYLayout1);
    panel1.add(coequalizer_button, new XYConstraints(9, 187, 84, 25));
    panel1.add(close_button, new XYConstraints(100, 187, -1, 25));
    panel1.add(viewbox, new XYConstraints(156, 9, 286, 204));
    panel1.add(alphaPath, new XYConstraints(9, 77, 138, 21));
    panel1.add(betaPath, new XYConstraints(8, 30, 138, 21));
    panel1.add(alphaLabel, new XYConstraints(10, 5, -1, 24));
    panel1.add(betaLabel, new XYConstraints(10, 54, 80, 22));
    panel1.add(coequalizerLabel, new XYConstraints(12, 133, 125, 20));
    panel1.add(coequalizerPath, new XYConstraints(9, 156, 138, 21));
    panel1.add(search_checkbox, new XYConstraints(11, 110, 133, 20));
    panel1.add(coequalizerChoice, new XYConstraints(9, 156, 138, 21));
  }

  void coequalizer_button_actionPerformed(ActionEvent e)
  {
    int alpha[] = new int[ed.ini.getMAXWORD()];
    int beta[] = new int[ed.ini.getMAXWORD()];
    int coequalizer[] = new int[ed.ini.getMAXWORD()];
    endopassed = false;

    if (!search_checkbox.isChecked() && (coequalizerPath.getText().length() == 0 || !ed.cat.check_string(coequalizerPath.getText())))
    {
      viewbox.append("Invalid coequalizer path.\n\n");
      return;
    }
    if (alphaPath.getText().length() == 0 || !ed.cat.check_string(alphaPath.getText()))
    {
      viewbox.append("Invalid second path.\n\n");
      return;
    }
    if (betaPath.getText().length() == 0 || !ed.cat.check_string(betaPath.getText()))
    {
      viewbox.append("Invalid first path.\n\n");
      return;
    }

    alpha = ed.cat.string_to_path(alphaPath.getText());
    beta = ed.cat.string_to_path(betaPath.getText());
    coequalizer = ed.cat.string_to_path(coequalizerPath.getText());

    if (alpha[0] < 0 && beta[0] < 0)
    {
      viewbox.append("Cannot check two identity paths on an unknown object.\n\n");
      return;
    }
    else if (alpha[0] < 0 && ed.cat.arr[beta[ed.cat.path_len(beta)-1]][0] != ed.cat.arr[beta[0]][1])
    {
      viewbox.append("Since alpha is an identity map, beta must have the same domain and codomain.\n\n");
      return;
    }
    else if (beta[0] < 0 && ed.cat.arr[alpha[ed.cat.path_len(alpha)-1]][0] != ed.cat.arr[alpha[0]][1])
    {
      viewbox.append("Since beta is an identity map, alpha must have the same domain and codomain.\n\n");
      return;
    }
    if (alpha[0] > 0 && beta[0] > 0)
    {
      if (ed.cat.arr[alpha[0]][1] != ed.cat.arr[beta[0]][1])
      {
        viewbox.append("The two paths must have the same codomain.\n\n");
        return;
      }
      else if (ed.cat.arr[alpha[ed.cat.path_len(alpha)-1]][0] != ed.cat.arr[beta[ed.cat.path_len(beta)-1]][0])
      {
        viewbox.append("The two paths must have the same domain.\n\n");
        return;
      }
      else if (!search_checkbox.isChecked() && ed.cat.arr[alpha[ed.cat.path_len(alpha)-1]][0] != ed.cat.arr[coequalizer[0]][1])
      {
        viewbox.append("The domain of the coequalizer path must be equal to the codomain of the two paths.\n\n");
        return;
      }
    }
    if (alpha[0] < 0)
    {
      int[] bob = beta;
      beta = alpha;
      alpha = bob;
    }

    // reverse the paths and perform the equalizer algorithm
    alpha = cat.reverse_path(alpha);
    beta = cat.reverse_path(beta);
    coequalizer = cat.reverse_path(coequalizer);

    if (search_checkbox.isChecked())
    {
      int i, j, k;
      int path[] = new int[ed.ini.getMAXARR()];
      int objects[] = new int[cat.numobj];
      HomTree yestree, notree;
      supress_output = true;
      numcoequalizers = 0;
      int codomain = cat.arr[alpha[cat.path_len(alpha)-1]][0];

      for (i=0; i<cat.numobj; i++)
      {
        if (i+1 == coequalizerChoice.getSelectedIndex() || coequalizerChoice.getSelectedItem().equals("Check all objects"))
        {
          for (j=0; j<cat.numobj; j++)
            objects[j] = 0;
          path[0] = -1;
          yestree = new HomTree();
          notree = new HomTree();
          generate_coequalizers(path, i, codomain, objects, yestree, notree, alpha, beta, ed.ini.getMaxLoop());
        }
      }
      if (numcoequalizers == 0)
        viewbox.append("No coequalizers found.\n");
      else if (numcoequalizers == 1)
        viewbox.append("1 coequalizer found.\n");
      else
        viewbox.append(Integer.toString(numcoequalizers) + " coequalizers found.\n");
    }
    else
    {
      supress_output = false;
      coequalizer(coequalizer, alpha, beta);
    }
    if (endopassed)
      viewbox.append("WARNING: Endomorphism limit reached! Results may be inaccurate!\n\n");
    else
      viewbox.append("\n");
  }

  public boolean coequalizer(int[] coequalizer, int[] alpha, int[] beta)
  {
    int arrows[] = new int[cat.numarr];
    int path[] = new int[ed.ini.getMAXWORD()];
    HomTree tree1, tree2, pathtree;
    int i, obj, number, domain, codomain;

    domain = cat.arr[coequalizer[cat.path_len(coequalizer)-1]][0];
    codomain = cat.arr[coequalizer[0]][1];

    for (obj=0; obj<cat.numobj; obj++)
    {
      tree1 = new HomTree();
      tree2 = new HomTree();

      pathtree = new HomTree();
      path[0] = -1;
      if (!makeEGammaTree(path, tree1, tree2, obj, domain, ed.ini.getMaxLoop(), coequalizer, pathtree))
        return false;

      tree2 = new HomTree();
      pathtree = new HomTree();
      path[0] = -1;
      makeEPrimeTree(path, tree2, obj, codomain, ed.ini.getMaxLoop(), alpha, beta, pathtree);

      if (!tree1.isEqual(tree2)) // && obj != codomain && obj != cat.arr[alpha[path_len(alpha)-1]][1])
      {
        if (!supress_output)
        {
          viewbox.append("Problem at object " + cat.obj[obj] + ".\n");
          viewbox.append(coequalizerPath.getText() + " is not a coequalizer.\n");
        }
        return false;
      }
    }
    viewbox.append(cat.path_to_string(cat.reverse_path(coequalizer)) + " is a coequalizer!\n");
    return true;
  }

  public void generate_coequalizers(int path[], int domain, int codomain, int objects[], HomTree yestree, HomTree notree, int[] alpha, int[] beta, int maxloop)
  /*
  Parameters:
         path:   the current path
         domain: the current object of the path
         codomain:       the object we are trying to find all arrows to
         objects:        an array of integers which keeps the function from exceeding
                                 the maximum number of loops
         yestree:  tree of verified epimorphisms
         notree:   tree of verified non-epimorphisms
  Purpose:
         To find all epimorphisms from domain to codomain
  */
  {
    int i, j, len, number;
    int arrow_array[] = new int [cat.numarr];
    path = cat.reduce(path);

    len = cat.path_len(path);
    if (!yestree.containsPath(path) && !notree.containsPath(path) && objects[domain] < maxloop)
    {
      if (len > 0 && cat.arr[path[0]][1] == codomain)
      {
        if (coequalizer(path, alpha, beta))
        {
          numcoequalizers++;
          yestree.addPath(path);
        }
        else
        {
          notree.addPath(path);
        }
      }

      number = cat.all_arr(domain, arrow_array);
      if (number > 0)
      for (i=0; i<number; i++)
      {
        domain = cat.arr[arrow_array[i]][1];
        objects[domain]++;
        if (path[0] == -2)
          path[0] = -1;
        for (j=cat.path_len(path); j>=0; j--)
          path[j+1] = path[j];
        path[0] = arrow_array[i];

        generate_coequalizers(path, domain, codomain, objects, yestree, notree, alpha, beta, maxloop);

        for (j=0; j<=len; j++)
          path[j] = path[j+1];
        objects[domain]--;
      }
    }
    else
    {
      notree.addPath(path);
    }
  }

  void close_button_actionPerformed(ActionEvent e)
  {
    ed.enableMenus(true);
    hide();
    dispose();
  }

  public void makeEPrimeTree(int path[], HomTree homtree, int obj1, int obj2, int maxloop, int alphapath[], int betapath[], HomTree pathtree)
  /*
    Parameters:
      path[]        - integer array containing the path followed so far
      objects[]     - integer array containing a list of all the objects visited along the path
      homtree       - the tree to contain the paths
      obj1 and obj2 - check for paths from obj1 to obj2
      maxloop       - max endomorphism limit
    Purpose:
      To generate the reduced hom set from one object to another as a tree
    Design:
      Creates a tree homtree of all the reduced paths from one object to another.
  */
  {
    int i, j;
    int pathlen;
    int endo = 0;
    int numarrs;

    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]][1] == cat.arr[path[pathlen-1]][0])
      {
        endo++;
      }
    }

    if (endo < maxloop && pathlen < ed.ini.getMAXWORD()-1)
    {
      if (!pathtree.containsPath(path) || pathlen == 0)
      {
        pathtree.addPath(path);
        // now check all paths from here, recursively
        int arrows[] = new int[cat.numarr];
        numarrs = cat.all_arr(obj1, arrows);

        if (pathlen < ed.ini.getMAXWORD()-1)
        for (i = 0; i<numarrs; 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];

          makeEPrimeTree(path, homtree, cat.arr[arrows[i]][1], obj2, maxloop, alphapath, betapath, pathtree);

          // 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 tree
        if ((pathlen == 0 && obj1 == obj2) || (pathlen != 0 && cat.arr[path[0]][1] == obj2))
        {
          int f[] = cat.reduce(cat.append_path(path, alphapath));
          int g[] = cat.reduce(cat.append_path(path, betapath));
          if (cat.equals(f, g))
            homtree.addPath(path);
        }
      }
    }
    else
      endopassed = true;
  }

  public boolean makeEGammaTree(int path[], HomTree homtree, HomTree gammatree, int obj1, int obj2, int maxloop, int coequalizer[], HomTree pathtree)
  /*
    Parameters:
      path[]        - integer array containing the path followed so far
      objects[]     - integer array containing a list of all the objects visited along the path
      homtree       - the tree to contain the paths
      obj1 and obj2 - check for paths from obj1 to obj2
      maxloop       - max endomorphism limit
    Purpose:
      To generate the reduced hom set from one object to another as a tree
    Design:
      Creates a tree homtree of all the reduced paths from one object to another.
  */
  {
    int i, j;
    int pathlen;
    int endo = 0;
    int numarrs;

    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]][1] == cat.arr[path[pathlen-1]][0])
      {
        endo++;
      }
    }

    if (endo < maxloop && pathlen < ed.ini.getMAXWORD()-1)
    {
      int newpath[] = cat.reduce(path);
      if (!pathtree.containsPath(newpath) || pathlen == 0)
      {
        pathtree.addPath(newpath);
        // now check all paths from here, recursively
        int arrows[] = new int[cat.numarr];
        numarrs = cat.all_arr(obj1, arrows);

        for (i = 0; i < numarrs; 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];

          if (!makeEGammaTree(path, homtree, gammatree, cat.arr[arrows[i]][1], obj2, maxloop, coequalizer, pathtree))
            return false;

          // 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 tree
        if ((pathlen == 0 && obj1 == obj2) || (pathlen != 0 && cat.arr[path[0]][1] == obj2))
        {
          if (!gammatree.containsPath(path))
          {
            gammatree.addPath(path);
            int reducedpath[] = cat.reduce(cat.append_path(path, coequalizer));
            if (homtree.containsPath(reducedpath))
              return false;
            homtree.addPath(reducedpath);
          }
        }
      }
    }
    else
      endopassed = true;
    return true;
  }

  void search_checkbox_itemStateChanged(ItemEvent e)
  {
    if (search_checkbox.isChecked())
    {
      coequalizerLabel.setText("Coequalizer object:");
      coequalizerPath.setVisible(false);
      coequalizerChoice.setVisible(true);
    }
    else
    {
      coequalizerLabel.setText("Coequalizer path:");
      coequalizerPath.setVisible(true);
      coequalizerChoice.setVisible(false);
    }
  }
}