/* ----------------------------------------------------------
%   (C)1992 Institute for New Generation Computer Technology
%       (Read COPYRIGHT for detailed information.)
----------------------------------------------------------- */
/*=====================================================================
*		cu-Prolog III (Constraint Unification Prolog)
*   Copyright: Institute for New Generation Computer Technology,Japan 
*                           1989--91
==================================================================== */
/*--------------------------------------------------------------------
*		<< UNIFY.C >>		
*		safe/unsafe/PST unification 
*      94.5.20   remove_pst_ob
*      94.6.27   pst_unify, remove_pst_object_if_not_equal()
--------------------------------------------------------------------*/

#include "include.h"

#define Npstobj(Head,Env,Tail,Flag)  Neclause(Head,Env,Tail,Flag)
#define UNSAFE 0
#define SAFE 1
#define NOEXTRACT 2
#define EXTRACT 3
#define PSTDEBUG 0
int Ocheck_max;

/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  int tunify(t,e,u,f,flag)
    term unification between (t,e) and (u,f)    
    flag = 0: unsafe
           1: safe, no extract
           2: safe, extract

  return_value --> TRUE/FALSE
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int tunify(t,e,u,f,flag)	/* term unification entry */
register struct term *t, *u;
register struct pair *e, *f;
int flag;     /* 1:safe no-extract, 2:safe extract, 0:unsafe */
{
	struct ustack *usave = usp;
	int  *hsave = hp, res;
	struct pair *esave = ep;

	Ocheck_max = 0;
	if (flag == 1)
	    res = safe_unify(t,e,u,f,NOEXTRACT);
	else if (flag == 2)
	    res = safe_unify(t,e,u,f,EXTRACT);
	else 
	    res = unify(t,e,u,f);
	if (res == FALSE)
	{
		undo(usave);
		hp = hsave;
		ep = esave;
		return(FALSE);
	}
	else return(TRUE);
}


struct pair *LastEnv;
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  int tunify_apply(t,e,u,newf,flag)
  newf= newly-defined environment
  does not push the address in newf
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int tunify_apply(t,e,u,f,flag)	/* term unification entry */
register struct term *t, *u;
register struct pair *e, *f;
int flag;     /* 1:safe no-extract, 2:safe extract, 0:unsafe (only) */
{
	struct ustack *usave = usp;
	int  *hsave = hp, res;
	struct pair *esave = ep;

	LastEnv=f;
	res = tunify(t,e,u,f,flag);
	LastEnv=NULL_ENV;
	return(res);
}

int ocheck(p, t, e)		/* occur check of normal unification      */
/* check if var p is contained in (t,e)   
   if contained, return FALSE,
   else return TRUE
*/
register struct pair *p;	/* var */
register struct term *t;
register struct pair *e;
{
  register struct pair *q;
  register int i, j;

  if (Ocheck_max++ > 50) return(FALSE); /* in case of infinite loop */
/*  printf("ocheck ");
  Pterm(p->p_body, p->p_env);
  printf(" in ");
  Pterm(t,e);
  NL;
 */ 
  if (t == NULL_TERM) return(TRUE);
  down(q, t, e);

  if (q != NULL_ENV) {	/* if t is var  */
    if (p == q)	/*  occured !!  ==> fail */
      return(FALSE);
    else
      return(TRUE);
  }

  switch (t->type.ident) {
    case ATOMIC_TYPE:
    case CONST_LIST_TYPE:
        return(TRUE);
    case LIST_TYPE:
    case CLAUSE_TYPE:
	if (ocheck(p,head_of_list(t),e) == TRUE && 
	    ocheck(p,tail_of_list(t),e) == TRUE)
	    return(TRUE);
	else return(FALSE);
    case PST_TYPE: { /* pst */
	struct eclause *ptt;
	struct pst_item *item;
	if ((item = find_pstitem(t,e)) == NULL_PSTIT) {
		ptt = ((struct pst *)t)->p_lists;
		while (ptt != NULL_ECL) {
			t = Arg2(ptt->c_form);
			if (ocheck(p,t,e) == FALSE) return(FALSE);
			ptt = ptt->c_link;
		}
	}
	else {
	    ptt = item->p_lists;
	    while (ptt != NULL_ECL) {
	    t = Arg2(ptt->c_form);
	    e = ptt->c_env;
	    if (ocheck(p, t, e) == FALSE) return(FALSE);
	    ptt=ptt->c_link;
	   }
	}
	return(TRUE);
      }
     default: /* functor */
	for(i = 0, j = t->t_arity;  i < j;  i++)
	      if (ocheck(p, Arg(t,i), e) == FALSE) return(FALSE);
       }
  return(TRUE);
}

