/* ----------------------------------------------------------
%   (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
==================================================================== */
/*--------------------------------------------------------------------
*		<< modular.c >>
*		constraint transformation entry, tools
*    94.6.28  termset speedup
--------------------------------------------------------------------*/

#include "include.h"

#if SUN4 == 1
#include <sys/time.h>
#else
#if CPUTIME != 0
#include <sys/types.h>
#include <sys/times.h>
#endif
#endif

#define in_cheap(X) (( &cheap[0] <= ((int *)X)) && (((int *)X) < chp))
#define in_upper_heap(X,Y) ( in_sheap(X) || ( (Y==MEDIUM) && in_cheap(X)) )
		     
long CONSTRAINT_OLD_TIME;

/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  modular(c)
   @ mode entry
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
void modular(c,vlist,anum)	/* constraint trans. from top level (@) */
struct clause *c;
struct term *vlist;
int anum;
{
	struct clause *sol;

	sol = startmodular(c, vlist, anum); /* tranformation */
	tprint0("solution = ");
	if (sol == MFAIL){	/* fail transformation */
		tprint0("fail.\n");
	}
	else if (sol == NULL){	/* nil constraint */
		tprint0("nil (true).\n");
	}
	else			/* c.t. success */
	{
		Pclause(sol, NULL_ENV); NL;
		show_newdefs();	/* print DEF_list */
	}
}


/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
   cu(t,e)
     process unify() built-in predicate
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
/* constraint transformation embedded in Prolog  : unify() pred. */

int cu(t,e)		/*  0: cu fail  1: success   */
struct term *t;
struct pair *e;
{
	register struct pair *p, *q;
	struct pair *ee;
	struct term *tt;
	struct clause *c, *clist;
#if CPUTIME != 0
	struct tms TIMES;
#endif

	if (t == NULL) return(TRUE);

	if (! isvar(Arg2(t))) return(FALSE);	/* second arg = var */
	p = &e[vnumber(Arg2(t))];
	if (p->p_body != NULL) return(FALSE);	/* second arg-->var */

#if SUN4 == 1
	CONSTRAINT_OLD_TIME = clock();
#else
#if CPUTIME != 0
	times(&TIMES);
	CONSTRAINT_OLD_TIME =  TIMES.tms_stime + TIMES.tms_utime;
#endif
#endif
	p->p_env = Nenv(0);	/*  cf. 'q' in termset()  */
	up_init();
	tt = Arg1(t);
	ee = e;
	down(q,tt,ee);
	if (tt == NIL){
	  p->p_body = NIL;
	  p->p_env = NULL;
#if SUN4 == 1
	  CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
	  times(&TIMES);
	  CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
	    CONSTRAINT_OLD_TIME;
#endif
#endif
	  return(TRUE);
	}

	clist = c = Nclause(termset(head_of_list(tt),ee,TEMPORAL),
			    NULL_CL,TEMPORAL);
	while (1) {
	  tt = tail_of_list(tt);
	  down(q,tt,ee);
	  if ((tt == NIL) || (! is_list(tt))) break;
	  c->c_link = Nclause(termset(head_of_list(tt),ee,TEMPORAL),
			      NULL_CL,TEMPORAL);
	  c = c->c_link;
	}

	if (tt != NIL) {
		up_restore();
		p->p_env = NULL;
		error("Illegal form of constraint list.");
	}

	if (p_number != 0) {
	  renum_pvars((struct pstvar *)pv_list,v_number);
	  q=Nenv(p_number);
	}
	up_restore();

	c = startmodular(clist,v_list,v_number+p_number); /* transformation */

	if (c == MFAIL){	/* fail transformation */
		p->p_env = NULL;
#if SUN4 == 1
		CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
		times(&TIMES);
		CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
		  CONSTRAINT_OLD_TIME;
#endif
#endif
		return(FALSE);	/* fail */
	}
	else if (c == NULL)
	{
		p->p_body = NIL;
		p->p_env = NULL;
#if SUN4 == 1
		CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
		times(&TIMES);
		CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
		  CONSTRAINT_OLD_TIME;
#endif
#endif
		return(TRUE);
	}
	else
	{
		p->p_body = tolist(c,STINGY);
TB
		tprint0("   ====> ");
		Pterm(p->p_body, p->p_env);
TE
#if SUN4 == 1
		CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
		times(&TIMES);
		CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
		  CONSTRAINT_OLD_TIME;
#endif
#endif
	        return(TRUE);	/* success */
	}
}

