/*---------------------------------------------------------------------------

  These are all the functions that have to do with TINS.

  They are for printing, creating, deleting, and unifying.

*/
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include "glob.h"


/*---------------------------------------------------------------------------
  print the term and all var bindings recursively (until depth is too much).
*/
#define DEEP 20

static int print2(lox *t,vars *v,int depth)
{
  if (t==NULL) return printf("<NULL>");

  switch (t->type) {
  case SKOL:
    printf("$%d",t->id);
    if (t->a != NULL) {
      printf("(");
      if (depth > DEEP) printf("<too deep>");
      else {
        t = t->a;
        while (1) {
          print2(t,v,depth+1);
          t = t->b;
          if (t==NULL) break;
          printf(",");
        }
      }
      printf(")");
    }
    break;
  case VAR:
    if (depth > DEEP) printf("<too deep>");
    else if (PrintTin(v->var[t->vc],depth+1))
      printf("%s",GetSymbol(t->id),t->vc);
    break;
  case TERM:
    printf("%s",GetSymbol(t->id));
    if (t->a != NULL) {
      printf("(");
      if (depth > DEEP) printf("<too deep>");
      else {
        t = t->a;
        while (1) {
          print2(t,v,depth+1);
          t = t->b;
          if (t==NULL) break;
          printf(",");
        }
      }
      printf(")");
    }
    break;
  default:
    printf("<type=%d>",t->type);
  }
  return 0;
}

/*---------------------------------------------------------------------------
  print the term and all var bindings recursively (until too much).
*/

int PrintTin(tin *t,int depth)
{
  if (t==NULL) return printf("<NULL>");

  while (t->st == NULL && t->nx != NULL) {   /* this is a chain */
    if (++depth > DEEP) {
      printf("<too deep>");
      return 0;
    }
    t = (tin *)t->nx;
  }

  if (t->st == NULL) return 1;
  print2(t->st,t->nx,depth+1);
  return 0;
}


static int dump2(lox *t,vars *v,int depth)
{
  if (t==NULL) return printf("<NULL>");

  switch (t->type) {
  case SKOL:
    printf("$%d",t->id);
    if (t->vc) printf("_%d",t->vc);
    if (t->a != NULL) {
      printf("(");
      if (depth > DEEP) printf("...");
      else {
        t = t->a;
        while (1) {
          dump2(t,v,depth+1);
          t = t->b;
          if (t==NULL) break;
          printf(",");
        }
      }
      printf(")");
    }
    break;
  case VAR:
    printf("%s_%d:",GetSymbol(t->id),t->vc);
    if (t->a != NULL) printf("?");
    if (depth > DEEP) printf("...");
    else DumpTin(v->var[t->vc],depth+1);
    break;
  case TERM:
    printf("%s",GetSymbol(t->id));
    if (t->vc) printf("_%d",t->vc);
    if (t->a != NULL) {
      printf("(");
      if (depth > DEEP) printf("...");
      else {
        t = t->a;
        while (1) {
          dump2(t,v,depth+1);
          t = t->b;
          if (t==NULL) break;
          printf(",");
        }
      }
      printf(")");
    }
    break;
  default:
    printf("<type=%d>",t->type);
  }
  return 0;
}

/*---------------------------------------------------------------------------
  print the term and all var bindings recursively (until too much).
*/

int DumpTin(tin *t,int depth)
{
  if (t==NULL) return printf("<NULL>");

  while (t->st == NULL && t->nx != NULL) {   /* this is a chain */
    if (++depth > DEEP) return printf("...too deep");
    printf(":");
    t = (tin *)t->nx;
  }

  if (t->st == NULL) printf("free:%p",t);
  else dump2(t->st,t->nx,depth+1);
  return 0;
}


/*---------------------------------------------------------------------------
  new tin
*/
tin *NewTin(lox *st)
{
  tin *t;

  t = malloc(sizeof(tin));
  if (t==NULL) eprintf("Alloc error in new-tin.",0,0,0);
  t->nx = NULL;
  t->st = st;
  t->copy = NULL;
  return t;
}

