/* ----------------------------------------------------------
%   (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
==================================================================== */
/*--------------------------------------------------------------------
*             << mainsub.c >>
*		system command etc.
*         1993.7.30   freeheap()
*         1993.8.3    calc_component(), recalc_component() sppedup
*         1994.6.28   component functions. speedup
*         1994.9.27   show statistics
*         1994.10.25   debug: set_head_component
--------------------------------------------------------------------*/

#include "include.h"

void putcursor () {
    if (Is_Notrace) {		/* trace off */
	tputc ('_');
    }
    else
	if (Is_Normaltrace) {	/*  trace on */
	    tputc ('$');
	}
	else
	    tputc ('>');	/*  step trace on */
}


void traceswitch () {
    if (Is_Normaltrace) {
	Notrace_mode;
	tprint0 ("\n +++ normal trace off +++\n");
    }
    else {
	Normaltrace_mode;
	tprint0 ("\n +++ normal trace on +++\n");
    }
}

void stepswitch () {
    if (Is_Steptrace) {
	Notrace_mode;
	tprint0 ("\n +++ step trace off +++\n");
    }
    else {
	Steptrace_mode;
	tprint0 ("\n +++ step trace on +++\n");
    }
}

int decode_pname(fname)		/* 'member/2' --> 'member', return 2 */
char *fname;
{
	for (; *fname != '\0'; fname++)
		if (*fname == '/') {
			*fname = '\0';
			return(atoi(fname + 1));
		}
	return(-1);
}

void spyswitch (fname)
char   *fname;
{
    struct func *f;
    int i,arity;

    if (strcmp (fname, "*") == 0) {
	tprint0 ("--- set all spy flag ---");
	NL;
	allspy(1);		/* set all spy flag */
	return;
    }
    if (strcmp (fname, ".") == 0) {
	tprint0 ("--- reset all spy flag ---");
	NL;
	allspy(0);		/* reset all spy flag */
	return;
    }
    if (strcmp (fname, "?") == 0) {/* list spyed predicates */
	tprint0 ("+++ list spyed predicates +++\n");
	for (i=0; i < HASH_SIZE; i++)
	  for (f = hash_list[i]; f != NULL; f = f -> f_link) {
	    if isspy(f) tprint2 ("%s(%u)  ", f -> f_name, f -> f_arity);
	}
	NL;
	return;
    }
    if (strcmp (fname, ">") == 0) /* spy fold/unfold */
    {
	    tprint0(" +++ ");
	    if  isspy(MODULAR_P) tprint0("no");
	    tprint0("spy fold/unfold transformation \n");
	    spychange(MODULAR_P);
	    spychange(INTEG_P);
	    return;
    }
    arity = decode_pname(fname);
    if (!exist_fname(fname))
    {
	    tprint1(" '%s' does not exist.\n", fname);
	    return;
    }
    if (arity == -1)		/* spy switch fname/?? */
    {
	    for(f = hash_list[hash(fname)]; f != NULL; f = f->f_link)
		    if (streq(fname,f->f_name)) {
			    tprint0 ("+++ ");
			    if isspy(f) tprint0 ("no");
			    tprint2("spy %s/%d\n", f->f_name, f->f_arity);
			    spychange(f);
		    }
    }
    else 
    {
	    f = funcsearch(fname, arity);
	    if (f != NULL) {
		    tprint0 (" +++");
		    if isspy(f) tprint0 ("no");
		    tprint2("spy %s/%d\n", f->f_name,f->f_arity);
		    spychange(f);		/*  switch spy flag on/off */
	    }
	    else 
		    tprint2(" '%s/%d' does not exist.\n", fname,arity);
    }
}

void allspy (n)	 /* if n == 1: set all spy flag, else resetall flag */
int     n;
{
    struct func *f;
    int i;

    if (n == 1)
    {
	    for (i = 0; i < HASH_SIZE; i++)
		    for (f = hash_list[i]; f != NULL; f = f -> f_link)
			    spyfun(f);
    }
    else
    {
	    for (i = 0; i < HASH_SIZE; i++)
		    for (f = hash_list[i]; f != NULL; f = f -> f_link)
			    nospyfun(f);
    }
}

void show_pred_roles(f)		/* show component */
struct func *f;
{
  int i, arity;
  struct component *cm;
  register struct component *c;

  for (i = 0, arity = f->f_arity; i < arity ; i++) {
	  cm = Component(f,i);
	  if (cm == NULL) {
		  tprint0("_");
	  }
	  else 
	  {
		  for (c = cm; c != NULL; c = c->c_next)
		  {
			  if (c->c_label == NULL) {
				  tprint0("+");
			  }
			  else {
				  tprint1("%s",c->c_label->f_name);
			  }
			  if (c->c_next == NULL) break;
			  else 
			  {
				  tprint0(".");
			  }
		  }
	  }
	  if (i == (arity -1)) return;
	  else 
	  {
		  tprint0("|");
	  }
  }
}

