/*
 *   $Source: /home/vkeselj/cvsroot/unifmachine/unifmachine.java,v $
 * $Revision: 1.10 $
 *     $Date: 2002/01/23 11:08:04 $
 *   Authors: (c) 2001-2002 Vlado Keselj and Nick Cercone
 */

import java.util.*;

public class unifmachine {

  static int A_len = 10000;
  static int[] A = new int[A_len]; /* the array */

  static int Alloc_last = -1;	/* last allocated cell */

  /* Attributes (features) */
  static final int att_a = -7;
  static final int att_b = -6;
  static final int att_d = -5;
  static final int att_e = -4;
  static final int att_g = -3;
  static final int att_h = -2;

  /* Atoms */
  static final int ATOM_A = -1;

  static String[] att_name = { null, null, "h", "g", "e", "d", "b",
			       "a" };

  static String[] atom_name = { null, "A" };

  /* Global generation counter */
  static int Generation = 1;

  /* Root nodes bookkeeping (2 entries per root):
   *  1. entry: root address
   *  2. entry: graph size */
  static int[] root = new int[10];
  static int root_last = -1;

  /**
     Set initial configuration.
  */
  static void init() {
    Alloc_last = -1;

    /* First graph */
    root[++root_last] = Alloc_last + 1; /* address 1 */
    {
      int[] a = { 0, 0, 1, att_a,  8, att_d, 15, -1,
		  0, 0, 1, att_b, 14, -1,
		  ATOM_A,
		  0, 0, 1, att_e, 21, -1,
		  0, 0, 0 };
      System.arraycopy(a, 0, A, Alloc_last+1, a.length);
      Alloc_last += a.length;
      root[++root_last] = a.length;     /* size 1 */
    }

    /* Second graph */
    root[++root_last] = Alloc_last + 1; /* address 2 */
    {
      int[] a = { 0, 0, 1, att_a,  34, att_d, 34, att_g, 43, -1,
		  0, 0, 1, att_b, 40, -1,
		  0, 0, 0,
		  0, 0, 1, att_h, 49, -1,
		  0, 0, 0 };
      System.arraycopy(a, 0, A, Alloc_last+1, a.length);
      Alloc_last += a.length;
      root[++root_last] = a.length;     /* size 2 */
    }
  }

  /** 
      The main function
  */
  public static void main(String[] args) {

    init();
    print_latex("Initial configuration", "initialconfiguration");

    System.out.println( "%" +
			" arg1="  + root[0] +
			" size1=" + root[1] +
			"  arg2=" + root[2] +
			" size2=" + root[3] );

    int result = unify1(0, 1);

    print_latex("After first phase", "firstphasenorepackaging");

    if (result > -1)
      result = unify_copy(result);

    print_latex("Final","secondphase");

    System.out.println("% Result adr=" + root[root_last-1] + " size="
		       + root[root_last]);

    System.exit(0);

  } /* end of main */


  /* Non-static variables */

  static int stack_top = -1;

  static int temp_first = -1;	/* first temp allocated cell */
  static int temp_last  = -1;	/* last temp allocated cell  */

  static int repack_limit = -1;