/*---------------------------------------------------------------------------
  new vars (for a tin)
*/
vars *NewVars(int size)
{
  vars *v;
  int i;

  v = malloc(sizeof(vars)+sizeof(tin*)*size);
  if (v==NULL) eprintf("Alloc error in new-vars.",0,0,0);
  for (i=0; i<size; ++i) v->var[i] = NULL;
  v->copy = NULL;
  return v;
}

/*---------------------------------------------------------------------------
  copy vars, recursively using the copy field
*/
static vars *CopyVars(vars *t,int size)
{
  vars *u;
  int i;

  if (t==NULL) return t;
  if (t->copy == NULL) {
    t->copy = u = NewVars(size);
    for (i=0; i<size; ++i)
      u->var[i] = CopyTin(t->var[i]);
  }
  return t->copy;
}

/*---------------------------------------------------------------------------
  this finds the end of a tin-chain.
*/
static tin *findend(tin *t)
{
  while (t->st == NULL && t->nx != NULL)      /* follow the chain */
    t = (tin*)t->nx;
  return t;
}

/*---------------------------------------------------------------------------
  returns 1 if t is a free variable tin
*/
#define isfree(t) (t->st == NULL && t->nx == NULL)

/*---------------------------------------------------------------------------
  copy tin, recursively using the copy field.
  if t is a chain, do chain shortening.
*/
tin *CopyTin(tin *t)
{
  tin *u;

  if (t==NULL) return t;
  t = findend(t);
  if (t->copy == NULL) {
    t->copy = u = NewTin(t->st);
    if (t->st != NULL)                    /* is this bound? */
      u->nx = CopyVars(t->nx,t->st->vc);
  }
  return t->copy;
}

/*---------------------------------------------------------------------------
  Set the copy pointer in the vars to NULL
*/
int ClearCopy2(vars *t,int size)
{
  int i;

  if (t==NULL) return 0;
  if (t->copy != NULL) {
    t->copy = NULL;
    for (i=0; i<size; ++i)
      ClearCopy(t->var[i]);
  }
  return 0;
}

/*---------------------------------------------------------------------------
  Set the copy pointer in the tin to NULL
*/
int ClearCopy(tin *t)
{
  if (t==NULL) return 0;
  while (t->st == NULL && t->nx != NULL) {
    t->copy = NULL;
    t = (tin*)t->nx;
  }
  if (t->copy != NULL) {
    t->copy = NULL;
    if (t->st != NULL) ClearCopy2(t->nx,t->st->vc);
  }
  return 0;
}

/*---------------------------------------------------------------------------
  Delete a tin and all its variables.  Only the tin, its variables, and the
  thing the variables points to are released.  (2 levels deep )
  This is based on two assumptions:
  1. Only tins pointing to predicates have their own vars list.
  2. A variable is never bound to a tin pointing to a predicate.
  This routine still has a problem:  When a var is shared in multiple tins
  (in the same clause) then it gets freed twice.
*/
int DeleteTin(tin *t)
{
  vars *v;
  int i;

  if (t==NULL || t->st==NULL || t->nx==NULL) {
    eprintf("Invalid tin in delete-tin.",0,0,0);
    return 1;
  }
  v = t->nx;
  for (i=0; i<t->st->vc; ++i) {
 /*   free(v->var[i]);     this will cause an error on some systems */
    v->var[i] = NULL;
  }
  t->nx = NULL;
  t->st = NULL;
  free(v);
  free(t);
  return 0;
}

/*---------------------------------------------------------------------------
  These are some data structures local to the unification functions for
  managing the changes list.
*/
#define CHLCHK 8
static tin **chglist = NULL;
static int numchg = 0;

/*---------------------------------------------------------------------------
  This reset the change list so that the unify-ununify procedures work
  in sync.
*/
int InitUnify(void)
{
  if (numchg) free(chglist);
  chglist = NULL;
  numchg = 0;
  return 0;
}

/*---------------------------------------------------------------------------
  this binds a var and makes an entry in the chglist.
*/
int bindvar(tin *t,lox *st,vars *nx)
{
  if ((numchg % CHLCHK)==0)          /* time to grow. */
    chglist = realloc(chglist,(numchg+CHLCHK)*sizeof(*chglist));
  if (chglist==NULL) {
    eprintf("Error null chglist in bindvar.",0,0,0);
    return 1;
  }
  chglist[numchg++] = t;
  t->st = st;
  t->nx = nx;
  return 0;
}

