32 auto bb = app->as<
App>()->arg();
33 auto bb_only = bb->as<
Lit>()->get<u64>();
34 builder.add_pass<
EtaRed>(app, bb_only);
59 return f->isa_mut<
Lam>();
65 auto tpl = def->isa<
Tuple>();
73 if (!lambda_or_branch || fnc->isa<
Lam>())
return ClosLit(tpl, a);
81 auto& w = env->
world();
82 auto pi = lam->
type()->as<
Pi>();
85 return w.tuple(ct, {env->
type(), lam, env})->isa<Tuple>();
96 auto [ty, pi, env] = c->projs<3>();
101 auto& w = closure->
world();
103 auto pi = fn->type()->as<
Pi>();
104 return w.app(fn,
DefVec(pi->num_doms(), [&](
auto i) { return clos_insert_env(i, env, args); }));
112 auto& w = def->
world();
114 if (!sig || sig->num_ops() < 3 || sig->op(0_u64) != w.type())
return nullptr;
115 auto var = sig->
var(0_u64);
116 if (sig->op(2_u64) != var)
return nullptr;
117 auto pi = sig->
op(1_u64)->isa<
Pi>();
122 auto& w = pi->
world();
123 auto doms = pi->doms();
129 auto& w = ct->
world();
130 auto pi = ct->
op(1_u64)->as<
Pi>();
132 return w.cn(new_dom);
147 auto sigma = w.mut_sigma(w.type(), 3_u64)->set(
"Clos");
148 sigma->set(0_u64, w.type());
149 sigma->set(1_u64,
ctype(w, doms, sigma->var(0_u64)));
150 sigma->set(2_u64, sigma->var(0_u64));
154 DefVec(doms.size() + 1, [&](
auto i) { return clos_insert_env(i, env_type, [&](auto j) { return doms[j]; }); }));
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.
Ref var(nat_t a, nat_t i)
A dependent function type.
static const Pi * isa_cn(Ref d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
Helper class to retrieve Infer::arg if present.
This is a thin wrapper for std::span<T, N> with the following additional features:
Data constructor for a Sigma.
The World represents the whole program and manages creation of MimIR nodes (Defs).
Wrapper around a Def that can be used to match closures (see isa_clos_lit).
ClosLit isa_clos_lit(Ref def, bool fn_isa_lam=true)
Tries to match a closure literal.
void register_normalizers(Normalizers &normalizers)
Ref clos_sub_env(Ref tup_or_sig, Ref new_env)
Sigma * clos_type(const Pi *pi)
Creates a typed closure type from pi.
std::tuple< Ref, Ref, Ref > clos_unpack(Ref c)
Deconstruct a closure into (env_type, function, env).
const Pi * clos_type_to_pi(Ref ct, Ref new_env_type=nullptr)
Convert a closure type to a Pi, where the environment type has been removed or replaced by new_env_ty...
Ref clos_apply(Ref closure, Ref args)
Apply a closure to arguments.
size_t shift_env(size_t i)
Ref clos_remove_env(size_t i, std::function< Ref(size_t)> f)
static constexpr size_t Clos_Env_Param
Describes where the environment is placed in the argument list.
const Sigma * isa_clos_type(Ref def)
Ref ctype(World &w, Defs doms, Ref env_type=nullptr)
size_t skip_env(size_t i)
Ref clos_pack(Ref env, Ref fn, Ref ct=nullptr)
Pack a typed closure. This assumes that fn expects the environment as its Clos_Env_Paramth argument.
Ref clos_insert_env(size_t i, Ref env, std::function< Ref(size_t)> f)
Vector< const Def * > DefVec
absl::flat_hash_map< flags_t, std::function< void(World &, PipelineBuilder &, const Def *)> > Passes
axiom ↦ (pipeline part) × (axiom application) → () The function should inspect Application to const...
void register_pass(Passes &passes, CArgs &&... args)
MIM_EXPORT mim::Plugin mim_get_plugin()
void register_phase(Passes &passes, CArgs &&... args)
absl::flat_hash_map< flags_t, NormalizeFn > Normalizers
constexpr decltype(auto) get(mim::Span< T, N > span)
static constexpr flags_t Base
Basic info and registration function pointer to be returned from a specific plugin.