int unify(t, e, u, f)
register struct term *t, *u;
register struct pair *e, *f;
{
	register struct pair *p, *q;

#if PSTDEBUG == 1
	printf("unify:");
	Pterm(t,e);
	printf(" and ");
	Pterm(u,f);
	NL; 
#endif
	down(p, t, e);
	down(q, u, f);
	if (p != NULL_ENV)		/* if t = var */
	  if (p==Anonymous_env) return(TRUE);  /* if t = Anonymous Var */
	  else if(q != NULL)		/* t:var, u:var */
		if(p == q) /* t,u : the same var */
			return(TRUE);
		else if (q==Anonymous_env) /* u : Anonymous Var */
			return(TRUE);
		else {
		        if (e != LastEnv)
			{
			    upush(&(p->p_body)); /* t->u */
			    upush(&(p->p_env));
			}
			p->p_body = u;
			p->p_env = f;
			return(TRUE);
		}
		else {			/* t:var, u:non-var */
		        if (e != LastEnv)
			{
			    upush(&(p->p_body)); /* t->u */
			    upush(&(p->p_env));
			}
		        p->p_body = u;
			p->p_env = f;
			return(TRUE);
		    }
	  else if(q != NULL) 
		if (q==Anonymous_env) return(TRUE);
		else {		/*  t:nonvar , u:var  */
		        if (f != LastEnv)
		        {
			    upush(&(q->p_body)); /* u->t */
			    upush(&(q->p_env));
			}
			q->p_body = t;
			q->p_env = e;
			return(TRUE);
        		}
	/* t,u : nonvar */

	switch (u->type.ident) {
	case ATOMIC_TYPE : /* t,u: atomic (string,num,quote) */
	  {
	    if ((t==u) || (atomic_equal(u,t))) return(TRUE);
	    else return(FALSE);
	  }
	case LIST_TYPE:
	case CONST_LIST_TYPE:
		if (is_list(t)) {
		    if(unify(head_of_list(t),e,head_of_list(u),f) &&
		       unify(tail_of_list(t),e,tail_of_list(u),f))
			return(TRUE);
		}
		return(FALSE);
	case CLAUSE_TYPE:
	  if (is_clause(t)) {
		while ((t != NULL) && (u != NULL)) {
		    if (unify(((struct clause *)t)->c_form,e,
			      ((struct clause *)u)->c_form,f) == FALSE)
			return(FALSE);
		    t=(struct term *)((struct clause *)t)->c_link;
		    u=(struct term *)((struct clause *)u)->c_link;
		}
		if (t == u) return(TRUE);
	      }
	  return(FALSE);
	case PST_TYPE:
	  if (is_pst(t)) {
	      return(pst_unify(t,e,u,f,UNSAFE));
	  }
	  return(FALSE);
        default : /* functor */
	  if(Pred(t) == Pred(u)) {/* t,u: complex term */
	      register int i, j;
	      for(i = 0, j = Pred(t)->f_arity;  i < j;  i++)
		  if (unify(Arg(t,i), e, Arg(u,i), f) == FALSE)
		      return(FALSE); 
	      /* unify each arg */
	      return(TRUE);
	  }
	  return(FALSE);
	}
}


int unify_pst_extract();

