15 if (
auto [_, ins] = analyzed_.emplace(def); !ins)
return;
17 if (
auto app = def->isa<
App>()) {
19 visit(app->callee(), Lattice::Single);
22 for (
auto d : def->
deps())
27void RetWrap::visit(
const Def* def, Lattice l) {
28 if (
auto lam = def->isa_mut<
Lam>()) {
29 if (
auto ret_var = lam->ret_var()) {
30 auto var = lam->has_var();
32 if (ret_var != lam->var()) {
33 DLOG(
"{} → {}", var, ret_var);
34 var2def_[var] = ret_var;
37 }
else if (
auto i = def2lattice_.find(def); i != def2lattice_.end()) {
38 i->second = join(i->second, l);
39 }
else if (
auto app = def->isa<
App>()) {
40 if (
auto var = app->arg()->isa<
Var>()) {
41 if (
auto i = var2def_.find(var); i != var2def_.end()) {
42 auto lam = var->mut()->as_mut<
Lam>();
43 DLOG(
"split: `{}`", lam);
45 def2lattice_[i->second] = Eta;
54 if (lattice(old_def) == Eta) {
55 auto [i, ins] = def2eta_.emplace(old_def,
nullptr);
57 DLOG(
"eta-expand: `{}` → `{}`", old_def, i->second);
64 if (split_.contains(old_lam)) {
66 auto split_vars = old_lam->
vars();
67 auto ret_var = old_lam->
ret_var();
68 assert(split_vars.back() == ret_var &&
"we assume that the last element is the ret_var");
71 split_vars.back() = ret_cont;
73 map(old_lam, new_lam);
78 return Rewriter::rewrite_mut_Lam(old_lam);
Defs deps() const noexcept
const Def * var(nat_t a, nat_t i) noexcept
static Lam * eta_expand(Filter, const Def *f)
const Def * ret_var()
Yields the Lam::var of the Lam::ret_pi.
A dependent function type.
World & new_world()
Create new Defs into this.
World & old_world()
Get old Defs from here.
const Def * rewrite_mut_Lam(Lam *) final
bool analyze() final
You can do an optional fixed-point loop on the RWPhase::old_world before rewriting.
const Def * rewrite(const Def *) final
virtual const Def * rewrite_stub(Def *, Def *)
virtual const Def * map(const Def *old_def, const Def *new_def)
virtual const Def * rewrite(const Def *)
Lam * mut_lam(const Pi *pi)
#define DLOG(...)
Vaporizes to nothingness in Debug build.
bool visit(IndexSet< Indexer, Key > &set, const Key &key)