Thorin 1.9.0
The Higher ORder INtermediate representation
Loading...
Searching...
No Matches
eta_exp.cpp
Go to the documentation of this file.
2
4
5using namespace std::literals;
6
7namespace thorin {
8
10 if (auto old = lookup(new2old_, new_lam)) {
11 auto root = new2old(old); // path compression
12 assert(root != new_lam);
13 new2old_[new_lam] = root;
14 return root;
15 }
16
17 return new_lam;
18}
19
21 if (std::ranges::none_of(def->ops(), [](Ref def) { return def->isa<Lam>(); })) return def;
22 if (auto n = lookup(old2new(), def)) return n;
23
24 auto [i, ins] = def2new_ops_.emplace(def, DefVec{});
25 auto& new_ops = i->second;
26 if (ins) new_ops.assign(def->ops().begin(), def->ops().end());
27
28 for (size_t i = 0, e = def->num_ops(); i != e; ++i) {
29 if (auto lam = def->op(i)->isa_mut<Lam>(); lam && lam->is_set()) {
30 if (isa_callee(def, i)) {
31 if (auto orig = lookup(exp2orig_, lam)) new_ops[i] = orig;
32 } else if (expand_.contains(lam)) {
33 if (new_ops[i] == lam) new_ops[i] = eta_exp(lam);
34 } else if (auto orig = lookup(exp2orig_, lam)) {
35 if (new_ops[i] == lam) new_ops[i] = eta_exp(orig);
36 }
37 }
38 }
39
40 auto new_def = def->rebuild(def->type(), new_ops);
41 return old2new()[new_def] = new_def;
42}
43
44Lam* EtaExp::eta_exp(Lam* lam) {
45 auto exp = lam->stub(lam->type());
46 exp2orig_.emplace(exp, lam);
47 exp->debug_suffix("eta_"s + lam->sym().str());
48 exp->app(false, lam, exp->var());
49 if (eta_red_) eta_red_->mark_irreducible(exp);
50 return exp;
51}
52
54 world().DLOG("found proxy: {}", proxy);
55 auto lam = proxy->op(0)->as_mut<Lam>();
56 if (expand_.emplace(lam).second) return undo_visit(lam);
57 return No_Undo;
58}
59
61 auto undo = No_Undo;
62 for (size_t i = 0, e = def->num_ops(); i != e; ++i) {
63 if (auto lam = def->op(i)->isa_mut<Lam>(); lam && lam->is_set()) {
64 lam = new2old(lam);
65 if (expand_.contains(lam) || exp2orig_.contains(lam)) continue;
66
67 if (isa_callee(def, i)) {
68 if (auto [_, p] = *pos().emplace(lam, Pos::Callee).first; p == Pos::Non_Callee_1) {
69 world().DLOG("Callee: Callee -> Expand: '{}'", lam);
70 expand_.emplace(lam);
71 undo = std::min(undo, undo_visit(lam));
72 } else {
73 world().DLOG("Callee: Bot/Callee -> Callee: '{}'", lam);
74 }
75 } else {
76 auto [it, first] = pos().emplace(lam, Pos::Non_Callee_1);
77
78 if (first) {
79 world().DLOG("Non_Callee: Bot -> Non_Callee_1: '{}'", lam);
80 } else {
81 world().DLOG("Non_Callee: {} -> Expand: '{}'", pos2str(it->second), lam);
82 expand_.emplace(lam);
83 undo = std::min(undo, undo_visit(lam));
84 }
85 }
86 }
87 }
88
89 return undo;
90}
91
92} // namespace thorin
auto ops() const
Definition def.h:268
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
Ref rebuild(World &w, Ref type, Defs ops) const
Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
Definition def.h:498
const Def * type() const
Yields the raw type of this Def, i.e. maybe nullptr.
Definition def.h:248
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
Sym sym() const
Definition def.h:470
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Definition def.h:457
undo_t analyze(const Proxy *) override
Definition eta_exp.cpp:53
const Proxy * proxy(Lam *lam)
Definition eta_exp.h:21
auto & pos()
Definition eta_exp.h:45
void new2old(Lam *new_lam, Lam *old_lam)
Definition eta_exp.h:22
auto & old2new()
Definition eta_exp.h:44
Ref rewrite(Ref) override
Definition eta_exp.cpp:20
static std::string_view pos2str(Pos pos)
Definition eta_exp.h:41
void mark_irreducible(Lam *lam)
Definition eta_red.h:22
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
Lam * stub(Ref type)
Definition lam.h:173
const Pi * type() const
Definition lam.h:109
World & world()
Definition pass.h:296
Helper class to retrieve Infer::arg if present.
Definition def.h:87
Definition cfg.h:11
static constexpr undo_t No_Undo
Definition pass.h:15
auto lookup(const C &container, const K &key)
Yields pointer to element (or the element itself if it is already a pointer), if found and nullptr ot...
Definition util.h:93
size_t undo_t
Definition pass.h:14
const App * isa_callee(const Def *def, size_t i)
Definition lam.h:231