/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                STANDARD UNIFICATION                    * */
/* *                                                        * */
/* *  $Module:   UNIFY                                      * */ 
/* *                                                        * */
/* *  Copyright (C) 1996, 1997, 1998, 2000, 2001            * */
/* *  MPI fuer Informatik                                   * */
/* *                                                        * */
/* *  This program is free software; you can redistribute   * */
/* *  it and/or modify it under the terms of the GNU        * */
/* *  General Public License as published by the Free       * */
/* *  Software Foundation; either version 2 of the License, * */
/* *  or (at your option) any later version.                * */
/* *                                                        * */
/* *  This program is distributed in the hope that it will  * */
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
/* *  License for more details.                             * */
/* *                                                        * */
/* *  You should have received a copy of the GNU General    * */
/* *  Public License along with this program; if not, write * */
/* *  to the Free Software Foundation, Inc., 59 Temple      * */
/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
/* *                                                        * */
/* *                                                        * */
/* $Revision$                                        * */
/* $State$                                            * */
/* $Date$                             * */
/* $Author$                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile$ */

#include "unify.h"

/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  INITIALIZATION           			            * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


void unify_Init(void)
/**********************************************************
  INPUT:   None.
  RETURNS: None.
  EFFECT:  Initializes the unify module.
********************************************************/
{

}

void unify_Free(void)
/**********************************************************
  INPUT:   None.
  RETURNS: None.
  EFFECT:  Frees internal structures of the unify module.
********************************************************/
{

}


/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  MISC FUNCTIONS                     	            * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  OCCUR CHECK            			            * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


BOOL unify_OccurCheckCom(SYMBOL Top, CONTEXT Context, TERM Term)
/**********************************************************
  INPUT:   A variable symbol, a context, and a term.
  RETURNS: TRUE if there is a occur check failure with respect
           to the variable symbol <Top> and <Term>.
	   The search is started in <Term>
***********************************************************/
{
  int  Bottom;
  LIST Args;

  Bottom = stack_Bottom();

  for (;;) {

    if (term_IsVariable(Term)) {
      if (symbol_Equal(Top, term_TopSymbol(Term))) {
	stack_SetBottom(Bottom);
	return TRUE;
      } else if (cont_VarIsBound(Context, term_TopSymbol(Term))) {
	Term = cont_ContextBindingTerm(Context, term_TopSymbol(Term));
	continue;
      }

    } else if (term_IsComplex(Term)) {

      Args = term_ArgumentList(Term);
      if (!list_Empty(list_Cdr(Args)))
	stack_Push(list_Cdr(Args));

      Term = list_Car(Args);
      continue;
    }

    if (stack_Empty(Bottom))
      return FALSE;
    else {
      Args = (LIST)stack_PopResult();
      Term = list_Car(Args);
      if (!list_Empty(list_Cdr(Args)))
	stack_Push(list_Cdr(Args));
    }
  }
}


BOOL unify_OccurCheck(CONTEXT CTop, SYMBOL Top, CONTEXT CTerm, TERM Term)
/**********************************************************
  INPUT:   A context, a variable symbol, a context, and a term.
  RETURNS: TRUE if there is a occur check failure with respect
           to the variable symbol <Top> and <Term>.
	   The search is started in <Term>
***********************************************************/
{
  int    Bottom;
  LIST   Args;
  SYMBOL TermTop;

  Bottom = stack_Bottom();

  for (;;) {

    if (term_IsVariable(Term)) {

      TermTop = term_TopSymbol(Term);

      if ((CTop == CTerm) && (symbol_Equal(Top, TermTop))) {
	stack_SetBottom(Bottom);
	return TRUE;
      } else if (cont_VarIsBound(CTerm, TermTop)) {
	Term  = cont_ContextBindingTerm(CTerm, TermTop);
	CTerm = cont_ContextBindingContext(CTerm, TermTop);
	continue;
      }
    } else if (term_IsComplex(Term)) {

      Args = term_ArgumentList(Term);
      if (!list_Empty(list_Cdr(Args))) {
	stack_Push(CTerm);
	stack_Push(list_Cdr(Args));
      }
      Term = list_Car(Args);
      continue;

    }

    if (stack_Empty(Bottom))
      return FALSE;
    else {
      Args = (LIST)stack_PopResult();
      Term = list_Car(Args);
      CTerm = (CONTEXT)stack_Top();
      if (list_Empty(list_Cdr(Args)))
	stack_Pop();
      else
	stack_Push(list_Cdr(Args));
    }
  }
}


