12 if (
auto [_, ins] = analyzed_.emplace(def); !ins)
return;
14 if (
auto app = def->isa<
App>()) {
16 visit(app->callee(), Lattice::Single);
19 for (
auto d : def->
deps())
24void RetWrap::visit(
const Def* def, Lattice l) {
25 if (
auto lam = def->isa_mut<
Lam>()) {
26 if (
auto ret_var = lam->ret_var()) {
27 auto var = lam->has_var();
29 if (ret_var != lam->var()) {
30 DLOG(
"{} → {}", var, ret_var);
31 var2def_[var] = ret_var;
34 }
else if (
auto i = def2lattice_.find(def); i != def2lattice_.end()) {
35 i->second = join(i->second, l);
36 }
else if (
auto app = def->isa<
App>()) {
37 if (
auto var = app->arg()->isa<
Var>()) {
38 if (
auto i = var2def_.find(var); i != var2def_.end()) {
39 auto lam = var->mut()->as_mut<
Lam>();
40 DLOG(
"split: `{}`", lam);
42 def2lattice_[i->second] = Eta;
51 if (lattice(old_def) == Eta) {
52 auto [i, ins] = def2eta_.emplace(old_def,
nullptr);
54 DLOG(
"eta-expand: `{}` → `{}`", old_def, i->second);
61 if (split_.contains(old_lam)) {
63 auto split_vars = old_lam->
vars();
64 auto ret_var = old_lam->
ret_var();
65 assert(split_vars.back() == ret_var &&
"we assume that the last element is the ret_var");
68 split_vars.back() = ret_cont;
70 map(old_lam, new_lam);
75 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 *)
const Def * map(const Def *old_def, const Def *new_def)
Map old_def to new_def and returns 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)