  /**
     Unify two graphs: first phase.
     @param g1 index of the first graph (2*g1 in root array)
     @param g2 index of the second graph (2*g2 in root array)
     @return -1 if unification fails,
             index of the resulting graph otherwise
  */
  static int unify1(int g1, int g2) {

    /* max_size = max(2, size1 + size2 - 3) */
    int max_size = root[2*g1+1]+root[2*g2+1]-3;
    if (max_size < 2) max_size = 2;

    temp_first = 2*(root[2*g1+1]+root[2*g2+1])/3 + 1;
    if (temp_first < 2) temp_first = 2;
    temp_first += Alloc_last + 1 + max_size;
    temp_last  = temp_first - 1;
    stack_top = temp_first;
    repack_limit = A_len - 5 * max_size / 2;

    /* Check the size of the array.  Keep doubling them until the
       length is sufficient.
    */
    while (temp_last >= repack_limit) {
      int[] tmp = new int[2 * A.length];
      System.arraycopy(A, 0, tmp, 0, A.length);
      A = tmp;

      A_len = A.length;
      repack_limit = A_len - 2 * max_size;
    }

    A[--stack_top] = root[2*g1];
    A[--stack_top] = root[2*g2];

    while (stack_top < temp_first) {
      int i2 = A[stack_top++];
      int i1 = A[stack_top++];

      if (i1==i2) continue;

      /* Dereference i1 with path compression */
      if ( A[i1] == Generation ) {
	int j = A[i1+1];
	if ( A[j] == Generation ) {
	  A[--stack_top] = -1;
	  do {
	    A[--stack_top] = i1 + 1;
	    i1 = j;
	    j = A[j+1];
	  }
	  while ( A[j] == Generation );

	  while (A[stack_top] > -1)
	    A[A[stack_top++]] = j;

	  stack_top++;
	}
	
	i1 = j;
      }

      /* Dereference i2 with path compression */
      if ( A[i2] == Generation ) {
	int j = A[i2+1];
	if ( A[j] == Generation ) {
	  A[--stack_top] = -1;
	  do {
	    A[--stack_top] = i1 + 1;
	    i2 = j;
	    j = A[j+1];
	  }
	  while ( A[j] == Generation );

	  while (A[stack_top] > -1)
	    A[A[stack_top++]] = j;

	  stack_top++;
	}
	
	i2 = j;
      }

      if (i1==i2) continue;

      /* Unify */
      /* at least one node is a leaf node */
      if ( A[i1]>=0 && A[i1+2]==0 ) {
	A[i1] = Generation;
	A[i1+1] = i2;
      } else if ( A[i2]>=0 && A[i2+2]==0) {
	A[i2] = Generation;
	A[i2+1] = i1;
      }
      /* at least one node is an atom */
      else if (A[i1] < 0 || A[i2] < 0) {
	/* they have to match */
	if ( A[i1] != A[i2] ) {
	  Generation++;
	  return -1;		/* unification fails: atoms mismatch
				 */
	}
      }
      /* otherwise, we have two complex nodes: we will merge them */
      else {
	int embed1 = 0, embed2 = 0; /* can result be embedded in one
				       of the graphs (0), otherwise,
				       index of the attribute from
				       which the tail can be shared */
	int src1 = i1, src2 = i2; /* shared source */

	int j1=i1+3, j2=i2+3, j3=temp_last+4; /* j1 and j2 are merged
						 to create j3 */

	/* types should be merged here for typed feature structures */
	A[j3-1] = 1;

	/* Merge lists */
	while ( A[j1] != -1 && A[j2] != -1 ) {

	  /* dereference */
	  while (A[j1] >= 0) j1 = A[j1];
	  while (A[j2] >= 0) j2 = A[j2];

	  /* merge step */
	  if ( A[j1] < A[j2] ) {
	    A[j3++] = A[j1++];
	    A[j3++] = A[j1++];
	    embed2 = j3; src2 = j2;
	  }
	  else if ( A[j2] < A[j1] ) {
	    A[j3++] = A[j2++];
	    A[j3++] = A[j2++];
	    embed1 = j3; src1 = j1;
	  }
	  else {
	    A[j3++] = A[j1++];
	    /* If values do not match? */
	    if ( A[j1] != A[++j2] ) {
	      
	      /* push refs on stack */
	      A[--stack_top] = A[j1];
	      A[--stack_top] = A[j2];
	    }
	    A[j3++] = A[j1++];
	    j2++;
	  }
	}
	/* Final check for complete embedding */
	if (A[j1] != -1) embed2 = -1;
	else if (A[j2] != -1) embed1 = -1;

	/* let's see what to do with the result */

	/* Is embedding possible?  For typed feature structures,
	   the resulting type should be copied. */
	/* embedding into i1 */
	if ( embed1==0 && (embed2!=0 || i1 <= i2 ) ) {
	  A[i2++] = Generation;
	  A[i2] = i1;
	}
	/* embedding into i2 */
	else if ( embed2 == 0) {
	  A[i1++] = Generation;
	  A[i1] = i2;
	}
	else { /* no embedding */
	  /* let us first decide about tail sharing */
	  if ( embed1 > -1 &&
	       (embed2 == -1 ||
		( j1 <= Alloc_last && j2 > Alloc_last ) ||
		embed1 <= embed2 ) ) {
	    A[ j3 = embed1 ] = src1;
	    embed2 = -1;
	  } else {
	    A[ j3 = embed2 ] = src2;
	    embed1 = -1;
	  }

	  /* Can we leave it as it is? */
	  if (j3 < repack_limit ||
	      ( i1 < temp_first && i2 < temp_first )) {
	    A[++temp_last] = 0;
	    A[i1++] = A[i2++] = Generation;
	    A[i1] = A[i2] = temp_last;
	    temp_last = j3;
	  }
	  /*  Else repackage */
	  else {
	    if ( i1 < temp_first ||
		 ( embed1 > -1 && i2 >= temp_first ) )
	      { int tmp=i1;i1=i2;i2=tmp; }
	    A[i2++] = Generation;
	    A[i2++] = i1; i2++; /* let i2 be on the first edge */
	    A[i1++] = 0;
	    ++i1;
	    j1 = temp_last + 3;	/* use j1 as the source index */
	    A[i1++] = A[j1++];	/* copy T */
	    while (A[j1] < -1) {
	      if (i1 < temp_last && A[i1] >= -1) { /* we have to find
						      new destination */
		int ii1 = i1;
		while (A[ii1] >= 0) ii1 = A[ii1];
		
		if ( ii1 < temp_first ) { /* have to break the chain */
		  if (i2 >= temp_first) {  /* we can switch to i2 */
		    ii1 = i2; i2 = -1;
		  }
		  else ii1 = temp_last + 1; /* we continue after temp_last */
		}
		
		A[i1] = ii1; i1 = ii1;
	      }
	      if ( i1 == A[j3] ) { /* we hit the shared tail! */
		int ii1 = i1;
		while (A[ii1] < -1) {
		  A[j3++] = A[ii1++]; A[j3++] = A[ii1++];
		}
		while ( A[ii1] > 0 ) ii1 = A[ii1];
		A[j3] = (A[ii1] == -1) ? -1 : ii1;
	      }
	      
	      /* copy pair */
	      A[i1++] = A[j1++];
	      A[i1++] = A[j1++];
	    } /* finished, just copy the last cell (-1 or ref to shared
		 tail ) */
	    A[i1] = A[j1];
	    if ( i1 > temp_last ) temp_last = i1;

	  }	/* end of else repackage */
      
	} /* end: no embedding */
      } /* end of complex node merging */

    }  /* end of unification, pop another pair from stack */

    return g1;

  } /* end of unify1 function */