/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  UNIFICATION           			            * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


BOOL unify_Unify(CONTEXT CtL, TERM TermL, CONTEXT CtR, TERM TermR)
/**********************************************************
  INPUT:   Two terms which may contain the same variable symbols.
           Equal variable symbols are interpreted different in
	   <TermL> and <TermR>, respectively.
  RETURNS: TRUE, if <TermL> and <TermR> are unifiable, FALSE otherwise.
  CAUTION: None.
***********************************************************/
{
  CONTEXT CHelp;
  LIST    ArgsL, ArgsR;
  int     Bottom;
  BOOL    Bound;

  Bound  = FALSE;
  Bottom = stack_Bottom();

  for (;;) {

    while (term_IsVariable(TermL) &&
	   cont_VarIsBound(CtL, term_TopSymbol(TermL))) {
      CHelp = cont_ContextBindingContext(CtL, term_TopSymbol(TermL));
      TermL = cont_ContextBindingTerm(CtL, term_TopSymbol(TermL));
      CtL   = CHelp;
    }

    while (term_IsVariable(TermR) &&
	   cont_VarIsBound(CtR, term_TopSymbol(TermR))) {
      CHelp = cont_ContextBindingContext(CtR, term_TopSymbol(TermR));
      TermR = cont_ContextBindingTerm(CtR, term_TopSymbol(TermR));
      CtR   = CHelp;
    }

    /* Caution: Bindings from variable to variable are made with priority
       from the right context into the left context. */

    if (term_IsVariable(TermL)) {
      if (term_IsVariable(TermR)) {
	if (!(CtL == CtR && term_EqualTopSymbols(TermL, TermR)))
	  Bound = cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL);
      } else if (Bound && unify_OccurCheck(CtL, term_TopSymbol(TermL), CtR, TermR)) {
	stack_SetBottom(Bottom);
	return FALSE;
      }	else
	Bound = cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR);

    } else if (term_IsVariable(TermR)) {
      if (Bound && unify_OccurCheck(CtR, term_TopSymbol(TermR), CtL, TermL)) {
	stack_SetBottom(Bottom);
	return FALSE;
      }	else
	Bound = cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL);

    } else if (term_EqualTopSymbols(TermL, TermR)) {
      if (term_IsComplex(TermL) && TermL != TermR) {
	ArgsL = term_ArgumentList(TermL);
	ArgsR = term_ArgumentList(TermR);
	if (!list_Empty(list_Cdr(ArgsL))) {
	  stack_Push(CtL);
	  stack_Push(CtR);
	  stack_Push(list_Cdr(ArgsL));
	  stack_Push(list_Cdr(ArgsR));
	}
	TermL = list_Car(ArgsL);
	TermR = list_Car(ArgsR);
	continue;
      }
    } else {
      stack_SetBottom(Bottom);
      return FALSE;
    }

    if (stack_Empty(Bottom))
      return TRUE;
    else {
      ArgsR = stack_PopResult();
      ArgsL = stack_PopResult();
      TermR = list_Car(ArgsR);
      TermL = list_Car(ArgsL);
      CtR   = (CONTEXT)stack_Top();
      CtL   = (CONTEXT)stack_NthTop(1);
      if (list_Empty(list_Cdr(ArgsL)))
	stack_NPop(2);
      else {
	stack_Push(list_Cdr(ArgsL));
	stack_Push(list_Cdr(ArgsR));
      }
    }
  }
}

