/******************************************************************************

			UNSW Prolog (version 4)

			Written by Claude Sammut
		     Department of Computer Science
		     University of New South Wales
		   (and St. Joseph's U., Philadelphia)

		   Copyright (c)  1983 - Claude Sammut

******************************************************************************/





		/*	Structure sharing Prolog interpreter 	*/

#include "g.h"
#include <stdio.h>
#include <setjmp.h>


#define CALL	0
#define EXIT	1
#define FAILG	2
#define REDO	3


binding	*stack;			/* the global variable stack	*/

environment *env_stack;		/* the local control stack	*/

static binding	**trail, *frame2;

static int STACK_SIZE, TRAIL_SIZE, ENV_SIZE;

short	sp = 0,
	tp = 0,
	parent = -1,
	env = -1;

static short
	S_BOTTOM = 0,
	BOTTOM = -1;

static char tracing;
pval termb;
binding *frameb;

jmp_buf env3;

static short tlevel;

char run = FALSE;
static char ss = FALSE;


extern atom *_cut;
extern integer *stack_int;


bind(v, f1, term, f2)
var *v;
pval term;
binding *f1, *f2;
{
	register binding *p;

#ifdef DEBUG
	printf("BIND ");
	run = FALSE;
	prin(v, 1200, f1);
	run = TRUE;
	printf(" TO ");
	print(term, 1200, f2);
#endif

	p = &(f1[v -> offset]);
	p -> termv = term;
	p -> framev = f2;
	if (f1 < frame2)
	{
#ifdef DEBUG
		printf("PUT ON TRAIL\n");
#endif
		if (tp <= TRAIL_SIZE)  trail[tp++] = p; 
		else fatal("TRAIL OVERFLOW");
	}
}

isbound(v, f)
var *v;
binding *f;
{
	register binding *p;

	p = &(f[v -> offset]);
	if (p -> termv == 0) return(FALSE);
	termb = p -> termv;
	frameb = p -> framev;
	return(TRUE);
}

static long n_unify = 0;

unify(term1, frame1, term2, frame2)
register pval term1, term2;
binding *frame1, *frame2;
{
	register int i;

#ifdef DEBUG
	run = FALSE;
	printf("***********\n");
	prin(term1,1200 , frame1); printf("  %d\n", frame1 - stack);
	prin(term2, 1200, frame2); printf("  %d\n", frame2 - stack);
	printf("===========\n");
	run = TRUE;
#endif

	n_unify++;
L1:	if (term1 == term2 && frame1 == frame2) return(TRUE);
	switch (TYPE(term1))
	{
	case ATOM:
	case STRING:
	case PREDEF:
		if (isatom(term2))
			return(term1 == term2);
		else break;
	case INT:
		if (isinteger(term2))
			return((term1 == (pval) stack_int ? (int) frame1 : term1 -> i.int_val)
				==
				(term2 == (pval) stack_int ? (int) frame2 : term2 -> i.int_val));
		else break;
	case VAR:
		if (isbound(term1, frame1))
		{
			term1 = termb;
			frame1 = frameb;
			goto L1;
		}
		else if (isvariable(term2))
			if (isbound(term2, frame2))
				bind(term1, frame1, termb, frameb);
			else if (frame2 > frame1)
				bind(term2, frame2, term1, frame1);
			else bind(term1, frame1, term2, frame2);
		else bind(term1, frame1, term2, frame2);
		return(TRUE);
	case FN:
		if (iscompound(term2))
		{
#ifdef PRINC_VAR	/* unifies principal term as well as args */

			if (SIZE(term1) != SIZE(term2)) return(FALSE);
			for (i = 0; i <= SIZE(term1); i++)
				if (! unify(term1 -> c.term[i], frame1,
					    term2 -> c.term[i], frame2))
					return(FALSE);
			return(TRUE);
#else
			if (term1 -> c.term[0] != term2 -> c.term[0])
				return(FALSE);
			if (SIZE(term1) != SIZE(term2)) return(FALSE);
			for (i = 1; i <= SIZE(term1); i++)
				if (! unify(term1 -> c.term[i], frame1,
					    term2 -> c.term[i], frame2))
					return(FALSE);
			return(TRUE);
#endif
		}
		else break;
	case LIST:
		if (islist(term2))
			if (unify(term1->c.term[0], frame1, term2->c.term[0], frame2))
			{
				term1 = term1 -> c.term[1];
				term2 = term2 -> c.term[1];
				goto L1;
			}
			else return(FALSE);
		else break;
	}
	if (isvariable(term2))
	{
		if (isbound(term2, frame2))
		{
			term2 = termb;
			frame2 = frameb;
			goto L1;
		}
		else bind(term2, frame2, term1, frame1);
		return(TRUE);
	}
	else return(FALSE);
}

