MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
clos_conv.cpp
Go to the documentation of this file.
2
3#include "mim/check.h"
4
6
7using namespace std::literals;
8
9namespace mim::plug::clos {
10
11namespace {
12
13bool is_toplevel(const Def* fd) {
14 return fd->has_const_dep() || fd->isa_mut<Global>() || fd->isa<Axiom>() || !fd->is_term();
15}
16
17bool is_memop_res(const Def* fd) {
18 auto proj = fd->isa<Extract>();
19 if (!proj) return false;
20 auto types = proj->tuple()->type()->ops();
21 return std::any_of(types.begin(), types.end(), [](auto d) { return match<mem::M>(d); });
22}
23
24} // namespace
25
26DefSet free_defs(const Nest& nest) {
27 DefSet bound;
28 DefSet free;
29 std::queue<const Def*> queue;
30 queue.emplace(nest.root()->mut());
31
32 while (!queue.empty()) {
33 auto def = pop(queue);
34 for (auto op : def->deps()) {
35 if (op->has_const_dep()) {
36 // do nothing
37 } else if (nest.contains(op)) {
38 if (auto [_, ins] = bound.emplace(op); ins) queue.emplace(op);
39 } else {
40 free.emplace(op);
41 }
42 }
43 }
44
45 return free;
46}
47
48/*
49 * Free variable analysis
50 */
51
52void FreeDefAna::split_fd(Node* node, const Def* fd, bool& init_node, NodeQueue& worklist) {
53 assert(!match<mem::M>(fd) && "mem tokens must not be free");
54 if (is_toplevel(fd)) return;
55 if (auto [var, lam] = ca_isa_var<Lam>(fd); var && lam) {
56 if (var != lam->ret_var()) node->add_fvs(fd);
57 } else if (auto q = match(attr::freeBB, fd)) {
58 node->add_fvs(q);
59 } else if (auto pred = fd->isa_mut()) {
60 if (pred != node->mut) {
61 auto [pnode, inserted] = build_node(pred, worklist);
62 node->preds.push_back(pnode);
63 pnode->succs.push_back(node);
64 init_node |= inserted;
65 }
66 } else if (fd->has_dep(Dep::Var) && !fd->isa<Tuple>()) {
67 // Note: Var's can still have Def::Top, if their type is a mut!
68 // So the first case is *not* redundant
69 node->add_fvs(fd);
70 } else if (is_memop_res(fd)) {
71 // Results of memops must not be floated down
72 node->add_fvs(fd);
73 } else {
74 for (auto op : fd->ops()) split_fd(node, op, init_node, worklist);
75 }
76}
77
78std::pair<FreeDefAna::Node*, bool> FreeDefAna::build_node(Def* mut, NodeQueue& worklist) {
79 auto& w = world();
80 auto [p, inserted] = lam2nodes_.emplace(mut, nullptr);
81 if (!inserted) return {p->second.get(), false};
82 w.DLOG("FVA: create node: {}", mut);
83 p->second = std::make_unique<Node>(Node{mut, {}, {}, {}, 0});
84 auto node = p->second.get();
85 auto nest = Nest(mut);
86 bool init_node = false;
87 for (auto v : free_defs(nest)) split_fd(node, v, init_node, worklist);
88 if (!init_node) {
89 worklist.push(node);
90 w.DLOG("FVA: init {}", mut);
91 }
92 return {node, true};
93}
94
95void FreeDefAna::run(NodeQueue& worklist) {
96 while (!worklist.empty()) {
97 auto node = worklist.front();
98 worklist.pop();
99 if (is_done(node)) continue;
100 auto changed = is_bot(node);
101 mark(node);
102 for (auto p : node->preds) {
103 auto& pfvs = p->fvs;
104 for (auto&& pfv : pfvs) changed |= node->add_fvs(pfv).second;
105 }
106 if (changed)
107 for (auto s : node->succs) worklist.push(s);
108 }
109}
110
112 auto worklist = NodeQueue();
113 auto [node, _] = build_node(lam, worklist);
114 if (!is_done(node)) {
115 cur_pass_id++;
116 run(worklist);
117 }
118
119 return node->fvs;
120}
121
122/*
123 * Closure Conversion
124 */
125
127 auto subst = Def2Def();
128 for (auto mut : world().copy_externals()) rewrite(mut, subst);
129 while (!worklist_.empty()) {
130 auto def = worklist_.front();
131 subst = Def2Def();
132 worklist_.pop();
133 if (auto i = closures_.find(def); i != closures_.end()) {
134 rewrite_body(i->second.fn, subst);
135 } else {
136 world().DLOG("RUN: rewrite def {}", def);
137 rewrite(def, subst);
138 }
139 }
140}
141
142void ClosConv::rewrite_body(Lam* new_lam, Def2Def& subst) {
143 auto& w = world();
144 auto it = closures_.find(new_lam);
145 assert(it != closures_.end() && "closure should have a stub if rewrite_body is called!");
146 auto [old_fn, num_fvs, env, new_fn] = it->second;
147
148 if (!old_fn->is_set()) return;
149
150 w.DLOG("rw body: {} [old={}, env={}]\nt", new_fn, old_fn, env);
151 auto env_param = new_fn->var(Clos_Env_Param)->set("closure_env");
152 if (num_fvs == 1) {
153 subst.emplace(env, env_param);
154 } else {
155 for (size_t i = 0; i < num_fvs; i++) {
156 auto fv = env->op(i);
157 auto sym = w.sym("fv_"s + (fv->sym() ? fv->sym().str() : std::to_string(i)));
158 subst.emplace(fv, env_param->proj(i)->set(sym));
159 }
160 }
161
162 auto params = w.tuple(DefVec(old_fn->num_doms(), [&](auto i) { return new_lam->var(skip_env(i)); }));
163 subst.emplace(old_fn->var(), params);
164
165 auto filter = rewrite(new_fn->filter(), subst);
166 auto body = rewrite(new_fn->body(), subst);
167 new_fn->reset({filter, body});
168}
169
170const Def* ClosConv::rewrite(const Def* def, Def2Def& subst) {
171 switch (def->node()) {
172 case Node::Type:
173 case Node::Univ:
174 case Node::Nat:
175 case Node::Bot: // TODO This is used by the AD stuff????
176 case Node::Top: return def;
177 default: break;
178 }
179
180 auto& w = world();
181 auto map = [&](const Def* new_def) {
182 subst[def] = new_def;
183 assert(subst[def] == new_def);
184 return new_def;
185 };
186
187 if (auto i = subst.find(def); i != subst.end()) {
188 return i->second;
189 } else if (auto pi = Pi::isa_cn(def)) {
190 return map(type_clos(pi, subst));
191 } else if (auto lam = def->isa_mut<Lam>(); lam && Lam::isa_cn(lam)) {
192 auto [_, __, fv_env, new_lam] = make_stub(lam, subst);
193 auto clos_ty = rewrite(lam->type(), subst);
194 auto env = rewrite(fv_env, subst);
195 auto closure = clos_pack(env, new_lam, clos_ty);
196 world().DLOG("RW: pack {} ~> {} : {}", lam, closure, clos_ty);
197 return map(closure);
198 } else if (auto a = match<attr>(def)) {
199 switch (a.id()) {
200 case attr::returning:
201 if (auto ret_lam = a->arg()->isa_mut<Lam>()) {
202 // assert(ret_lam && ret_lam->is_basicblock());
203 // Note: This should be cont_lam's only occurance after η-expansion, so its okay to
204 // put into the local subst only
205 auto new_doms
206 = DefVec(ret_lam->num_doms(), [&](auto i) { return rewrite(ret_lam->dom(i), subst); });
207 auto new_lam = ret_lam->stub(w.cn(new_doms));
208 subst[ret_lam] = new_lam;
209 if (ret_lam->is_set()) {
210 new_lam->set_filter(rewrite(ret_lam->filter(), subst));
211 new_lam->set_body(rewrite(ret_lam->body(), subst));
212 }
213 return new_lam;
214 }
215 break;
216 case attr::fstclassBB:
217 case attr::freeBB: {
218 // Note: Same thing about η-conversion applies here
219 auto bb_lam = a->arg()->isa_mut<Lam>();
220 assert(bb_lam && Lam::isa_basicblock(bb_lam));
221 auto [_, __, ___, new_lam] = make_stub({}, bb_lam, subst);
222 subst[bb_lam] = clos_pack(w.tuple(), new_lam, rewrite(bb_lam->type(), subst));
223 rewrite_body(new_lam, subst);
224 return map(subst[bb_lam]);
225 }
226 default: break;
227 }
228 } else if (auto [var, lam] = ca_isa_var<Lam>(def); var && lam && lam->ret_var() == var) {
229 // HACK to rewrite a retvar that is defined in an enclosing lambda
230 // If we put external bb's into the env, this should never happen
231 auto new_lam = make_stub(lam, subst).fn;
232 auto new_idx = skip_env(Lit::as(var->index()));
233 return map(new_lam->var(new_idx));
234 }
235
236 auto new_type = rewrite(def->type(), subst);
237
238 if (auto mut = def->isa_mut()) {
239 if (auto global = def->isa_mut<Global>()) {
240 if (auto i = glob_muts_.find(global); i != glob_muts_.end()) return i->second;
241 auto subst = Def2Def();
242 return glob_muts_[mut] = rewrite_mut(global, new_type, subst);
243 }
244 assert(!isa_clos_type(mut));
245 w.DLOG("RW: mut {}", mut);
246 auto new_mut = rewrite_mut(mut, new_type, subst);
247 // Try to reduce the amount of muts that are created
248 if (!mut->isa_mut<Global>() && Checker::alpha<Checker::Check>(mut, new_mut)) return map(mut);
249 if (auto imm = new_mut->immutabilize()) return map(imm);
250 return map(new_mut);
251 } else {
252 auto new_ops = DefVec(def->num_ops(), [&](auto i) { return rewrite(def->op(i), subst); });
253 if (auto app = def->isa<App>(); app && new_ops[0]->type()->isa<Sigma>())
254 return map(clos_apply(new_ops[0], new_ops[1]));
255 else if (def->isa<Axiom>())
256 return def;
257 else
258 return map(def->rebuild(new_type, new_ops));
259 }
260
261 fe::unreachable();
262}
263
264Def* ClosConv::rewrite_mut(Def* mut, const Def* new_type, Def2Def& subst) {
265 auto new_mut = mut->stub(new_type);
266 subst.emplace(mut, new_mut);
267 for (size_t i = 0; i < mut->num_ops(); i++)
268 if (mut->op(i)) new_mut->set(i, rewrite(mut->op(i), subst));
269 return new_mut;
270}
271
272const Pi* ClosConv::rewrite_type_cn(const Pi* pi, Def2Def& subst) {
273 assert(Pi::isa_basicblock(pi));
274 auto new_ops = DefVec(pi->num_doms(), [&](auto i) { return rewrite(pi->dom(i), subst); });
275 return world().cn(new_ops);
276}
277
278const Def* ClosConv::type_clos(const Pi* pi, Def2Def& subst, const Def* env_type) {
279 if (auto i = glob_muts_.find(pi); i != glob_muts_.end() && !env_type) return i->second;
280 auto& w = world();
281 auto new_doms = DefVec(pi->num_doms(), [&](auto i) {
282 return (i == pi->num_doms() - 1 && Pi::isa_returning(pi)) ? rewrite_type_cn(pi->ret_pi(), subst)
283 : rewrite(pi->dom(i), subst);
284 });
285 auto ct = ctype(w, new_doms, env_type);
286 if (!env_type) {
287 glob_muts_.emplace(pi, ct);
288 w.DLOG("C-TYPE: pct {} ~~> {}", pi, ct);
289 } else {
290 w.DLOG("C-TYPE: ct {}, env = {} ~~> {}", pi, env_type, ct);
291 }
292 return ct;
293}
294
295ClosConv::Stub ClosConv::make_stub(const DefSet& fvs, Lam* old_lam, Def2Def& subst) {
296 auto& w = world();
297 auto env = w.tuple(DefVec(fvs.begin(), fvs.end()));
298 auto num_fvs = fvs.size();
299 auto env_type = rewrite(env->type(), subst);
300 auto new_fn_type = type_clos(old_lam->type(), subst, env_type)->as<Pi>();
301 auto new_lam = old_lam->stub(new_fn_type);
302 // TODO
303 // new_lam->set_debug_name((old_lam->is_external() || !old_lam->is_set()) ? "cc_" + old_lam->name() :
304 // old_lam->name());
305 if (!isa_workable(old_lam)) {
306 auto new_ext_type = w.cn(clos_remove_env(new_fn_type->dom()));
307 auto new_ext_lam = old_lam->stub(new_ext_type);
308 w.DLOG("wrap ext lam: {} -> stub: {}, ext: {}", old_lam, new_lam, new_ext_lam);
309 if (old_lam->is_set()) {
310 old_lam->transfer_external(new_ext_lam);
311 new_ext_lam->app(false, new_lam, clos_insert_env(env, new_ext_lam->var()));
312 new_lam->set(old_lam->filter(), old_lam->body());
313 } else {
314 new_ext_lam->unset();
315 new_lam->app(false, new_ext_lam, clos_remove_env(new_lam->var()));
316 }
317 } else {
318 new_lam->set(old_lam->filter(), old_lam->body());
319 }
320 w.DLOG("STUB {} ~~> ({}, {})", old_lam, env, new_lam);
321 auto closure = Stub{old_lam, num_fvs, env, new_lam};
322 closures_.emplace(old_lam, closure);
323 closures_.emplace(closure.fn, closure);
324 return closure;
325}
326
327ClosConv::Stub ClosConv::make_stub(Lam* old_lam, Def2Def& subst) {
328 if (auto i = closures_.find(old_lam); i != closures_.end()) return i->second;
329 auto fvs = fva_.run(old_lam);
330 auto closure = make_stub(fvs, old_lam, subst);
331 worklist_.emplace(closure.fn);
332 return closure;
333}
334
335} // namespace mim::plug::clos
static bool alpha(Ref d1, Ref d2)
Definition check.h:65
Base class for all Defs.
Definition def.h:212
Defs deps() const
Definition def.cpp:410
constexpr auto ops() const noexcept
Definition def.h:261
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:432
bool has_const_dep() const
Neither a Dep::Mut nor a Dep::Var; can often be used as shortcut as an optimization.
Definition def.h:317
Ref var(nat_t a, nat_t i) noexcept
Definition def.h:381
bool has_dep() const
Definition def.h:313
A function.
Definition lam.h:105
Lam * stub(Ref type)
Definition lam.h:177
Lam * set_filter(Filter)
Set filter first.
Definition lam.cpp:28
Lam * set_body(Ref body)
Set body second.
Definition lam.h:165
static const Lam * isa_cn(Ref d)
Definition lam.h:136
static const Lam * isa_basicblock(Ref d)
Definition lam.h:137
static T as(Ref def)
Definition def.h:736
Def * mut() const
The mutable capsulated in this Node or nullptr, if it's a virtual root comprising several Nodes.
Definition nest.h:22
Builds a nesting tree of all immutables‍/binders.
Definition nest.h:11
const Node * root() const
Definition nest.h:129
bool contains(const Def *def) const
Definition nest.h:131
World & world()
Definition phase.h:27
static const Pi * isa_cn(Ref d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
Definition lam.h:44
static const Pi * isa_basicblock(Ref d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
Definition lam.h:48
const Pi * cn()
Definition world.h:274
void start() override
Actual entry.
DefSet & run(Lam *lam)
FreeDefAna::run will compute free defs (FD) that appear in lams body.
@ Type
Definition def.h:40
@ Univ
Definition def.h:40
@ Nat
Definition def.h:40
@ Bot
Definition def.h:40
@ Top
Definition def.h:40
@ Extract
Definition def.h:40
@ Global
Definition def.h:40
@ Pi
Definition def.h:40
@ Lam
Definition def.h:40
The clos Plugin
Definition clos.h:7
Ref clos_apply(Ref closure, Ref args)
Apply a closure to arguments.
Definition clos.cpp:100
DefSet free_defs(const Nest &nest)
Definition clos_conv.cpp:26
Ref clos_remove_env(size_t i, std::function< Ref(size_t)> f)
Definition clos.cpp:143
static constexpr size_t Clos_Env_Param
Describes where the environment is placed in the argument list.
Definition clos.h:107
const Sigma * isa_clos_type(Ref def)
Definition clos.cpp:111
std::tuple< const Extract *, N * > ca_isa_var(Ref def)
Checks is def is the variable of a mut of type N.
Definition clos.h:79
Ref ctype(World &w, Defs doms, Ref env_type=nullptr)
Definition clos.cpp:145
size_t skip_env(size_t i)
Definition clos.h:113
Ref clos_pack(Ref env, Ref fn, Ref ct=nullptr)
Pack a typed closure. This assumes that fn expects the environment as its Clos_Env_Paramth argument.
Definition clos.cpp:78
Ref clos_insert_env(size_t i, Ref env, std::function< Ref(size_t)> f)
Definition clos.cpp:139
DefMap< const Def * > Def2Def
Definition def.h:60
auto pop(S &s) -> decltype(s.top(), typename S::value_type())
Definition util.h:80
Vector< const Def * > DefVec
Definition def.h:62
auto match(Ref def)
Definition axiom.h:112
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
Definition lam.h:248
GIDSet< const Def * > DefSet
Definition def.h:59