/* ----------------------------------------------------------
%   (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
==================================================================== */
/*--------------------------------------------------------------------
*		<<<< refute.c >>>>
*		Prolog refutation
--------------------------------------------------------------------*/

#include "include.h"
#include <signal.h>

#define is_dead(n) (n->n_set == NULL)
#define is_tip(n)  (n->n_clause == NULL)
#define is_root(n) (n->n_link == NULL)

struct node *Psolution(), *extend(), *proceed_node();
struct node *Newnode(),*backtrack_node();
struct set *init_set();
void Trace_True(),Trace_False(),Trace_Unification(),Trace_Answer();
void Trace_True2(), Trace_False2();
int Trace_Goal();
void Pbinding();
/*
[refute]-----------------------------------
.   backtrack_node
.   .   Trace_False2
.   Trace_False	
.   Trace_Goal	
.   .   print_ancestors+
.   Trace_True	
.   is_dead.	
.   extend	
.   .   [system_function]
.   .   init_set
.   .   resolve+	
.   .   .   [tunify]
.   .   .   Trace_Unification
.   is_tip.	
.   proceed_node
.   .   Trace_True2.
.   .   next_goal+
.   .   have_nextgoal+
*/

/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++
  Prolog refutation entry
+++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int refute(Root,n,Status)
struct node *Root, *n;
int Status;			/* UP,DOWN,BACKTRACK */
{
  struct node *m;

  while(1)
    {
      if (n == NULL || n->n_spy)
	  if (Trace_Goal(n)==FALSE) return(FALSE);
      m = extend(n, Status);
      if (!is_dead(n)) Last_BT = n;
      if (m == NULL_NODE)	/* fail */
	{
	  if (n->n_spy) Trace_False(n);
	  if (n == Root) return(FALSE);
	  Status = BACKTRACK;
	  Last_BT = n = backtrack_node(n->n_last);
	}
      else if (is_tip(m)) /* nil clause */
	{
	  if (n->n_spy) Trace_True(n);
	  Status = UP;
	  n = proceed_node(m,Last_BT);
	  if (n == NULL_NODE) return(TRUE);
	}
      else {
	Status = DOWN; 
	n = m;
      }
    }
}

/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++
  head unification
+++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct node *extend(n, status) /* extend goal */
struct node *n;
int status;
{
	register struct term *sliteral;	/* selected literal */
	struct node *m;
	register struct pair *p,*env;

	if (n->n_count > Refcount) {
		tprint1("  <<%d] fail! (over refute counter)\n",n->n_count);
		return(NULL); /* counter over = fail */
	}
	if (is_tip(n)) return(n); /* no goal */
	sliteral = n->n_clause->c_form;
	env = n->n_env;
	down(p,sliteral,env);
	if (p != NULL) return(NULL); /* goal is real var */
	m = Newnode(NULL_CL,n->n_constraint,
		    NULL_ENV,n,n);
	if (is_funcsys(sliteral->type.t_func)) /* functional syspred */
	{
		if (system_function(sliteral, env, n) == SYSFAIL)
			return(NULL);
		else {
		  n->n_set = (struct set *)NULL;
		  return(m);
		}
	}
	if (is_nofuncsys(sliteral->type.t_func)) /* sys pred.  */
	{
		if (system_pred(sliteral, env, n, m, status) == SYSFAIL) 
			return(NULL);
		else {
		  return(m);
		}
		/* n->n_set may be DUMMY_DEF */
	}
	if (is_dead(n)) return(NULL);
	if (resolve(n, m, sliteral, env) == FALSE) 
		return(NULL); /* user pred.: resolution */
	m->n_usp = usp;
	m->n_hp = hp;
	m->n_ep = ep;
	m->n_set = init_set(m);
	return(m);
}


int resolve(n0, n, sliteral, env) /* resolution: called by extend() */
struct node *n0,*n;
struct term *sliteral;
struct pair *env;
{
  struct ustack *usave;
  int *hsave,tunify_apply();
  struct pair *esave;
  register struct set *s;
  register struct eclause *ec;
  
  usave = usp;hsave = hp;esave = ep;
  STAT_REFUTE++;		/* statistics */
  for (s = n0->n_set; s != NULL; s = s->s_link)
    {
	if (s->s_ground_head)	/* no variable/PST in the head */
	{
	    if (tunify(sliteral, env, s->s_clause->c_form, 
		       NULL_ENV,0) == FALSE)
	    {
		STAT_BACKTRACK_SHAL++; /* statistics */
		hp = hsave;	ep = esave;
		continue;
	    }
	    if (s->s_anumber > 0)
		n->n_env = Nenv((int)s->s_anumber);	/* body environment */
	}
	else
	{
	    if (s->s_anumber > 0) 
		n->n_env = Nenv((int)s->s_anumber);	/* head&body env */
	    if (tunify_apply(sliteral, env, 
			     s->s_clause->c_form, n->n_env,0) == FALSE){
		/* undo(usave); */
		hp = hsave;	ep = esave;
		STAT_BACKTRACK_SHAL++; /* statistics */
		continue;
	    }
	}
	ec = transform(n0->n_constraint, s->s_constraint, n->n_env);
	if (ec == (struct eclause *)MFAIL) {
	/* constraint transformation failure */
	    undo(usave);hp = hsave;	ep = esave;
	    continue;
	}
      n->n_constraint = ec;
	n0->n_scount++;
	if (n->n_spy) Trace_Unification(n0,s);
      n0->n_set = s->s_link;
      n->n_clause = s->s_clause->c_link;
      return(TRUE);
    }
  return(FALSE);
}