int safe_unify(t, e, u, f, extflag)	/* unify with occur check */
register struct term *t, *u;
register struct pair *e, *f;
int extflag;			/* NOEXTRACT or EXTRACT */
{
  register struct pair *p, *q;
  int i, j;

#if PSTDEBUG == 1
  printf("safe_unify ");
  Pterm(t,e);
  printf(" and ");
  Pterm(u,f);
  NL; 
#endif
  down(p, t, e);
  down(q, u, f);
  if(p != NULL)			/* if t = var */
    if (p==Anonymous_env) return(TRUE);  /* if t = Anonymous Var */
    else if(q != NULL)		/* t:var, u:var */
      if(p == q) /* t,u : the same var */
	return(TRUE);
      else if (q==Anonymous_env) /* u : Anonymous Var */
	return(TRUE);
      else {
	if (e != LastEnv) {
	    upush(&(p->p_body)); /* t->u */
	    upush(&(p->p_env));
	}
	p->p_body = u;
	p->p_env = f;
	return(TRUE);
      }
    else {			/* t:var, u:non-var */
      if (ocheck(p,u,f) == FALSE) return(FALSE);
      if (e != LastEnv)
      {
	  upush(&(p->p_body)); /* t->u */
	  upush(&(p->p_env));
      }
      p->p_body = u;
      p->p_env = f;
      return(TRUE);
    }
  else if(q != NULL) 
    if (q==Anonymous_env) return(TRUE);
    else {		/*  t:nonvar , u:var  */
      if (ocheck(q,t,e) == FALSE) return(FALSE);
      if (f != LastEnv)
      {
	  upush(&(q->p_body)); /* u->t */
	  upush(&(q->p_env));
      }
      q->p_body = t;
      q->p_env = e;
      return(TRUE);
    }
  /* t,u : nonvar */
  switch (u->type.ident) {
  case ATOMIC_TYPE : /* t,u: atomic (string,num,quote) */
    {
      if ((t==u) || (atomic_equal(u,t))) return(TRUE);
      else return(FALSE);
    }
  case LIST_TYPE:
  case CONST_LIST_TYPE:
    if (is_list(t) && 
	safe_unify(head_of_list(t),e,head_of_list(u),f,extflag) == TRUE &&
	safe_unify(tail_of_list(t),e,tail_of_list(u),f,extflag) == TRUE)
	return(TRUE);
    else return(FALSE);
  case CLAUSE_TYPE:
    if (is_clause(t)) {
      while ((t != NULL) && (u != NULL)) {
	if (safe_unify(((struct clause *)t)->c_form,e,
		   ((struct clause *)u)->c_form,f,extflag) == FALSE)
	    return(FALSE);
	t=(struct term *)((struct clause *)t)->c_link;
	u=(struct term *)((struct clause *)u)->c_link;
      }
      if (t == u) return(TRUE);
    }
    return(FALSE);
  case PST_TYPE:
    if (is_pst(t)) {
/*	    if (extflag == NOEXTRACT) 
		    pst_unify(t,e,u,f,SAFE);
	    else 
		    unify_pst_extract(t,e,u,f); */
	return(pst_unify(t,e,u,f,SAFE)); 
    }
    else return(FALSE);
  default : /* functor */
    if(Pred(t) == Pred(u)) {/* t,u: complex term */
      for(i = 0, j = Pred(t)->f_arity;  i < j;  i++)
	if (safe_unify(Arg(t,i), e, Arg(u,i), f,extflag) == FALSE)
	    return(FALSE); 
      /* unify each arg */
      return(TRUE);
    }
    return(FALSE);
  }
}


int  pst_unify(t,e,u,f,safeflag)
register struct term *t,*u;
register struct pair *e,*f;
int safeflag;			/* SAFE(1) or UNSAFE(0) */
{
  struct pst_item *target, *object;

#if PSTDEBUG != 0
  printf("pst_unify %d ",safeflag);
  Pterm(t,e);
  printf(" & ");
  Pterm(u,f);
  printf(" ---> ");
#endif
  
  target = find_pstitem(t,e);
  if (target != NULL_PSTIT) { 
      object = remove_pstitem_if_not_equal(u,f,target);
      if (object == target) /* p.var==t.var */
      {
#if PSTDEBUG != 0
	  printf("<C#0>");
#endif
	  return(TRUE);
      }
      else if (object != NULL_PSTIT) /* t,u exist in psttable */
      {
#if PSTDEBUG != 0
	  printf("<C#1>");
#endif
	  if (unify_merge_psts(target,object->p_lists,safeflag) == FALSE)
	      return(FALSE);
      }
      else {			/* t exist, u doesn't exist */
#if PSTDEBUG != 0
	  printf("<C#2>"); 
#endif
	  if (unify_pstlist_objects(target,((struct pst *)u)->p_lists, f,
				    safeflag) == FALSE) return(FALSE);
      }
      if (unify(((struct pst *)u)->p_var,f,
		((struct pst *)t)->p_var,e) == FALSE) return(FALSE); 
      /* u.var -> t.var */
  }
  else {
    object = find_pstitem(u,f);
    if (object != NULL_PSTIT) /* t doesn't exist, u:exists */
    {
#if PSTDEBUG != 0
	    printf("<C#3>");
#endif
	    if (unify_pstlist_objects(object,((struct pst *)t)->p_lists, e, 
				      safeflag) == FALSE) return(FALSE);
	    if (unify(((struct pst *)t)->p_var,e,
		      ((struct pst *)u)->p_var,f) == FALSE) return(FALSE); 
				/* t.var -> u.var */
    }
    else {			/* t,u don't exist */
#if PSTDEBUG != 0
	printf("<C#4>");
#endif
	target = record_pstobjects((struct pst *)t,e);
	if (unify_pstlist_objects(target,((struct pst *)u)->p_lists, f, 
				  safeflag)==FALSE) return(FALSE);
	if (unify(((struct pst *)u)->p_var,f,
		  ((struct pst *)t)->p_var,e) == FALSE) return(FALSE); 
				/* u.var -> t.var */
    }
  }
#if PSTDEBUG != 0
  Pterm(t,e);  NL; 
#endif
  return(TRUE);
}

				/* one-way unification */