/* the number of pred names printed in one line */
#define PRED_IN_LINE 5

void show_syspred_name()
{
	int i, j = 0;
	register struct func *f;

	tprint0("   +------<system>---------[ +:recursive, ^:functor ]--\n");
	for (i = 0; i < HASH_SIZE; i++)	/* print system predicates */
	for (f = hash_list[i]; f != NULL; f = f -> f_link)
	    if issystem(f) {
	      tprint2 ("%s/%u", f -> f_name, f -> f_arity);
	      if isrecursive(f) tprint0 ("+");
	      if (f->def.f_sysfunc == NULL) tprint0("^");
	      tputc('\t');
	      if (++j >= PRED_IN_LINE) {j = 0; NL;}
	    };
	NL;
}

void show_userpred_name()
{
	int i, j = 0;
	register struct func *f;

	tprint0("   +-------<user>------");
	tprint0("--[ *:spy, -:reduced, +:recursive, #:new ]--\n");
	for (i = 0; i < HASH_SIZE; i++)	/* print user predicates */
		for (f = hash_list[i]; f != NULL; f = f -> f_link) {
/*			if (f->f_arity < 0) continue; */
			if (f->def.f_sysfunc == NULL) 
				continue;	/* cut constant. */
			if issystem(f) continue;
			tprint2 ("%s/%u", f -> f_name, f -> f_arity);
			if isspy(f) tprint0 ("*");
			if isreduced(f) tprint0 ("-");
			if isrecursive(f) tprint0 ("+");
			if isnewpred(f) tprint0("#");
			tputc('\t');
			if (++j >= PRED_IN_LINE) {j = 0; NL;}
		}
	NL;
}

void show_syspred_status(f)
struct func *f;
{
  tprint0("--<system>---[");
  show_pred_roles(f);
  tprint1("]--<%s>---+\n",
	  ((is_funcsys(f)) ? "functional" : "multi-valued"));
}		
	
void show_pred_def(f)		/* show def of each pred */
struct func *f;
{
  void show_pred_roles();

	if (f->def.f_set == NULL) return; /* constant */
	tprint2 (" +--------( %s/%u )-----", f->f_name, f->f_arity);
	if issystem(f)
	{
		show_syspred_status(f);
		return;
	}
	if is_nofuncsys(f)
	{
		tprint0("--<system>---<multi-valued>-+\n");
		return;
	}
	if isspy(f) tprint0 ("-<spy>-");
	if isreduced(f) tprint0 ("-<reduced>-");
	if isrecursive(f) tprint0("-<recursive>-");
	if isnewpred(f) tprint0("-<new>-");
	tprint0("["); show_pred_roles(f);
	tprint2("]--%d/%d--+\n",f->f_unitcount,f->f_setcount); 
	if (f -> f_integ != NULL) {
	    tprint0 ("<def> ");
	    P_dclause (f -> f_integ -> it_clause,NULL_ENV);
	    NL; NL;
	}
	Showfunc(f);
}
	
void showdef (fname)		/* list definition   (%d command)   */
char   *fname;
{
    register struct func *f;
    int i,arity;

    check_recursion();
    if (streq(fname, "/")) {
	tprint0 (" +-- List all predicates ---+ \n");
	for (i = 0; i < HASH_SIZE; i++)
		for (f = hash_list[i]; f != NULL; f = f -> f_link)
			Showfunc (f);
	return;
    }
    if (streq(fname, "*")){
	tprint0 (" +-- List predicates ---+ \n")
	for ( i=0; i < HASH_SIZE; i++)
	    for (f = hash_list[i]; f != NULL; f = f -> f_link) {
	    if isnoreduced(f) Showfunc (f);
	}
	return;
    }
    if (streq(fname, "?")){
	    show_syspred_name();
	    show_userpred_name();
	    return;
    }
    if (streq(fname, "-"))
    {
	    show_userpred_name();
	    return;
    }
    arity = decode_pname(fname);
    if (exist_fname(fname) == NULL) { 
	    tprint1 ("'%s' does not exist.\n", fname);
	    return;
    }
    if (arity == -1)		/* show fname/?? */
    {
	    for (f =  hash_list[hash(fname)]; f != NULL; f = f->f_link)
		    if (streq(f->f_name,fname))
			    show_pred_def(f);
    }
    else
    {
	    f = funcsearch(fname,arity);
	    if (f != NULL)
		    show_pred_def(f);
	    else
		    tprint2("'%s/%d' does not exist.\n",fname,arity);
    }
}

void loghandle (fname)		/* log file	(%l command) */
char   *fname;
{
    if (strcmp (fname, "no") == 0) {
	tprint0 ("===  log stop  === \n");
	if (lfp != NULL)
	    fclose (lfp);
	lfp = NULL;
	strcpy (logfile, "no");
    }
    else
	if ((fopen (fname, "r")) != NULL) {
	    tprint1 ("'%s' : already exist \n", fname);
	}
	else
	    if ((fopen (fname, "w")) == NULL) {
		tprint1 (" '%s' : can't open \n", fname);
	    }
	    else {
		if (lfp != NULL) {
		    fclose (lfp);
		    tprint1 (" == %s : close ==\n", logfile);
		}
		lfp = fopen (fname, "w");
		tprint1 (" log file '%s' \n", fname);
		strcpy (logfile, fname);
	    }
}


