Don't use strings to identify vars, use numbers

9 files changed, 128 insertions, 117 deletions

diff --git a/builtins.c b/builtins.c
index 0256699..7d32d98 100644
--- a/builtins.c
+++ b/builtins.c
@@ -374,12 +374,7 @@ compareterms(Term *t1, Term *t2)
 		/* Same type term */
 		switch(t1->tag){
 		case VariableTerm:
-			if(runestrcmp(t1->text, L"_") == 0 && runestrcmp(t2->text, L"_") == 0)
-				result = 1; /* Special case since _ and _ are always different */
-			else if(t1->clausenr == t2->clausenr)
-				result = runestrcmp(t1->text, t2->text);
-			else
-				result = Compare(t1->clausenr, t2->clausenr);
+			result = Compare(t1->varnr, t2->varnr);
 			break;
 		case FloatTerm:
 			result = Compare(t1->dval, t2->dval);
@@ -465,7 +460,7 @@ builtinfunctor(Term *goal, Binding **bindings, Module *module)
 			int i;
 			Term *args = nil;
 			for(i = 0; i < arity->ival; i++){
-				Term *arg = mkvariable(L"_");
+				Term *arg = mkvariable();
 				args = appendterm(args, arg);
 			}
 			Term *realterm = mkcompound(name->text, arity->ival, args);
@@ -823,77 +818,10 @@ builtinsetoutput(Term *goal, Binding **bindings, Module *module)
 	return 1;
 }
 
-Term *
-readtermvars(Term *t)
-{
-	Term *vars;
-	switch(t->tag){
-	case VariableTerm:
-		vars = copyterm(t, nil);
-		break;
-	case CompoundTerm:
-		vars = nil;
-		int n = t->arity;
-		for(t = t->children; n > 0; t = t->next, n--){
-			Term *childvars = readtermvars(t);
-			while(childvars){
-				Term *childvarscopy = copyterm(childvars, nil);
-				vars = appendterm(vars, childvarscopy);
-				childvars = childvars->next;
-			}
-		}
-		break;
-	default:
-		vars = nil;
-	}
-	return vars;
-}
-
-Term *
-varsandnames(Term *vars)
-{
-	Term *varsnames = nil;
-	Term *var;
-	for(var = vars; var != nil; var = var->next){
-		if(runestrcmp(var->text, L"_") == 0)
-			continue;
-		Term *varname = mkatom(var->text);
-		varname->next = copyterm(var, nil);
-		Term *pair = mkcompound(L"=", 2, varname);
-		varsnames = appendterm(varsnames, pair);
-	}
-	return varsnames;
-}
-
-Term *
-singletons(Term *vars)
-{
-	Term *var;
-	Term *varsnames = varsandnames(vars);
-	Term *singles = nil;
-
-	for(var = varsnames; var != nil; var = var->next){
-		Term *tmp;
-		int duplicate = 0;
-		for(tmp = varsnames; tmp != nil ; tmp = tmp->next){
-			if(tmp == var)
-				continue;
-			if(runestrcmp(var->children->text, tmp->children->text) == 0){
-				duplicate = 1;
-				break;
-			}
-		}
-		if(!duplicate)
-			singles = appendterm(singles, copyterm(var, nil));
-	}
-	return singles;
-}
-
 int
 builtinreadterm(Term *goal, Binding **bindings, Module *module)
 {
 	USED(bindings);
-
 	Term *stream = goal->children;
 	Term *term = stream->next;
 	Term *options = term->next;
@@ -910,7 +838,8 @@ builtinreadterm(Term *goal, Binding **bindings, Module *module)
 		Throw(permissionerror(L"input", L"binary_stream", stream));
 
 	Term *realterm;
-	int error = readterm(stream, &realterm, module);
+	VarName *varnames;
+	int error = readterm(stream, &realterm, module, &varnames);
 	if(error)
 		Throw(realterm);
 
@@ -921,25 +850,16 @@ builtinreadterm(Term *goal, Binding **bindings, Module *module)
 	Term *uniquevars = nil;
 	Term *varsnames = nil;
 	if(options->tag == CompoundTerm){
-		Term *allvars = readtermvars(realterm);
-		Term *tmp1;
-		for(tmp1 = allvars; tmp1 != nil; tmp1 = tmp1->next){
-			Term *tmp2;
-			int duplicate = 0;
-			for(tmp2 = uniquevars; tmp2 != nil; tmp2 = tmp2->next){
-				if(runestrcmp(tmp2->text, tmp1->text) == 0){
-					duplicate = 1;
-					break;
-				}
-			}
-			if(!duplicate){
-				Term *v = copyterm(tmp1, nil);
-				uniquevars = appendterm(uniquevars, v);
-			}
+		VarName *vn;
+		for(vn = varnames; vn != nil; vn = vn->next){
+			uniquevars = appendterm(uniquevars, copyterm(vn->var, nil));
+			Term *name = mkatom(vn->name);
+			name->next = copyterm(vn->var, nil);
+			Term *vnpair = mkcompound(L"=", 2, name);
+			varsnames = appendterm(varsnames, vnpair);
+			if(vn->count == 1)
+				singlevars = appendterm(singlevars, copyterm(vnpair, nil));
 		}
-
-		varsnames = varsandnames(uniquevars);
-		singlevars = singletons(allvars);
 	}
 
 	Term *op;
diff --git a/dat.h b/dat.h
index b2ae80b..2855a3e 100644
--- a/dat.h
+++ b/dat.h
@@ -8,6 +8,7 @@ typedef struct Choicepoint Choicepoint;
 typedef struct Clause Clause;
 typedef struct Predicate Predicate;
 typedef struct Module Module;
+typedef struct VarName VarName;
 typedef int (*Builtin)(Term *, Binding **, Module *);
 
 struct Operator
@@ -35,14 +36,14 @@ struct Term
 	union {
 		vlong ival;
 		double dval;
+		uvlong varnr;
 		struct Compound;
 	};
 };
 
 struct Binding
 {
-	Rune *name;
-	uvlong nr; /* Unique number for each clause. Every time a clause is used, it gets a new number. */
+	uvlong varnr;
 	Term *value;
 	Binding *next;
 };
@@ -93,6 +94,14 @@ struct Module
 	Module *next;
 };
 
