Better error reporting when unification fails (report both locations, and preserve locations during substitution).

git-svn-id: http://svn.drobilla.net/resp/resp@256 ad02d1e2-f140-0410-9f75-f8b11f17cedd

6 files changed, 72 insertions, 36 deletions

diff --git a/src/constrain.cpp b/src/constrain.cpp
index 024dce4..d0490bf 100644
--- a/src/constrain.cpp
+++ b/src/constrain.cpp
@@ -126,7 +126,7 @@ ACall::constrain(TEnv& tenv, Constraints& c) const throw(Error)
 				(format("expected %1% arguments, got %2%") % numArgs % (size() - 1)).str());
 	}
 
-	const AType* retT  = tenv.var();
+	const AType* retT  = tenv.var(this);
 	AType*       argsT = tup<AType>(loc, 0);
 	for (const_iterator i = begin() + 1; i != end(); ++i)
 		argsT->push_back(const_cast<AType*>(tenv.var(*i)));
@@ -146,7 +146,6 @@ ADef::constrain(TEnv& tenv, Constraints& c) const throw(Error)
 	tenv.def(sym, tvar);
 	body()->constrain(tenv, c);
 	c.constrain(tenv, sym, tvar);
-	c.constrain(tenv, this, tenv.named("Nothing"));
 }
 
 void
diff --git a/src/lift.cpp b/src/lift.cpp
index 6a53165..7e7ec57 100644
--- a/src/lift.cpp
+++ b/src/lift.cpp
@@ -81,7 +81,6 @@ AFn::lift(CEnv& cenv, Code& code) throw()
 	 */
 	impl->prot()->push_front(cenv.penv.sym("_"));
 
-
 	// Lift body
 	const AType* implRetT = NULL;
 	iterator ci = impl->begin() + 2;
diff --git a/src/repl.cpp b/src/repl.cpp
index 92fb621..472d1a5 100644
--- a/src/repl.cpp
+++ b/src/repl.cpp
@@ -38,7 +38,17 @@ readParseType(CEnv& cenv, Cursor& cursor, istream& is, AST*& exp, AST*& ast)
 	Constraints c(cenv.tsubst);
 	ast->constrain(cenv.tenv, c); // Constrain types
 
-	cenv.tsubst = unify(c); // Solve type constraints
+	const Subst subst = unify(c); // Solve type constraints
+	for (Subst::const_iterator i = subst.begin(); i != subst.end(); ++i) {
+		if (!cenv.tsubst.contains(i->first)) {
+			//cout << "New variable " << i->first << " = " << i->second << endl;
+			cenv.tsubst.push_back(*i);
+		}
+	}
+
+	//cout << "**** SUBST\n" << subst << "********" << endl;
+	//cout << "**** CENV.SUBST\n" << cenv.tsubst << "********" << endl;
+	//cenv.tsubst = Subst::compose(cenv.tsubst, subst);
 
 	// Add types in type substition as GC roots
 	for (Subst::iterator i = cenv.tsubst.begin(); i != cenv.tsubst.end(); ++i) {
@@ -74,8 +84,8 @@ eval(CEnv& cenv, const string& name, istream& is, bool execute)
 		while (readParseType(cenv, cursor, is, exp, ast))
 			parsed.push_back(ast);
 
-		//for (list< pair<SExp, AST*> >::const_iterator i = parsed.begin(); i != parsed.end(); ++i)
-		//	pprint(cout, i->second->cps(cenv.tenv, cenv.penv.sym("cont")));
+		/*for (list<AST*>::const_iterator i = parsed.begin(); i != parsed.end(); ++i)
+			pprint(cout, (*i)->cps(cenv.tenv, cenv.penv.sym("halt")));*/
 
 		CVal  val = NULL;
 		CFunc f   = NULL;
@@ -89,10 +99,18 @@ eval(CEnv& cenv, const string& name, istream& is, bool execute)
 				concrete.push_back(c);
 		}
 