void helpmenu () {		/* on-line help */
  tprint0 ("\t%%h\t: help\t\t\t%%Q : quit \n");
  tprint0 ("\t# <OS command>: OS command interpreter \n");
  tprint0 ("\t%%d <predicate name>: list definition\n");
	tprint0 ("\t\t%%d* %%d/: list all   %%d?: list names   %%d-: user pred\n");
  tprint2 ("\t%c <file name> %c: consult file (no echo)\n", '"', '"');
  tprint1 ("\t%c <file name> ?: consult file (with echo)\n", '"');
  tprint1 ("\t%%l <file name>: set log file ['%s']\n", logfile);
  tprint0 ("\t%%w <file name>: save program\n");
  tprint0 ("\t%%p <predicate name>: spy switch\n");
	tprint0 ("\t\t%%p*:spy all\t%%p.:nospy all\t%%p?:list spyed preds.\n");
  tprint1 ("\t%%t\t: normal trace switch [%s]\n",
	((Is_Normaltrace) ? "on" : "off"));
  tprint1 ("\t%%s\t: step trace switch [%s]\n",
	((Is_Steptrace) ? "on" : "off"));
  tprint0 ("\t%%a\t: all modular mode ");
	if (Is_Modular) tprint0(" <=now");
  tprint0 ("\n\t%%o\t: M-Solvable mode ");
	if (Is_Msolvable) tprint0(" <=now\n")
	else NL;
  tprint1 ("\t%%c <number>: max number of refutation node [%u]\n",
	     Refcount);
  tprint0 ("\t%%n <name>\t: new predicate name ");
    tprint1 ("['%s']\n", genname);
  tprint0 ("\t%%L\t: list new predicate definitions\n");
  tprint0 ("\t%%f\t: show the system heap size\n");
  tprint0 ("\t%%C [Feature,type,... ]. : set cat() functor\n");
  tprint0 ("\t\t ==> ");show_category();NL;
  tprint0 ("\t%%G\t: Garbage Collection \n");
  tprint1 ("\t%%D <number> : Max Depth of Printing, now is %d\n", Print_Depth);
  tprint1 ("\t%%u\t: Undefined Predicate Handling Switch [%s]\n",
	((Handle_Undefined == TRUE) ? "ERROR" : "FAIL"));
  tprint1("\t%%M <number> : Max number of Variables in Transformation[%u]\n",
	MODULARMAX);
  tprint0 ("\t%%P <predicate name>: Preprocess Constraints\n");
  tprint0 ("\t\t%%P*: preprocess all\t%%P?: predicates with nonmodular\n");
  tprint0 ("\t%%R\t: system Reset \n");
  tprint0 ("\t%%S\t: show statistics of the previous question.\n");
}

void freeheap () {		/* print shp status */
    tprint3 ("\npermanent data area:\n\tSystem_heap : %d%%(%d/%dK)  ",
	     (int)(100 * (shp - sheap) *SHEAP_UNIT / SHEAP_SIZE),
	     ((int)(shp-sheap)*SHEAP_UNIT/1000),(int)(SHEAP_SIZE/1000));
    tprint3 ("Name_heap : %d%%(%d/%dK)\n",
	     (int)(100 * (nhp - nheap) * NAME_UNIT / NAME_SIZE),
	     (int)((nhp-nheap)*NAME_UNIT/1000),(int)(NAME_SIZE/1000));
	show_heap_max();
}

void show_heap_max()			/* for debug */
{
	tprint0("temporal data area (max. used)\n\t");
	tprint3 ("Cstr. heap : %d%%(%d/%dK)  ",
    	 (int)((Cheap_Max - cheap) * 100 * CHEAP_UNIT / CHEAP_SIZE),
    	 (int)((Cheap_Max - cheap)*CHEAP_UNIT/1000),(int)(CHEAP_SIZE/1000));
	tprint3("Heap : %d%%(%d/%dK)  ",
		 (int)(((Heap_Max - heap) * 100 * HEAP_UNIT) / HEAP_SIZE),
		 (int)((Heap_Max - heap)*HEAP_UNIT/1000),(int)(HEAP_SIZE/1000));
	tprint3 ("\n\tUser stack : %d%%(%d/%dK)  ", 
		(int)(((Stack_Max - ustack) * 100 * USTACK_UNIT)/ USTACK_SIZE),
		(int)((Stack_Max - ustack)*USTACK_UNIT/1000),(int)(USTACK_SIZE/1000));
	tprint3 ("Env. stack : %d%%(%d/%dK) \n", 
		(int)(((Esp_Max - eheap) * 100 * ESP_UNIT)/ ESP_SIZE),
		(int)((Esp_Max - eheap)*ESP_UNIT/1000),(int)(ESP_SIZE/1000));
}

