9 if (
auto [_, ins] =
data().emplace(lam); ins) {
10 world().DLOG(
"beta-reduction {}", lam);
11 return lam->reduce(app->arg()).back();
13 return proxy(app->type(), {lam, app->arg()}, 0);
22 if (keep_.emplace(lam).second) {
23 world().DLOG(
"found proxy app of '{}' within '{}'", lam,
curr_mut());
32 for (
auto op : def->
ops()) {
34 auto [_, ins] =
data().emplace(lam);
36 world().DLOG(
"non-callee-position of '{}'; undo inlining of {} within {}", lam, lam,
curr_mut());
undo_t analyze(const Proxy *) override
Ref rewrite(Ref) override
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
const Def * op(size_t i) const
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
undo_t undo_visit(Def *mut) const
const Proxy * proxy(Ref type, Defs ops, u32 tag=0)
Helper class to retrieve Infer::arg if present.
std::pair< const App *, Lam * > isa_apped_mut_lam(const Def *def)
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
static constexpr undo_t No_Undo