10const Def* insert_ret(
const Def* def,
const Def* ret) {
11 auto new_ops =
DefVec(def->num_projs() + 1, [&](
auto i) { return (i == def->num_projs()) ? ret : def->proj(i); });
12 auto&
w = def->world();
13 return def->is_term() ?
w.tuple(new_ops) :
w.sigma(new_ops);
21 auto externals = std::vector(
world().externals().begin(),
world().externals().end());
22 for (
auto [_, n] : externals) rewrite(n);
23 while (!worklist_.empty()) {
24 auto [lvm, lcm, lam] = worklist_.front();
28 world().DLOG(
"in {} (lvm={}, lcm={})", lam, lvm_, lcm_);
30 auto new_f = rewrite(lam->filter());
31 auto new_b = rewrite(lam->body());
32 lam->reset({new_f, new_b});
36 for (
auto lam : new_externals_) lam->make_external();
39Lam* LowerTypedClos::make_stub(
Lam* lam,
enum Mode mode,
bool adjust_bb_type) {
40 assert(lam &&
"make_stub: not a lam");
41 if (
auto i = old2new_.find(lam); i != old2new_.end() && i->second->isa_mut<
Lam>())
return i->second->as_mut<
Lam>();
43 auto new_dom = w.sigma(
DefVec(lam->num_doms(), [&](
auto i) ->
const Def* {
44 auto new_dom = rewrite(lam->dom(i));
45 if (i == Clos_Env_Param) {
49 return world().call<mem::Ptr0>(new_dom);
53 if (
Lam::isa_basicblock(lam) && adjust_bb_type) new_dom = insert_ret(new_dom, dummy_ret_->type());
54 auto new_type = w.cn(new_dom);
55 auto new_lam = lam->
stub(new_type);
56 w.DLOG(
"stub {} ~> {}", lam, new_lam);
60 new_externals_.emplace_back(new_lam);
67 lcm = w.extract(env_mem, 0_u64)->set(
"mem");
68 env = w.extract(env_mem, 1_u64)->set(
"closure_env");
69 }
else if (mode == Unbox) {
72 auto new_args =
w.tuple(
DefVec(lam->num_doms(), [&](
auto i) {
73 return (i == Clos_Env_Param) ? env : (lam->var(i) == mem::mem_var(lam)) ? lcm : *new_lam->var(i);
75 assert(new_args->num_projs() == lam->num_doms());
76 assert(lam->num_doms() <= new_lam->num_doms());
77 map(lam->
var(), new_args);
79 return map(lam, new_lam)->as<
Lam>();
82const Def* LowerTypedClos::rewrite(
const Def* def) {
83 switch (def->node()) {
93 if (
auto i = old2new_.find(def); i != old2new_.end())
return i->second;
94 if (
auto var = def->isa<
Var>();
95 var && var->mut()->isa_mut<Lam>())
96 assert(
false &&
"Lam vars should appear in a map!");
98 auto new_type =
rewrite(def->type());
103 auto env_type =
rewrite(ct->op(2));
104 return map(def,
w.sigma({pi, env_type}));
105 }
else if (
auto proj = def->isa<Extract>()) {
106 auto tuple = proj->tuple();
109 assert(idx && idx <= 2 &&
"unknown proj from closure tuple");
111 return map(def, env_type());
113 return map(def,
rewrite(tuple)->proj(*idx - 1));
114 }
else if (
auto var = tuple->isa<
Var>(); var &&
isa_clos_type(var->mut())) {
115 assert(
false &&
"proj fst type form closure type");
122 const Def* fn = make_stub(
c.fnc_as_lam(), mode,
true);
123 if (env->
type() ==
w.sigma()) {
125 env =
w.bot(env_type());
128 auto mem =
w.extract(mem_ptr, 0_u64);
129 auto env_ptr = mem_ptr->proj(1_u64);
136 return map(def,
w.tuple({fn, env}));
137 }
else if (
auto lam = def->isa_mut<Lam>()) {
138 return make_stub(lam, No_Env,
false);
139 }
else if (
auto mut = def->isa_mut()) {
141 auto new_mut = mut->stub(new_type);
143 for (
size_t i = 0; i < mut->num_ops(); i++)
144 if (mut->op(i)) new_mut->set(i,
rewrite(mut->op(i)));
145 if (!def->isa_mut<Global>() &&
Check::alpha(mut, new_mut))
return map(mut, mut);
146 if (
auto imm = new_mut->immutabilize())
return map(mut, imm);
148 }
else if (def->isa<
Axiom>()) {
151 auto new_ops =
DefVec(def->num_ops(), [&](
auto i) { return rewrite(def->op(i)); });
153 if (
auto app = def->isa<App>()) {
155 if (
auto p = app->callee()->isa<Extract>();
157 new_ops[1] = insert_ret(new_ops[1], dummy_ret_);
160 auto new_def = def->rebuild(new_type, new_ops);
171 for (
size_t i = 0; i < new_def->num_ops(); i++)
172 if (new_def->op(i)->type() ==
w.annex<
mem::M>()) new_def = new_def->refine(i, lcm_);
174 if (new_type ==
w.annex<
mem::M>()) {
177 }
else if (new_type->isa<Sigma>()) {
178 for (
size_t i = 0; i < new_type->num_ops(); i++) {
179 if (new_type->op(i) ==
w.annex<
mem::M>()) {
180 lcm_ =
w.extract(new_def, i);
181 lvm_ =
w.extract(def, i);
187 return map(def, new_def);
static bool alpha(Ref d1, Ref d2)
Are d1 and d2 α-equivalent?
bool is_set() const
Yields true if empty or the last op is set.
Ref var(nat_t a, nat_t i)
static const Lam * isa_basicblock(Ref d)
static std::optional< T > isa(Ref def)
static const Pi * isa_basicblock(Ref d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
This is a thin wrapper for std::span<T, N> with the following additional features:
void start() override
Actual entry.
ClosLit isa_clos_lit(Ref def, bool fn_isa_lam=true)
Tries to match a closure literal.
static constexpr size_t Clos_Env_Param
Describes where the environment is placed in the argument list.
const Sigma * isa_clos_type(Ref def)
Ref op_alloc(Ref type, Ref mem)
Ref mem_var(Lam *lam)
Returns the memory argument of a function if it has one.
Ref op_slot(Ref type, Ref mem)
Vector< const Def * > DefVec
DefVec rewrite(Def *mut, Ref arg)