/*  $Id$

    Part of SWI-Prolog

    Author:        Kuniaki Mukai Wielemaker
    E-mail:        mukai@sfc.keio.ac.jp
    WWW:           http://www.swi-prolog.org
    Copyright (C): 2011, Kuniaki Mukai

    This library is free software; you can redistribute it and/or
    modify it under the terms of the GNU Lesser General Public
    License as published by the Free Software Foundation; either
    version 2.1 of the License, or (at your option) any later version.

    This library 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
    Lesser General Public License for more details.

    You should have received a copy of the GNU Lesser General Public
    License along with this library; if not, write to the Free Software
    Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
*/

/*#define O_DEBUG 1*/
#include "pl-incl.h"


		/********************************
		*	     VARIANT	        *
		*********************************/

#define consVar(w) (((intptr_t)(w)<<LMASK_BITS) | TAG_VAR | FIRST_MASK)
#define valVar(w)  ((intptr_t)(w) >> LMASK_BITS)

#define TAG_COMPOUND_x    (STG_STATIC|TAG_COMPOUND)
#define isCompound_x(w) \
  (( (intptr_t)(w) & (STG_MASK|TAG_MASK) ) == TAG_COMPOUND_x )
#define valCompound_x(w)  ((intptr_t)(w) >> LMASK_BITS)
#define consCompound_x(i)  (((i)<<LMASK_BITS) | TAG_COMPOUND_x)

#define node_bp(p)	((p)->bp)
#define node_orig(p)	((p)->orig)
#define node_variant(p) ((p)->a)
#define node_isom(p)	((p)->b)

typedef struct aWork
{ word *	left;			/* left term arguments */
  word *	right;			/* right term arguments */
  int		arg;
  int		arity;
} aWork;


typedef struct argPairs
{ aWork	work;				/* current work */
  segstack	stack;
  aWork		first_chunk[16];
} argPairs;


typedef struct node
{ Word  bp;			/* pointer to the original term */
  word  orig;			/* saved word */
  int	a;			/* variant at left */
  int	b;			/* link to isomophic node */
} node;


static void
init_agenda(argPairs *a)
{ initSegStack(&a->stack, sizeof(aWork),
	       sizeof(a->first_chunk), a->first_chunk);
}


static inline bool
push_args(argPairs *a, Word left, Word right, int arity)  /* plural */
{ if ( !pushSegStack(&a->stack, a->work, aWork) )
    return FALSE;

  a->work.left  = left;
  a->work.right = right;
  a->work.arg   = 0;
  a->work.arity = arity;

  return TRUE;
}

static inline bool
next_arg(argPairs *a, Word *lp, Word *rp)   /* singular (not plural !) */
{ if ( emptySegStack(&a->stack) )
    return FALSE;

  *lp = a->work.left;
  *rp = a->work.right;

  a->work.arg++ ;
  a->work.left++ ;
  a->work.right++ ;

  if ( a->work.arg >= a->work.arity )
  { if ( !popSegStack(&a->stack, &a->work, aWork) )
      return FALSE;
  }

  return TRUE;
}

static inline node *
Node(int i, Buffer buf)
{ return  &fetchBuffer(buf, i, node);
}

static inline bool
add_node_buffer(Buffer b, node *obj)
{ if ( ((b->top) + sizeof(node)) > (b->max) )
  { if ( !growBuffer(b, sizeof(node)) )
      return FALSE;
  }

  *((node *)(b)->top) = *obj;
  b->top += sizeof(node);

  return TRUE;
}

static inline int
var_id(Word p, Buffer buf)
{ word w = *p;

  if ( w )
  { return (int)valVar(w);		/* node id truncated to int: */
  } else				/* < 2^31 nodes */
  { int n = (int)entriesBuffer(buf, node);
    node new = {p, w, 0, 0};

    if ( !add_node_buffer((Buffer)buf, &new) )
      return MEMORY_OVERFLOW;

    *p = (word)consVar(n);
    return n;
  }
}

static inline int
term_id(Word p, Buffer buf)
{ word w = *p;

  if ( isCompound_x(w) )
  { return (int)valCompound_x(w);
  } else
  { int n = (int)entriesBuffer(buf, node);
    node new = {p, w, 0, 0};

    if ( !add_node_buffer((Buffer)buf, &new) )
      return MEMORY_OVERFLOW;

    *p = (word)consCompound_x(n);
    return n;
  }
}