/*  change clause(t1,t2,t3)  to list([t1,t2,t3])  <- cu() */
struct term *tolist(c,flag)
struct clause *c;
int flag;
{
  register struct clause *cc, *croot;

  if (c == NULL) return(NIL);
  
  switch (flag) {
    case STINGY:
       for (cc = c; cc->c_link != NULL; cc=cc->c_link)
	   cc->c_type = LIST_TYPE;
       cc->c_link = (struct clause *)NIL;
       return((struct term *)c);
    default:
       croot=cc=Nlist(head_of_list(c),(struct clause *)NIL,flag);
       while (c->c_link != NULL) {
	  c=c->c_link;
          cc->c_link=Nlist(head_of_list(c),(struct clause *)NIL,flag);
	  cc = cc->c_link;
	}
       return((struct term *)croot);
     }
}

/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
   transform(precond,newc,newenv)
   constriant solver of CAHC , called by resolve() in refute.c
      precond: old constraint (from goal)
      newc, newenv: new constraint (from program)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
/* constraint transformation entry <- resolve() */
struct eclause *transform(precond, newc, newenv)
struct eclause *precond;
struct clause *newc;
struct pair *newenv;
{
    struct eclause *eclause_append();
   	struct eclause *cond;
	struct clause *c,*clist;
	struct pair *env,*q;
#if CPUTIME != 0
	struct tms TIMES;
#endif

	if (precond == NULL && newc == NULL) return(NULL);	

#if SUN4 == 1
	CONSTRAINT_OLD_TIME = clock();
#else
#if CPUTIME != 0
	times(&TIMES);
	CONSTRAINT_OLD_TIME =  TIMES.tms_stime + TIMES.tms_utime;
#endif
#endif
  cond = eclause_append(precond, reduce_clause(newc,newenv));
    if (cond == (struct eclause *)MFAIL) /* reduce_clause failure */
    {
	    TB tprint0("fail (reducetion)"); TE
	    return((struct eclause *)MFAIL);
    }
  env = Nenv(0);
  up_init();
  clist = up_eclause(cond,MEDIUM); /* set clause */
  up_restore();
  if (p_number != 0) {
    renum_pvars((struct pstvar *)pv_list,v_number);
    q=Nenv(p_number);  /* 1991-03-10 */
  }
  if (clist == NULL) {
#if SUN4 == 1
	  CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
	  times(&TIMES);
	  CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
	    CONSTRAINT_OLD_TIME;
#endif
#endif
	  return(NULL); /* no constraint */
	}
TB
  tprint0(">>transform: ");
  Peclause(cond);
  tprint0(" ==> ");
TE
  c = startmodular(clist,v_list,v_number+p_number);

  if (c == MFAIL) {	/* constraint transformation failure */
	  TB   tprint0("fail"); TE
#if SUN4 == 1
	  CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
	  times(&TIMES);
	  CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
	    CONSTRAINT_OLD_TIME;
#endif
#endif
 	return((struct eclause *)MFAIL);
  }

  cond = reduce_clause(c,env);
  if (cond == NULL_ECL) {
	  TB tprint0("null"); TE
  }
  else if (cond == (struct eclause *)MFAIL)
  {
	  TB tprint0("fail (reduction)"); TE
  }
  else	{
	  TB Peclause(cond); TE
  }
#if SUN4 == 1
    CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
    times(&TIMES);
    CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
      CONSTRAINT_OLD_TIME;
#endif
#endif
  return(cond);
}

struct eclause *eclause_append(head,tail) /* <- transform() */
register struct eclause *head, *tail;
{
  if (head == (struct eclause *)MFAIL || 
      tail == (struct eclause *)MFAIL) 
	  return((struct eclause *)MFAIL);
  while (head != NULL_ECL) {
    tail = Neclause(head->c_form,head->c_env,tail,TEMPORAL);
    head = head->c_link;
  }
  return(tail);
}