void init_heap_max()
{
	Cheap_Max = cheap;
	Stack_Max = ustack;
	Heap_Max = heap;
}

void filewrite (n) /* write program to file */
char   *n;
{
    FILE * lfpsave;
    int i;
    register struct func *f;

    if ((wfp = fopen (n, "r")) != NULL) {
	fclose (wfp);
	wfp = stdout;
	tprint1 (" %s : already exist \n", n);
	return;
    }

    if ((wfp = fopen (n, "w")) == NULL) {
	wfp = stdout;
	tprint1 (" %s : can't open \n", n);
	return;
    }

    fprintf(wfp,"%%%%%% cu-Prolog predicates  %%%%%%%% \n");
    lfpsave = lfp;
    lfp = NULL;
    writenewfunc(); NL;
    for (i = 0; i< HASH_SIZE; i++)
	    for (f = hash_list[i]; f != NULL; f = f->f_link)
		    if (isuser(f) && isnoreduced(f))
			    Showfunc(f);
    fclose (wfp);
    wfp = stdout;
    lfp = lfpsave;
    tprint1 ("=== write to: %s ===\n", n);
    return;
}


void disp_func_def (f_from, f_to)/* show defs of f_from--->f_to  */
struct func *f_from,
           *f_to;
{
    if (f_from == NULL)
	return;
    if (f_from == f_to)
	return;
    disp_func_def (f_from -> f_link, f_to);
    if (isuser (f_from) && isnoreduced (f_from))
	Showfunc (f_from);
}

void set_inputfile (n)
char   *n;			/* file name */
{
    fp = fopen (n, "r");
    if (fp == NULL) {		/* open error */
	fp = stdin;
	tprint1 ("%s  ", n);
	error ("can't open !");
    }
    else {
      tprint1 ("=== open '%s'\n", n);
    }
  }

void readfile () {		/*  "file name" or "file name?"	 */
    int     i;

/*    if (!KEYIN)
	error ("file already opened"); */
    for (i = 0; ((cbuf != '"') && (cbuf != '?')); advance)
	nbuf[i++] = cbuf;
    nbuf[i] = '\0';		/* n[] <- file name */
    if (cbuf == '?')
	ECHO_BACK = TRUE;		/* echo back on */
    skipline;
	upush(&fp);
	utop = usp;
    set_inputfile (nbuf);	/* set file pointer */
    if (ECHO_BACK == TRUE)    wfp = stdout;	/* echo back on */
}


void set_eof () {		/* file EOF */

	clearerr(fp);	/* clear eof */
	if (tty && KEYIN){		/* from keyboard */
		error(" ");	/* EOF (^D in UNIX)  */
	}
	fclose (fp);
	if (utop != &ustack[0]) {
		utop -= 1;
		undo(utop);
		}
	else fp = stdin;
	if (wfp == NULL)
		wfp = stdout;		/* echo back on */
	tprint0 ("\n ****** end of file ******* \n");
}

/* -----------   static program analyzer  ---------------   */
/* +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
*    check_recursion()  check recursive/finite predicates
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */
int REC_to_FINITE = 1;
void check_all_unit(),rec_to_finite(),check_unitpred();
int is_body_finite();

void check_recursion()		/* check recursive user predicates */
{
	int i;
	void reset_component(),calc_component();

	if (Def_Modified == 0) return;
	for (i = 0; i < HASH_SIZE; i++)
		check_all_unit(hash_list[i]);
	REC_to_FINITE = 1;
	while(REC_to_FINITE != 0)
	{
		REC_to_FINITE = 0; /* global flag */
		rec_to_finite(); /* traverse predicates */
	}
	Def_Modified = 0;	/* def modified flag off */
	reset_component();
	calc_component();
}

void check_unitpred(f)
struct func *f;
{
	if (issystem(f)) return;
	if ((f->f_setcount == 0) || (f->f_setcount == f->f_unitcount))
	{
		finitefun(f);
		return;
	}
	recursivefun(f);
}

void check_all_unit(fl)
struct func *fl;
{
	register struct func *f;
	
	if (fl == NULL) return;
	for (f = fl; f != NULL; f = f->f_link) 
	{
		check_unitpred(f);
	}
}
	
void rec_to_finite()		/* recursive pred -> finite pred */
{
	register int i;
	register struct func *f;

	for (i = 0; i < HASH_SIZE; i++)
		for(f = hash_list[i]; f != NULL; f = f->f_link)
		{
			if (issystem(f) || isfinite(f)) continue;
			else if (is_body_finite(f) != 0) 
			{
				REC_to_FINITE = 1;
				finitefun(f);
			}
		}
}

int is_body_finite(f)		/* if all the body is finite  */
struct func *f;
{
	register struct set *s;
	register struct clause *c;
	