/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++
    make and process node
+++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct node *Newnode(goal, icons, env, nlink, nlast)
struct clause *goal;
struct eclause *icons;
struct pair *env;
struct node *nlink, *nlast;
{
	register struct node *n;

	n = new(node);
	n->n_last = nlast;	/* backtrack node */
	n->n_link = nlink;	/* mother node */
	n->n_clause = goal;	/* goal */
	n->n_env = env;
	n->n_hp = hp;
	n->n_ep = ep;
	n->n_usp = usp;
	if (nlink == NULL_NODE) n->n_count = 0;
	else n->n_count = nlink->n_count + 1;
	n->n_tmp = 0;		
	n->n_scount = 0;
	n->n_constraint = icons;
	if (goal == NULL_CL) {
	    n->n_set = (struct set *)NULL;
	    n->n_spy = 0;
	}
	else
	    n->n_set = init_set(n);
	return(n);
}

struct set *init_set(n)
register struct node *n;
{
	register struct term *t;
	register struct func *f;
	register struct pair *e,*p;
	register struct set *s;	

	if (n->n_clause == NULL_CL) return((struct set *)NULL);
        t = n->n_clause->c_form;
	e = n->n_env;
	down(p,t,e);
	if (p != NULL) return(NULL); /* goal is var */
	f = t->type.t_func;
	n->n_spy = Is_Trace && isspy(f);
	if (isuser(f)) {
	  if (((s = f->def.f_set) == (struct set *)NULL)
	      && (Handle_Undefined == TRUE)) {
	    sprintf(nbuf,">>> %s <<< is UNDEFINED!",f->f_name);
	    error(nbuf);
	  }
	  else return(s);
	}
	else return((struct set *)NULL);
}


struct node *backtrack_node(n)	/* restore stack, heap */
struct node *n;
{
	if (usp > Stack_Max) Stack_Max = usp; 
	if (chp > Cheap_Max) Cheap_Max = chp;
	if (hp > Heap_Max) Heap_Max = hp; 
	if (ep > Esp_Max) Esp_Max = ep; 
	STAT_BACKTRACK_DEEP++;	/* statistics */

  while (n != NULL_NODE)
    {
      if (n->n_spy) Trace_False2(n);
      if(! is_dead(n)) {
	undo(n->n_usp);
	hp = n->n_hp;
	ep = n->n_ep;
	return(n);
      }
      n = n->n_last;
    }
  return(NULL_NODE);
}
	
struct node *proceed_node(n,btnode)
struct node *n,*btnode;
{
	register struct node *m;
	int have_nextgoal();
	struct node *next_goal();
	
	for (m = n; m != NULL; m = m->n_link)
	{
	  if (m->n_spy) Trace_True2(m);
	  if (have_nextgoal(m->n_clause)) 
	    return(next_goal(m,n,btnode));
	}
	return(NULL_NODE);
}

int have_nextgoal(c)		/* called by proceed_node() */
register struct clause *c;
{
    if (c != NULL_CL && c->c_link != NULL_CL) return(TRUE);
    else return(FALSE);
}

struct node *next_goal(m,oldnode,btnode) /* called by proceed_node() */
struct node *m, *oldnode,*btnode;
{
	struct node *n;
	
	n = Newnode(m->n_clause->c_link, oldnode->n_constraint, 
		    m->n_env, m->n_link, btnode);
	n->n_count = oldnode->n_count +1;
	return(n);
}

/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++
  print answer & binding
+++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int Panswer(root, vlist)	/* print solution */
struct node *root;
struct term *vlist;
{
  if (!Is_Notrace) Trace_Answer(root);
  Pbinding(vlist, root->n_env);
  if (root->n_constraint != NULL_ECL) {
    tprint0("\n where ");
     Peclause(root->n_constraint);
  }

  if (Last_BT == NULL) {
    tprint0("\n");
    return(FALSE); /* no backtrack point */
  }
  if ((fp != stdin) || (!keyread(';')))
    return(FALSE);	
  return(TRUE);	/* more solution */
}

void Pbinding(vlist, env)	/* print var binding */
struct term *vlist;
struct pair *env;
{
	if (vlist == NULL_TERM) return;
	Pbinding(vlink(vlist),env);
	if ((strcmp(vname(vlist),"_") == 0) ||
	    (vlist->type.ident == VAR_PST_TYPE)) return;
	tprint1("  %s = ",vname(vlist));
	Pterm(vlist,env);
}