/*  ---------  term set -------------  */
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  struct term *termset(t,e,flag)
  struct clause *up_eclause(ec,flag)
   make variant of terms with an environment
   Before termset, up_init() and after termset,  up_restore().
   Before termset, set p=Nenv(0), then p will be a unifier.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct up_log
{
	struct term *u_old,*u_new;
	struct pair *u_oldenv;
	struct up_log *u_link;
};

struct ustack *ustack_save_up; /* save old usp */
int UHASHSIZE=17;
struct up_log *UP_Log[17], *UP_pstLog[17];

int log_size(n)			/* for debug */
int n;
{
    register int i;
    register struct up_log *u;
    for (u=UP_Log[n],i=0; u!=NULL; u=u->u_link,i++);
    return(i);
}

int pstlog_size(n)			/* for debug */
int n;
{
    register int i;
    register struct up_log *u;
    for (u=UP_pstLog[n],i=0; u!=NULL; u=u->u_link,i++);
    return(i);
}

void initialize_log()
{
	register int i;
	for (i=0; i<UHASHSIZE; i++) UP_Log[i]=UP_pstLog[i]=NULL;
}

int print_tepair_length()	/* for debug */
{
    int i;
    for (i=0; i<UHASHSIZE; i++)
	printf("%d/%d ",log_size(i),pstlog_size(i));
    putchar('\n');
}

int tepairtype(t,e)
struct term *t;
struct pair *e;
{
    return(((int)t + (int)e) % UHASHSIZE); 
}

void up_init0()
{

	ustack_save_up = usp;	
	v_number = 0; v_list = NULL_TERM;
	p_number = 0; pv_list = NULL_TERM;
}

void up_restore0()
{
	undo(ustack_save_up);
}

void up_init()
{
    up_init0();
    initialize_log();
}

void up_restore()
{
	initialize_log();
	up_restore0();
}

void push_log(oldt,oldenv,newt)
struct term *oldt,*newt;
struct pair *oldenv;
{
	register struct up_log *u;
	register int tt;
	
	MEMORY_ALLOC(u,up_log,TEMPORAL);
	u->u_old = oldt;
	u->u_new = newt;
	u->u_oldenv = oldenv;
	tt = tepairtype(oldt,oldenv);
	u->u_link = UP_Log[tt];
	UP_Log[tt] = u;
}

struct term *search_log(t,e)	/* search (t,e) in UP_log */
struct term *t;
struct pair *e;
{
	register struct up_log *u;
	for (u = UP_Log[tepairtype(t,e)]; u != NULL; u = u->u_link)
		if (u->u_old == t && u->u_oldenv == e)
			return(u->u_new);
	return(NULL);
}

void push_pstlog(oldt,oldenv,newt)
struct term *oldt,*newt;
struct pair *oldenv;
{
	register struct up_log *u;
	register int tt;

	MEMORY_ALLOC(u,up_log,TEMPORAL);
	u->u_old = oldt;
	u->u_new = newt;
	u->u_oldenv = oldenv;
	tt = tepairtype(oldt,oldenv);
	u->u_link = UP_pstLog[tt];
	UP_pstLog[tt] = u;
}

struct term *search_pstlog(t,e)	/* search (t,e) in UP_log */
struct term *t;
struct pair *e;
{
	register struct up_log *u;
	for (u = UP_pstLog[tepairtype(t,e)]; u != NULL; u = u->u_link)
		if (u->u_old == t && u->u_oldenv == e)
			return(u->u_new);
	return(NULL);
}

void check_constant_term(t) 
struct term *t;
{
	register int i;
	
	if (t->t_arity < 0) t->t_arity = - t->t_arity;
	for (i = 0; i < Pred(t)->f_arity; i++)
		if (! isconst(Arg(t,i))) return;
	t->t_arity = - t->t_arity;
}