clear_frame(n)
register int n;
{
#ifdef DEBUG
	printf("CLEAR %d STARTING AT %d\n", n, sp);
#endif
	if ((sp + n) >= STACK_SIZE) fatal("STACK OVERFLOW");
	while (n-- != 0) {stack[sp].termv = 0; stack[sp++].framev = 0;}
}

unbind(v, f)
var *v;
binding *f;
{
	termb = (pval) v; frameb = f;
	while (isvariable(termb) && isbound(termb, frameb));
}


#define MAXARGS 16


static
eval(a, t, frame1)
register pval a;
compterm *t;
binding *frame1;
{
	register int i, nargs;
	pval arg[MAXARGS];
	binding *frame[MAXARGS];

	nargs = a -> p.nargs;
	if(t -> size != nargs && nargs != NPRED)
	{
		warning("Incorrect number of arguments to built-in");
		return(FALSE);
	}
	if (t -> size > MAXARGS)
	{
		warning("TOO MANY ARGUMENTS FOR BUILT IN PREDICATE");
		return(FALSE);
	}
	for (i = 1; i <= t -> size; i++)
		if (isvariable(t -> term[i]))
		{
			unbind(t -> term[i], frame1);
			arg[i-1] = termb; frame[i-1] = frameb;
		}
		else {
			arg[i-1] = t -> term[i];
			frame[i-1] = frame1;
		}
	if (nargs == NPRED)
		return FVAL(a)(arg, frame, t -> size);
	else return FVAL(a)(arg, frame);
}



static long n_calls = 0;
static int successful = FALSE;

