MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
copy_prop.cpp
Go to the documentation of this file.
2
3#include <mim/pass/beta_red.h>
4#include <mim/pass/eta_exp.h>
5
6#include "mim/plug/mem/mem.h"
7
8namespace mim::plug::mem::pass {
9
11 bb_only_ = bb_only;
12 name_ += bb_only_ ? " tt" : " ff";
13}
14
17 beta_red_ = man->find<BetaRed>();
18 eta_exp_ = man->find<EtaExp>();
19}
20
21const Def* CopyProp::rewrite(const Def* def) {
22 auto [app, var_lam] = isa_apped_mut_lam(def);
23 if (!isa_workable(var_lam) || (bb_only_ && Lam::isa_returning(var_lam))) return def;
24
25 auto n = app->num_targs();
26 if (n == 0) return app;
27
28 auto [it, _] = lam2info_.emplace(var_lam, std::tuple(Lattices(n), (Lam*)nullptr, DefVec(n)));
29 auto& [lattice, prop_lam, old_args] = it->second;
30
31 if (mem::mem_var(var_lam)) lattice[0] = Lattice::Keep;
32 if (std::ranges::all_of(lattice, [](auto l) { return l == Lattice::Keep; })) return app;
33
34 DefVec new_args, new_doms, appxy_ops = {var_lam};
35 auto& args = data(var_lam);
36 args.resize(n);
37
38 for (size_t i = 0; i != n; ++i) {
39 switch (lattice[i]) {
40 case Lattice::Dead: break;
41 case Lattice::Prop:
42 if (app->arg(n, i)->has_dep(Dep::Proxy)) {
43 DLOG("found proxy within app: {}@{} - wait till proxy is gone", var_lam, app);
44 return app;
45 } else if (args[i] == nullptr) {
46 args[i] = app->arg(n, i);
47 } else if (args[i] != app->arg(n, i)) {
48 appxy_ops.emplace_back(world().lit_nat(i));
49 } else {
50 assert(args[i] == app->arg(n, i));
51 }
52 break;
53 case Lattice::Keep:
54 new_doms.emplace_back(var_lam->var(n, i)->type());
55 new_args.emplace_back(app->arg(n, i));
56 break;
57 default: fe::unreachable();
58 }
59 }
60
61 DLOG("app->args(): {, }", app->args());
62 DLOG("args: {, }", args);
63 DLOG("new_args: {, }", new_args);
64
65 if (appxy_ops.size() > 1) {
66 auto appxy = proxy(app->type(), appxy_ops, Appxy);
67 DLOG("appxy: '{}': {, }", appxy, appxy_ops);
68 return appxy;
69 }
70
71 assert(new_args.size() < n);
72 if (prop_lam == nullptr || !std::ranges::equal(old_args, args)) {
73 old_args = args;
74 auto prop_dom = world().sigma(new_doms);
75 auto new_pi = world().pi(prop_dom, var_lam->codom());
76 prop_lam = var_lam->stub(new_pi);
77
78 DLOG("new prop_lam: {}", prop_lam);
79 if (beta_red_) beta_red_->keep(prop_lam);
80 if (eta_exp_) eta_exp_->new2old(prop_lam, var_lam);
81
82 size_t j = 0;
83 auto new_vars = DefVec(n, [&, prop_lam = prop_lam](size_t i) -> const Def* {
84 switch (lattice[i]) {
85 case Lattice::Dead: return proxy(var_lam->var(n, i)->type(), {var_lam, world().lit_nat(i)}, Varxy);
86 case Lattice::Prop: return args[i];
87 case Lattice::Keep: return prop_lam->var(j++);
88 default: fe::unreachable();
89 }
90 });
91
92 prop_lam->set(var_lam->reduce(world().tuple(new_vars)));
93 }
94
95 DLOG("var_lam => prop_lam: {}: {} => {}: {}", var_lam, var_lam->dom(), prop_lam, prop_lam->dom());
96 auto res = app->world().app(prop_lam, new_args);
97
98 // Don't optimize again. Also, keep this line here at the very bottom as this invalidates all references.
99 Lam* key = prop_lam; // prop_lam is a Lam*& which might get invalidated by the very insertion happening next.
100 lam2info_.insert_or_assign(key, std::tuple(Lattices(new_doms.size(), Lattice::Keep), (Lam*)nullptr, DefVec()));
101 return res;
102}
103
105 DLOG("found proxy: {}", proxy);
106 auto var_lam = proxy->op(0)->as_mut<Lam>();
107 auto& [lattice, prop_lam, old_args] = lam2info_[var_lam];
108
109 if (proxy->tag() == Varxy) {
110 auto i = Lit::as(proxy->op(1));
111 if (auto& l = lattice[i]; l == Lattice::Dead) {
112 l = Lattice::Prop;
113 DLOG("Dead -> Prop: @{}#{}", var_lam, i);
114 return undo_visit(var_lam);
115 }
116 } else {
117 assert(proxy->tag() == Appxy);
118 for (auto ops = proxy->ops(); auto op : ops.subspan(1)) {
119 auto i = Lit::as(op);
120 if (auto& l = lattice[i]; l != Lattice::Keep) {
121 l = Lattice::Keep;
122 DLOG("Prop -> Keep: @{}#{}", var_lam, i);
123 }
124 }
125
126 return undo_visit(var_lam);
127 }
128
129 return No_Undo;
130}
131
132} // namespace mim::plug::mem::pass
Optimistically performs β-reduction (aka inlining).
Definition beta_red.h:9
Base class for all Defs.
Definition def.h:251
Performs η-expansion: f -> λx.f x, if f is a Lam with more than one user and does not appear in calle...
Definition eta_exp.h:13
undo_t undo_visit(Def *mut) const
Definition pass.h:360
A function.
Definition lam.h:111
static const Lam * isa_returning(const Def *d)
Definition lam.h:144
static T as(const Def *def)
Definition def.h:830
const Proxy * proxy(const Def *type, Defs ops, u32 tag=0)
Definition pass.h:141
virtual void init(PassMan *)
Definition pass.cpp:30
PassMan & man()
Definition pass.h:97
friend class PassMan
Definition pass.h:166
Pi * stub(const Def *type)
Definition lam.h:93
World & world()
Definition pass.h:64
std::string name_
Definition pass.h:76
const Def * sigma(Defs ops)
Definition world.cpp:277
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:265
undo_t analyze(const Proxy *) override
const Def * rewrite(const Def *) override
Definition copy_prop.cpp:21
void init(PassMan *) final
Definition copy_prop.cpp:15
#define DLOG(...)
Vaporizes to nothingness in Debug build.
Definition log.h:95
const Def * mem_var(Lam *lam)
Returns the memory argument of a function if it has one.
Definition mem.h:38
The tuple Plugin
Vector< const Def * > DefVec
Definition def.h:77
@ Proxy
Definition def.h:128
std::pair< const App *, Lam * > isa_apped_mut_lam(const Def *def)
Definition lam.h:354
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
Definition lam.h:349
size_t undo_t
Definition pass.h:21
static constexpr undo_t No_Undo
Definition pass.h:22