  static final int FORWARD = 1;
  static final int BACKWARD = -1;
  static final int END = 0;

  static int unify_copy(int graph) {

    /* Copy with hidden structure sharing, using depth-first search
       Overview:
       END:   finished, final address in i
       FORWARD: go forward using address in ind and leave it in i,
       BACKWARD: go backward, last address in i
       
       Node statuses for nodes <= Alloc_last
       G < Generation    not visited
       G=Generation F>=0 forward
       G=Generation F<=-1 visit finished or being visited
                    -F is address of original T
       
       set i=graph go FORWARD
    */
    int i = root[2*graph];

    int state = FORWARD;
    int size = 0;
    int new_Alloc_last = Alloc_last;

    while ( state != END ) {
      /*
       * FORWARD:
       */
      if ( state == FORWARD ) {

	/* Dereference i with path compression */
	if ( A[i] == Generation && A[i+1] >= 0 ) {
	  int j = A[i+1];
	  if ( A[j] == Generation && A[j+1] >= 0 ) {
	    A[--stack_top] = -1;
	    do {
	      A[--stack_top] = i + 1;
	      i = j;
	      j = A[j+1];
	    }
	    while ( A[j] == Generation && A[j+1] >= 0);

	    while (A[stack_top] > -1)
	      A[A[stack_top++]] = j;

	    stack_top++;
	  }
	  
	  i = j;
	}

	/* if the node is an atom, or it was visited, or being
	   visited, or it is a leaf, or it does not have children and
	   it is in charts area then go back */ 
	if ( A[i] < 0 ) {
	  state = BACKWARD;
	  size ++;
	} else if ( A[i] == Generation && A[i+1] <= -1 )
	  state = BACKWARD;
	else if ( i <= Alloc_last &&
		  ( A[i+2] == 0 || A[i+3] == -1 ) ) {
	  A[i] = Generation; A[i+1] = -1;
	  size += A[i+2] == 0 ? 3 : 4;
	}

	/* otherwise, copy node to reserved area, with replacing F
	   with negative address of F, and attributes with addresses
	   of original attributes
	*/
	else {

	  /* make a copy and the reference to it
	     (size is accumulated in new_Alloc_last */
	  A[++new_Alloc_last] = Generation; /* new G */
	  A[i] = Generation;	            /* old G */
	  A[i+1] = new_Alloc_last;          /* old F */
	  A[++new_Alloc_last] = - (i+1); /* new F: negative address of F */
	  A[++new_Alloc_last] = A[i+2];     /* copy T */
	  /* we know that it is a complex node (leaf nodes are always
	     shared) */
	  for (int src=i+3; ; ) {
	    while ( A[src]>=0 ) src = A[src];
	    if ( A[src]==-1 ) {
	      A[++new_Alloc_last] = -1;
	      break;
	    }
	    A[++new_Alloc_last] = src++; /* address of attribute */
	    A[++new_Alloc_last] = A[src++];
	  }
	  i = A[i+1];

	  /* The copy is maid, start iteration over children (if there
	     are any).  Iterate backwards.
	     push on stack: child ptr address
	  */
	  if (A[i+3]==-1) {	/* no children */
	    if ( - A[i+1] <= Alloc_last ) {
	      A[ - A[i+1] ] = -1; /* shared */
	      new_Alloc_last -= 4;
	      size += 4;
	      i = - A[i+1] - 1;
	    }
	    state = BACKWARD;
	  }
	  else {
	    A[--stack_top] = new_Alloc_last - 1; /* child ptr address */
	    i = A[new_Alloc_last - 1];           /* child ptr */
	    /* continue with state=FORWARD */
	  }
	}
      }	/* end of state FORWARD */

      /*
       * BACKWARD
       */
      if ( state == BACKWARD ) {
	/* if stack is empty, it is the end */
	if (stack_top == temp_first) state = END;
	else {
	  /* pop the ptr address */
	  int ptr_address = A[stack_top++];

	  /* can we tail share this address? */
	  if ( A[ptr_address+1] >= -1 && i <= Alloc_last && i ==
	       A[ptr_address] && A[ptr_address-1] <= Alloc_last ) {
	    new_Alloc_last -= 2;
	    size += 2;
	    ptr_address -= 2;
	  } else {
	    A[ptr_address--] = i;
	    A[ptr_address] = A[A[ptr_address]];	/* set attribute */
	    ptr_address--;
	  }

	  if ( A[ptr_address-1] >= 0 ) { /* next child to visit */
	    A[--stack_top] = ptr_address;
	    i = A[ptr_address];
	    state = FORWARD;
	  } else {		/* node finished */
	    /* can we share the whole node */
	    if ( A[ptr_address+1] >= 0 &&
		 -A[ptr_address-1] <= Alloc_last ) {
	      new_Alloc_last -= 4;
	      size += 4;
	      i = - A[ ptr_address - 1 ] - 1;
	      A[i+1] = -1;
	    }
	    else i = ptr_address - 2;
	  }
	} /* BACKWARD and not END */
      }	/* state BACKWARD */
    } /* while state != END */

    size += new_Alloc_last - Alloc_last;
    Alloc_last = new_Alloc_last;
    temp_first = temp_last = -1;
    root[++root_last] = i;
    root[++root_last] = size;
    ++Generation;
    return root_last - 1;
  }