	for (s = f->def.f_set; s != NULL; s = s->s_link)
		for (c = s->s_clause->c_link; c != NULL; c = c->c_link)
			if (isvar(c->c_form) || 
			    isrecursive(c->c_form->type.t_func))
			  return(FALSE);
	return(TRUE);
}

/* +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
*    recalc_component()  component of each argument
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */
void mark_component_checked_all(), set_all_head_component(), 
    set_head_component(),
    set_head_component2(), set_all_body_component(),set_body_component(),
    add_component_pst(), add_component_pst2(), add_label(),calc_all_var();

#define is_globalvar(t)   (((struct var *)t)->v_type == VAR_GLOBAL_TYPE)
struct component *merge_component();

int COMPONENT_CHANGED;
int HAS_BODY;          /* changed in set_head_component() */

struct funclist			/* temporal funclist structure  */
{
    struct func *func;
    struct funclist *next;
};
#define NULL_fl  (struct funclist *)NULL

void calc_component()
{
	register int i;
	register struct func *f;
	register struct funclist *FL,*fl;
	int  *hsave = hp;

	FL=fl=NULL_fl;
	for (i = 0; i < HASH_SIZE; i++)
	    for (f = hash_list[i]; f != (struct func *)NULL; f = f->f_link)
		if (isuser(f) && f->def.f_set != (struct set *)NULL)
		{
		    HAS_BODY=0;	/* changed in set_head_component() */
		    set_head_component(f);
		    if (HAS_BODY != 0) /* not unit def predicates */
		    {
			MEMORY_ALLOC(fl,funclist,TEMPORAL);
			fl->func=f; fl->next=FL;    FL=fl;
		    }
		    else	/* no body clause --> end  */
		    {
			component_checked(f);
			calc_all_var(f);
		    }
		}
	do
	{
		COMPONENT_CHANGED = 0;
		for (fl=FL; fl != NULL_fl; fl=fl->next)
		    set_body_component(fl->func);
		for (fl=FL; fl != NULL_fl; fl=fl->next)
		    set_head_component2(fl->func);
	}
	while(COMPONENT_CHANGED != 0);
	for (fl=FL; fl != NULL_fl; fl=fl->next)
	{
	    component_checked(fl->func);
	    calc_all_var(fl->func);
	}
	hp=hsave;
}

void recalc_component()		/* calc component for newly defined preds */
{
	register int i;
	register struct func *f;
	register struct funclist *FL,*fl;
	int  *hsave = hp;

	FL=fl=NULL_fl;
	for (i = 0; i < HASH_SIZE; i++)
	    for (f = hash_list[i]; f != (struct func *)NULL; f = f->f_link)
		if (isuser(f) && is_component_not_checked(f) && 
		    f->def.f_set != (struct set *)NULL )
		    
		{
		    HAS_BODY=0;	/* changed in set_head_component() */
		    set_head_component(f);
		    if (HAS_BODY != 0) /* if f has a body clause */
		    {
			MEMORY_ALLOC(fl,funclist,TEMPORAL);
			fl->func=f; fl->next=FL;    FL=fl;
		    }
		    else	/* f has only unit clauses. */
		    {
			component_checked(f);
			calc_all_var(f);
		    }
		}
	do
	{
		COMPONENT_CHANGED = 0;
		for (fl=FL; fl != NULL_fl; fl=fl->next)
		    set_body_component(fl->func);
		for (fl=FL; fl != NULL_fl; fl=fl->next)
		    set_head_component2(fl->func);
	}
	while(COMPONENT_CHANGED != 0);
	for (fl=FL; fl != NULL_fl; fl=fl->next)
	{
	    component_checked(fl->func);
	    calc_all_var(fl->func);
	}
	hp=hsave;
}

void calc_all_var(f)
struct func *f;
{
	register struct set *s;
	for (s = f->def.f_set; s != NULL; s = s->s_link)
		recalc_voccurrence(s->s_clause, s->s_vlist);
}

void reset_component()		/* reset all Component() */
{
	int i;
	register int j;
	struct func *f;
	register struct set *s;
	register struct term *v;

	for (i = 0; i < HASH_SIZE; i++)
		for(f = hash_list[i]; f != NULL; f = f->f_link)
		if (isuser(f))	
		{
			for(j = f->f_arity - 1; j >= 0; j--)
				Component(f,j) = NULL;
			for(s = f->def.f_set; s != NULL; s = s->s_link)
				for (v = s->s_vlist; v != NULL; v = vlink(v))
					vcomponent(v) = NULL;
		}
}

void set_head_component(f)	/* check heads of f */
struct func *f;
{
	register int i;
	register struct set *s;
	register struct term *t,*arg;

	if (f->f_arity == 0) return;
	for(s = f->def.f_set; s != NULL; s = s->s_link)
	{
		t = s->s_clause->c_form; /* head  */
		if (s->s_clause->c_link != NULL_CL) HAS_BODY=1;
		for (i = f->f_arity - 1; i >= 0; i--)
		{
		      arg = Arg(t,i);
		      if (isvar(arg)) 
		      {
			  if (is_globalvar(arg))
			  {
			      Component(f,i) = 
			      merge_component(Component(f,i),
					      vcomponent(arg),ETERNAL);
			  }
		      }
		      else if(is_pst(arg)) 
		        add_component_pst(f,i,((struct pst *)arg)->p_lists);
		      else add_label(f,i,NOPSTLABEL,ETERNAL);	
		      /* normal term ; bug 94.10.25 */
	      }
	}
}