+struct VarName
+{
+	Rune *name;
+	Term *var;
+	int count;
+	VarName *next;
+};
+
 /* Operator types */
 enum {
 	Xf	= 1<<0, /* 1 */
diff --git a/eval.c b/eval.c
index 429d98f..c8388e6 100644
--- a/eval.c
+++ b/eval.c
@@ -157,6 +157,7 @@ findclause(Clause *clauses, Term *goal, Binding **bindings)
 	Clause *clause;
 	for(; clauses != nil; clauses = clauses->next){
 		clause = copyclause(clauses, &clausenr);
+		renameclausevars(clause);
 		clausenr++;
 		clause->next = clauses->next;
 		if(unify(clause->head, goal, bindings))
@@ -216,12 +217,8 @@ unify(Term *a, Term *b, Binding **bindings)
 				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->varnr = left->varnr;
 			b->value = right;
 			b->next = *bindings;
 			*bindings = b;
@@ -267,7 +264,7 @@ equalterms(Term *a, Term *b)
 	case AtomTerm:
 		return runestrcmp(a->text, b->text) == 0;
 	case VariableTerm:
-		return (runestrcmp(a->text, b->text) == 0 && a->clausenr == b->clausenr);
+		return a->varnr == b->varnr;
 	case FloatTerm:
 		return a->dval == b->dval;
 	case IntegerTerm:
@@ -283,7 +280,7 @@ 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){
+			if(b->varnr == t->varnr){
 				Term *next = t->next;
 				memcpy(t, b->value, sizeof(Term));
 				t->next = next;
diff --git a/fns.h b/fns.h
index a14f968..a45af7e 100644
--- a/fns.h
+++ b/fns.h
@@ -1,15 +1,16 @@
 /* parser.c */
-Term *parse(Biobuf *, Module *);
+Term *parse(Biobuf *, Module *, VarName **);
 
 /* prettyprint.c */
 Rune *prettyprint(Term *, int, int, int, Module *);
 
 /* misc.c */
 Term *copyterm(Term *, uvlong *);
+void renameclausevars(Clause *);
 Term *appendterm(Term *, Term *);
 int termslength(Term *);
 Term *mkatom(Rune *);
-Term *mkvariable(Rune *);
+Term *mkvariable(void);
 Term *mkcompound(Rune *, int, Term *);
 Term *mkfloat(double);
 Term *mkinteger(vlong);
@@ -58,7 +59,7 @@ int isoutputstream(Term *);
 int istextstream(Term *);
 int isbinarystream(Term *);
 int canreposition(Term *);
-int readterm(Term *, Term **, Module *);
+int readterm(Term *, Term **, Module *, VarName **);
 void writeterm(Term *, Term *, Term *, Module *);
 Rune getchar(Term *);
 Rune peekchar(Term *);
diff --git a/misc.c b/misc.c
index f25c583..bf7010f 100644
--- a/misc.c
+++ b/misc.c
@@ -5,6 +5,8 @@
 #include "dat.h"
 #include "fns.h"
 
+static uvlong varnr = 0;
+
 Term *
 copyterm(Term *orig, uvlong *clausenr)
 {
@@ -18,17 +20,71 @@ copyterm(Term *orig, uvlong *clausenr)
 	else
 		new->clausenr = orig->clausenr;
 
-	Term *child;
-	for(child = orig->children; child != nil; child = child->next)
-		new->children = appendterm(new->children, copyterm(child, clausenr));
+	if(orig->tag == CompoundTerm){
+		Term *child;
+		for(child = orig->children; child != nil; child = child->next)
+			new->children = appendterm(new->children, copyterm(child, clausenr));
+	}
 	return new;
 }
 
+uvlong
+smallestvar(Term *t)
+{
+	if(t == nil)
+		return varnr;
+
+	if(t->tag == VariableTerm)
+		return t->varnr;
+	if(t->tag == CompoundTerm){
+		Term *child;
+		uvlong min = varnr;
+		for(child = t->children; child != nil; child = child->next){
+			uvlong v = smallestvar(child);
+			if(v < min)
+				min = v;
+		}
+		return min;
+	}else
+		return varnr;
+}
+
+void
+addvarnr(Term *t, uvlong offset)
+{
+	if(t == nil)
+		return;
+
+	if(t->tag == VariableTerm){
+		t->varnr += offset;
+		if(t->varnr >= varnr)
+			varnr = t->varnr+1;
+	}
+	if(t->tag == CompoundTerm){
+		Term *child;
+		for(child = t->children; child != nil; child = child->next)
+			addvarnr(child, offset);
+	}
+}
+
+void
+renameclausevars(Clause *c)
+{
+	uvlong minhead = smallestvar(c->head);
+	uvlong minbody = smallestvar(c->body);
+	uvlong minvar = minhead < minbody ? minhead : minbody;
+	uvlong offset = varnr - minvar;
+	addvarnr(c->head, offset);
+	addvarnr(c->body, offset);
+}
+
 Term *
 appendterm(Term *a, Term *b)
 {
 	if(a == nil)
 		return b;
+	if(b == nil)
+		return a;
 
 	Term *tmp;
 	for(tmp = a; tmp->next != nil; tmp = tmp->next);
@@ -54,6 +110,7 @@ mkterm(int tag)
 	t->text = nil;
 	t->clausenr = 0;
 	t->inparens = 0;
+	t->varnr = 0;
 	return t;
 }
 
@@ -66,10 +123,10 @@ mkatom(Rune *name)
 }
 
 Term *
-mkvariable(Rune *name)
+mkvariable(void)
 {
 	Term *t = mkterm(VariableTerm);
-	t->text = name;
+	t->varnr = varnr++;
 	return t;
 }
 
diff --git a/module.c b/module.c
index e255483..ead591e 100644
--- a/module.c
+++ b/module.c
@@ -32,7 +32,8 @@ addtousermod(char *file)
 	Predicate *currentpred = nil;
 
 	Term *t;
-	while(t = parse(bio, usermodule)){
+	VarName *varnames;
+	while(t = parse(bio, usermodule, &varnames)){
 		Clause *cl = gmalloc(sizeof(Clause));
 		int arity;
 		cl->clausenr = 0;
diff --git a/parser.c b/parser.c
index 51eb436..9ce68f1 100644
--- a/parser.c
+++ b/parser.c
@@ -42,6 +42,7 @@ enum {
 static Biobuf *parsein;
 static Token lookahead;
 static Module *currentmod;
+static VarName *varnames;
 
 void nexttoken(void);
 Term *fullterm(int, Rune *, Term *);
@@ -49,19 +50,22 @@ Term *term(void);
 Term *listterm(int);
 Term *curlybracketterm(void);
 Term *compound(void);
+Term *parsevar(void);
 Term *parseoperators(Term *);
 void match(int);
 void syntaxerror_parser(char *);
 Term *parseterm(void);
 
 Term *
-parse(Biobuf *bio, Module *mod)
+parse(Biobuf *bio, Module *mod, VarName **vns)
 {
 	parsein = bio;
 	currentmod = mod;
+	varnames = nil;
 	nexttoken();
 
 	Term *result = parseterm();
+	*vns = varnames;
 	if(result){
 		result = copyterm(result, &clausenr);
 		clausenr++;
@@ -107,8 +111,7 @@ term(void)
 		result = compound();
 		break;
 	case VarTok:
-		result = mkvariable(lookahead.text);
-		match(VarTok);
+		result = parsevar();
 		break;
 	case IntTok:
 		result = mkinteger(lookahead.ival);
@@ -202,6 +205,29 @@ compound(void)
 }
 
 Term *
+parsevar(void)
+{
+	Rune *name = lookahead.text;
+	match(VarTok);
+
+	VarName *vn;
+	uvlong i = 0;
+	for(vn = varnames; vn != nil; vn = vn->next, i++)
+		if(runestrcmp(vn->name, name) == 0 && !runestrcmp(vn->name, L"_") == 0){
+			vn->count++;
+			return copyterm(vn->var, nil);
+		}
+
+	VarName *new = gmalloc(sizeof(VarName));
+	new->name = name;
+	new->var = mkvariable();
+	new->count = 1;
+	new->next = varnames;
+	varnames = new;
+	return new->var;
+}
+
+Term *
 parseoperators(Term *list)
 {
 	int i;
diff --git a/prettyprint.c b/prettyprint.c
index b980f1e..01fed46 100644
--- a/prettyprint.c
+++ b/prettyprint.c
@@ -75,7 +75,7 @@ prettyprint(Term *t, int quoted, int ignoreops, int numbervars, Module *mod)
 			result = runesmprint("%S", t->text);
 		break;
 	case VariableTerm:
-		result = runesmprint("_%S", t->text);
+		result = runesmprint("_%ulld", t->varnr);
 		break;
 	case FloatTerm:
 		result = runesmprint("%f", t->dval);
diff --git a/streams.c b/streams.c
index 4b4b965..29e8746 100644
--- a/streams.c
+++ b/streams.c
@@ -217,14 +217,14 @@ canreposition(Term *t)
 }
 
 int
-readterm(Term *stream, Term **term, Module *mod)
+readterm(Term *stream, Term **term, Module *mod, VarName **vns)
 {
 	Stream *s = getstream(stream);
 	if(s == nil){
 		*term = existenceerror(L"stream", stream);
 		return 1;
 	}
-	*term = parse(s->bio, mod);
+	*term = parse(s->bio, mod, vns);
 
 	return 0;
 }