diff options
| -rw-r--r-- | Makefile | 11 | ||||
| -rw-r--r-- | typing.cpp | 75 | ||||
| -rw-r--r-- | unify.cpp | 94 |
3 files changed, 100 insertions, 80 deletions
@@ -11,13 +11,14 @@ builddir: mkdir -p build OBJECTS = \ + build/cps.o \ + build/gc.o \ + build/gclib.so \ + build/llvm.so \ build/tuplr.o \ build/typing.o \ - build/llvm.so \ - build/gclib.so \ - build/write.o \ - build/gc.o \ - build/cps.o + build/unify.o \ + build/write.o build/tuplr: $(OBJECTS) g++ -o $@ $^ $(LDFLAGS) @@ -230,78 +230,3 @@ APrimitive::constrain(TEnv& tenv, Constraints& c) const } } - -/*************************************************************************** - * 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()); - } -} - 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()); + } +} + |