shithub: pprolog

ref: d5ce41f05bc322fa2fb4d0eee66080b3b3004853
dir: /eval.c/

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

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

typedef struct Binding Binding;
typedef struct Goal Goal;

struct Binding
{
	Rune *name;
	Term *value;
	Binding *next;
};

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

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

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

	while(goals != nil){
		Term *goal = goals->goal;
		goals = goals->next;

		if(goal == nil){
			print("Done with body\n");
			continue;
		}

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

		/* Find a clause where the head unifies with the goal */
		Binding *bindings = nil;
		Term *clause = findclause(database, goal, &bindings);
		if(clause != nil){
			print("Solving it using clause %S with new bindings: ", prettyprint(clause));
			Binding *b;
			for(b = bindings; b != nil; b = b->next){
				print("%S = %S ", b->name, prettyprint(b->value));
			}
			print("\n");
			/* Apply bindings to all goals on the top of the stack, down to the "bodystart" goal */
			Goal *g;
			for(g = goals; g != nil && g->next != 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);
				applybinding(subgoal, bindings);
				goals = addgoals(goals, subgoal);
			}
		}else{
			print("No clause unifies with the goal, backtracking...(not really yet haha)\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;
		print("Added goal: %S\n", prettyprint(t));
		goals = g;
	}
	return goals;
}

Term *
findclause(Term *database, Term *goal, Binding **bindings)
{
	Term *clause;
	for(clause = database; clause != nil; clause = clause->next){
		Term *head;
		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);
	rightstack = copyterm(b);

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

		print("Unifying:\n\t%S\n\t%S\n", prettyprint(left), prettyprint(right));
		if(equalterms(left, right))
			continue;
		else if(left->tag == VariableTerm || right->tag == VariableTerm){
			if(right->tag == VariableTerm){
				Term *tmp = left;
				left = right;
				right = tmp;
			}
			Binding *b = malloc(sizeof(Binding));
			b->name = left->text;
			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);
				t1->next = leftstack;
				leftstack = t1;
				leftchild = leftchild->next;

				Term *t2 = copyterm(rightchild);
				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){
				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);
	}
}