shithub: pprolog

ref: 18ae80eac7b678d71b13710b978a03863c7e3fd2
dir: /eval.c/

View raw version
#include <u.h>
#include <libc.h>
#include <bio.h>

#include "dat.h"
#include "fns.h"

int equalterms(Term *, Term *);
Goal *copygoals(Goal *);
Builtin findbuiltin(Term *);
void addchoicepoints(Clause *, Term *, Goal *, Module *);

int
evalquery(Term *query)
{
	Binding *replbindings = nil;
	goalstack = addgoals(goalstack, query, usermodule);

	while(goalstack->goal != nil){
		Term *goal = goalstack->goal;
		Term *catcher = goalstack->catcher;
		Module *module = goalstack->module;
		goalstack = goalstack->next;

		if(catcher)
			continue;

		if(flagdebug)
			print("Working goal: %S:%S\n", module->name, prettyprint(goal, 0, 0, 0, nil));

		Binding *bindings = nil;
		Clause *clause = nil;
		
		/* Try to see if the goal can be solved using a builtin first */
		Builtin builtin = findbuiltin(goal);
		if(builtin != nil){
			int success = builtin(goal, &bindings, module);
			if(!success)
				goto Backtrack;
		}else{
			Predicate *pred = findpredicate(module->predicates, goal);
			if(pred == nil){
				Rune *name;
				int arity;
				Term *replacement = nil;
				Term *procedure;
				Term *pi;
				if(goal->tag == CompoundTerm){
					name = goal->text;
					arity = goal->arity;
				}else{
					name = prettyprint(goal, 0, 0, 0, nil);
					arity = 0;
				}
				switch(flagunknown){
				case UnknownError:
					procedure = mkatom(name);
					procedure->next = mkinteger(arity);
					pi = mkcompound(L"/", 2, procedure);
					replacement = existenceerror(L"procedure", pi);
					break;
				case UnknownWarning:
					print("Warning: no such predicate in module %S: %S/%d\n", module->name, name, arity);
				case UnknownFail:
					replacement = mkatom(L"fail");
				}
				goalstack = addgoals(goalstack, replacement, module);
				continue;
			}

			/* Find a clause where the head unifies with the goal */
			clause = findclause(pred->clauses, goal, &bindings);
			if(clause != nil)
				addchoicepoints(clause, goal, goalstack, module);
			else{
Backtrack:
				if(choicestack == nil)
					return 0;
				if(flagdebug)
					print("Backtracking..\n");
				Choicepoint *cp = choicestack;
				choicestack = cp->next;
				goalstack = cp->goalstack;
				module = cp->currentmodule;
				clause = cp->alternative;
				bindings = cp->altbindings;
			}
		}

		/* Apply bindings to all goals on the stack except catchframes */
		Goal *g;
		for(g = goalstack; g != nil; g = g->next){
			if(g->goal != nil && g->catcher == nil)
				applybinding(g->goal, bindings);
		}

		/* Add clause body as goals, with bindings applied */
		if(clause != nil && clause->body != nil){
			Term *subgoal = copyterm(clause->body, nil);
			applybinding(subgoal, bindings);
			goalstack = addgoals(goalstack, subgoal, module);
		}
	}
	goalstack = goalstack->next;
	unify(query, goalstack->goal, &replbindings);
	return 1;
}

Goal *
addgoals(Goal *goals, Term *t, Module *module)
{
	if(t->tag == CompoundTerm && runestrcmp(t->text, L",") == 0 && t->arity == 2){
		goals = addgoals(goals, t->children->next, module);
		goals = addgoals(goals, t->children, module);
	}else{
		if(t->tag == CompoundTerm && runestrcmp(t->text, L":") == 0 && t->arity == 2){
			Term *moduleterm = t->children;
			if(moduleterm->tag == AtomTerm){
				Module *m = getmodule(moduleterm->text);
				if(m == nil)
					t = existenceerror(L"module", moduleterm);
				else{
					t = moduleterm->next;
					module = m;
				}
			}else
				t = typeerror(L"module", moduleterm);
		}
		Goal *g = gmalloc(sizeof(Goal));
		g->goal = t;
		g->module = module;
		g->catcher = nil;
		g->next = goals;
		goals = g;
	}
	return goals;
}

Clause *
findclause(Clause *clauses, Term *goal, Binding **bindings)
{
	Clause *clause;
	for(; clauses != nil; clauses = clauses->next){
		clause = copyclause(clauses, &clausenr);
		clausenr++;
		clause->next = clauses->next;
		if(unify(clause->head, goal, bindings))
			return clause;
	}
	return nil;
}

Predicate *
findpredicate(Predicate *preds, Term *goal)
{
	Rune *name;
	int arity;

	name = goal->text;
	if(goal->tag == AtomTerm)
		arity = 0;
	else
		arity = goal->arity;

	Predicate *p;
	for(p = preds; p != nil; p = p->next){
		if(runestrcmp(p->name, name) == 0 && p->arity == arity)
			return p;
	}
	return nil;
}