BOOL unify_UnifyCom(CONTEXT Context, TERM TermL, TERM TermR)
/**********************************************************
  INPUT:   Two terms which may contain the same variable symbols.
           Equal variable symbols are interpreted equally in
	   <TermL> and <TermR>, respectively.
  RETURNS: TRUE, if <TermL> and <TermR> are unifiable, FALSE otherwise.
  CAUTION: None.
***********************************************************/
{
  LIST ArgsL, ArgsR;
  int  Bottom;

  Bottom = stack_Bottom();

  for (;;) {

    while (term_IsVariable(TermL) &&
	   cont_VarIsBound(Context, term_TopSymbol(TermL)))
      TermL = cont_ContextBindingTerm(Context, term_TopSymbol(TermL));

    while (term_IsVariable(TermR) &&
	   cont_VarIsBound(Context, term_TopSymbol(TermR)))
      TermR = cont_ContextBindingTerm(Context, term_TopSymbol(TermR));

    if (term_EqualTopSymbols(TermL, TermR)) {
      if (term_IsComplex(TermL) && TermL != TermR) {
	ArgsL = term_ArgumentList(TermL);
	ArgsR = term_ArgumentList(TermR);
	if (!list_Empty(list_Cdr(ArgsL))) {
	  stack_Push(list_Cdr(ArgsL));
	  stack_Push(list_Cdr(ArgsR));
	}
	TermL = list_Car(ArgsL);
	TermR = list_Car(ArgsR);
	continue;
      }
    } else if (term_IsVariable(TermL)) {
      if (term_IsVariable(TermR))
	cont_CreateBinding(Context, term_TopSymbol(TermL), Context, TermR);
      else if (unify_OccurCheckCom(term_TopSymbol(TermL), Context, TermR)) {
	stack_SetBottom(Bottom);
	return FALSE;
      } else
	cont_CreateBinding(Context, term_TopSymbol(TermL), Context, TermR);
      
    } else if (term_IsVariable(TermR)) {
      if (unify_OccurCheckCom(term_TopSymbol(TermR), Context, TermL)) {
	stack_SetBottom(Bottom);
	return FALSE;
      }	else
	cont_CreateBinding(Context, term_TopSymbol(TermR), Context, TermL);

    } else {
      stack_SetBottom(Bottom);
      return FALSE;
    }

    if (stack_Empty(Bottom))
      return TRUE;
    else {
      ArgsR = stack_PopResult();
      ArgsL = stack_PopResult();
      TermR = list_Car(ArgsR);
      TermL = list_Car(ArgsL);
      if (!list_Empty(list_Cdr(ArgsL))) {
	stack_Push(list_Cdr(ArgsL));
	stack_Push(list_Cdr(ArgsR));
      }
    }
  }
}


BOOL unify_UnifyNoOC(CONTEXT CtL, TERM TermL, CONTEXT CtR, TERM TermR)
/**********************************************************
  INPUT:   Two terms which may contain the same variable symbols.
           Equal variable symbols are interpreted different in
	   <TermL> and <TermR>, respectively.
  RETURNS: TRUE, if <TermL> and <TermR> are unifiable, FALSE otherwise.
  CAUTION: None.
***********************************************************/
{
  CONTEXT CHelp;
  LIST    ArgsL, ArgsR;
  int     Bottom;

  Bottom = stack_Bottom();

  for (;;) {

    while (term_IsVariable(TermL) &&
	   cont_VarIsBound(CtL, term_TopSymbol(TermL))) {
      CHelp = cont_ContextBindingContext(CtL, term_TopSymbol(TermL));
      TermL = cont_ContextBindingTerm(CtL, term_TopSymbol(TermL));
      CtL   = CHelp;
    }

    while (term_IsVariable(TermR) &&
	   cont_VarIsBound(CtR, term_TopSymbol(TermR))) {
      CHelp = cont_ContextBindingContext(CtR, term_TopSymbol(TermR));
      TermR = cont_ContextBindingTerm(CtR, term_TopSymbol(TermR));
      CtR   = CHelp;
    }

    /* Caution: Bindings from variable to variable are made with priority
       from the right context into the left context. */

    if (term_IsVariable(TermL)) {
      if (term_IsVariable(TermR)) {
	if (!(CtL == CtR && term_EqualTopSymbols(TermL, TermR)))
	  cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL);
      } else 
	cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR);

    } else if (term_IsVariable(TermR))
      cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL);

    else if (term_EqualTopSymbols(TermL, TermR)) {
      if (term_IsComplex(TermL) && TermL != TermR) {
	ArgsL = term_ArgumentList(TermL);
	ArgsR = term_ArgumentList(TermR);
	if (!list_Empty(list_Cdr(ArgsL))) {
	  stack_Push(CtL);
	  stack_Push(CtR);
	  stack_Push(list_Cdr(ArgsL));
	  stack_Push(list_Cdr(ArgsR));
	}
	TermL = list_Car(ArgsL);
	TermR = list_Car(ArgsR);
	continue;
      }
    } else {
      stack_SetBottom(Bottom);
      return FALSE;
    }

    if (stack_Empty(Bottom))
      return TRUE;
    else {
      ArgsR = stack_PopResult();
      ArgsL = stack_PopResult();
      TermR = list_Car(ArgsR);
      TermL = list_Car(ArgsL);
      CtR   = (CONTEXT) stack_Top();
      CtL   = (CONTEXT) stack_NthTop(1);
      if (list_Empty(list_Cdr(ArgsL)))
	stack_NPop(2);
      else {
	stack_Push(list_Cdr(ArgsL));
	stack_Push(list_Cdr(ArgsR));
      }
    }
  }
}


