10using namespace std::literals;
16bool is_toplevel(
const Def* fd) {
17 return fd->dep_const() || fd->isa_mut<
Global>() || fd->isa<
Axiom>() || !fd->is_term();
20bool is_memop_res(
const Def* fd) {
22 if (!proj)
return false;
23 auto types = proj->tuple()->type()->ops();
24 return std::any_of(types.begin(), types.end(), [](
auto d) { return match<mem::M>(d); });
33void FreeDefAna::split_fd(Node* node,
const Def* fd,
bool& init_node, NodeQueue& worklist) {
35 if (is_toplevel(fd))
return;
37 if (var != lam->ret_var()) node->add_fvs(fd);
40 }
else if (
auto pred = fd->isa_mut()) {
41 if (pred != node->mut) {
42 auto [pnode, inserted] = build_node(pred, worklist);
43 node->preds.push_back(pnode);
44 pnode->succs.push_back(node);
45 init_node |= inserted;
47 }
else if (fd->dep() ==
Dep::Var && !fd->isa<Tuple>()) {
51 }
else if (is_memop_res(fd)) {
55 for (
auto op : fd->ops()) split_fd(node, op, init_node, worklist);
59std::pair<FreeDefAna::Node*, bool> FreeDefAna::build_node(Def* mut, NodeQueue& worklist) {
61 auto [p, inserted] = lam2nodes_.emplace(mut,
nullptr);
62 if (!inserted)
return {p->second.get(),
false};
63 w.DLOG(
"FVA: create node: {}", mut);
64 p->second = std::make_unique<Node>(Node{mut, {}, {}, {}, 0});
65 auto node = p->second.get();
66 auto scope = Scope(mut);
67 bool init_node =
false;
68 for (
auto v : scope.free_defs()) split_fd(node, v, init_node, worklist);
71 w.DLOG(
"FVA: init {}", mut);
77 while (!worklist.empty()) {
78 auto node = worklist.front();
80 if (is_done(node))
continue;
81 auto changed = is_bot(node);
83 for (
auto p : node->preds) {
85 for (
auto&& pfv : pfvs) changed |= node->add_fvs(pfv).second;
88 for (
auto s : node->succs) worklist.push(s);
93 auto worklist = NodeQueue();
94 auto [node, _] = build_node(lam, worklist);
108 auto externals =
Vector(
world().externals().begin(),
world().externals().end());
110 for (
auto [_, ext_def] : externals) rewrite(ext_def, subst);
111 while (!worklist_.empty()) {
112 auto def = worklist_.front();
115 if (
auto i = closures_.find(def); i != closures_.end()) {
116 rewrite_body(i->second.fn, subst);
118 world().DLOG(
"RUN: rewrite def {}", def);
124void ClosConv::rewrite_body(
Lam* new_lam,
Def2Def& subst) {
126 auto it = closures_.find(new_lam);
127 assert(it != closures_.end() &&
"closure should have a stub if rewrite_body is called!");
128 auto [old_fn, num_fvs, env, new_fn] = it->second;
130 if (!old_fn->is_set())
return;
132 w.DLOG(
"rw body: {} [old={}, env={}]\nt", new_fn, old_fn, env);
135 subst.emplace(env, env_param);
137 for (
size_t i = 0; i < num_fvs; i++) {
138 auto fv = env->op(i);
139 auto sym = w.sym(
"fv_"s + (fv->sym() ? fv->sym().str() : std::to_string(i)));
140 subst.emplace(fv, env_param->proj(i)->set(sym));
144 auto params = w.tuple(
DefVec(old_fn->num_doms(), [&](
auto i) { return new_lam->var(skip_env(i)); }));
145 subst.emplace(old_fn->var(), params);
147 auto filter = rewrite(new_fn->filter(), subst);
148 auto body = rewrite(new_fn->body(), subst);
149 new_fn->reset({filter, body});
152const Def* ClosConv::rewrite(
const Def* def,
Def2Def& subst) {
153 switch (def->node()) {
163 auto map = [&](
const Def* new_def) {
164 subst[def] = new_def;
165 assert(subst[def] == new_def);
169 if (
auto i = subst.find(def); i != subst.end()) {
172 return map(type_clos(pi, subst));
173 }
else if (
auto lam = def->isa_mut<Lam>(); lam &&
Lam::isa_cn(lam)) {
174 auto [_, __, fv_env, new_lam] = make_stub(lam, subst);
175 auto clos_ty = rewrite(lam->type(), subst);
176 auto env = rewrite(fv_env, subst);
177 auto closure =
clos_pack(env, new_lam, clos_ty);
178 world().DLOG(
"RW: pack {} ~> {} : {}", lam, closure, clos_ty);
183 if (
auto ret_lam =
a->arg()->isa_mut<Lam>()) {
188 =
DefVec(ret_lam->num_doms(), [&](
auto i) { return rewrite(ret_lam->dom(i), subst); });
189 auto new_lam = ret_lam->
stub(
w.cn(new_doms));
190 subst[ret_lam] = new_lam;
191 if (ret_lam->is_set()) {
192 new_lam->
set_filter(rewrite(ret_lam->filter(), subst));
193 new_lam->
set_body(rewrite(ret_lam->body(), subst));
201 auto bb_lam =
a->arg()->isa_mut<
Lam>();
203 auto [_, __, ___, new_lam] = make_stub({}, bb_lam, subst);
204 subst[bb_lam] =
clos_pack(
w.tuple(), new_lam, rewrite(bb_lam->type(), subst));
205 rewrite_body(new_lam, subst);
206 return map(subst[bb_lam]);
210 }
else if (
auto [var, lam] =
ca_isa_var<Lam>(def); var && lam && lam->ret_var() == var) {
213 auto new_lam = make_stub(lam, subst).fn;
215 return map(new_lam->
var(new_idx));
218 auto new_type = rewrite(def->type(), subst);
220 if (
auto mut = def->isa_mut()) {
221 if (
auto global = def->isa_mut<Global>()) {
222 if (
auto i = glob_muts_.find(global); i != glob_muts_.end())
return i->second;
224 return glob_muts_[mut] = rewrite_mut(global, new_type, subst);
227 w.DLOG(
"RW: mut {}", mut);
228 auto new_mut = rewrite_mut(mut, new_type, subst);
230 if (!mut->isa_mut<Global>() &&
Check::alpha(mut, new_mut))
return map(mut);
231 if (
auto imm = new_mut->immutabilize())
return map(imm);
234 auto new_ops =
DefVec(def->num_ops(), [&](
auto i) { return rewrite(def->op(i), subst); });
235 if (
auto app = def->isa<App>(); app && new_ops[0]->type()->isa<Sigma>())
236 return map(
clos_apply(new_ops[0], new_ops[1]));
237 else if (def->isa<
Axiom>())
240 return map(def->rebuild(new_type, new_ops));
246Def* ClosConv::rewrite_mut(Def* mut,
const Def* new_type,
Def2Def& subst) {
247 auto new_mut = mut->stub(new_type);
248 subst.emplace(mut, new_mut);
249 for (
size_t i = 0; i < mut->num_ops(); i++)
250 if (mut->op(i)) new_mut->set(i, rewrite(mut->op(i), subst));
254const Pi* ClosConv::rewrite_type_cn(
const Pi* pi,
Def2Def& subst) {
256 auto new_ops =
DefVec(pi->num_doms(), [&](
auto i) { return rewrite(pi->dom(i), subst); });
260const Def* ClosConv::type_clos(
const Pi* pi,
Def2Def& subst,
const Def* env_type) {
261 if (
auto i = glob_muts_.find(pi); i != glob_muts_.end() && !env_type)
return i->second;
263 auto new_doms =
DefVec(pi->num_doms(), [&](
auto i) {
264 return (i == pi->num_doms() - 1 && Pi::isa_returning(pi)) ? rewrite_type_cn(pi->ret_pi(), subst)
265 : rewrite(pi->dom(i), subst);
267 auto ct =
ctype(w, new_doms, env_type);
269 glob_muts_.emplace(pi, ct);
270 w.DLOG(
"C-TYPE: pct {} ~~> {}", pi, ct);
272 w.DLOG(
"C-TYPE: ct {}, env = {} ~~> {}", pi, env_type, ct);
277ClosConv::Stub ClosConv::make_stub(
const DefSet& fvs, Lam* old_lam,
Def2Def& subst) {
279 auto env =
w.tuple(
DefVec(fvs.begin(), fvs.end()));
280 auto num_fvs = fvs.size();
281 auto env_type = rewrite(env->type(), subst);
282 auto new_fn_type = type_clos(old_lam->type(), subst, env_type)->as<
Pi>();
283 auto new_lam = old_lam->
stub(new_fn_type);
289 auto new_ext_lam = old_lam->stub(new_ext_type);
290 w.DLOG(
"wrap ext lam: {} -> stub: {}, ext: {}", old_lam, new_lam, new_ext_lam);
291 if (old_lam->is_set()) {
292 old_lam->transfer_external(new_ext_lam);
293 new_ext_lam->app(
false, new_lam,
clos_insert_env(env, new_ext_lam->var()));
294 new_lam->set(old_lam->filter(), old_lam->body());
296 new_ext_lam->unset();
300 new_lam->set(old_lam->filter(), old_lam->body());
302 w.DLOG(
"STUB {} ~~> ({}, {})", old_lam, env, new_lam);
303 auto closure = Stub{old_lam, num_fvs, env, new_lam};
304 closures_.emplace(old_lam, closure);
305 closures_.emplace(closure.fn, closure);
309ClosConv::Stub ClosConv::make_stub(Lam* old_lam,
Def2Def& subst) {
310 if (
auto i = closures_.find(old_lam); i != closures_.end())
return i->second;
311 auto fvs = fva_.
run(old_lam);
312 auto closure = make_stub(fvs, old_lam, subst);
313 worklist_.emplace(closure.fn);
static bool alpha(Ref d1, Ref d2)
Are d1 and d2 α-equivalent?
Ref var(nat_t a, nat_t i)
Lam * set_filter(Filter)
Set filter first.
Lam * set_body(const Def *body)
Set body second.
static const Lam * isa_cn(Ref d)
static const Lam * isa_basicblock(Ref d)
static const Pi * isa_cn(Ref d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
static const Pi * isa_basicblock(Ref d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
void start() override
Actual entry.
DefSet & run(Lam *lam)
FreeDefAna::run will compute free defs (FD) that appear in lams body.
Ref clos_apply(Ref closure, Ref args)
Apply a closure to arguments.
Ref clos_remove_env(size_t i, std::function< Ref(size_t)> f)
static constexpr size_t Clos_Env_Param
Describes where the environment is placed in the argument list.
const Sigma * isa_clos_type(Ref def)
std::tuple< const Extract *, N * > ca_isa_var(Ref def)
Checks is def is the variable of a mut of type N.
Ref ctype(World &w, Defs doms, Ref env_type=nullptr)
size_t skip_env(size_t i)
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.
Ref clos_insert_env(size_t i, Ref env, std::function< Ref(size_t)> f)
DefMap< const Def * > Def2Def
Vector< const Def * > DefVec
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
GIDSet< const Def * > DefSet
Vector(I, I, A=A()) -> Vector< typename std::iterator_traits< I >::value_type, Default_Inlined_Size< typename std::iterator_traits< I >::value_type >, A >