int
unify(Term *a, Term *b, Binding **bindings)
{
	Term *leftstack;
	Term *rightstack;
	Term *left;
	Term *right;

	leftstack = copyterm(a, nil);
	rightstack = copyterm(b, nil);

	while(leftstack != nil && rightstack != nil){
		left = leftstack;
		leftstack = left->next;
		right = rightstack;
		rightstack = right->next;

		if(equalterms(left, right))
			continue;
		else if(left->tag == VariableTerm || right->tag == VariableTerm){
			if(left->tag != VariableTerm && right->tag == VariableTerm){
				Term *tmp = left;
				left = right;
				right = tmp;
			}
			if(left->tag == VariableTerm && right->tag == VariableTerm && right->clausenr > left->clausenr){
				Term *tmp = left;
				left = right;
				right = tmp;
			}

			if(runestrcmp(left->text, L"_") == 0)
				continue; /* _ doesn't introduce a new binding */

			Binding *b = gmalloc(sizeof(Binding));
			b->name = left->text;
			b->nr = left->clausenr;
			b->value = right;
			b->next = *bindings;
			*bindings = b;

			Term *t;
			for(t = leftstack; t != nil; t = t->next)
				applybinding(t, b);
			for(t = rightstack; t != nil; t = t->next)
				applybinding(t, b);
			Binding *tmpb;
			for(tmpb = *bindings; tmpb != nil; tmpb = tmpb->next)
				applybinding(tmpb->value, b);
		}else if(left->tag == CompoundTerm && right->tag == CompoundTerm && left->arity == right->arity && runestrcmp(left->text, right->text) == 0){
			Term *leftchild = left->children;
			Term *rightchild = right->children;
			while(leftchild != nil && rightchild != nil){
				Term *t1 = copyterm(leftchild, nil);
				t1->next = leftstack;
				leftstack = t1;
				leftchild = leftchild->next;

				Term *t2 = copyterm(rightchild, nil);
				t2->next = rightstack;
				rightstack = t2;
				rightchild = rightchild->next;
			}
		}else{
			*bindings = nil;
			return 0; /* failure */
		}
	}
	return 1;
}

int
equalterms(Term *a, Term *b)
{
	/* Check that two non-compound terms are identical */
	if(a->tag != b->tag)
		return 0;

	switch(a->tag){
	case AtomTerm:
		return runestrcmp(a->text, b->text) == 0;
	case VariableTerm:
		return (runestrcmp(a->text, b->text) == 0 && a->clausenr == b->clausenr);
	case FloatTerm:
		return a->dval == b->dval;
	case IntegerTerm:
		return a->ival == b->ival;	
	default:
		return 0;
	}
}

void
applybinding(Term *t, Binding *bindings)
{
	if(t->tag == VariableTerm){
		Binding *b;
		for(b = bindings; b != nil; b = b->next){
			if(runestrcmp(t->text, b->name) == 0 && t->clausenr == b->nr){
				Term *next = t->next;
				memcpy(t, b->value, sizeof(Term));
				t->next = next;
				return;
			}
		}
	}else if(t->tag == CompoundTerm){
		Term *child;
		for(child = t->children; child != nil; child = child->next)
			applybinding(child, bindings);
	}
}

Goal *
copygoals(Goal *goals)
{
	if(goals != nil){
		Goal *g = gmalloc(sizeof(Goal));
		g->module = goals->module;
		if(goals->goal)
			g->goal = copyterm(goals->goal, nil);
		else
			g->goal = nil;
		if(goals->catcher)
			g->catcher = copyterm(goals->catcher, nil);
		else
			g->catcher = nil;
		g->next = copygoals(goals->next);
		return g;
	}else
		return nil;
}

void
addchoicepoints(Clause *clause, Term *goal, Goal *goals, Module *mod){
	/* Find all alternative clauses that would have matched, and create a choicepoint for them */
	Choicepoint *cps = nil;
	Choicepoint *last = nil;

	Clause *alt = clause->next;
	while(alt != nil){
		Binding *altbindings = nil;
		clause = findclause(alt, goal, &altbindings);
		if(clause){
			/* Add choicepoint here */
			Choicepoint *cp = gmalloc(sizeof(Choicepoint));
			cp->goalstack = copygoals(goals);
			cp->next = nil;
			cp->alternative = clause;
			cp->altbindings = altbindings;
			cp->id = clause->clausenr;
			cp->currentmodule = mod;
			if(cps == nil){
				cps = cp;
				last = cp;
			}else{
				last->next = cp;
				last = cp;
			}
			alt = clause->next;
		}else
			alt = nil;
	}

	if(last){
		last->next = choicestack;
		choicestack = cps;
	}
}