static inline int
Root(int i, node **r, Buffer buf)
{ int k;
  node * n;

  do
  { k = i;
    n = Node(i, buf);
    DEBUG(CHK_SECURE, assert(n > 0));
    i = node_isom(n);
  } while ( i != 0 );

  *r = n;

  return k;
}

static inline void
univ(word t, Word d, Word *a ARG_LD)
{ Functor f;

  f = valueTerm(t);
  while ( isRef(f->definition) )
    f = (Functor)unRef(f->definition);
  *d = f->definition;
  *a = f->arguments;
}

static inline void
reset_terms(node * r)
{ *(r->bp)  =  r->orig;
}

/* isomorphic (==) */

static int
isomorphic(argPairs *a, int i, int j, Buffer buf ARG_LD)
{ Word l = NULL, r = NULL, lm, ln;
  word dm, dn;
  Word dummy = NULL;

  if ( i == j )
    return TRUE;

  if ( !push_args(a, dummy, dummy, 1) )
    return MEMORY_OVERFLOW;

  univ(node_orig(Node(i, buf)), &dm, &lm PASS_LD);
  univ(node_orig(Node(j, buf)), &dn, &ln PASS_LD);

  if ( dm != dn )
    return FALSE;

  if ( !push_args(a,  lm, ln, arityFunctor(dm)) )
    return MEMORY_OVERFLOW;

  while( next_arg(a, &l, &r) )
  { word wl, wr;
    if ( l == NULL )
      return TRUE;

  attvar:
    deRef(l);
    deRef(r);

    wl = *l;
    wr = *r;

    if ( tag(wl) != tag(wr) )
      return FALSE;

    if ( tag(wl) == TAG_VAR )
    { if ( l != r )		/* identity test on variables */
	return FALSE;
      continue;
    }

    if ( tag(wl) == TAG_ATTVAR )
    { l = valPAttVar(wl);
      r = valPAttVar(wr);
      goto attvar;
    }

    if ( wl == wr && !isTerm(wl) )
      continue;

    switch(tag(wl))
    { case TAG_ATOM:
	return FALSE;
      case TAG_INTEGER:
	if ( storage(wl) == STG_INLINE ||
	     storage(wr) == STG_INLINE )
	  return FALSE;
      case TAG_STRING:
      case TAG_FLOAT:
	if ( equalIndirect(wl, wr) )
	  continue;
        return FALSE;
      case TAG_COMPOUND:
      { Word lm, ln;
	word dm, dn;
	int i, j;
	node  *m,  *n;

	if ( (i = term_id(l, buf)) < 0 )
	  return MEMORY_OVERFLOW;
	i = Root(i, &m, buf);

	if ( (j = term_id(r, buf)) < 0 )
	  return MEMORY_OVERFLOW;
	j = Root(j, &n, buf);

	if ( i==j )
	  continue;

	univ(node_orig(m), &dm, &lm PASS_LD);
	univ(node_orig(n), &dn, &ln PASS_LD);

	if ( dm != dn )
	  return FALSE;

	if ( i <= j )
	  node_isom(m) = j;		/* union */
	else
	  node_isom(n) = i;

	if ( !push_args(a, lm, ln, arityFunctor(dm)) )
	  return MEMORY_OVERFLOW;

	continue;
      }
      default:
	assert(0);
    }
  }

  return TRUE;
}