static
lush(c, argn, print_vars)
clause *c;
int argn;
int print_vars;
{
	register environment *p;
	register pval t;
	short old_sp, old_tp, base;
	binding *frame1;
	register clause *clist;
	pval a, *cl;
	int kind = CALL;

#ifdef DEBUG
	printf("LUSH\n");
	parent = env = -1;
	sp = tp = 0;
#endif

	old_tp = tp;
	frame2 = &(stack[sp]);
	cl = &(c -> goal[1]);
	clear_frame(argn);
NEW_CLAUSE:
#ifdef DEBUG
	printf("GO NEW_CLAUSE\n");
#endif
	frame1 = frame2;
	parent = env;
	base = sp;
NEW_GOAL:
#ifdef DEBUG
	printf("NEW GOAL\n");
#endif
	if (*cl == 0) goto SUCCEED;
	n_calls++;
	t = *cl;
	if (isvariable(t))
	{
		unbind(t, frame1); t = (pval) termb; frame1 = frameb;
#ifdef DEBUG
		printf("\nFrame1 = %o; offset = %d\n", frame1, t -> v.offset);
		print(t, 1200, frame1);
#endif
	}
	if (t == (pval) _cut)
	{
#ifdef DEBUG
		printf("CUT %d %d\n", parent, env);
#endif
		env = parent;
		cl++;
		env_stack[env].clist = 0;
		goto NEW_GOAL;
	}
	switch (TYPE(t))
	{
	   case ATOM:	if (clist = t -> a.val)
				tracing = t -> a.traced;
			else goto FAIL;
			break;
	   case PREDEF:	if (t -> p.traced) trace_print(t, frame1, CALL);
			if ((*(t -> p.fn))())
			{
				cl++;
				old_tp = tp;
				goto NEW_GOAL;
			}
			else goto FAIL;
	   case FN:	a = t -> c.term[0];
#ifdef PRINC_VAR
			if (isvariable(a))
			{
				unbind(a, frame1);
				if (isatom(termb))
					a = termb;
				else {
					fprintf(stderr, "Principal term must be an atom: ");
					run = FALSE;
					print(termb, 1200, frameb);
					run = TRUE;
					goto FAIL;
			
				}
			}
#endif
			if (TYPE(a) == PREDEF)
			{
#ifdef DEBUG
				printf("*** ");   print(t, 1200, frame1); 
#endif
				if (a -> p.traced)
					trace_print(t, frame1, CALL);
				if (eval(a, t, frame1))
				{
					cl++;
					old_tp = tp;
					goto NEW_GOAL;
				}
				else goto FAIL;
			}
			else if (clist = a -> a.val)
				tracing = a -> a.traced;
			else goto FAIL;
			break;
	   default:	warning("Cannot execute goal");
			print(t, 1200, frame1);
			return;
	}
BACKTRACK_POINT:
#ifdef DEBUG
	printf("BACKTRACK POINT\n");
#endif
	frame2 = &(stack[sp]);
	old_sp = sp;
ALTERNATIVE:
#ifdef DEBUG
	printf("ALTERNATIVE\n");
	print(t, 1200, frame1);
#endif
	if (clist == 0) goto FAIL;
	clear_frame(clist -> nvars);
	if (unify(clist -> goal[0], frame2, t, frame1))
	{
		if (tracing)
		{
			trace_print(clist -> goal[0], frame2, kind);
			kind = CALL;
		}
		if (++env == ENV_SIZE) fatal("ENVIRONMENT STACK FULL");
#ifdef DEBUG
		printf("MAKING NEW ENVIRONMENT AT %d\n", env);
#endif
		p = &(env_stack[env]);
		p -> cl = cl;
		p -> tracing = tracing ? tlevel : 0;
		p -> sp = old_sp;
		p -> clist = clist -> rest;
		p -> parent = parent;
		p -> tp = old_tp;
		old_tp = tp;
#ifdef DEBUG1
		dump_stack();
		dump_env();
#endif
		cl = &(clist -> goal[1]);
		goto NEW_CLAUSE;
	}
	else {
		sp = old_sp;
#ifdef DEBUG
		printf("TRAIL is %d, old TRAIL is %d\n", tp, old_tp);
		print(t, 1200, frame1);
#endif
		while (tp > old_tp)
			trail[--tp] -> termv = 0;
		clist = clist -> rest;
		goto ALTERNATIVE;
	}
SUCCEED:
#ifdef DEBUG
	printf("SUCCESS %d\n", parent);
#endif
	if (parent > BOTTOM)
	{
#ifdef DEBUG
		printf("POP %d\n", parent);
#endif
		p = &(env_stack[parent]);
		parent = p -> parent;
		if (parent == BOTTOM) base = S_BOTTOM;
		else base = env_stack[parent].sp;
		frame1 = &stack[base];
		if (tracing = p -> tracing)
		{
			tlevel = tracing - 1;
			trace_print(*(p -> cl), frame1, EXIT);
			--tlevel;
		}
		cl = (p -> cl) + 1;
		goto NEW_GOAL;
	}
	else if (print_vars) prvars(argn);
	else return;

FAIL:
#ifdef DEBUG
	printf("BACKTRACKING %d\n", env);
#endif
	if (tracing) trace_print(t, frame1, FAILG);
	if (env < 0)
	{
		if (! successful && print_vars) printf("** no\n");
		return;
	}
	p = &(env_stack[env--]);
	cl = p -> cl;
	sp = p -> sp;
	clist = p -> clist;
	parent = p -> parent;
	if (parent == -1) base = 0;
	else base = env_stack[parent].sp;
	old_tp = p -> tp;
	frame1 = &(stack[base]);
	t = *cl;
	while (tp > old_tp) trail[--tp] -> termv = 0;
	if (tracing = p -> tracing)
	{
		tlevel = tracing - 1;
		kind = REDO;
	}
	goto BACKTRACK_POINT;
}





static
trace_print(cl, frame2, kind)
clause *cl;
binding *frame2;
int kind;
{
	extern FILE *output;
	int i;
	static char trace_type[] = {'C', 'E', 'F', 'R'};
	static char arrow_head[] = {'>', '<', '<', '>'};

	if (tlevel < 80) ++tlevel;
	putc(trace_type[kind], output);
	for (i = tlevel; i != 0; i--)
		putc('|', output);
	putc(arrow_head[kind], output);
	print(cl, 1200, frame2); 
}


static
prvars(argn)
int argn;
{
	register i;
	extern var **varcell;
	extern atom *anon;
	extern FILE *output;
	FILE *old_output;

	successful = TRUE;
	old_output = output;
	output = stdout;
	if (argn)
	{
		putchar('\n');
		for (i = 0; i != argn; i++)
		{
			if (varcell[i] -> pname == anon) continue;
			printf("%s = ", varcell[i] -> pname -> name);
			print(varcell[i], 1200, &(stack[S_BOTTOM]));
		}
	}
	else printf("** yes\n");
	output = old_output;
}

