21 void enter()
override;
38 auto [entry, inserted] = old2wrapper_.emplace(def,
nullptr);
39 auto& wrapper = entry->second;
41 wrapper = w.mut_lam(def->
type()->as<
Pi>());
42 wrapper->app(
false, def, wrapper->
var());
44 wrapper_.emplace(wrapper);
const Def * var(nat_t a, nat_t i) noexcept
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Vars free_vars() const
Compute a global solution by transitively following mutables as well.
Performs η-expansion: f -> λx.f x, if f is a Lam with more than one user and does not appear in calle...
A dependent function type.
RWPass(PassMan &man, std::string_view name)
bool has_intersection(Set other) const noexcept
Is ?.
const Def * call(Id id, Args &&... args)
Complete curried call of annexes obeying implicits.
const Def * rewrite(const Def *) override
const App * rewrite_callee(const App *app)
void enter() override
Invoked just before Pass::rewriteing PassMan::curr_mut's body.
const App * rewrite_arg(const App *app)
bool from_outer_scope(const Def *lam)
ClosConvPrep(PassMan &man, EtaExp *eta_exp)
bool from_outer_scope(Lam *lam)
const Def * eta_wrap(const Def *def, attr a)
GIDMap< const Def *, To > DefMap
GIDSet< const Def * > DefSet