ref: 9fd0e7fc78740ec3a0a1a5e97d571d0f9d02b85a
dir: pprolog/eval.c
#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 **resultbindings)
{
if(choicestack == nil){
/*
The goal stack has the original query at the very bottom, protected by a catch frame where 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.
*/
goalstack = gmalloc(sizeof(Goal));
goalstack->goal = copyterm(query, nil);
goalstack->module = usermodule;
goalstack->catcher = nil;
goalstack->next = nil;
Goal *protector = gmalloc(sizeof(Goal));
protector->goal = nil;
protector->module = usermodule;
protector->catcher = mkvariable(L"catch-var");
protector->next = goalstack;
goalstack = protector;
/* Now add the actual goals */
goalstack = addgoals(goalstack, query, usermodule);
}else{
goto Backtrack;
}
while(goalstack->goal != nil){
Term *goal = goalstack->goal;
Term *catcher = goalstack->catcher;
Module *module = goalstack->module;
goalstack = goalstack->next;
if(catcher)
continue;
if(debug)
print("Working goal: %S:%S\n", module->name, prettyprint(goal, 0, 0, 0));
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){
print("No predicate matches: %S:%S\n", module->name, prettyprint(goal, 0, 0, 0));
goto Backtrack;
}
/* 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(debug)
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, resultbindings);
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;
}
}