void set_body_component(ff)
struct func *ff;
{
	struct set *s;
	register struct clause *c;
	register struct term *t,*arg;
	register struct func *f;
	int i;

	if (ff->f_arity == 0) return;
	for(s=ff->def.f_set; s != NULL; s = s->s_link)
	for(c=s->s_clause->c_link; c !=NULL; c= c->c_link)
	{
		t = c->c_form;
		if (isvar(t)) continue;	/* 94.12.2 call(X):-X. */
		f = Pred(t);
		for (i = f->f_arity - 1; i >= 0; i--)
		{
		        arg = Arg(t,i);
			if (is_globalvar(arg)) 
				vcomponent(arg)=
					merge_component(vcomponent(arg),
					Component(f,i),TEMPORAL);
		}
	}
}

void set_head_component2(f)	/* check heads of f (later than 2nd loop)*/
struct func *f;
{
	register int i;
	register struct set *s;
	register struct term *t,*arg;

	if (f->f_arity == 0) return;
	for(s = f->def.f_set; s != NULL; s = s->s_link)
	{
	    if (s->s_clause->c_link == NULL_CL) continue;
	    			/* omit unit clause */
	    t = s->s_clause->c_form; /* head  */
		for (i = f->f_arity - 1; i >= 0; i--)
		{
		      arg = Arg(t,i);
			/* check only var and pst */
		      if (is_globalvar(arg)) 
			      Component(f,i) = merge_component(Component(f,i),
					vcomponent(arg),ETERNAL);
		      else if(is_pst(arg)) 
			  add_component_pst2(f,i,((struct pst *)arg)->p_lists);
	      }
	}
}

void add_component_pst(f,a,ec)	/* add pst ec to f/a */
struct func *f;
int a;
struct eclause *ec;
{
	register struct eclause *e;
	register struct term *value;
	register struct func *label;
	
	for (e = ec; e != NULL_ECL; e = e->c_link)
	{
		label = Pred(Arg1(e->c_form));
		value = Arg2(e->c_form);
		if (isvar(value) && vcomponent(value) == NULL) continue;
		else add_label(f,a,label,ETERNAL);
	}
}

void add_component_pst2(f,a,ec)	/* add pst ec to f/a (later than 2nd loop) */
struct func *f;
int a;
struct eclause *ec;
{
	register struct eclause *e;
	register struct term *value;
	register struct func *label;

	for (e = ec; e != NULL_ECL; e = e->c_link)
	{
		label = Pred(Arg1(e->c_form));
		value = Arg2(e->c_form);
		if is_globalvar(value)	/* check var values only */
		    if (vcomponent(value) == NULL) continue;
		    else add_label(f,a,label,ETERNAL);
	}
}

int cmp_label(l1,l2)		/* 0:equal -1:l1<l2, 1:l1>l2 */
struct func *l1,*l2;
{
    register int dif;
    if (l1 == l2) return(0);
    else if (l1 == NULL) return(-1);
    else if (l2 == NULL) return(1);
    else return(l1->f_number - l2->f_number);
}

/* component : ascending order  */
void add_label(f,a,l,flag)		/* add label l to f/a */
struct func *f,*l;
int a,flag;			/* flag = ETERNAL or TEMPORAL */
{
	register struct component *c,*cprev,*nc;
	register int cmp;

	for (cprev=NULL,c=Component(f,a); c != NULL; cprev= c, c = c->c_next)
	{
		cmp = cmp_label(l,c->c_label);
		if (cmp == 0) return;
		else if (cmp < 0) break; /* l < c_label */
	}
	MEMORY_ALLOC(nc,component,flag);
	nc->c_next = c;
	nc->c_label = l;
	if (cprev == NULL) Component(f,a) = nc;
	else cprev->c_next = nc;
	COMPONENT_CHANGED++;
}

struct component *copy_component(cb,flag) /* make a copy of cb */
struct component *cb;
int flag;			/* ETERNAL or TEMPORAL */
{
    register struct component *nc;

    if (cb == (struct component *)NULL) return(cb);
    MEMORY_ALLOC(nc,component,flag);
    nc->c_label = cb->c_label;
    nc->c_next = copy_component(cb->c_next,flag);
    return(nc);
}

struct component *merge_component(ca,cb,flag) /* merge cb in ca */
struct component *ca,		/* ca will be changed */
	*cb;
