From 84274ac380968df9fb49bcbf6f3d494536d7a548 Mon Sep 17 00:00:00 2001
From: David Robillard <d@drobilla.net>
Date: Sun, 28 Jun 2009 23:21:30 +0000
Subject: Split unification into a separate file than type constraints.
git-svn-id: http://svn.drobilla.net/resp/tuplr@159 ad02d1e2-f140-0410-9f75-f8b11f17cedd
---
unify.cpp | 94 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 94 insertions(+)
create mode 100644 unify.cpp
(limited to 'unify.cpp')
diff --git a/unify.cpp b/unify.cpp
new file mode 100644
index 0000000..2a8e6a0
--- /dev/null
+++ b/unify.cpp
@@ -0,0 +1,94 @@
+/* Tuplr Unification
+ * Copyright (C) 2008-2009 David Robillard <dave@drobilla.net>
+ *
+ * Tuplr 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.
+ *
+ * Tuplr 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 Tuplr. If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include <set>
+#include "tuplr.hpp"
+
+/***************************************************************************
+ * Type Inference/Substitution *
+ ***************************************************************************/
+
+static void
+substitute(ATuple* tup, const AST* from, AST* to)
+{
+ if (!tup) return;
+ for (size_t i = 0; i < tup->size(); ++i)
+ if (*tup->at(i) == *from)
+ tup->at(i) = to;
+ else if (tup->at(i) != to)
+ substitute(tup->at(i)->to<ATuple*>(), from, to);
+}
+
+Subst
+Subst::compose(const Subst& delta, const Subst& gamma) // TAPL 22.1.1
+{
+ 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;
+}
+
+void
+substConstraints(Constraints& constraints, AType* s, AType* t)
+{
+ for (Constraints::iterator c = constraints.begin(); c != constraints.end();) {
+ Constraints::iterator next = c; ++next;
+ if (*c->first == *s) c->first = t;
+ if (*c->second == *s) c->second = t;
+ substitute(c->first, s, t);
+ substitute(c->second, s, t);
+ c = next;
+ }
+}
+
+Subst
+TEnv::unify(const Constraints& constraints) // TAPL 22.4
+{
+ if (constraints.empty()) return Subst();
+ AType* s = constraints.begin()->first;
+ AType* t = constraints.begin()->second;
+ Constraints cp = constraints;
+ cp.erase(cp.begin());
+
+ if (*s == *t) {
+ return unify(cp);
+ } else if (s->var() && !t->contains(s)) {
+ substConstraints(cp, s, t);
+ return Subst::compose(unify(cp), Subst(s, t));
+ } else if (t->var() && !s->contains(t)) {
+ substConstraints(cp, t, s);
+ return Subst::compose(unify(cp), Subst(t, s));
+ } else if (s->kind == AType::EXPR && s->kind == t->kind && s->size() == t->size()) {
+ for (size_t i = 0; i < s->size(); ++i) {
+ AType* si = s->at(i)->to<AType*>();
+ AType* ti = t->at(i)->to<AType*>();
+ if (si && ti)
+ cp.push_back(Constraint(si, ti, si->loc));
+ }
+ return unify(cp);
+ } else {
+ throw Error(s->loc ? s->loc : t->loc,
+ (format("type is `%1%' but should be `%2%'") % s->str() % t->str()).str());
+ }
+}
+
--
cgit v1.2.1