  static void print_a() {
    for (int i=0; i < A.length; ++i) {
      if (i>Alloc_last && i > temp_last) break;
      System.out.print("a["+spacePadded(i,3)+"]="+spacePadded(A[i],-4));
      if (i % 10 == 9) System.out.println();
    }
    System.out.println();
  }

  /**
     Auxiliary function -- space padding on left or right to an integer.
     @param i an integer to be represented as astring
     @param pad the min length, if negative pad on right, otherwise
     pad on left
     @return string representation
  */
  static String spacePadded(int i, int pad) {
    String r = "" + i;
    int apad = (pad < 0 ? -pad : pad);
    while (r.length() < apad)
      r = (pad<0 ? r+" " : " "+r);
    return r;
  }

  /* kind_of_cell: 0 - not used, 1 - GFT, 2 - attribute */
  static void mark_gft(int i, int[] mark) {
    if (mark[i] != 0) return;
    mark[i] = 1;
    if (A[i] == Generation && A[i+1] >= 0) mark_gft(A[i+1], mark);
    else if (A[i] >=0 && A[i+2]!=0) mark_att(i+3, mark);
  }
  static void mark_att(int i, int[] mark) {
    if (mark[i] != 0) return;
    mark[i] = 2;
    if ( A[i] >= 0 ) mark_att( A[i], mark );
    else if (A[i] < -1) {
      mark_gft(A[i+1], mark);
      mark_att(i+2, mark);
    }
  }

