/* Resp Unification
 * Copyright (C) 2008-2009 David Robillard <dave@drobilla.net>
 *
 * Resp is free software: you can redistribute it and/or modify it under
 * the terms of the GNU Affero General Public License as published by the
 * Free Software Foundation, either version 3 of the License, or (at your
 * option) any later version.
 *
 * Resp is distributed in the hope that it will be useful, but WITHOUT
 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
 * or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU Affero General
 * Public License for more details.
 *
 * You should have received a copy of the GNU Affero General Public License
 * along with Resp.  If not, see <http://www.gnu.org/licenses/>.
 */

/** @file
 * @brief Unify type constraints
 */

#include <set>
#include "resp.hpp"

/** Build a type substitution for calling a generic function type
 * with a specific set of argument types
 */
Subst
TEnv::buildSubst(const AType* genericT, const AType& argsT)
{
	Subst subst;

	// Build substitution to apply to generic type
	const ATuple* genericProtT = (*(genericT->begin() + 1))->as<const ATuple*>();
	ATuple::const_iterator g = genericProtT->begin();
	AType::const_iterator  a = argsT.begin();
	for (; a != argsT.end(); ++a, ++g) {
		const AType* genericArgT = (*g)->to<const AType*>();
		AType*       callArgT    = (*a)->to<AType*>();
		if (callArgT->kind == AType::EXPR) {
			assert(genericArgT->kind == AType::EXPR);
			ATuple::const_iterator gi = genericArgT->begin();
			ATuple::const_iterator ci = callArgT->begin();
			for (; gi != genericArgT->end(); ++gi, ++ci) {
				const AType* gT = (*gi)->to<const AType*>();
				AType*       aT = (*ci)->to<AType*>();
				if (gT && aT)
					subst.add(gT, aT);
			}
		} else {
			subst.add(genericArgT, callArgT);
		}
	}

	return subst;
}

void
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));
}

template<typename T, typename E>
static const T*
substitute(const T* tup, const E* from, const E* to)
{
	if (!tup) return NULL;
	T* ret = new T(*tup);
	typename T::iterator ri = ret->begin();
	FOREACHP(typename T::const_iterator, i, tup) {
		if (**i == *from) {
			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)
				*ri++ = const_cast<E*>(substitute(subTup, from, to));
			else
				*ri++ = *i;
		} else {
			++ri;
		}
	}
	return ret;
}

/// Compose two substitutions (TAPL 22.1.1)
Subst
Subst::compose(const Subst& delta, const Subst& gamma)
{
	Subst r;
	for (Subst::const_iterator g = gamma.begin(); g != gamma.end(); ++g) {
		Subst::const_iterator d = delta.find(g->second);
		r.add(g->first, ((d != delta.end()) ? d : g)->second);
	}
	for (Subst::const_iterator d = delta.begin(); d != delta.end(); ++d) {
		if (gamma.find(d->first) == gamma.end())
			r.add(d->first, d->second);
	}
	return r;
}

/// Replace all occurrences of @a s with @a t
Constraints&
Constraints::replace(const AType* s, const AType* t)
{
	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;
}

/// Unify a type constraint set (TAPL 22.4)
Subst
unify(const Constraints& constraints)
{
	if (constraints.empty())
		return Subst();

	Constraints::const_iterator i  = constraints.begin();
	const AType*                s  = i->first;
	const AType*                t  = i->second;
	Constraints                 cp(++i, constraints.end());

	if (*s == *t) {
		return unify(cp);
	} else if (s->kind == AType::VAR && !t->contains(s)) {
		return Subst::compose(unify(cp.replace(s, t)), Subst(s, t));
	} else if (t->kind == AType::VAR && !s->contains(t)) {
		return Subst::compose(unify(cp.replace(t, s)), Subst(t, s));
	} else if (s->kind == AType::EXPR && t->kind == AType::EXPR) {
		AType::const_iterator si = s->begin() + 1;
		AType::const_iterator ti = t->begin() + 1;
		for (; si != s->end() && ti != t->end(); ++si, ++ti) {
			AType* st = (*si)->as<AType*>();
			AType* tt = (*ti)->as<AType*>();
			if (st->kind == AType::DOTS || tt->kind == AType::DOTS)
				return unify(cp);
			else
				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,
			(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());
}