// FILE. . . . . d:/hak/hlt/src/hlt/fot/FirstOrderTerm.java
// EDIT BY . . . Hassan Ait-Kaci
// ON MACHINE. . Hak-Laptop
// STARTED ON. . Sat Jul 14 07:23:41 2018

/**
 * @version     Last modified on Wed May 15 05:02:56 2019 by hak
 * @author      <a href="mailto:hak@acm.org">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; <a href="http://www.hassan-ait-kaci.net/">by the author</a>
 */

package hlt.fot;

import java.util.Stack;
import java.util.HashMap;
import java.util.ArrayList;
import java.util.Iterator;

/**
 * This is an interface for first-order terms defined on a signature of
 * <a href="Functor.html"><tt>Functor</tt></a>s. It is either
 * implemented by the class <a
 * href="FirstOrderTermStructure.html"><tt>FirstOrderTermStructure</tt></a>
 * and the class <a href="Variable.html"><tt>Variable</tt></a>.
 *
 * @see         Variable
 * @see         FirstOrderTermStructure
 * @see         Functor
 */
public interface FirstOrderTerm
{
  /* ************************************************************************ */
  // To be implemented by instantiating classes:
  /* ************************************************************************ */

  /**
   * Returns <tt>true</tt> iff <tt>this</tt> is a <tt>Variable</tt>.
   */
  public boolean isVariable ();

  /**
   * Returns a term that is equal to this term after having all
   * dereferencing of its contents.
   */
  public FirstOrderTerm deref ();

  /**
   * Returns a <tt>String</tt> value for this term taking all its
   * variable bindings into account. This provides a simple default
   * implementation which is overridden in the classes implementing this
   * class (<tt>Variable</tt> and <tt>FirstOrderTermStructure</tt>) to
   * prevent it from building a new term explicitly each time its string
   * form is wanted (as this default does).
   */
  default public String derefToString ()
  {
    return deref().toString();    
  }

  /**
   * Returns <tt>true</tt> is this term is equal symbol for symbol to
   * the given one (although they may be different individuals).
   */
  public boolean equal (FirstOrderTerm term);

  /* ************************************************************************ */
  // Static structures and methods:
  /* ************************************************************************ */

  /* ************************************************************************ */
  // Lattice operations:
  /* ************************************************************************ */

  /**
   * UNIFICATION
   */

  static Stack unifyStack = new Stack();

  /**
   * Unify the given pair of first-order terms and return <tt>true</tt>
   * iff they are unifiable. This will possibly bind variables that
   * occur in either term.
   */
  public static boolean unify (FirstOrderTerm lhs, FirstOrderTerm rhs)
  {
    unifyStack.clear();

    unifyStack.push(lhs);
    unifyStack.push(rhs);

    boolean unifiable = true;

    while (unifiable && !unifyStack.isEmpty())
      {
	lhs = (FirstOrderTerm)unifyStack.pop();
	rhs = (FirstOrderTerm)unifyStack.pop();

	if (lhs.isVariable())
	  lhs = ((Variable)lhs).deref();

	if (rhs.isVariable())
	  rhs = ((Variable)rhs).deref();

	if (lhs == rhs)
	  continue;

	if (lhs.isVariable())
	  {
	    Variable V = ((Variable)lhs);

	    if (V.occursIn(rhs))
	      unifiable = false;
	    else
	      V.bind(rhs);

	    continue;
	  }

	if (rhs.isVariable())
	  {
	    Variable V = ((Variable)rhs);

	    if (V.occursIn(lhs))
	      unifiable = false;
	    else
	      V.bind(lhs);

	    continue;
	  }

	// both are structures:
	FirstOrderTermStructure L = (FirstOrderTermStructure)lhs;
	FirstOrderTermStructure R = (FirstOrderTermStructure)rhs;

	if (L.functor().equal(R.functor()))
	  for (int i=1; i <= L.functor.arity(); i++)
	    {
	      unifyStack.push(L.argument(i));
	      unifyStack.push(R.argument(i));
	    }
	else
	  unifiable = false;
      }

    return unifiable;
  }

  /* ************************************************************************ */

  /**
   * GENERALIZATION
   */

  /**
   * The generated generalizing variables.
   */
  public static ArrayList generatedVariables  = new ArrayList();

  /**
   * The substitution mapping generated variables to the subterms of the
   * generalized lhs.
   */
  public static HashMap lSubstitution = new HashMap();

  /**
   * The substitution mapping generated variables to the subterms of the
   * generalized rhs.
   */
  public static HashMap rSubstitution = new HashMap();

  /**
   * Clears all substitutions and generated variables.
   */
  public static void resetGeneralizer ()
  {
    generatedVariables.clear();
    lSubstitution.clear();
    rSubstitution.clear();
  }

  /**
   * Unapplying the current left and right substitutions to the given
   * terms, and returning a pair of terms.
   */
  private static FirstOrderTermPair unapply (FirstOrderTerm lhs, FirstOrderTerm rhs)
  {
    Variable V;
    FirstOrderTerm L;
    FirstOrderTerm R;

    for (int i = 0; i < generatedVariables.size(); i++)
      {
	V = (Variable)generatedVariables.get(i);
	L = (FirstOrderTerm)lSubstitution.get(V);
	R = (FirstOrderTerm)rSubstitution.get(V);

	if (lhs.equal(L) && rhs.equal(R))
	  return new FirstOrderTermPair(V,V);
      }

    return new FirstOrderTermPair(lhs,rhs);
  }

  /**
   * This returns the term generalizing the given pair of terms.  It
   * proceed recursively on pairs structures with equal-functors. As it
   * proceeds it simultaneously builds up the left and right
   * generalizing substitutions as needed.
   */
  public static FirstOrderTerm generalize (FirstOrderTerm lhs, FirstOrderTerm rhs)
  {
    // Equal Variables
    if (lhs.isVariable() && lhs == rhs)
      return lhs;

    // Variable-Term:
    if ((lhs.isVariable() || rhs.isVariable()) && !lhs.equal(rhs))
      {
	Variable newVariable = Variable.anonymousVariable();
	lSubstitution.put(newVariable,lhs);
	rSubstitution.put(newVariable,rhs);
	generatedVariables.add(newVariable);
	return newVariable;
      }

    FirstOrderTermStructure L = (FirstOrderTermStructure)lhs;
    FirstOrderTermStructure R = (FirstOrderTermStructure)rhs;
    
    // Unequal Functors:
    if (!L.functor().equal(R.functor()))
      {
	Variable newVariable = Variable.anonymousVariable();
	lSubstitution.put(newVariable,lhs);
	rSubstitution.put(newVariable,rhs);
	generatedVariables.add(newVariable);
	return newVariable;
      }

    // Equal Functors:
    Functor F = L.functor();
    int N = F.arity();

    FirstOrderTermStructure
      newStructure = N==0 ? new FirstOrderTermStructure(F)
                          : new FirstOrderTermStructure(F,new FirstOrderTerm[N]);

    for (int i = 1; i <= N; i++)
      {
	FirstOrderTermPair P = unapply(L.argument(i),R.argument(i));
	newStructure.setArgument(i,generalize(P.left(),P.right()));
      }

    return newStructure;
  }

}