ref: 85adea62d7e8eee9d0e3525d572325db4e58d21a
dir: pprolog/eval.c
#include <u.h>
#include <libc.h>
#include "dat.h"
#include "fns.h"
Goal *addgoals(Goal *, Term *);
Term *findclause(Term *, Term *, Binding **);
int equalterms(Term *, Term *);
void applybinding(Term *, Binding *);
Goal *copygoals(Goal *);
Builtin findbuiltin(Term *);
static uvlong clausenr;
int
evalquery(Term *database, Term *query, Binding **resultbindings, Choicepoint **resultchoicestack)
{
Goal *goals;
Choicepoint *choicestack = *resultchoicestack;
if(choicestack == nil){
/*
The goal stack has the original query at the very bottom, protected by a goal there the ->goal field is nil.
This makes it so that we can continue until we hit the protective goal, at which point we have solved everything
and to get the result we can unify the original query with the one at the bottom of the stack, to get the bindings
applied.
*/
goals = malloc(sizeof(Goal));
goals->goal = copyterm(query, nil);
goals->next = nil;
Goal *protector = malloc(sizeof(Goal));
protector->goal = nil;
protector->next = goals;
goals = protector;
/* Now add the actual goals */
goals = addgoals(goals, query);
clausenr = 2; /* Start at two since 0 is for the facts in the database, and 1 is for queries */
}else{
goto Backtrack;
}
while(goals->goal != nil){
Term *dbstart;
Term *goal;
dbstart = database;
Retry:
goal = goals->goal;
if(debug)
print("Working goal: %S\n", prettyprint(goal));
Binding *bindings = nil;
Term *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(database, goal, &goals->next, &choicestack, &bindings);
if(!success)
goto Backtrack;
}else{
/* Find a clause where the head unifies with the goal */
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;
cp->id = clause->clausenr;
choicestack = cp;
}
}else{
Backtrack:
if(choicestack == nil)
return 0;
if(debug)
print("Backtracking..\n");
Choicepoint *cp = choicestack;
choicestack = cp->next;
/* freegoals(goals) */
goals = cp->goalstack;
dbstart = cp->retryclause;
goto Retry;
}
}
goals = goals->next;
/* Apply bindings to all goals on the stack. */
Goal *g;
for(g = goals; g != nil; g = g->next){
if(g->goal != nil)
applybinding(g->goal, bindings);
}
/* Add clause body as goals, with bindings applied */
if(clause != nil && clause->tag == CompoundTerm && clause->arity == 2 && runestrcmp(clause->text, L":-") == 0){
Term *subgoal = copyterm(clause->children->next, nil);
applybinding(subgoal, bindings);
goals = addgoals(goals, subgoal);
}
}
goals = goals->next;
unify(query, goals->goal, resultbindings);
*resultchoicestack = choicestack;
return 1;
}
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){
clause = copyterm(database, &clausenr);
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;
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 StringTerm:
return !runestrcmp(a->text, b->text);
case VariableTerm:
return (runestrcmp(a->text, b->text) == 0 && a->clausenr == b->clausenr);
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;
}