/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  UNIFICATION WITH FULL OCCUR CHECK	(recursive)         * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


BOOL unify_UnifyAllOC(CONTEXT IndexContext, CONTEXT CtL, TERM TermL, CONTEXT CtR, TERM TermR)
{
  while (term_IsVariable(TermL)) {
    SYMBOL TermTop;

    TermTop = term_TopSymbol(TermL);

    if (cont_VarIsBound(CtL, TermTop)) {
      CONTEXT CHelp;

      CHelp = cont_ContextBindingContext(CtL, TermTop);
      TermL = cont_ContextBindingTerm(CtL, TermTop);
      CtL   = CHelp;
    } else
      break;
  }

  while (term_IsVariable(TermR)) {
    SYMBOL TermTop;

    TermTop = term_TopSymbol(TermR);

    if (cont_VarIsBound(CtR, TermTop)) {
      CONTEXT CHelp;

      CHelp = cont_ContextBindingContext(CtR, TermTop);
      TermR = cont_ContextBindingTerm(CtR, TermTop);
      CtR   = CHelp;
    } else
      break;
  }
  
  if (term_IsVariable(TermL)) {
    
    if (term_IsVariable(TermR)) {
      if ((CtL != CtR || !term_EqualTopSymbols(TermL, TermR))) {
	if (term_IsIndexVariable(TermL))
	  cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR);
	else 
	  if (term_IsIndexVariable(TermR) || (CtR == IndexContext))
	    cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL);
	  else
	    cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR);
      }
      return TRUE;
    } 
    else 
      if (unify_OccurCheck(CtL, term_TopSymbol(TermL), CtR, TermR))
	return FALSE;
      else {
	cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR);
	return TRUE;
      }
  } 
  else 
    if (term_IsVariable(TermR)) { 
      if (unify_OccurCheck(CtR, term_TopSymbol(TermR), CtL, TermL))
	return FALSE;
      else {
	cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL);
	return TRUE;
      }
    } 
    else 
      if (term_EqualTopSymbols(TermL, TermR)) {
	if (term_IsComplex(TermL)) {
	  LIST ArgL, ArgR;
	  for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR);
	       !list_Empty(ArgL);
	       ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR))
	    if (!unify_UnifyAllOC(IndexContext, CtL, list_Car(ArgL), CtR, list_Car(ArgR)))
	      return FALSE;
	}
	return TRUE;
      } 
      else
	return FALSE;
}


/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  GENERALIZATION TEST      			            * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


BOOL unify_Match(CONTEXT Context, TERM TermL, TERM TermR)
{
  if (term_IsVariable(TermL)) {
    if (cont_VarIsBound(Context, term_TopSymbol(TermL)))
      return term_Equal(cont_ContextBindingTerm(Context, term_TopSymbol(TermL)), TermR);
    else {
      cont_CreateBinding(Context, term_TopSymbol(TermL), cont_InstanceContext(), TermR);
      return TRUE;
    }
  } else if (term_EqualTopSymbols(TermL, TermR)) {
    if (term_IsComplex(TermL)) {
      LIST ArgL;
      LIST ArgR;
      for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR);
	   !list_Empty(ArgL);
	   ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR))
	if (!unify_Match(Context, list_Car(ArgL), list_Car(ArgR)))
	  return FALSE;
    }
    return TRUE;
  } else
    return FALSE;
}

