shithub: pprolog

--- a/dat.h

+++ b/dat.h

@@ -10,6 +10,7 @@

 	int numbertype;

 	vlong ival;

 	double dval;

+	uvlong clausenr;

};

 enum {

--- a/eval.c

+++ b/eval.c

@@ -6,10 +6,12 @@

 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;

};

@@ -20,23 +22,40 @@

 	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 *goal = goals->goal;

-		goals = goals->next;

+		Term *dbstart;

+		Term *goal;

+		dbstart = database;

+Retry:

+		goal = goals->goal;

 		if(goal == nil){

-			print("Done with body\n");

+			goals = goals->next;

 			continue;

@@ -44,17 +63,20 @@

 		/* Find a clause where the head unifies with the goal */

 		Binding *bindings = nil;

-		Term *clause = findclause(database, goal, &bindings);

+		Term *clause = findclause(dbstart, 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));

+			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;

-			print("\n");

+			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->next != nil; g = g->next)

+			for(g = goals; g != nil && g->goal != nil; g = g->next)

 				applybinding(g->goal, bindings);

 			/* Add clause body as goals, with bindings applied */

@@ -64,14 +86,26 @@

 				bodystart->next = goals;

 				goals = bodystart;

-				Term *subgoal = copyterm(clause->children->next);

+				Term *subgoal = copyterm(clause->children->next, nil);

 				applybinding(subgoal, bindings);

 				goals = addgoals(goals, subgoal);

 		}else{

-			print("No clause unifies with the goal, backtracking...(not really yet haha)\n");

+			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 *

@@ -84,7 +118,6 @@

 		Goal *g = malloc(sizeof(Goal));

 		g->goal = t;

 		g->next = goals;

-		print("Added goal: %S\n", prettyprint(t));

 		goals = g;

 	return goals;

@@ -94,8 +127,11 @@

 findclause(Term *database, Term *goal, Binding **bindings)

 	Term *clause;

-	for(clause = database; clause != nil; clause = clause->next){

-		Term *head;

+	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

@@ -116,8 +152,8 @@

 	Term *right;

 	*bindings = nil;

-	leftstack = copyterm(a);

-	rightstack = copyterm(b);

+	leftstack = copyterm(a, nil);

+	rightstack = copyterm(b, nil);

 	while(leftstack != nil && rightstack != nil){

 		left = leftstack;

@@ -125,7 +161,6 @@

 		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){

@@ -136,6 +171,7 @@

 			Binding *b = malloc(sizeof(Binding));

 			b->name = left->text;

+			b->nr = left->clausenr;

 			b->value = right;

 			b->next = *bindings;

 			*bindings = b;

@@ -151,12 +187,12 @@

 			Term *leftchild = left->children;

 			Term *rightchild = right->children;

 			while(leftchild != nil && rightchild != nil){

-				Term *t1 = copyterm(leftchild);

+				Term *t1 = copyterm(leftchild, nil);

 				t1->next = leftstack;

 				leftstack = t1;

 				leftchild = leftchild->next;

-				Term *t2 = copyterm(rightchild);

+				Term *t2 = copyterm(rightchild, nil);

 				t2->next = rightstack;

 				rightstack = t2;

 				rightchild = rightchild->next;

@@ -198,7 +234,7 @@

 	if(t->tag == VariableTerm){

 		Binding *b;

 		for(b = bindings; b != nil; b = b->next){

-			if(runestrcmp(t->text, b->name) == 0){

+			if(runestrcmp(t->text, b->name) == 0 && t->clausenr == b->nr){

 				Term *next = t->next;

 				memcpy(t, b->value, sizeof(Term));

 				t->next = next;

@@ -210,4 +246,19 @@

 		for(child = t->children; child != nil; child = child->next)

 			applybinding(child, bindings);

-}

\ No newline at end of file

+}

+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;

+}

--- a/example.pl

+++ b/example.pl

@@ -25,4 +25,10 @@

 =(A,A).

-:- initialization(could_be_friends(bob, sam)).

\ No newline at end of file

+length([], zero).

+length([Head|Tail], suc(Length)) :-

+	length(Tail, Length).

+:- initialization(could_be_friends(bob, sam)).

+:- initialization(length([a,b,c,d], Len)).

--- a/fns.h

+++ b/fns.h

@@ -5,7 +5,7 @@

 Rune *prettyprint(Term *);

 /* misc.c */

-Term *copyterm(Term *);

+Term *copyterm(Term *, uvlong *);

 Term *appendterm(Term *, Term *);

 int termslength(Term *);

 Term *mkatom(Rune *);

--- a/main.c

+++ b/main.c

@@ -30,10 +30,7 @@

 		if(fd < 0)

 			exits("open");

 		Term *prog = parse(fd);

-		Term *clause;

-		for(clause = prog; clause != nil; clause = clause->next)

-			print("%S.\n", prettyprint(clause));

 		Term *goal;

 		for(goal = initgoals; goal != nil; goal = goal->next)

 			evalquery(prog, goal);

--- a/misc.c

+++ b/misc.c

@@ -5,7 +5,7 @@

 #include "fns.h"

 Term *

-copyterm(Term *orig)

+copyterm(Term *orig, uvlong *clausenr)

 	Term *new = malloc(sizeof(Term));

 	memcpy(new, orig, sizeof(Term));

@@ -12,9 +12,14 @@

 	new->next = nil;

 	new->children = nil;

+	if(clausenr)

+		new->clausenr = *clausenr;

+	else

+		new->clausenr = orig->clausenr;

 	Term *child;

 	for(child = orig->children; child != nil; child = child->next)

-		new->children = appendterm(new->children, copyterm(child));

+		new->children = appendterm(new->children, copyterm(child, clausenr));

 	return new;

@@ -46,6 +51,7 @@

 	t->next = nil;

 	t->children = nil;

 	t->text = nil;

+	t->clausenr = 0;

 	return t;

--- a/prettyprint.c

+++ b/prettyprint.c

@@ -19,8 +19,10 @@

 		free(args);

 		break;

 	case AtomTerm:

-	case VariableTerm:

 		result = runesmprint("%S", t->text);

+		break;

+	case VariableTerm:

+		result = runesmprint("%S(%ulld)", t->text, t->clausenr);

 		break;

 	case NumberTerm:

 		if(t->numbertype == NumberInt)