#define chknul(fv) \
  if (fv==NULL) {                                            \
    eprintf("Error, null varlist found in unify-2.",0,0,0);  \
    return 4;                                                \
  }

static int moc = 1;
/*---------------------------------------------------------------------------
  occurs check,
*/
int occurs(tin *t,lox *st,vars *v,int depth)
{
  tin *u;

  if (!depth) return 0;
  if (st==NULL || v==NULL) return 0;
  if (st->type==VAR) {
    u = findend(v->var[st->vc]);
    if (u == t) return 1;
    return occurs(t,u->st,u->nx,depth-1);
  }
  st = st->a;
  while (st != NULL) {
    if (occurs(t,st,v,depth)) return 1;
    st = st->b;
  }
  return 0;
}

/*---------------------------------------------------------------------------
  this is the recursive part of unify.
*/
int unif2(lox *f, vars *fv, lox *g, vars *gv)
{
  int rc;
  tin *ft,*gt;

  if (f==NULL && g==NULL) return 0;
  if (f==NULL) return 4;
  if (g==NULL) return 4;

  if (f->type==VAR && g->type==VAR) {  /* See if both are vars */
    chknul(fv);
    chknul(gv);
    ft = findend(fv->var[f->vc]);
    gt = findend(gv->var[g->vc]);
    if (ft == gt)
      rc = 0;
    else if (isfree(ft)) {
      rc = 1;
      if (occurs(ft,gt->st,gt->nx,moc)) rc = 4;
      else bindvar(ft,NULL,(vars *)gt);
    }
    else if (isfree(gt)) {
      rc = 2;
      if (occurs(gt,ft->st,ft->nx,moc)) rc = 4;
      else bindvar(gt,NULL,(vars *)ft);
    }
    else rc = unif2(ft->st,ft->nx,gt->st,gt->nx);
  }
  else if (f->type==VAR) {         /* See if f is a var and g is not */
    chknul(fv);
    ft = findend(fv->var[f->vc]);
    if (isfree(ft)) {
      rc = 1;
      if (occurs(ft,g,gv,moc)) rc = 4;
      else bindvar(ft,g,gv);
    }
    else rc = unif2(ft->st,ft->nx,g,gv);
  }
  else if (g->type==VAR) {         /* See if g is a var and f is not */
    chknul(gv);
    gt = findend(gv->var[g->vc]);
    if (isfree(gt)) {
      rc = 2;
      if (occurs(gt,f,fv,moc)) rc = 4;
      else bindvar(gt,f,fv);
    }
    else rc = unif2(f,fv,gt->st,gt->nx);
  }
  else {                           /* Neither one is a var */
    if (f->type!=g->type || f->id!=g->id)
      rc = 4;
    else {
      rc = 0;
      f = f->a;
      g = g->a;
      while (1) {
        rc |= unif2(f,fv,g,gv);
        if (rc > 3 || f==NULL || g==NULL) break;
        f = f->b;
        g = g->b;
      }
    }
  }
  return rc;
}

/*---------------------------------------------------------------------------
  Unification.  This tries to unify t1 t2.  If success, returns less than 4
  depending on what variables were bound 0=none were bound, 1=vars in t1 only,
  2=in t2 only, 3=in both.  The tins are changed and a changes list is
  kept so you can un-unify.  On fail returns 4..7.  Un-unify should be called
  even on a failure.  This will try to bind vars in t1 first.
*/
int Unify(tin *t1, tin *t2,int occur)
{
  if (t1==NULL || t2==NULL) {
    eprintf("Invalid tin in unify.",0,0,0);
    return 0;
  }
  t1 = findend(t1);
  t2 = findend(t2);
  moc = occur;
  return unif2(t1->st,t1->nx,t2->st,t2->nx);
}

/*---------------------------------------------------------------------------
  this undoes the effects of all unifications since the last undo or init.
  it uses the chglist.
*/
int Ununify(void)
{
  int i;

  for (i=0; i<numchg; ++i) {
    chglist[i]->st = NULL;            /* make it a free var */
    chglist[i]->nx = NULL;
  }
  InitUnify();
  return 0;
}