/* t =@= u */
static int
variant(argPairs *agenda, Buffer buf ARG_LD)
{ Word l = NULL, r =NULL;

  while( next_arg(agenda, &l, &r) )
  { word wl, wr;

 attvar:
   deRef(l);
   deRef(r);

   wl = *l;
   wr = *r;

   if ( tag(wl) != tag(wr) )
     return FALSE;

   if ( tag(wl) == TAG_VAR )
   { int i, j, m, n;
     node *vl, *vr;

     if ((i = var_id(l, buf)) < 0)
       return MEMORY_OVERFLOW;
     if ((j = var_id(r, buf)) < 0)
       return MEMORY_OVERFLOW;

     vl = Node(i, buf);
     vr = Node(j, buf);

     m = vl->a;
     n = vr->b;

     if ( (m==0) && (n==0) )
     { vl->a = j;
       vr->b = i;
       continue;
     }
     if ( (m != 0) && (n != 0) )
     { if ( (m == j) && (n == i) )
	 continue;
     }
     return FALSE;
    }

    if ( tag(wl) == TAG_ATTVAR )
    { l = valPAttVar(wl);
      r = valPAttVar(wr);
      goto attvar;
    }

    if ( wl == wr && !isTerm(wl) )
      continue;

    switch(tag(wl))
    { case TAG_ATOM:
	return FALSE;
      case TAG_INTEGER:
	if ( storage(wl) == STG_INLINE ||
	     storage(wr) == STG_INLINE )
	  return FALSE;
      case TAG_STRING:
      case TAG_FLOAT:
	if ( equalIndirect(wl, wr) )
	  continue;
        return FALSE;
      case TAG_COMPOUND:
	{ int i, j, k, h;
	  node *m;

	  word dm, dn;			/* definition (= functor/arity) */
	  Word lm, ln;			/* arguments list */

	  if ( (i = term_id(l, buf)) < 0 )
	    return MEMORY_OVERFLOW;
	  if ( (j = term_id(r, buf)) < 0 )
	    return MEMORY_OVERFLOW;

	  m = Node(i, buf);
	  k = node_variant(m);

	  if ( 0 != k )
	  { if ( ( h = isomorphic(agenda, k, j, buf PASS_LD) ) <= 0 )
	      return  h;
	    continue;
	  }

	  univ(node_orig(m), &dm, &lm PASS_LD);
	  univ(node_orig(Node(j,buf)), &dn, &ln PASS_LD);

	  if ( dm != dn )
	    return FALSE;

	  node_variant(m) = j;

	  if ( !push_args(agenda, lm, ln, arityFunctor(dm)) )
	    return MEMORY_OVERFLOW;

	  continue;
	}
    }
  }

  return TRUE;
}


static
PRED_IMPL("=@=", 2, variant, 0)
{ PRED_LD
  argPairs agenda;
  tmp_buffer buf;
  Buffer VARIANT_BUFFER = (Buffer)&buf;
  bool rval;
  node *r;
  Word p1 = valTermRef(A1);
  Word p2 = valTermRef(A2);
  node new = {NULL, 0, 0, 0};   /* dummy node as 0-th element*/

  deRef(p1);
  deRef(p2);

  if ( *p1 == *p2 )                     /* same term */
    return TRUE;
  if ( tag(*p1) != tag(*p2) )           /* different type */
    return FALSE;
again:
  switch(tag(*p1))                      /* quick tests */
  { case TAG_VAR:
      return TRUE;
    case TAG_ATTVAR:
      p1 = valPAttVar(*p1);
      p2 = valPAttVar(*p2);
      goto again;
    case TAG_ATOM:
      return FALSE;
    case TAG_INTEGER:
      if ( !(isIndirect(*p1) && isIndirect(*p2)) )
        return FALSE;
      /*FALLTHROUGH*/
    case TAG_FLOAT:
    case TAG_STRING:
      return equalIndirect(*p1, *p2);
    case TAG_COMPOUND:
    { Functor t1 = valueTerm(*p1);
      Functor t2 = valueTerm(*p2);

      if ( t1->definition != t2->definition )
        return FALSE;
      break;
    }
    default:
      assert(0);
      return FALSE;
  }

  startCritical;
  initBuffer(&buf);	/* can be faster! */
  init_agenda(&agenda);

  if ( (add_node_buffer(VARIANT_BUFFER, &new) >= 0) &&
       (push_args(&agenda, p1, p2, 1) >=0) )
    rval = variant(&agenda, VARIANT_BUFFER PASS_LD);
  else
    rval = MEMORY_OVERFLOW;

  for(r = baseBuffer(VARIANT_BUFFER, node) + 1;
      r < topBuffer(VARIANT_BUFFER, node); r++ )
    reset_terms(r);

  discardBuffer(VARIANT_BUFFER);
  clearSegStack(&agenda.stack);

  DEBUG(CHK_SECURE, checkStacks(NULL));

  if ( !endCritical )
    return FALSE;

  if ( rval >= 0 )
    return rval;

  return PL_error(NULL, 0, NULL, ERR_NOMEM);
}


static
PRED_IMPL("\\=@=", 2, not_variant, 0)
{ return pl_variant2_va(PL__t0, PL__ac, PL__ctx) ? FALSE : TRUE;
}

		 /*******************************
		 *      PUBLISH PREDICATES	*
		 *******************************/

BeginPredDefs(variant)
  PRED_DEF("=@=", 2, variant, 0)
  PRED_DEF("\\=@=", 2, not_variant, 0)
EndPredDefs