  /**
     Print contents of the array in LaTeX form.
   */
  static void print_latex(String comment, String command) {

    int[] kind_of_cell = new int[ (temp_last > Alloc_last ?
				   temp_last : Alloc_last) + 1 ];

    /*
     * Print out up to Alloc_last and mark first GFT's
     */

    System.out.println("% " + comment + "\n");

    System.out.println("\\newcommand{\\" + command + "}{" +
		       "\\setcounter{cell}{0}\\raggedright");

    for (int i=0; i <= Alloc_last; ) {
      mark_gft(i, kind_of_cell);
      i = print_latex_gft( i );
    }

    System.out.println("\\\\$\\mbox{\\it Alloc\\_last}="+Alloc_last+"$");

    if (temp_first > Alloc_last && temp_last > Alloc_last) {

      System.out.println("\\quad\\setcounter{cell}{"+temp_first+
			 "}$\\mbox{\\it temp\\_first}="+temp_first+"$\\\\");

      /* Print out the temporary area */
      for (int i = temp_first; i <= temp_last; ) {
	switch ( kind_of_cell[i] ) {
	case 1: i = print_latex_gft( i ); break;
	case 2: i = print_latex_att( i ); break;
	case 0:
	  System.out.println("\\cells{"+A[i]+"}{}% " + i);
	  ++i;
	}
      }

    }

    System.out.println("}\n");

  } /* end of function print_latex */

  /** Print continous part of the node and return next i */
  static int print_latex_gft( int i ) {

    if ( A[i] < 0 )		/* atom */
      System.out.println("\\celle{"+ atom_name[-A[i++]] + "} % " +
			 (i-1));
    else if (A[i] == Generation && i > Alloc_last)   /* forward */
      System.out.println("\\cell{" + A[i++] + "}{G}\\cell{" + A[i++] +
			 "}{F} % " + (i-2) );
    else {			/* gft ... */
      int bg = i;
      System.out.print("\\cellgft{"+A[i++]+"}{"+A[i++]+"}{"+A[i++]+"}");
      if ( A[i-1] == 0 )	/* leaf */
	System.out.println(" % " + bg);
      else {
	i = print_latex_att( i );
	System.out.println(" % " + bg);
      }
    }

    return i;
  }

  /** Print continous edge sequence, return next i */
  static int print_latex_att( int i ) {
    while ( A[i] < -1 ) {
      System.out.print("\\cellp{" + att_name[ -A[i++] ] + "}{" +
		       A[i++] + "}");
    }
    System.out.print("\\celle{" + A[i++] + "}");
    return i;
  }

} /* end of class */