int flag;			/* ETERNAL or TEMPORAL */
{
	int a;
	register struct component *nc;
	if (cb == (struct component *)NULL) return(ca);
	else if (ca == (struct component *)NULL)
	{
	    COMPONENT_CHANGED++;
	    return(copy_component(cb,flag));
	}
	else if (ca != (struct component *)NULL)
	{
		a = cmp_label(ca->c_label,cb->c_label);
		if (a == 0) {
			ca->c_next = 
				merge_component(ca->c_next,cb->c_next,flag);
			return(ca);
		}
		else if (a < 0)		/* ca < cb */
		{
			ca->c_next = merge_component(ca->c_next,cb,flag);
			return(ca);
		}
		else		/* ca > cb */
		{
		    COMPONENT_CHANGED++; /* global var */
		    MEMORY_ALLOC(nc,component,flag);
		    nc->c_label = cb->c_label;
		    nc->c_next = merge_component(ca,cb->c_next,flag);
		    return(nc);
		}
	}
}

int has_common_label(ec,cm)	/* TRUE/FALSE */
struct eclause *ec;
struct component *cm;
{
	register int cmp;
	if (ec == NULL || cm == NULL) return(FALSE);
	if (cm->c_label == NOPSTLABEL) return(TRUE); /* cm is not vacuous */
	cmp = cmp_label(Pred(Arg1(ec->c_form)), cm->c_label);
	if (cmp == 0) return(TRUE);
	else if (cmp < 0) return(has_common_label(ec->c_link,cm));
	else return(has_common_label(ec,cm->c_next));
}

/* -------------- end of component part --------------- */

void oscommand () {		/* os command interpreter */
    int     i;

    for (i = 0; (cbuf != '\n'); next ())
	nbuf[i++] = cbuf;
    nbuf[i] = '\0';
    if (system (nbuf) != 0)
	tprint0 ("== OS command error == \n");
}


void delete_tmp () {		/* delete temp file */
	FILE *fptmp;

	if ((fptmp = fopen("TEMPF.###","r")) != NULL)
	{
		fclose(fptmp);
#if MSDOS == 0			/* for UNIX */
    system ("rm -f TEMPF.###");
#else				/* for MS-DOS */
    system ("del TEMPF.###");
#endif
	}
}

void quit_prolog () {		/* system quit */
    tprint0("\n---- Quit cu-Prolog ? (y/n) ----");
    skipline;
    if (keyread('y')) {
	    if (lfp != NULL)
		    fclose (lfp);	/* close log file */
	    delete_tmp ();		/* delete temp file */
	    exit (1);			/* end */
    }
    tprint0("\n.... Return to Prolog ....\n");/* cansel */
    return;
}

void preprocess_constraints(fn)
char *fn;
{
	struct func *f;
	int arity;
	void preprocess_constr_sub(), preprocess_unit();

	if (strcmp(fn,"*") == 0) {
		tprint0("--- preprocess all predicates ---\n");
		preprocess_constr_sub(TRUE);
		tprint0("Done\n");
		return;
		}
	if (strcmp(fn,"?") == 0) {
	  tprint0("--- showing predicates with nonmodular constraints ---\n");
	  preprocess_constr_sub(FALSE);
	  NL;
	  return;
	  }
	arity = decode_pname(fn);
	if (! exist_fname(fn)) {
		tprint1("'%s' does not exist\n",fn);
		return;
	}
	if (arity == -1) { /* any arity */
	  for (f =  hash_list[hash(fn)]; f != NULL; f = f->f_link)
	    if (streq(f->f_name,fn))
	      preprocess_unit(f,TRUE);
	}
	else {
	  f = funcsearch(fn,arity);
	  if (f == NULL) {
	    tprint2("'%s/%d' does not exist.\n",fn,arity);
	    return;
	  }
	  preprocess_unit(f,TRUE);
	}
	tprint0("Done\n");
}

void preprocess_constr_sub(flag)
int flag;	/* preproces control flag */
{
	register int i;
	void preprocess_all_unit();

	for (i = 0; i < HASH_SIZE; i++)
		preprocess_all_unit(hash_list[i],flag);
}

void preprocess_all_unit(fl,flag)
struct func *fl;
int flag;
{
	register struct func *f;
	void preprocess_unit();

	if (fl == NULL) return;
	for (f = fl; f != NULL; f = f->f_link)
		preprocess_unit(f,flag);
}

void preprocess_unit(f,flag)
struct func *f;
int flag;
{
	register struct set *s;
	struct clause *c, *sol, *reduce_cstr();
	struct pair *env;
	int check_modularity();	/* cf. is_modular_clause() */

	if (issystem(f)) return;
	for (s = f->def.f_set; s != (struct set *)NULL; s = s->s_link) {
		c = s->s_constraint;
		if (c == NULL_CL) continue;
		if (check_modularity(c) == TRUE) continue;
		if (flag == FALSE) { 
			Showhorn(s->s_clause,s->s_constraint,
				 NULL_ENV);	NL;
			continue;
		}
		tprint2("%s/%d\t", f->f_name,f->f_arity);
		env = Nenv(s->s_anumber);
		sol = reduce_cstr(c,s->s_vlist,s->s_anumber,env);
		if (sol == MFAIL) { /* failing transformation */
			wfp = stderr;
			tprint1("Warning: Failing transformation in %s\n",
				f->f_name);
			c->c_form = FAIL;
			c->c_link = NULL_CL;
			Showhorn(s->s_clause,s->s_constraint,
				 NULL_ENV);NL;
			wfp = stdout;
			continue;
		}
		up_init();
		s->s_constraint = (struct clause *)termset(sol,env,ETERNAL);
		s->s_clause = (struct clause *)
			termset(s->s_clause,env,ETERNAL);
		up_restore();
		if (p_number != 0) {
			renum_pvars((struct pstvar *)pv_list,v_number);
		}
		s->s_anumber = (unsigned short int)(v_number+p_number);
		s->s_vlist = v_list;
	}
}