int unify_pst_extract(t,e,u,f)	/* safe, extract pst unification */
struct pst *t,*u;		/* t may be changed */
struct pair *e,*f;
{
	struct pst_item *object,*target;
	struct eclause *nttbegin,*ntt,*ot,*tt;
	int i;

	target = find_pstitem(t,e);
	object = find_pstitem(u,f);
	if (target == NULL_PSTIT)
		target = record_pstobjects((struct pst *)t,e);
	if (object == NULL_PSTIT) 
		object = record_pstobjects((struct pst *)u,f);
	nttbegin=NULL_ECL;
	for(ot=object->p_lists,tt=target->p_lists; ((ot!=NULL) && (tt!=NULL));)
	{
		i = Pred(Arg1(tt->c_form))->f_number - 
			Pred(Arg1(ot->c_form))->f_number;
		if (i == 0)
		{
			if (safe_unify(tt->c_form,e,ot->c_form,f,1) == FALSE)
			    return(FALSE);
			tt = tt->c_link;
			ot = ot->c_link;
		}
		else if (i < 0) tt = tt->c_link;
		else
		{		/* ntt is in (u,f), but not in (t,e) */
			if (nttbegin==NULL) nttbegin=ntt=ot;
			else {
				upush(&(ntt->c_link));
				ntt->c_link = ot;
				ntt = ot;
			}
			ot = ot->c_link;
		}
	}
	if (nttbegin != NULL) {
		upush(&(ntt->c_link));
		ntt->c_link = ot;
	}
	else nttbegin = ot;
	upush(&(target->p_lists));
	target->p_lists = nttbegin; /* new target = (u,f)-(t,e) */
	return(TRUE);
}