/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++
  trace ---  interaction with user
+++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int Trace_Goal(n)
	struct node *n;
{
   void print_ancestors();

   if (n == NULL) return(FALSE);
   if (Is_Notrace) return(TRUE);
   if (Last_SKIP == n) Last_SKIP = NULL_NODE;
   if (Last_SKIP != NULL_NODE) return(TRUE);
   tprint1(" [%d>>",n->n_count);
   Pgoal(n);
   if ((Is_Steptrace) || (Is_Leap && (n->n_spy)))
   {
	   Steptrace_mode;
	   while(1) {
		tprint0("  #<trace ?>");
		switch (getchar()) {
		  case 'a' :
		  case 'A' : print_ancestors(n); getchar(); break;
		  case 'b' :
		  case 'B' : {
		  	int  *hsave;
			struct pair *esave;
			struct ustack *usave = utop;
		  	hsave = hp; esave = ep;
		  	utop = usp; 
		  	if (setjmp(unbreak_reset)) {
		  		utop = usave; hp = hsave; ep = esave;
		  		break;
		  	  }
		  	while(1) {
		  	  prolog_execution();
			}
		      }
		  case 'z' :
		  case 'Z' :
		  case 'q' :
		  case 'Q' : NL; tprint0("\n Execution Abort \n");
		    longjmp(reset,0);
		  case '?' :
		  case 'h' :
		  case 'H' :
   tprint0("\na : ancestors\tb : break\th : help\tl : leap\ts : skip\n");
   tprint0("<cr> : next\tq: abort\tf : fail return\n");
		   getchar(); break;
		  case 'f' :
		  case 'F' : return(FALSE);
		  case 'l' :
		  case 'L' : tflag = 3; return(TRUE);
		  case 's' :
		  case 'S' : Last_SKIP = n; return(TRUE);
		  default :  Last_SKIP = NULL_NODE; return(TRUE);
		  }
	      }
       }
	else NL; return(TRUE);
 }

void Trace_False(n)
struct node *n;
{
	struct func *f;
	struct pair *p, *e;
	struct term *t;

	if (Is_Leap) Steptrace_mode;
	if (Last_SKIP == n) Last_SKIP = NULL_NODE;
	if (Last_SKIP != NULL_NODE) return;
	t = n->n_clause->c_form;
	if (isvar(t)) {
	  e = n->n_env;
	  down(p,t,e);
	}
	f = t->type.t_func;
	if (is_funcsys(f))
	{
		tprint2("  <<%d] false (%s)\n",n->n_count,f->f_name);
	}
	else if (is_nofuncsys(f))
	{
		tprint2("  <<%d] fail (%s)\n",n->n_count,f->f_name);
	}
	else			/* user pred */
	{
		tprint2("   <=%d-no= fail %s.\n",n->n_count,f->f_name);
	}
}

void Trace_True(n)
struct node *n;
{
	struct func *f;
	struct term *t;
	struct pair *p, *e;

	if (Is_Leap) Steptrace_mode;
	if (Last_SKIP == n) Last_SKIP = NULL_NODE;
	if (Last_SKIP != NULL_NODE) return;
	t = n->n_clause->c_form;
	e = n->n_env;
	down(p,t,e);
	f = t->type.t_func;
	if (isuser(f)) return;
	tprint1("  <<%d] ",n->n_count);	
	if (is_funcsys(f))
	{
		tprint1("true (%s)\n",f->f_name);
	}
	else 
	{
		tprint1("success (%s)\n",f->f_name);
	}
}

void Trace_False2(n)
struct node *n;
{
	if (Is_Leap) Steptrace_mode;
	if (Last_SKIP == n){
		tprint1("  <<%d] fail\n",n->n_count);
		Last_SKIP = NULL_NODE;
	}
}

void Trace_True2(n)
struct node *n;
{
	if (Last_SKIP == n){
		/* tprint1("  <<%d] true",n->n_count); */
		Last_SKIP = NULL_NODE;
	}
}

void Trace_Unification(n,s)
struct node *n;
struct set *s;
{
	if (Is_Leap) Steptrace_mode;
	if (Last_SKIP != NULL_NODE) return;
	tprint2("   <=%d-%d=",n->n_count, n->n_scount);
	Showhorn(s->s_clause, s->s_constraint, NULL_ENV);
	NL;
}

void Trace_Answer(root)
struct node *root;
{
	Last_SKIP = NULL_NODE;
	tprint0("success.\n");
	Pclause(root->n_clause, root->n_env);
	if (root->n_constraint != NULL_ECL) {
		tprint0(" ; ");
		Peclause(root->n_constraint);
	}
	NL;
}

void print_ancestors(n)		/* called by Trace_goal() */
struct node *n;
{
   while (n != NULL) {
     tprint1(" [%d>>",n->n_count); Pgoal(n); NL;
     n = n->n_link;
     }
 }