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 const auto& first = doms().front();
228 return first->decl_ = e.world().mut_pi(type, first->implicit())->set(
loc());
234 for (
const auto& dom : doms()) dom->
emit_type(e);
236 auto cod = codom() ? codom()->
emit(e) : e.world().type_bot();
237 for (
const auto& dom : doms() | std::ranges::views::reverse) {
242 return doms().front()->pi_;
255 auto c = callee()->emit(e);
256 auto a = arg()->emit(e);
257 return is_explicit() ? e.world().app(c, a) : e.world().iapp(c, a);
261 auto c = callee()->emit(e);
263 auto con = e.world().mut_lam(cn);
264 auto pair = e.world().tuple({arg()->emit(e), con});
265 auto app = e.world().app(c, pair)->set(c->loc() + arg()->
loc());
266 ptrn()->emit_value(e, con->var());
267 con->set(
false, body()->
emit(e));
271 error(c->loc(),
"callee of a ret expression must type as a returning continuation but got '{}' of type '{}'", c,
280 DefVec elems(num_elems(), [&](
size_t i) {
return elem(i)->emit(e); });
281 return e.world().tuple(elems);
285 auto s = shape()->emit_type(e);
286 if (shape()->dbg().is_anon()) {
287 auto b = body()->emit(e);
288 return arr ? e.world().arr(s, b) : e.world().pack(s, b);
291 auto t = e.world().type_infer_univ();
292 auto a = e.world().mut_arr(t);
297 shape()->emit_value(e, var);
298 a->set_body(body()->
emit(e));
299 if (
auto imm = a->immutabilize())
return imm;
302 auto p = e.world().mut_pack(a);
304 shape()->emit_value(e, var);
305 auto b = body()->emit(e);
306 a->set_body(b->type());
308 if (
auto imm = p->immutabilize())
return imm;
317 auto tup = tuple()->emit(e);
318 if (
auto dbg = std::get_if<Dbg>(&index())) {
319 if (
auto sigma = tup->type()->isa_mut<
Sigma>()) {
320 if (
auto i = e.sigma2sym2idx.find(sigma); i != e.sigma2sym2idx.end()) {
321 auto sigma = i->first->as_mut<
Sigma>();
322 const auto& sym2idx = i->second;
323 if (
auto i = sym2idx.find(dbg->sym()); i != sym2idx.end())
324 return e.world().extract(tup, sigma->num_ops(), i->second);
328 if (decl())
return e.world().extract(tup, decl()->def());
329 error(dbg->loc(),
"cannot resolve index '{}' for extraction", dbg);
333 auto i = expr->emit(e);
334 return e.world().extract(tup, i);
338 auto t = tuple()->emit(e);
339 auto i = index()->emit(e);
340 auto v = value()->emit(e);
341 return e.world().insert(t, i, v);
349 mim_type_ = type()->emit(e);
350 auto&
id = annex_->id;
354 if (curry_.lit_u() >
id.curry)
355 error(curry_.loc(),
"curry counter cannot be greater than {}",
id.curry);
357 id.curry = curry_.lit_u();
361 if (trip_.lit_u() >
id.curry)
362 error(trip_.loc(),
"trip counter cannot be greater than curry counter '{}'", (
int)
id.curry);
364 id.trip = trip_.lit_u();
367 auto pi = mim_type_->isa<
Pi>();
370 else if (
bool(pi) ^
bool(*annex_->pi))
371 error(dbg().
loc(),
"all declarations of annex '{}' have to be function types if any is", dbg().sym());
373 if (num_subs() == 0) {
374 auto norm = e.driver().normalizer(
id.plugin,
id.tag, 0);
375 auto axiom = e.world().axiom(norm,
id.curry,
id.trip, mim_type_,
id.plugin,
id.tag, 0)->set(dbg());
377 e.world().register_annex(
id.plugin,
id.tag, 0, axiom);
379 sub_t offset = annex_->subs.size();
380 for (
sub_t i = 0, n = num_subs(); i != n; ++i) {
381 auto& aliases = annex_->subs.emplace_back(std::deque<Sym>());
382 sub_t s = i + offset;
383 auto norm = e.driver().normalizer(
id.plugin,
id.tag, s);
384 auto name = e.world().sym(dbg().sym().str() +
"."s + sub(i).front()->dbg().sym().str());
385 auto axiom = e.world().axiom(norm,
id.curry,
id.trip, mim_type_,
id.plugin,
id.tag, s)->set(name);
386 e.world().register_annex(
id.plugin,
id.tag, s, axiom);
388 for (
const auto& alias : sub(i)) {
390 aliases.emplace_back(alias->dbg().sym());
397 auto v = value()->emit(e);
398 def_ = ptrn()->emit_value(e, v);
399 e.register_annex(annex_, sub_, def_);
403 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_decl(e);
404 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_body(e);
408 auto t = type() ? type()->emit(e) : e.world().type_infer_univ();
409 def_ = body()->emit_decl(e, t);
414 body()->emit_body(e, def_);
416 e.register_annex(annex_, sub_, def_);
420 lam_ = e.world().mut_lam(pi_);
421 auto var = lam_->var();
424 ptrn()->emit_value(e, var->proj(2, 0));
425 ret()->emit_value(e, var->proj(2, 1));
427 ptrn()->emit_value(e, var);
434 auto _ = e.world().push(
loc());
435 bool is_cps = tag_ == Tag::K_cn || tag_ == Tag::K_con || tag_ == Tag::K_fn || tag_ == Tag::K_fun;
438 for (
size_t i = 0, n = num_doms(); i != n; ++i) {
439 for (
const auto& dom : doms() | std::ranges::views::drop(i)) dom->
emit_type(e);
440 auto cod = codom() ? codom()->
emit(e) : is_cps ? e.world().type_bot() : e.world().mut_infer_type();
442 for (
const auto& dom : doms() | std::ranges::views::drop(i) | std::ranges::views::reverse) {
448 auto lam = cur->emit_value(e);
449 auto filter = cur->filter() ? cur->filter()->emit(e)
450 : i + 1 == n && is_cps ? e.world().lit_ff()
451 : e.world().lit_tt();
452 lam->set_filter(filter);
455 def_ = lam->set(dbg().sym());
457 dom(i - 1)->lam_->set_body(lam);
462 doms().back()->lam_->set_body(body()->
emit(e));
463 if (is_external()) doms().front()->lam_->make_external();
464 e.register_annex(annex_, sub_, def_);
469 if (tag() == Tag::K_cfun) {
470 auto ret_t = codom()->
emit(e);
471 def_ = e.world().mut_fun(dom_t, ret_t)->set(dbg());
473 def_ = e.world().mut_con(dom_t)->set(dbg());
static std::pair< u8, u8 > infer_curry_and_trip(const Def *type)
Def * set(size_t i, const Def *def)
Successively set from left to right.
const Def * 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.
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Ref var(nat_t a, nat_t i)
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
void error(Loc loc, const char *f, Args &&... args)
constexpr decltype(auto) get(mim::Span< T, N > span)
struct mim::ast::AnnexInfo::@1 id