7 if (def->isa<
Var>())
return true;
8 if (
auto extract = def->isa<Extract>())
return extract->tuple()->isa<
Var>();
13const App* eta_rule(Lam* lam) {
14 if (
auto app = lam->body()->isa<App>()) {
15 if (app->arg() == lam->var() && (is_var(app->callee()) || app->callee()->isa<Lam>()))
return app;
22 for (
size_t i = 0, e = def->
num_ops(); i != e; ++i) {
25 if (
auto app = eta_rule(lam); app && !irreducible_.contains(lam)) {
27 auto new_def = def->
refine(i, app->callee());
28 world().DLOG(
"eta-reduction '{}' -> '{}' by eliminating '{}'", def, new_def, lam);
40 auto succ = irreducible_.emplace(lam).second;
42 world().DLOG(
"irreducible: {}; found {}", lam, var);
bool is_set() const
Yields true if empty or the last op is set.
const Def * op(size_t i) const
const Def * refine(size_t i, const Def *new_op) const
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
@ Reduce
η-reduction performed.
Ref rewrite(Ref) override
undo_t analyze(const Var *) override
undo_t undo_visit(Def *mut) const
Helper class to retrieve Infer::arg if present.
const App * isa_callee(const Def *def, size_t i)
static constexpr undo_t No_Undo