3using namespace std::literals;
20 const auto&
id = annex->
id;
41 auto _ = e.world().push(
loc());
43 for (
const auto&
import :
imports())
import->emit(e);
44 for (
const auto& decl :
decls()) decl->emit(e);
65 auto _ = e.world().push(
loc());
78 auto _ = e.world().push(
loc());
79 return type() ?
type()->
emit(e) : e.world().mut_infer_type();
89 auto _ = e.world().push(
loc());
95 auto type = e.world().type_infer_univ();
96 sigma = e.world().mut_sigma(type, n);
98 auto var = sigma->
var();
99 auto& sym2idx = e.sigma2sym2idx[sigma];
101 for (
size_t i = 0; i != n; ++i) {
104 if (
auto id =
ptrn(i)->isa<IdPtrn>()) sym2idx[
id->dbg().sym()] = i;
112 auto _ = e.world().push(
loc());
113 type = type ? type : e.world().type_infer_univ();
114 return e.world().mut_sigma(type,
num_ptrns());
122 auto _ = e.world().push(
loc());
136 return e.world().type(l);
142 case Tag::K_Univ:
return e.world().univ();
143 case Tag::K_Nat:
return e.world().type_nat();
144 case Tag::K_Idx:
return e.world().type_idx();
145 case Tag::K_Bool:
return e.world().type_bool();
146 case Tag::K_ff:
return e.world().lit_ff();
147 case Tag::K_tt:
return e.world().lit_tt();
148 case Tag::K_i1:
return e.world().lit_i1();
149 case Tag::K_i8:
return e.world().lit_i8();
150 case Tag::K_i16:
return e.world().lit_i16();
151 case Tag::K_i32:
return e.world().lit_i32();
152 case Tag::K_i64:
return e.world().lit_i64();
153 case Tag::K_I1:
return e.world().type_i1();
154 case Tag::K_I8:
return e.world().type_i8();
155 case Tag::K_I16:
return e.world().type_i16();
156 case Tag::K_I32:
return e.world().type_i32();
157 case Tag::K_I64:
return e.world().type_i64();
158 case Tag::T_star:
return e.world().type<0>();
159 case Tag::T_box:
return e.world().type<1>();
160 default: fe::unreachable();
171 case Tag::L_u:
return t ? e.world().lit(t,
tok().lit_u()) : e.world().lit_nat(
tok().lit_u());
172 case Tag::L_i:
return tok().
lit_i();
173 case Tag::L_c:
return e.world().lit_i8(
tok().lit_c());
174 case Tag::L_str:
return e.world().tuple(
tok().sym());
175 case Tag::T_bot:
return t ? e.world().bot(t) : e.world().type_bot();
176 case Tag::T_top:
return t ? e.world().top(t) : e.world().type_top();
177 default: fe::unreachable();
184 for (
const auto& decl :
decls() | std::ranges::views::reverse) decl->emit(e);
186 for (
const auto& decl :
decls()) decl->emit(e);
198 auto d = dom()->
emit(e);
199 auto c = codom()->
emit(e);
200 return e.world().pi(d, c);
208 auto sigma = e.world().mut_sigma(2)->set(
loc());
209 auto var = sigma->var()->set(
ret()->
loc().anew_begin());
210 sigma->set(0, dom_t);
213 sigma->set(1, ret_t);
215 if (
auto imm = sigma->immutabilize())
227 return dom()->
decl_ = e.world().mut_pi(type, dom()->is_implicit())->set(
loc());
234 auto cod = codom() ? codom()->
emit(e) : e.world().type_bot();
248 auto c = callee()->emit(e);
249 auto a = arg()->emit(e);
250 return is_explicit() ? e.world().app(c, a) : e.world().implicit_app(c, a);
254 auto c = callee()->emit(e);
256 auto con = e.world().mut_lam(cn);
257 auto pair = e.world().tuple({arg()->emit(e), con});
258 auto app = e.world().app(c, pair)->set(c->loc() + arg()->
loc());
259 ptrn()->emit_value(e, con->var());
260 con->set(
false, body()->
emit(e));
264 error(c->loc(),
"callee of a ret expression must type as a returning continuation but got '{}' of type '{}'", c,
273 DefVec elems(num_elems(), [&](
size_t i) {
return elem(i)->emit(e); });
274 return e.world().tuple(elems);
278 auto s = shape()->emit_type(e);
279 if (shape()->dbg().is_anon()) {
280 auto b = body()->emit(e);
281 return arr ? e.world().arr(s, b) : e.world().pack(s, b);
284 auto t = e.world().type_infer_univ();
285 auto a = e.world().mut_arr(t);
290 shape()->emit_value(e, var);
291 a->set_body(body()->
emit(e));
292 if (
auto imm = a->immutabilize())
return imm;
295 auto p = e.world().mut_pack(a);
297 shape()->emit_value(e, var);
298 auto b = body()->emit(e);
299 a->set_body(b->type());
301 if (
auto imm = p->immutabilize())
return imm;
310 auto tup = tuple()->emit(e);
311 if (
auto dbg = std::get_if<Dbg>(&index())) {
312 if (
auto sigma = tup->type()->isa_mut<
Sigma>()) {
313 if (
auto i = e.sigma2sym2idx.find(sigma); i != e.sigma2sym2idx.end()) {
314 auto sigma = i->first->as_mut<
Sigma>();
315 const auto& sym2idx = i->second;
316 if (
auto i = sym2idx.find(dbg->sym()); i != sym2idx.end())
317 return e.world().extract(tup, sigma->num_ops(), i->second);
321 if (decl())
return e.world().extract(tup, decl()->def());
322 error(dbg->loc(),
"cannot resolve index '{}' for extraction", dbg);
326 auto i = expr->emit(e);
327 return e.world().extract(tup, i);
331 auto t = tuple()->emit(e);
332 auto i = index()->emit(e);
333 auto v = value()->emit(e);
334 return e.world().insert(t, i, v);
344 mim_type_ = type()->emit(e);
345 auto&
id = annex_->id;
349 if (curry_.lit_u() >
id.curry)
350 error(curry_.loc(),
"curry counter cannot be greater than {}",
id.curry);
352 id.curry = curry_.lit_u();
356 if (trip_.lit_u() >
id.curry)
357 error(trip_.loc(),
"trip counter cannot be greater than curry counter '{}'", (
int)
id.curry);
359 id.trip = trip_.lit_u();
362 auto pi = mim_type_->isa<
Pi>();
365 else if (
bool(pi) ^
bool(*annex_->pi))
366 error(dbg().
loc(),
"all declarations of annex '{}' have to be function types if any is", dbg().sym());
368 if (num_subs() == 0) {
369 auto norm = e.driver().normalizer(
id.plugin,
id.tag, 0);
370 auto axiom = e.world().axiom(norm,
id.curry,
id.trip, mim_type_,
id.plugin,
id.tag, 0)->set(dbg());
372 e.world().register_annex(
id.plugin,
id.tag, 0, axiom);
374 sub_t offset = annex_->subs.size();
375 for (
sub_t i = 0, n = num_subs(); i != n; ++i) {
376 auto& aliases = annex_->subs.emplace_back(std::deque<Sym>());
377 sub_t s = i + offset;
378 auto norm = e.driver().normalizer(
id.plugin,
id.tag, s);
379 auto name = e.world().sym(dbg().sym().str() +
"."s + sub(i).front()->dbg().sym().str());
380 auto axiom = e.world().axiom(norm,
id.curry,
id.trip, mim_type_,
id.plugin,
id.tag, s)->set(name);
381 e.world().register_annex(
id.plugin,
id.tag, s, axiom);
383 for (
const auto& alias : sub(i)) {
385 aliases.emplace_back(alias->dbg().sym());
392 auto v = value()->emit(e);
393 def_ = ptrn()->emit_value(e, v);
394 e.register_annex(annex_, sub_, def_);
398 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_decl(e);
399 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_body(e);
403 auto t = type() ? type()->emit(e) : e.world().type_infer_univ();
404 def_ = body()->emit_decl(e, t);
409 body()->emit_body(e, def_);
411 e.register_annex(annex_, sub_, def_);
415 lam_ = e.world().mut_lam(pi_);
416 auto var = lam_->var();
419 ptrn()->emit_value(e, var->proj(2, 0));
420 ret()->emit_value(e, var->proj(2, 1));
422 ptrn()->emit_value(e, var);
429 auto _ = e.world().push(
loc());
430 bool is_cps = tag_ == Tag::K_cn || tag_ == Tag::K_con || tag_ == Tag::K_fn || tag_ == Tag::K_fun;
433 for (
size_t i = 0, n = num_doms(); i != n; ++i) {
434 for (
const auto& dom : doms() | std::ranges::views::drop(i)) dom->
emit_type(e);
435 auto cod = codom() ? codom()->
emit(e) : is_cps ? e.world().type_bot() : e.world().mut_infer_type();
437 for (
const auto& dom : doms() | std::ranges::views::drop(i) | std::ranges::views::reverse) {
443 auto lam = cur->emit_value(e);
444 auto filter = cur->filter() ? cur->filter()->emit(e)
445 : i + 1 == n && is_cps ? e.world().lit_ff()
446 : e.world().lit_tt();
447 lam->set_filter(filter);
450 def_ = lam->set(dbg().sym());
452 dom(i - 1)->lam_->set_body(lam);
457 doms().back()->lam_->set_body(body()->
emit(e));
458 if (is_external()) doms().front()->lam_->make_external();
459 e.register_annex(annex_, sub_, def_);
464 if (tag() == Tag::K_cfun) {
465 auto ret_t = codom()->
emit(e);
466 def_ = e.world().mut_fun(dom_t, ret_t)->set(dbg());
468 def_ = e.world().mut_con(dom_t)->set(dbg());
static std::pair< u8, u8 > infer_curry_and_trip(const Def *type)
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Def * set(size_t i, Ref)
Successively set from left to right.
Ref var(nat_t a, nat_t i)
Ref proj(nat_t a, nat_t i) const
Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.
Some "global" variables needed all over the place.
A dependent function type.
Pi * set_codom(Ref codom)
const Pi * ret_pi() const
Yields the last Pi::dom, if it Pi::isa_basicblock.
Helper class to retrieve Infer::arg if present.
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Sigma * set(size_t i, const Def *def)
The World represents the whole program and manages creation of MimIR nodes (Defs).
const Driver & driver() const
const Def * register_annex(flags_t f, const Def *)
Ref emit_type(Emitter &) const override
const Ptrn * ptrn() const
Ref emit_value(Emitter &, Ref) const override
Ref emit_(Emitter &) const override
Ref emit_(Emitter &) const override
Ref emit_(Emitter &) const override
void emit_body(Emitter &, Ref decl) const override
Ref emit_decl(Emitter &, Ref type) const override
void emit(Emitter &) const override
void emit(Emitter &) const override
const Expr * expr() const
const auto & decls() const
Ref emit_(Emitter &) const override
absl::node_hash_map< Sigma *, fe::SymMap< size_t >, GIDHash< const Def * >, GIDEq< const Def * > > sigma2sym2idx
void register_annex(AnnexInfo *annex, sub_t sub, Ref def)
Ref emit_(Emitter &) const override
Ref emit_value(Emitter &, Ref) const override
Ref emit_type(Emitter &) const override
virtual Ref emit_(Emitter &) const =0
Ref emit(Emitter &) const
Ref emit_value(Emitter &, Ref) const override
Ref emit_type(Emitter &) const override
const IdPtrn * id() const
const Decl * decl() const
Ref emit_(Emitter &) const override
Ref emit_type(Emitter &) const override
const Expr * type() const
Ref emit_value(Emitter &, Ref) const override
void emit(Emitter &) const
const Module * module() const
Ref emit_(Emitter &) const override
Ref emit_(Emitter &) const override
Lam * emit_value(Emitter &) const
void emit_decl(Emitter &) const override
void emit_body(Emitter &) const override
Ref emit_decl(Emitter &, Ref type) const override
void emit_body(Emitter &, Ref decl) const override
Ref emit_(Emitter &) const override
void emit(Emitter &) const override
const Expr * type() const
Ref emit_(Emitter &) const override
const auto & decls() const
const auto & implicit_imports() const
const auto & imports() const
virtual void emit_type(Emitter &) const
const IdPtrn * ret() const
const Ptrn * ptrn() const
void emit_body(Emitter &, Ref decl) const override
Ref emit_(Emitter &) const override
Ref emit_decl(Emitter &, Ref type) const override
virtual Ref emit_value(Emitter &, Ref) const =0
virtual Ref emit_type(Emitter &) const =0
void emit(Emitter &) const override
virtual void emit_body(Emitter &) const
virtual void emit_decl(Emitter &) const
Ref emit_(Emitter &) const override
void emit_body(Emitter &, Ref decl) const override
Ref emit_(Emitter &) const override
Ref emit_decl(Emitter &, Ref type) const override
const Lit * lit_i() const
Ref emit_(Emitter &) const override
const Ptrn * ptrn(size_t i) const
Ref emit_value(Emitter &, Ref) const override
Ref emit_type(Emitter &) const override
Ref emit_decl(Emitter &, Ref type) const
Ref emit_body(Emitter &, Ref decl) const
const Expr * level() const
Ref emit_(Emitter &) const override
Ref emit_(Emitter &) const override
void error(Loc loc, const char *f, Args &&... args)
constexpr decltype(auto) get(mim::Span< T, N > span)
struct mim::ast::AnnexInfo::@1 id