BOOL unify_MatchFlexible(CONTEXT Context, TERM TermL, TERM TermR)
/**************************************************************
  INPUT:   Two terms where symbols with flexible arity are allowed.
  RETURNS: TRUE if <TermL> matches <TermR>.        
***************************************************************/
{
  if (term_IsVariable(TermL)) {
    if (cont_VarIsBound(Context, term_TopSymbol(TermL)))
      return term_Equal(cont_ContextBindingTerm(Context, term_TopSymbol(TermL)), TermR);
    else {
      cont_CreateBinding(Context, term_TopSymbol(TermL), cont_InstanceContext(), TermR);
      return TRUE;
    }
  } else 
    if (term_EqualTopSymbols(TermL, TermR) 
	&& list_Length(term_ArgumentList(TermL)) == list_Length(term_ArgumentList(TermR))) {
      if (term_IsComplex(TermL)) {
	LIST ArgL;
	LIST ArgR;
	for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR);
	     !list_Empty(ArgL);
	     ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR))
	  if (!unify_MatchFlexible(Context, list_Car(ArgL), list_Car(ArgR)))
	    return FALSE;
      }
      return TRUE;
    } 
    else
      return FALSE;
}


void unify_EstablishMatcher(CONTEXT Context, SUBST Subst)
{
  while (subst_Exist(Subst)) {
    /* Index to query */
    cont_CreateBinding(Context, subst_Dom(Subst), cont_InstanceContext(), subst_Cod(Subst));
    Subst = subst_Next(Subst);
  }
}


BOOL unify_MatchBindingsHelp(const CONTEXT IndexContext, TERM TermL, CONTEXT CtR, TERM TermR)
{
  while (term_IsVariable(TermR)) {
    SYMBOL TermTop;

    TermTop = term_TopSymbol(TermR);

    if (symbol_IsIndexVariable(TermTop))
      CtR = IndexContext;
    else if (CtR == cont_InstanceContext())
      break;

    if (cont_VarIsBound(CtR, TermTop)) {
      CONTEXT CHelp;

      CHelp = cont_ContextBindingContext(CtR, TermTop);
      TermR = cont_ContextBindingTerm(CtR, TermTop);
      CtR   = CHelp;
    } else
      break;
  }

  if (term_IsVariable(TermL)) {
    /* Assertion: Variables of 'TermL' are bound in the index context only. */

    if (cont_VarIsBound(IndexContext, term_TopSymbol(TermL)))
      return
	cont_TermEqualModuloBindings(IndexContext,
					cont_ContextBindingContext(IndexContext,
								      term_TopSymbol(TermL)),
					cont_ContextBindingTerm(IndexContext,
								   term_TopSymbol(TermL)),
					CtR,
					TermR);
    else {
      cont_CreateBinding(IndexContext, term_TopSymbol(TermL), CtR, TermR);
      return TRUE;
    }
  } else if (term_EqualTopSymbols(TermL, TermR)) {
    if (term_IsComplex(TermL)) {
      LIST ArgL;
      LIST ArgR;

      for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR);
	   !list_Empty(ArgL);
	   ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR))
	if (!unify_MatchBindingsHelp(IndexContext, list_Car(ArgL), CtR, list_Car(ArgR)))
	  return FALSE;
    }

    return TRUE;
  } else
    return FALSE;
}


BOOL unify_MatchBindings(const CONTEXT IndexContext, TERM TermL, TERM TermR)
{
  return unify_MatchBindingsHelp(IndexContext, TermL, cont_InstanceContext(), TermR);
}


/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  INSTANCE TEST      			            * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


BOOL unify_MatchReverse(const CONTEXT IndexContext, TERM TermL,	CONTEXT CtR, 
			TERM TermR)
