aboutsummaryrefslogtreecommitdiffstats
path: root/typing.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'typing.cpp')
-rw-r--r--typing.cpp75
1 files changed, 0 insertions, 75 deletions
diff --git a/typing.cpp b/typing.cpp
index 0e63f26..5791fdc 100644
--- a/typing.cpp
+++ b/typing.cpp
@@ -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());
- }
-}
-