dump_stack()
{
	extern FILE *output;
	register i, j;

	run = FALSE;
	fprintf(output, "\n------------- VARIABLE STACK  -------------\n");
	for (i = sp - 1; i >= 0; i--)
	{
		fprintf(output, "%3d :", i);
		if (stack[i].termv == (pval) stack_int)
			fprintf(output, "	    %d\n",
					(int) stack[i].framev);
		else {
			if ((j = (int) (stack[i].framev - stack)) || TYPE(stack[i].termv) == VAR)
				fprintf(output, "  %-3d  ", j);
			else fprintf(output, "       ");
			print(stack[i].termv, 1200 , stack[i].framev);
		}
	}
	run = TRUE;
}

dump_env()
{
	extern FILE *output;
	register i, base;

	ss = TRUE;
	fprintf(output, "\n------------- ENVIRONMENT STACK ------------\n");
	for (i = env; i != -1; i--)
	{
		if (env_stack[i].parent == BOTTOM)
			base = S_BOTTOM;
		else base = env_stack[env_stack[i].parent].sp;
#ifdef DEBUG
		fprintf(output, "%3d :  %4d %4d %4d %4d    ", 
				i,
				env_stack[i].parent,
				base,
				env_stack[i].sp,
				env_stack[i].tp
		);
#else
		fprintf(output, "%3d : %4d %4d    ",
				i,
				env_stack[i].parent,
				base
		);
#endif
		print(*(env_stack[i].cl), 1200, &stack[base]);
/*		fprintf(output, "  %d ",&(stack[env_stack[i].sp])); */
	}
	ss = FALSE;
	fprintf(output, "============================================\n");
}


struct tbuffer
{
	long utime;
	long stime;
	long cutime;
	long cstime;
};


int do_timing = FALSE;

execute(c, argn, print_vars)
clause *c;
int argn;
int print_vars;
{
	extern FILE *input, *piport, *output, *poport;
	extern atom *init_prompt, *read_prompt, *prompt_string;
	extern long times();
	struct tbuffer buffer[2];
	FILE *old_input, *old_output;
	register int i;
	double total;
	short	O_BOTTOM = BOTTOM,
		O_S_BOTTOM = S_BOTTOM,
		O_parent = parent,
		O_tp = tp;
	binding *O_frame2 = frame2;

#ifdef DEBUG
	printf("BEGIN EXECUTION\n");
#endif
	BOTTOM = env;
	S_BOTTOM = sp;
#ifdef DEBUG
	fprintf(stderr, "BOTTOM = %d, sp = %d\n", BOTTOM, sp);
#endif
	old_input = input; input = piport;
	old_output = output; output = poport;
	prompt_string = read_prompt;

	successful = FALSE;
	run = TRUE;
	tlevel = 0;
	n_calls = n_unify = 0;

	if (do_timing)
	{
		times(&(buffer[0]));
		for (i = 0; i < 100 && do_timing; i++)
		{
			if (! setjmp(env3))
				lush(c, argn, print_vars);

			env = BOTTOM;
			sp = S_BOTTOM;
			BOTTOM = O_BOTTOM;
			S_BOTTOM = O_S_BOTTOM;
			parent = O_parent;
			tp = O_tp;
			frame2 = O_frame2;
		}
		times(&(buffer[1]));
		total = (double)(buffer[1].utime - buffer[0].utime) / 60;
		fprintf(output,
			"\n%d procedure calls executed in %1.2f seconds\n",
			n_calls,
			total
		);
		fprintf(output, "Run executed %d calls to unify\n", n_unify);
		if (total > 0.0001)
			fprintf(output, "%1.2f procedure calls/sec\n",
				(double)(n_calls) / total
			);
	}
	else if (! setjmp(env3))
		lush(c, argn, print_vars);

	run = FALSE;

	input = old_input; output = old_output;
	prompt_string = init_prompt;

	env = BOTTOM;
	sp = S_BOTTOM;
	BOTTOM = O_BOTTOM;
	S_BOTTOM = O_S_BOTTOM;
	parent = O_parent;
	tp = O_tp;
	frame2 = O_frame2;
#ifdef DEBUG
	fprintf(stderr, "BOTTOM = %d, sp = %d\n", BOTTOM, sp);
	printf("END EXECUTION\n");
#endif
}


set_stacks(n)
int n;
{
	extern char *calloc();

	STACK_SIZE = n;
	ENV_SIZE = n/3;
	TRAIL_SIZE = n/4;

	stack = (binding *) calloc(STACK_SIZE, sizeof(binding));
	env_stack = (environment *) calloc(ENV_SIZE, sizeof(environment));
	trail = (binding **) calloc(TRAIL_SIZE, sizeof(binding *));

	if (stack == 0 || env_stack == 0 || trail == 0)
	{
		fprintf(stderr, "Not enough memory for Prolog\n");
		exit();
	}
}