/*********************************************************
  INPUT:   'TermL' is in IndexContext and the codomain of a subst.,
           'CtR' is the context of 'TermR' which is the codomain of a subst.
           obtained by a variable binding, 'Bindings' is
           the number of established bindings.
  RETURNS: TRUE, if 'TermL' is an instance of 'TermR';
           FALSE, otherwise.
**********************************************************/
{
  while (term_IsVariable(TermR)) {
    SYMBOL TermTop;

    TermTop = term_TopSymbol(TermR);

    if (symbol_IsIndexVariable(TermTop))
      CtR = IndexContext;
    else if (CtR == cont_InstanceContext())
      break;

    if (cont_VarIsBound(CtR, TermTop)) {
      CONTEXT CHelp;

      CHelp = cont_ContextBindingContext(CtR, TermTop);
      TermR = cont_ContextBindingTerm(CtR, TermTop);
      CtR   = CHelp;
    } else
      break;
  }

  if (term_IsVariable(TermL)) {
    if ((CtR == cont_InstanceContext()) && term_EqualTopSymbols(TermL, TermR))
      /* 'TermL' and 'TermR' are exactly the same variables (via bindings),
	 therefore do not bind them, just return positive. */
      return TRUE;

    else if (term_IsIndexVariable(TermL)) {
      cont_CreateBinding(IndexContext, term_TopSymbol(TermL), CtR, TermR);
      return TRUE;

    } else if (term_IsVariable(TermR) &&
	       (term_IsIndexVariable(TermR) || (CtR == IndexContext))) {
      cont_CreateBinding(IndexContext, term_TopSymbol(TermR), cont_InstanceContext(), TermL);
      return TRUE;

    } else
      return FALSE;

  } else if (term_IsVariable(TermR)) {
    if (term_IsIndexVariable(TermR) || (CtR == IndexContext)) {
      cont_CreateBinding(IndexContext, term_TopSymbol(TermR), cont_InstanceContext(), TermL);
      return TRUE;
    } else
      return FALSE;

  } else if (term_EqualTopSymbols(TermL, TermR)) {
    
    if (term_IsComplex(TermL)) {
      LIST ArgL, ArgR;
      for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR);
	   !list_Empty(ArgL);
	   ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR))
	if (!unify_MatchReverse(IndexContext,
				list_Car(ArgL),
				CtR,
				list_Car(ArgR)))
	  return FALSE;
    }
    return TRUE;
  } else
    return FALSE;
}


/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  VARIATION TEST      			            * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


BOOL unify_Variation(const CONTEXT Context, TERM TermL, TERM TermR)
{
  if (term_IsVariable(TermL)) {
    if (term_EqualTopSymbols(TermL, TermR))
      /* TermL and TermR are in different contexts
	 but both are term variables which do not need to be variated.
	 Index variables cannot occur in TermR
	 which is the term to be inserted. */
      return TRUE;
    else if (term_IsIndexVariable(TermL)) {
      if (cont_VarIsBound(Context, term_TopSymbol(TermL)))
	return term_Equal(cont_ContextBindingTerm(Context, term_TopSymbol(TermL)), TermR);
      else {
	/* Index to query */
	cont_CreateBinding(Context, term_TopSymbol(TermL), Context, TermR);
	return TRUE;
      }
    }
    else
      return FALSE;

  } else if (term_EqualTopSymbols(TermL, TermR)) {
    if (term_IsComplex(TermL)) {
      LIST ArgL;
      LIST ArgR;
      for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR);
	   !list_Empty(ArgL);
	   ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR))
	if (!unify_Variation(Context, list_Car(ArgL), list_Car(ArgR)))
	  return FALSE;
    }
    return TRUE;
  } else 
    return FALSE;
}


/**************************************************************/
/* ********************************************************** */
/* *							    * */
/* *  COMMON GENERALIZATIONS   			            * */
/* *							    * */
/* ********************************************************** */
/**************************************************************/


TERM unify_ComGenLinear(const CONTEXT IndexContext,
			SUBST* SubstL, TERM TermL, SUBST* SubstR, TERM TermR)
{
  if (term_IsIndexVariable(TermR)) {
    *SubstL = subst_Add(term_TopSymbol(TermR), term_Copy(TermL), *SubstL);

    return term_Copy(TermR);
  
  } else if (term_EqualTopSymbols(TermL, TermR)) {
   
    LIST ArgList, ArgL, ArgR;

    ArgList   = list_Nil();
    for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR);
	 !list_Empty(ArgL);
	 ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR))
      ArgList = list_Nconc(ArgList,
			   list_List(unify_ComGenLinear(IndexContext,
							SubstL,
							list_Car(ArgL),
							SubstR,
							list_Car(ArgR))));
    return term_Create(term_TopSymbol(TermL), ArgList);
    
  } else {
    
    SYMBOL Symbol;
    
    Symbol  = cont_NextIndexVariable(IndexContext);

    *SubstL = subst_Add(Symbol, term_Copy(TermL), *SubstL);
    *SubstR = subst_Add(Symbol, term_Copy(TermR), *SubstR);
    
    return term_Create(Symbol, list_Nil());
  }
}