int unify_pstlist_objects(entry, ol, e, safeflag)
struct pst_item *entry;
struct eclause *ol;
struct pair *e;
int safeflag;			/* SAFE or UNSAFE */
{
  register int i;
  struct eclause *pl;

  if (ol==NULL_ECL) return(TRUE);

  pl=entry->p_lists; /* pl must NOT be NULL */

#if PSTDEBUG != 0
  printf("unify_pstlist_obj ");
  Peclause(pl);
  printf(" -- ");
  Peclause(ol);
  NL;
#endif
  
  if (pl == NULL_ECL) {
    upush(&(entry->p_lists));
    entry->p_lists=record_pstlists(ol,e);
    return(TRUE);
  }

  i = Pred(Arg1(pl->c_form))->f_number - Pred(Arg1(ol->c_form))->f_number;
  if (i == 0) {
      if (safeflag == UNSAFE)
      {
	  if (unify(pl->c_form,pl->c_env,ol->c_form,e) == FALSE) 
	      return(FALSE);
      }
      else
      {
	  if (safe_unify(pl->c_form,pl->c_env,ol->c_form,e,NOEXTRACT) == FALSE) return(FALSE);
      }
      ol=ol->c_link;
  }
  /* pl={f1/v1,f2/v2,..} object={g1/t1,g2/t2,...}, f1 > g1 */
  /* --> pl={g1/t1,f1/v1,...} object={g2/t2,...} */
  else if (i > 0) {	
    upush(&(entry->p_lists));
    entry->p_lists = Npstobj(ol->c_form,e,pl,MEDIUM);
    ol = ol->c_link;
    pl=entry->p_lists;
  }
 /*  else  goes on */

  for (; ol != NULL_ECL && 
       pl->c_link != NULL_ECL; )
  {
      i = Pred(Arg1(pl->c_link->c_form))->f_number - 
	  Pred(Arg1(ol->c_form))->f_number;
      if (i == 0) {
	  if (safeflag== UNSAFE)
	  {
	      if (unify(pl->c_link->c_form,pl->c_link->c_env,
			ol->c_form,e) == FALSE) return(FALSE);
	  }
	  else
	  {
	      if (safe_unify(pl->c_link->c_form,pl->c_link->c_env,
			     ol->c_form,e,NOEXTRACT) == FALSE) return(FALSE);
	  }
	  ol = ol->c_link;
	  pl = pl->c_link;
      }
      else if (i > 0) {
	  upush(&(pl->c_link));
	  pl->c_link = Npstobj(ol->c_form,e,pl->c_link,MEDIUM);
	  ol = ol->c_link;
	  pl = pl->c_link;
      }
      else
      {
	  pl = pl->c_link;
      }
  }
  if (pl->c_link == NULL_ECL) {
      upush(&(pl->c_link));
      pl->c_link = record_pstlists(ol,e);
  }
  return(TRUE);
}


int unify_merge_psts(target,object,safeflag)
struct pst_item *target;
struct eclause *object;
int safeflag;			/* SAFE or UNSAFE */
{
  register int i;
  struct eclause *pnext,*onext, *pl;

  if (object==NULL_ECL) return(TRUE);

  pl=target->p_lists;
  
  if (pl == NULL_ECL) {
    upush(&(target->p_lists));
    target->p_lists = object;
    return(TRUE);
  }

  i = Pred(Arg1(pl->c_form))->f_number - Pred(Arg1(object->c_form))->f_number;
  if (i == 0) {
      if (safeflag == UNSAFE)
      {
	  if (unify(pl->c_form,pl->c_env,
		    object->c_form,object->c_env) == FALSE) return(FALSE);
      }
      else
      {
	  if (safe_unify(pl->c_form,pl->c_env,
			 object->c_form,object->c_env,EXTRACT) == FALSE)
	      return(FALSE);
      }
      object=object->c_link;
  }
  /* pl={f1/v1,f2/v2,..} object={g1/t1,g2/t2,...}, f1 > g1 */
  /* --> pl={g1/t1,f1/v1,...} object={g2/t2,...} */
  else if (i > 0) {		/* 93.8.17 by H.Sirai */
    upush(&(target->p_lists));	/* pl.. > ol.. -> ol,pl.. & ol... */
    target->p_lists =
      Npstobj(object->c_form,object->c_env,pl,MEDIUM);
    object = object->c_link;
    pl = target->p_lists;
  }
 /* else goes on */


  for (; object != NULL_ECL && 
       pl->c_link != NULL_ECL; )
  {
      i = Pred(Arg1(pl->c_link->c_form))->f_number - 
	  Pred(Arg1(object->c_form))->f_number;
      if (i == 0) {
	  if (safeflag == UNSAFE)
	  {
	      if (unify(pl->c_link->c_form,pl->c_link->c_env,
			object->c_form,object->c_env) == FALSE) return(FALSE);
	  }
	  else
	  {
	      if(safe_unify(pl->c_link->c_form,pl->c_link->c_env,
			    object->c_form,object->c_env,NOEXTRACT) == FALSE)
		  return(FALSE);
	  }
	  pl=pl->c_link;
	  object=object->c_link;
       }
      else if (i > 0) {		/* pl->pnext-> ==> pl->object->pnext   */
	  pnext=pl->c_link;
	  onext=object->c_link;
	  upush(&(pl->c_link));
	  pl->c_link = object;
	  upush(&(object->c_link));
	  object->c_link = pnext;
	  pl=pl->c_link;
	  object=onext;
      }
      else {
	  pl=pl->c_link;
      }
  }
  if (pl->c_link == NULL_ECL) {
      upush(&(pl->c_link));
      pl->c_link = object;
  }
  return(TRUE);
}