7using namespace std::literals;
13bool is_toplevel(
const Def* fd) {
14 return fd->has_const_dep() || fd->isa_mut<
Global>() || fd->isa<
Axiom>() || !fd->is_term();
17bool is_memop_res(
const Def* fd) {
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); });
29 std::queue<const Def*> queue;
30 queue.emplace(nest.
root()->
mut());
32 while (!queue.empty()) {
33 auto def =
pop(queue);
34 for (
auto op : def->
deps()) {
38 if (
auto [_, ins] = bound.emplace(op); ins) queue.emplace(op);
52void FreeDefAna::split_fd(Node* node,
const Def* fd,
bool& init_node, NodeQueue& worklist) {
54 if (is_toplevel(fd))
return;
56 if (var != lam->ret_var()) node->add_fvs(fd);
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;
70 }
else if (is_memop_res(fd)) {
74 for (
auto op : fd->
ops()) split_fd(node, op, init_node, worklist);
78std::pair<FreeDefAna::Node*, bool> FreeDefAna::build_node(Def* mut, NodeQueue& worklist) {
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);
90 w.DLOG(
"FVA: init {}", mut);
96 while (!worklist.empty()) {
97 auto node = worklist.front();
99 if (is_done(node))
continue;
100 auto changed = is_bot(node);
102 for (
auto p : node->preds) {
104 for (
auto&& pfv : pfvs) changed |= node->add_fvs(pfv).second;
107 for (
auto s : node->succs) worklist.push(s);
112 auto worklist = NodeQueue();
113 auto [node, _] = build_node(lam, worklist);
114 if (!is_done(node)) {
128 for (
auto mut :
world().copy_externals()) rewrite(mut, subst);
129 while (!worklist_.empty()) {
130 auto def = worklist_.front();
133 if (
auto i = closures_.find(def); i != closures_.end()) {
134 rewrite_body(i->second.fn, subst);
136 world().DLOG(
"RUN: rewrite def {}", def);
142void ClosConv::rewrite_body(
Lam* new_lam,
Def2Def& subst) {
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;
148 if (!old_fn->is_set())
return;
150 w.DLOG(
"rw body: {} [old={}, env={}]\nt", new_fn, old_fn, env);
153 subst.emplace(env, env_param);
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));
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);
165 auto filter = rewrite(new_fn->filter(), subst);
166 auto body = rewrite(new_fn->body(), subst);
167 new_fn->reset({filter, body});
170const Def* ClosConv::rewrite(
const Def* def,
Def2Def& subst) {
171 switch (def->node()) {
181 auto map = [&](
const Def* new_def) {
182 subst[def] = new_def;
183 assert(subst[def] == new_def);
187 if (
auto i = subst.find(def); i != subst.end()) {
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);
201 if (
auto ret_lam =
a->arg()->isa_mut<Lam>()) {
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));
219 auto bb_lam =
a->arg()->isa_mut<
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]);
228 }
else if (
auto [var, lam] =
ca_isa_var<Lam>(def); var && lam && lam->ret_var() == var) {
231 auto new_lam = make_stub(lam, subst).fn;
233 return map(new_lam->
var(new_idx));
236 auto new_type = rewrite(def->type(), subst);
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;
242 return glob_muts_[mut] = rewrite_mut(global, new_type, subst);
245 w.DLOG(
"RW: mut {}", mut);
246 auto new_mut = rewrite_mut(mut, new_type, subst);
249 if (
auto imm = new_mut->immutabilize())
return map(imm);
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>())
258 return map(def->rebuild(new_type, new_ops));
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));
272const Pi* ClosConv::rewrite_type_cn(
const Pi* pi,
Def2Def& subst) {
274 auto new_ops =
DefVec(pi->num_doms(), [&](
auto i) { return rewrite(pi->dom(i), subst); });
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;
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);
285 auto ct =
ctype(w, new_doms, env_type);
287 glob_muts_.emplace(pi, ct);
288 w.DLOG(
"C-TYPE: pct {} ~~> {}", pi, ct);
290 w.DLOG(
"C-TYPE: ct {}, env = {} ~~> {}", pi, env_type, ct);
295ClosConv::Stub ClosConv::make_stub(
const DefSet& fvs, Lam* old_lam,
Def2Def& subst) {
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);
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());
314 new_ext_lam->unset();
318 new_lam->set(old_lam->filter(), old_lam->body());
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);
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);
static bool alpha(Ref d1, Ref d2)
constexpr auto ops() const noexcept
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
bool has_const_dep() const
Neither a Dep::Mut nor a Dep::Var; can often be used as shortcut as an optimization.
Ref var(nat_t a, nat_t i) noexcept
Lam * set_filter(Filter)
Set filter first.
Lam * set_body(Ref body)
Set body second.
static const Lam * isa_cn(Ref d)
static const Lam * isa_basicblock(Ref d)
Def * mut() const
The mutable capsulated in this Node or nullptr, if it's a virtual root comprising several Nodes.
Builds a nesting tree of all immutables/binders.
const Node * root() const
bool contains(const Def *def) const
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.
DefSet free_defs(const Nest &nest)
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
auto pop(S &s) -> decltype(s.top(), typename S::value_type())
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