/* term prepare for cu() : v_list and v_number are changed */
struct term *termset(t,e,flag)
register struct term *t;
register struct pair *e;
int flag;
{
  register struct pair *p,*q;
  register struct term *nt;
  
  if (t == NULL) return(t);
  down(p,t,e);
  if (p != NULL)	{	/*	if t is a free var */
    if (p == Anonymous_env)
      return(Anonymous_var);
    if (p->p_env == NULL)	{/*	if t is a new var */
      /* use p->p_env as work area */
      upush(&(p->p_env));
      Nvar(vname(t),flag);
      p->p_env = (struct pair *)v_list;
      q = Nenv(1);
      q->p_body = t;
      q->p_env  = e;
      return(v_list);
    }
    else{
      ((struct var *)p->p_env)->v_occurrence++;
      return( (struct term *)p->p_env );
    }
  }
  if (t->type.ident == PST_TYPE)
    return(up_pst(((struct pst *)t),e,flag)); 
  if (flag==ETERNAL && (nt = search_log(t,e)) != NULL)  return(nt); 
  /* already set */
  switch (t->type.ident) {
  case ATOMIC_TYPE:
    nt = up_atomic(t,flag); /* constant term */
    break;
  case CLAUSE_TYPE:
    nt = (struct term *)Nclause(termset(head_of_list(t),e,flag),
	   (struct clause *)termset(tail_of_list(t),e,flag),flag);
    break;
  case LIST_TYPE:
  case CONST_LIST_TYPE:
    nt = (struct term *)Nlist(termset(head_of_list(t),e,flag),
	    (struct clause *)termset(tail_of_list(t),e,flag),flag);
    break;
  default:
    if (isconst_functor(t))
    {
	nt = up_const_functor(t,flag);
	break;
    }
    nt = Nterm(t->t_arity,flag);
    nt->type.t_func = t->type.t_func;
    {
      register int i;
      for (i = 0; i < t->t_arity; i++)
	Arg(nt,i) = termset(Arg(t,i), e, flag);
    }
    check_constant_term(nt);	/* check if nt is constant term */
  }
  /* print_tepair_length(); */
  if (flag == ETERNAL) push_log(t,e,nt);
  return(nt);
}

struct term *up_pst(pt,e,flag)
struct pst *pt;
struct pair *e;
int flag;
{
  struct pst_item *target;
  struct pst *nt;
  struct pstvar *pv;
  struct eclause *t0,*targetobj;
  struct pair *e0;
  struct term *oldt;

  if ((target = find_pstitem((struct term *)pt,e)) != NULL_PSTIT)
  {
	  t0 = target->p_lists;
	  e0 = NULL;
	  if (flag==ETERNAL && (oldt = search_pstlog(t0,e0)) != NULL) 
	      return(oldt);
	  targetobj = termset_pstobj(target->p_lists,flag);
  }
  else
  {
 	  t0 = pt->p_lists;
	  e0 = e;
	  if ((oldt = search_pstlog(t0,e0)) != NULL) return(oldt);
	  targetobj = termset_pstobj_sub(pt->p_lists,e,flag);
  }
  MEMORY_ALLOC(nt,pst,flag);
  nt->type = PST_TYPE;

  MEMORY_ALLOC(pv,pstvar,flag);
  pv->v_type = VAR_PST_TYPE;
  pv->v_name = vname(Anonymous_var);
  pv->v_number = p_number++;
  pv->v_link = pv_list;
  pv->old_var = pt->p_var;
  nt->p_var = pv_list = (struct term *)pv;
  nt->p_lists = targetobj;
  if (flag == ETERNAL) push_pstlog(t0,e0,(struct term *)nt);
  return((struct term *)nt);
}


struct eclause *termset_pstobj(pobj,flag)
struct eclause *pobj;
int flag;
{
  if (pobj==NULL_ECL) return(pobj);
  else
    return(Npstobj(termset(pobj->c_form,pobj->c_env,flag),
    		   NULL_ENV,
    		   termset_pstobj(pobj->c_link,flag),
    		   flag));
}

