MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
lam_spec.cpp
Go to the documentation of this file.
1#include "mim/pass/lam_spec.h"
2
3#include "mim/nest.h"
4
5// TODO This is supposed to recreate what lower2cff did, but we should really consider another strategy and nuke this.
6
7namespace mim {
8
10 if (auto i = old2new_.find(def); i != old2new_.end()) return i->second;
11
12 auto [app, old_lam] = isa_apped_mut_lam(def);
13 if (!isa_workable(old_lam)) return def;
14
15 // Skip recursion to avoid infinite inlining if not "aggressive_lam_spec".
16 // This is a hack - but we want to get rid off this Pass anyway.
17 Nest nest(old_lam);
18 if (!world().flags().aggressive_lam_spec && nest.is_recursive()) return def;
19
20 DefVec new_doms, new_vars, new_args;
21 auto skip = old_lam->ret_var() && old_lam->is_closed();
22 auto old_doms = old_lam->doms();
23
24 for (auto dom : old_doms.view().rsubspan(skip))
25 if (!dom->isa<Pi>()) new_doms.emplace_back(dom);
26
27 if (skip) new_doms.emplace_back(old_lam->doms().back());
28 if (new_doms.size() == old_lam->num_doms()) return def;
29
30 auto new_lam = old_lam->stub(world().cn(new_doms));
31
32 for (size_t arg_i = 0, var_i = 0, n = app->num_args() - skip; arg_i != n; ++arg_i) {
33 auto arg = app->arg(arg_i);
34 if (old_lam->dom(arg_i)->isa<Pi>()) {
35 new_vars.emplace_back(arg);
36 } else {
37 new_vars.emplace_back(new_lam->var(var_i++));
38 new_args.emplace_back(arg);
39 }
40 }
41
42 if (skip) {
43 new_vars.emplace_back(new_lam->vars().back());
44 new_args.emplace_back(app->args().back());
45 }
46
47 new_lam->set(old_lam->reduce(world().tuple(new_vars)));
48 world().DLOG("{} -> {}: {} -> {})", old_lam, new_lam, old_lam->dom(), new_lam->dom());
49
50 return old2new_[def] = world().app(new_lam, new_args);
51}
52
53} // namespace mim
Def * set(size_t i, Ref)
Successively set from left to right.
Definition def.cpp:243
Def * stub(World &w, Ref type)
Definition def.h:490
Ref rewrite(Ref) override
Definition lam_spec.cpp:9
Builds a nesting tree of all immutables‍/binders.
Definition nest.h:11
bool is_recursive() const
Definition nest.h:132
World & world()
Definition pass.h:296
A dependent function type.
Definition lam.h:11
Helper class to retrieve Infer::arg if present.
Definition def.h:86
Ref app(Ref callee, Ref arg)
Definition world.cpp:168
Definition ast.h:14
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
Definition lam.h:248
std::pair< const App *, Lam * > isa_apped_mut_lam(Ref def)
Definition lam.h:253