Thorin 1.9.0
The Higher ORder INtermediate representation
Loading...
Searching...
No Matches
eta_red.cpp
Go to the documentation of this file.
2
3namespace thorin {
4
5namespace {
6bool is_var(Ref def) {
7 if (def->isa<Var>()) return true;
8 if (auto extract = def->isa<Extract>()) return extract->tuple()->isa<Var>();
9 return false;
10}
11
12// For now, only η-reduce `lam x.e x` if e is a @p Var or a @p Lam.
13const App* eta_rule(Lam* lam) {
14 if (auto app = lam->body()->isa<App>()) {
15 if (app->arg() == lam->var() && (is_var(app->callee()) || app->callee()->isa<Lam>())) return app;
16 }
17 return nullptr;
18}
19} // namespace
20
22 for (size_t i = 0, e = def->num_ops(); i != e; ++i) {
23 // TODO (ClosureConv): Factor this out
24 if (auto lam = def->op(i)->isa_mut<Lam>(); (!callee_only_ || isa_callee(def, i)) && lam && lam->is_set()) {
25 if (auto app = eta_rule(lam); app && !irreducible_.contains(lam)) {
26 data().emplace(lam, Lattice::Reduce);
27 auto new_def = def->refine(i, app->callee());
28 world().DLOG("eta-reduction '{}' -> '{}' by eliminating '{}'", def, new_def, lam);
29 return new_def;
30 }
31 }
32 }
33
34 return def;
35}
36
38 if (auto lam = var->mut()->isa_mut<Lam>()) {
39 auto [_, l] = *data().emplace(lam, Lattice::Bot).first;
40 auto succ = irreducible_.emplace(lam).second;
41 if (l == Lattice::Reduce && succ) {
42 world().DLOG("irreducible: {}; found {}", lam, var);
43 return undo_visit(lam);
44 }
45 }
46
47 return No_Undo;
48}
49
50} // namespace thorin
const Def * refine(size_t i, const Def *new_op) const
Definition def.cpp:226
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:315
const Def * op(size_t i) const
Definition def.h:269
size_t num_ops() const
Definition def.h:270
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:449
undo_t analyze(const Var *) override
Definition eta_red.cpp:37
@ Reduce
η-reduction performed.
Definition eta_red.h:17
@ Bot
Never seen.
Definition eta_red.h:16
Ref rewrite(Ref) override
Definition eta_red.cpp:21
undo_t undo_visit(Def *mut) const
Retrieves the point to backtrack to just before mut was seen the very first time.
Definition pass.h:273
A function.
Definition lam.h:97
World & world()
Definition pass.h:296
Helper class to retrieve Infer::arg if present.
Definition def.h:87
Def * mut() const
Definition def.h:656
Definition cfg.h:11
static constexpr undo_t No_Undo
Definition pass.h:15
size_t undo_t
Definition pass.h:14
const App * isa_callee(const Def *def, size_t i)
Definition lam.h:231