struct eclause *termset_pstobj_sub(pobj,e,flag)
struct eclause *pobj;
struct pair *e;
int flag;
{
  struct eclause *pl, *ptop;

  if (pobj == NULL_ECL)
    return(pobj);
  ptop = pl = Npstobj(termset(pobj->c_form,e,flag),
		      NULL_ENV,NULL_ECL,flag);
  while (pobj->c_link != NULL_ECL) {
    pl->c_link=
      Npstobj(termset(pobj->c_link->c_form,e,flag),
	      NULL_ENV,NULL_ECL,flag);
    pobj = pobj->c_link;
    pl = pl->c_link;
  }
  return(ptop);
}

struct term *up_const(t,flag)
register struct term *t;
int flag;
{
  struct term *up_atomic(), *up_const_functor();

  if (in_upper_heap(t,flag)) return(t);
  switch (t->type.ident) {
    case ATOMIC_TYPE:
      return(up_atomic(t,flag));
    case CONST_LIST_TYPE:
     return((struct term *)Nlist(up_const(head_of_list(t),flag),
			       (struct clause *)up_const(tail_of_list(t),flag),
			       flag));
    default: /* functor */
      return(up_const_functor(t,flag));
    }
}

struct term *up_atomic(t,flag)
register struct term *t;
int flag;
{
  register struct term *tt;

  if (flag == TEMPORAL || in_upper_heap(t,flag)) return(t);
  tt = Nterm(0,flag);
  tt->type.ident = t->type.ident;
  tt->t_arity = t->t_arity;
  if (is_int(t)) num_value(tt) = num_value(t);
  else if (! is_string(t)) num_value(tt) = num_value(t);
  else str_value(tt) = nalloc(str_value(t),flag);
  return(tt);
}

struct term *up_const_functor(t,flag)
register struct term *t;
int flag;
{
     register struct term *tt;
     register int i;

     if (flag == TEMPORAL || in_upper_heap(t,flag)) return(t);     
     i = -t->t_arity;
     if (i == 0) 	/* constant */
     {
       tt = Nterm(0,flag);
       Pred(tt) = Pred(t);
       return(tt);
     }
     tt = Nterm(i,flag);

     Pred(tt) = Pred(t);
     tt->t_arity = -i;

     while (i > 0) {
	  i--;
          Arg(tt,i) = up_const(Arg(t,i),flag);
      }
     return(tt);
}

struct clause *up_eclause(ec,flag)
struct eclause *ec;
int flag;
{
  if (ec == NULL) return(NULL);
  return(Nclause(termset(ec->c_form, ec->c_env,flag),
		 up_eclause(ec->c_link,flag),
		 flag));
}

struct clause *up_itrace_clause(cl,anum)
struct clause *cl;
int anum;
{
	register struct variant *va;
	struct variant *variant();

	va = variant(cl,ETERNAL);
	return(va->v_clause);
}

/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  try_fold(c,n)
    try fold transformation
       c: clause
       n: # of vars + # of psts in c
    if there is H<=>C in new predicate derivation clauses and Cu=cu, 
       return Hu (u is a variable replacement).
    else return NULL

try_fold() is called by new_constraint() in trans.c
.   .   .   try_fold+
.   .   .   .   match+
.   .   .   .   .   match_term+
.   .   .   .   termnumber
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct term *try_fold(c,n)	/* fold transformation */
struct clause *c;		/* target clause */
int n;				/* # of different vars and psts in c */
{
  register struct itrace *it;
  struct ustack *usave;
  struct term *t,*head;
  struct pair *e;
  struct pair *esave = ep;
  int j, count,termnumber();

  if (c == NULL) return(NULL);
  if (newf_list == NULL) return(NULL);

  count = literalnumber(c);  /* number of terms in c */
  usave = usp;
  esave = ep;
  e = Nenv(n);
  for (it = newf_list; it != NULL; it = it->it_link ) {
	  if ((it->it_anumber == n) && (it->it_cnumber == count) ) 
		  if (match(c, it->it_clause->c_link, e) == FALSE)
		  {
			  undo(usave);
			  ep = esave;
			  continue;
		  }
		  else{
			  if (it->it_clause->c_form == FAIL) {
				  undo(usave); ep = esave;
				  return(FAIL);
			  }
			  head = it->it_clause->c_form;
			  t = Nterm(Pred(head)->f_arity, MEDIUM);
			  Pred(t) = Pred(head);
			  for (j = 0; j < Pred(head)->f_arity ; j++) {
				Arg(t,j) = e[termnumber(Arg(head,j))].p_body;
				/* patch for PST var 1991-03-02 */
				if (Arg(t,j)==NULL) Arg(t,j)=Anonymous_var;
			  }
			  undo(usave); ep = esave; /* patch 1991-03-03 */
			  return(t);	/*  found something  */
		  }
  }
  return(NULL);
}