int check_modularity(cst)	/* cf. is_modular_clause */
struct clause *cst;
{
	register struct clause *c;
	register struct term *t;

	for (c= cst; c != NULL; c = c->c_link)
	{
		t = c->c_form;
		if (Pred(t) == EQ2_P || 
		    (! is_modular_literal(t))) return(FALSE);
	}
	return(TRUE);
}


#define NOREDUCED_CLAUSE (struct clause *)11

struct clause *reduce_cstr(cst,vlist,anum,env)
struct clause *cst;
struct term *vlist;
int anum;
struct pair *env;
{
	struct clause *nc,*reduce_substitute();
	int reduced = 0;

	nc = reduce_substitute(cst,env); /* reduce x=y */
	if (nc == MFAIL) return(MFAIL);
	else if (nc == NOREDUCED_CLAUSE) /* no reduction */
		return(startmodular(cst,vlist,anum));
	else if (nc == NULL) return(NULL);
	else 
	{
		up_init();
		nc = (struct clause *)termset(nc,env,MEDIUM);
		up_restore();
		if (p_number != 0) {
			renum_pvars((struct pstvar *)pv_list,v_number);
		}
		return(startmodular(nc,v_list,v_number + p_number));
	}
}


struct clause *reduce_substitute(cst,e)/* preprocess constraint */
struct clause *cst;
struct pair *e;
{
	register struct clause *c;
	struct clause *compress_clause();
	int reduced = 0;
	struct term *t;
	
	for (c = cst; c != NULL_CL; c = c->c_link)
	{
		t = c->c_form;
		if (Pred(t) == EQ2_P) /* '=' */
		{
			reduced = 1;
			c->c_form = NULL;
			if (tunify(Arg(t,0),e,Arg(t,1),e,0) == FALSE)
				return(MFAIL);
		}
	}
	if (reduced == 0) return(NOREDUCED_CLAUSE);
	else return(compress_clause(cst));
}

struct clause *compress_clause(cst) /* cut c (c->c_form == NULL) */
struct clause *cst;
{
	if (cst == NULL_CL) return(NULL);
	if (cst->c_form == NULL) return(compress_clause(cst->c_link));
	else 
	{
		cst->c_link = compress_clause(cst->c_link);
		return(cst);
	}
}


/************* print CPU time ******************************/
#if SUN4 == 1 /* print CPU time */
#include <sys/time.h>
long    TIMESAVE;		/* system time saver (time_t = long) */

void printtime () {		/* print CPU time from the previous settime()*/
  long clock();
  tprint2 ("CPU time = %.3lf sec (Constraints Handling = %.3lf sec)\n",
	   ((double)(clock() - TIMESAVE))/ 1000000.0,
	   ((double)CONSTRAINT_HANDLING_TIME/1000000.0));
}

void settimer () {		/* set clock	 */
  long clock();
  TIMESAVE = clock();
  CONSTRAINT_HANDLING_TIME = 0L;
}
#else
#if CPUTIME == 0		/* do not print CPU-time */
void printtime () {
}
void settimer () {
}

#else  /* BSD */
#include <sys/types.h>
#include <sys/times.h>
time_t    TIMESAVE;		/* system time saver (time_t = long) */
struct tms TIMES;		/* cf. times() */

/*
* Structure returned by old times() interface
*     struct tms {
*          time_t    tms_utime;           user time 
*          time_t    tms_stime;           system time 
*          time_t    tms_cutime;          user time, children 
*          time_t    tms_cstime;          system time, children
*     };
*/

void printtime () {		/* print CPU time from the previous settime()*/
	time_t  ttemp;

	times(&TIMES);		/* get time */
	ttemp = TIMES.tms_stime + TIMES.tms_utime;
	tprint2 ("CPU time = %.3lf sec (Constraints Handling = %.3lf sec)\n", 
	     (ttemp - TIMESAVE) / (float)CPUTIME,
	     (CONSTRAINT_HANDLING_TIME / (float)CPUTIME));
}

void settimer() {		/* set clock	 */
	times(&TIMES);
	TIMESAVE = TIMES.tms_stime + TIMES.tms_utime;
	CONSTRAINT_HANDLING_TIME = 0L;
}

#endif
#endif