-		cout << endl << ";;;; CONCRETE {" << endl << endl;
-		for (Code::iterator i = concrete.begin(); i != concrete.end(); ++i)
-			cout << *i << endl << endl;
-		cout << ";;;; } CONCRETE" << endl << endl;*/
+		if (cenv.args.find("-d") != cenv.args.end()) {
+			cout << endl << ";;;; CONCRETE {" << endl << endl;
+			for (Code::iterator i = concrete.begin(); i != concrete.end(); ++i) {
+				cout << *i << endl;
+				ADef* def = (*i)->to<ADef*>();
+				if (def)
+					std::cout << " :: " << cenv.type(def->body()) << std::endl;
+				cout << endl;
+			}
+			cout << ";;;; } CONCRETE" << endl << endl;
+		}
+		*/
 
 		// Lift all expressions
 		Code lifted;
diff --git a/src/resp.hpp b/src/resp.hpp
index f172548..1edf9e6 100644
--- a/src/resp.hpp
+++ b/src/resp.hpp
@@ -339,7 +339,7 @@ struct AType : public ATuple {
 	AType(Cursor c, unsigned i) : ATuple(c), kind(VAR), id(i) {}
 	AType(Cursor c, Kind k=EXPR) : ATuple(c), kind(k), id(0) {}
 	AType(Cursor c, AST* ast, va_list args) : ATuple(c, ast, args), kind(EXPR), id(0) {}
-	AType(const AType& copy) : ATuple(copy), kind(copy.kind), id(copy.id) {}
+	AType(const AType& copy) : ATuple(copy), kind(copy.kind), id(copy.id) { }
 	CVal compile(CEnv& cenv) throw() { return NULL; }
 	const ATuple* prot() const { assert(kind == EXPR); return (*(begin() + 1))->to<const ATuple*>(); }
 	ATuple*       prot()       { assert(kind == EXPR); return (*(begin() + 1))->to<ATuple*>(); }
@@ -556,18 +556,17 @@ struct PEnv : private map<const string, ASymbol*> {
 
 /// Type constraint
 struct Constraint : public pair<const AType*,const AType*> {
-	Constraint(const AType* a, const AType* b, Cursor c)
-		: pair<const AType*, const AType*>(a, b), loc(c) {}
-	Cursor loc;
+	Constraint(const AType* a, const AType* b)
+		: pair<const AType*, const AType*>(a, b) {}
 };
 
 /// Type substitution
 struct Subst : public list<Constraint> {
 	Subst(const AType* s=0, const AType* t=0) {
-		if (s && t) { assert(s != t); push_back(Constraint(s, t, t->loc)); }
+		if (s && t) { assert(s != t); push_back(Constraint(s, t)); }
 	}
 	static Subst compose(const Subst& delta, const Subst& gamma);
-	void add(const AType* from, const AType* to) { push_back(Constraint(from, to, Cursor())); }
+	void add(const AType* from, const AType* to) { push_back(Constraint(from, to)); }
 	const_iterator find(const AType* t) const {
 		for (const_iterator j = begin(); j != end(); ++j)
 			if (*j->first == *t)
@@ -592,6 +591,14 @@ struct Subst : public list<Constraint> {
 			}
 		}
 	}
+	bool contains(const AType* type) const {
+		if (find(type) != end())
+			return true;
+		FOREACHP(const_iterator, j, this)
+			if (*j->second == *type || j->second->contains(type))
+				return true;
+		return false;
+	}
 };
 
 inline ostream& operator<<(ostream& out, const Subst& s) {
@@ -604,13 +611,12 @@ inline ostream& operator<<(ostream& out, const Subst& s) {
 struct Constraints : public list<Constraint> {
 	Constraints() : list<Constraint>() {}
 	Constraints(const Subst& subst) : list<Constraint>() {
-		FOREACH(Subst::const_iterator, i, subst) {
-			push_back(Constraint(new AType(*i->first), new AType(*i->second), Cursor()));
-		}
+		FOREACH(Subst::const_iterator, i, subst)
+			push_back(Constraint(new AType(*i->first), new AType(*i->second)));
 	}
 	Constraints(const_iterator begin, const_iterator end) : list<Constraint>(begin, end) {}
 	void constrain(TEnv& tenv, const AST* o, const AType* t);
-	Constraints replace(const AType* s, const AType* t);
+	Constraints& replace(const AType* s, const AType* t);
 };
 
 inline ostream& operator<<(ostream& out, const Constraints& c) {
@@ -713,7 +719,11 @@ struct CEnv {
 	Engine* engine() { return _engine; }
 	void    push() { code.push(); tenv.push(); vals.push(); }
 	void    pop()  { code.pop(); tenv.pop();  vals.pop();  }
-	void    lock(AST* ast) { Object::pool.addRoot(ast); Object::pool.addRoot(type(ast)); }
+	void    lock(AST* ast) {
+		Object::pool.addRoot(ast);
+		if (type(ast))
+				Object::pool.addRoot(type(ast));
+	}
 	const AType* type(AST* ast, const Subst& subst = Subst()) const {
 		ASymbol* sym = ast->to<ASymbol*>();
 		if (sym) {
diff --git a/src/unify.cpp b/src/unify.cpp
index 1b25861..aadc032 100644
--- a/src/unify.cpp
+++ b/src/unify.cpp
@@ -61,7 +61,7 @@ Constraints::constrain(TEnv& tenv, const AST* o, const AType* t)
 	assert(o);
 	assert(t);
 	assert(!o->to<const AType*>());
-	push_back(Constraint(tenv.var(o), t, o->loc));
+	push_back(Constraint(tenv.var(o), t));
 }
 
 template<typename T, typename E>
@@ -73,7 +73,9 @@ substitute(const T* tup, const E* from, const E* to)
 	typename T::iterator ri = ret->begin();
 	FOREACHP(typename T::const_iterator, i, tup) {
 		if (**i == *from) {
-			*ri++ = const_cast<E*>(to);
+			T* type = new T(*to);
+			type->loc = (*i)->loc;
+			*ri++ = type;
 		} else if (static_cast<const E*>(*i) != static_cast<const E*>(to)) {
 			const T* subTup = dynamic_cast<const T*>(*i);
 			if (subTup)
@@ -104,17 +106,24 @@ Subst::compose(const Subst& delta, const Subst& gamma)
 }
 
 /// Replace all occurrences of @a s with @a t
-Constraints
+Constraints&
 Constraints::replace(const AType* s, const AType* t)
 {
-	Constraints cp(*this);
-	for (Constraints::iterator c = begin(); c != end();) {
-		Constraints::iterator next = c; ++next;
-		if (*c->first  == *s) c->first  = t;
-		if (*c->second == *s) c->second = t;
-		c->first = substitute(c->first, s, t);
-		c->second = substitute(c->second, s, t);
-		c = next;
+	for (Constraints::iterator c = begin(); c != end(); ++c) {
+		if (*c->first == *s) {
+			AType* type = new AType(*t);
+			type->loc = c->first->loc;
+			c->first = type;
+		} else {
+			c->first = substitute(c->first, s, t);
+		}
+		if (*c->second == *s) {
+			AType* type = new AType(*t);
+			type->loc = c->second->loc;
+			c->second = type;
+		} else {
+			c->second = substitute(c->second, s, t);
+		}
 	}
 	return *this;
 }
@@ -146,12 +155,13 @@ unify(const Constraints& constraints)
 			if (st->kind == AType::DOTS || tt->kind == AType::DOTS)
 				return unify(cp);
 			else
-				cp.push_back(Constraint(st, tt, st->loc));
+				cp.push_back(Constraint(st, tt));
 		}
 		if (si == s->end() && (ti == t->end() || (*ti)->as<AType*>()->kind == AType::DOTS)
 				|| ti == t->end() && (*si)->as<AType*>()->kind == AType::DOTS)
 			return unify(cp);
 	}
-	throw Error(s->loc ? s->loc : t->loc,
-			(format("type is `%1%' but should be `%2%'") % s->str() % t->str()).str());
+	throw Error(s->loc,
+			(format("type is `%1%' but should be `%2%'\n%3%: error: to match `%4%' here")
+			 % s->str() % t->str() % t->loc.str() % t->str()).str());
 }
diff --git a/test/poly.resp b/test/poly.resp
index 33922e3..1857fdf 100644
--- a/test/poly.resp
+++ b/test/poly.resp
@@ -1,4 +1,4 @@
-(def eq (fn (x y) (= x y)))
+(def (eq x y) (= x y))
 
 (eq 1 2)
 (eq 1 1)