shithub: pprolog

ref: 79d1fe1cf2eb6748e2c12ffe9c36a678655302b1
dir: /eval.c/

#include <u.h>
#include <libc.h>

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

typedef struct Binding Binding;
typedef struct Goal Goal;
typedef struct Choicepoint Choicepoint;

struct Binding
{
	Rune *name;
	uvlong nr; /* Unique number for each clause. Every time a clause is used, it gets a new number. */
	Term *value;
	Binding *next;
};

struct Goal
{
	Term *goal;
	Goal *next;
};

struct Choicepoint
{
	Goal *goalstack;
	Term *retryclause;
	Choicepoint *next;
};

Goal *addgoals(Goal *, Term *);
Term *findclause(Term *, Term *, Binding **);
int unify(Term *, Term *, Binding **);
int equalterms(Term *, Term *);
void applybinding(Term *, Binding *);
Goal *copygoals(Goal *);

static uvlong clausenr;

void
evalquery(Term *database, Term *query)
{
	Goal *goals = addgoals(nil, query);
	Choicepoint *choicestack = nil;

	clausenr = 0;

	while(goals != nil){
		Term *dbstart;
		Term *goal;

		dbstart = database;
Retry:
		goal = goals->goal;

		if(goal == nil){
			goals = goals->next;
			continue;
		}

		print("Solving goal %S\n", prettyprint(goal));

		/* Find a clause where the head unifies with the goal */
		Binding *bindings = nil;
		Term *clause = findclause(dbstart, goal, &bindings);
		if(clause != nil){
			if(clause->next != nil){
				/* Add a choicepoint. Note we create a choicepoint every time, so there is room for improvement. */
				Choicepoint *cp = malloc(sizeof(Choicepoint));
				cp->goalstack = copygoals(goals);
				cp->next = choicestack;
				cp->retryclause = clause->next;
				choicestack = cp;
			}
			goals = goals->next;
			/* Apply bindings to all goals on the top of the stack, down to the "bodystart" goal */
			Goal *g;
			for(g = goals; g != nil && g->goal != nil; g = g->next)
				applybinding(g->goal, bindings);
			
			/* Add clause body as goals, with bindings applied */
			if(clause->tag == CompoundTerm && clause->arity == 2 && runestrcmp(clause->text, L":-") == 0){
				Goal *bodystart = malloc(sizeof(Goal));
				bodystart->goal = nil;
				bodystart->next = goals;
				goals = bodystart;

				Term *subgoal = copyterm(clause->children->next, nil);
				applybinding(subgoal, bindings);
				goals = addgoals(goals, subgoal);
			}
		}else{
			if(choicestack == nil){
				print("Fail\n");
				return;
			}
			print("Backtracking...\n");
			Choicepoint *cp = choicestack;
			choicestack = cp->next;
			/* freegoals(goals) */
			goals = cp->goalstack;
			dbstart = cp->retryclause;

			goto Retry;
		}
	}
	print("Success.\n");
}

Goal *
addgoals(Goal *goals, Term *t)
{
	if(t->tag == CompoundTerm && runestrcmp(t->text, L",") == 0 && t->arity == 2){
		goals = addgoals(goals, t->children->next);
		goals = addgoals(goals, t->children);
	}else{
		Goal *g = malloc(sizeof(Goal));
		g->goal = t;
		g->next = goals;
		goals = g;
	}
	return goals;
}

Term *
findclause(Term *database, Term *goal, Binding **bindings)
{
	Term *clause;
	Term *head;
	for(; database != nil; database = database->next){
		clausenr++;
		clause = copyterm(database, &clausenr);
		clause->next = database->next;
		if(clause->tag == CompoundTerm && runestrcmp(clause->text, L":-") == 0 && clause->arity == 2)
			head = clause->children;
		else
			head = clause;

		if(unify(head, goal, bindings))
			return clause;
	}
	return nil;
}

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

	*bindings = nil;
	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(right->tag == VariableTerm){
				Term *tmp = left;
				left = right;
				right = tmp;
			}

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

			Binding *b = malloc(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
			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:
	case VariableTerm:
	case StringTerm:
		return !runestrcmp(a->text, b->text);
	case NumberTerm:
		if(a->numbertype != b->numbertype)
			return 0;
		if(a->numbertype == NumberInt && a->ival == b->ival)
			return 1;
		if(a->numbertype == NumberFloat && a->dval == b->dval)
			return 1;
		return 0;	
	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 = malloc(sizeof(Goal));
		if(goals->goal)
			g->goal = copyterm(goals->goal, nil);
		else
			g->goal = nil;
		g->next = copygoals(goals->next);
		return g;
	}else
		return nil;
}