int termnumber(t)
struct term *t;			/* var or PST */
{
	if (isvar(t)) return(vnumber(t));
	else if (is_pst(t)) return(vnumber( ((struct pst *)t)->p_var));
	else printf("illegal term type : termnumber");
}

int match(clo,clt,e)		/*  clause matcher  */
struct clause *clo,*clt;
struct pair *e;
{
	register struct clause *c1,*c2;

	for (c1 = clo,c2 = clt; c1 != NULL ; c1 = c1->c_link,c2 = c2->c_link)
		if (Pred(c1->c_form) != Pred(c2->c_form))
			return(FALSE); /* fail */

	for (c1 = clo, c2 = clt; c1 != NULL; c1 = c1->c_link, c2 = c2->c_link)
		if (match_term(c1->c_form , c2->c_form , e) == FALSE)
		    return(FALSE);
	return(TRUE);		/* success */
}


int match_term(t1,t2,e)	/*  term unification (t1,e) = (t2,e) */
struct term *t1,*t2;
struct pair *e;			/*  return envs */
{
	register struct pair *p;

	if (isvar(t2)) {
		if (!isvar(t1)) return(FALSE);
		p = &e[vnumber(t2)];
		if (p->p_body == NULL) {
			p->p_body = t1;
			return(TRUE);
		}
		else if(p->p_body == t1) return(TRUE);
		else return(FALSE);
	}
	else if (isvar(t1)) return(FALSE);

	if (Pred(t1) != Pred(t2)) return(FALSE);
	switch (t1->type.ident) {
	case ATOMIC_TYPE:
	  if ((t1==t2) ||(atomic_equal(t1,t2))) return(TRUE);
	  else return(FALSE);
	case LIST_TYPE:
	case CONST_LIST_TYPE:
	  if (match_term(head_of_list(t1),head_of_list(t2),e) && 
	      match_term(tail_of_list(t1),tail_of_list(t2),e))
	      return(TRUE);
	  else return(FALSE);
	case CLAUSE_TYPE:
	  while ((t1!=NULL) && (t2!=NULL)) {
	    if (match_term(head_of_list(t1),head_of_list(t2),e) == FALSE)
		return(FALSE);
	    t1=tail_of_list(t1);
	    t2=tail_of_list(t2);
	  }
	  if (t1==t2) return(TRUE);
	  else return(FALSE);
	case PST_TYPE:
	  if (t2->type.ident != PST_TYPE) return(FALSE);
	  p = &e[termnumber(t2)];
	  if (p->p_body == NULL)
	  {
		  if (match_term((struct term *)((struct pst *)t1)->p_lists,
				 (struct term *)((struct pst *)t2)->p_lists,e)
		      == FALSE) return(FALSE);
		  p->p_body = t1;
		  return(TRUE);
	  }
	  else if (p->p_body == t1) return(TRUE);
	  else if (p->p_body != t1) return(FALSE);
	case ECLAUSE_TYPE: /* pst_objects */
	  while ((t1!=NULL) && (t2!=NULL)) {
	    if (match_term(((struct eclause *)t1)->c_form,
		 ((struct eclause *)t2)->c_form,e) == FALSE) return(FALSE);
	    t1=(struct term *)((struct eclause *)t1)->c_link;
	    t2=(struct term *)((struct eclause *)t2)->c_link;
	  }
	  if (t1==t2) return(TRUE);
	  else return(FALSE);
	default: {
	  register int i,j = t1->t_arity;
	  if (j < 0) j = -j;
	  for(i = 0 ; i<j ; i++)
	    if (match_term(Arg(t1,i), Arg(t2,i), e) == FALSE) return(FALSE);
	  return(TRUE);
	}
      }
}