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);
54 auto _ = e.world().push(
loc());
71 auto _ = e.world().push(
loc());
72 return type() ?
type()->
emit(e) : e.world().mut_infer_type();
80 auto _ = e.world().push(
loc());
86 auto type = e.world().type_infer_univ();
87 sigma = e.world().mut_sigma(type, n)->set(
dbg().sym());
90 auto& sym2idx = e.sigma2sym2idx[sigma];
92 for (
size_t i = 0; i != n; ++i) {
103 auto _ = e.world().push(
loc());
104 type = type ? type : e.world().type_infer_univ();
105 return e.world().mut_sigma(type,
num_ptrns())->set(
dbg().sym());
113 auto _ = e.world().push(
loc());
127 return e.world().type(l);
133 case Tag::K_Univ:
return e.world().univ();
134 case Tag::K_Nat:
return e.world().type_nat();
135 case Tag::K_Idx:
return e.world().type_idx();
136 case Tag::K_Bool:
return e.world().type_bool();
137 case Tag::K_ff:
return e.world().lit_ff();
138 case Tag::K_tt:
return e.world().lit_tt();
139 case Tag::K_i1:
return e.world().lit_i1();
140 case Tag::K_i8:
return e.world().lit_i8();
141 case Tag::K_i16:
return e.world().lit_i16();
142 case Tag::K_i32:
return e.world().lit_i32();
143 case Tag::K_i64:
return e.world().lit_i64();
144 case Tag::K_I1:
return e.world().type_i1();
145 case Tag::K_I8:
return e.world().type_i8();
146 case Tag::K_I16:
return e.world().type_i16();
147 case Tag::K_I32:
return e.world().type_i32();
148 case Tag::K_I64:
return e.world().type_i64();
149 case Tag::T_star:
return e.world().type<0>();
150 case Tag::T_box:
return e.world().type<1>();
151 default: fe::unreachable();
162 case Tag::L_u:
return t ? e.world().lit(t,
tok().lit_u()) : e.world().lit_nat(
tok().lit_u());
163 case Tag::L_i:
return tok().
lit_i();
164 case Tag::L_c:
return e.world().lit_i8(
tok().lit_c());
165 case Tag::L_str:
return e.world().tuple(
tok().sym());
166 case Tag::T_bot:
return t ? e.world().bot(t) : e.world().type_bot();
167 case Tag::T_top:
return t ? e.world().top(t) : e.world().type_top();
168 default: fe::unreachable();
175 for (
const auto& decl :
decls() | std::ranges::views::reverse) decl->emit(e);
177 for (
const auto& decl :
decls()) decl->emit(e);
189 auto d = dom()->
emit(e);
190 auto c = codom()->
emit(e);
191 return e.world().pi(d, c);
199 auto sigma = e.world().mut_sigma(2)->set(
loc());
200 auto var = sigma->var()->set(
ret()->
loc().anew_begin());
201 sigma->set(0, dom_t);
204 sigma->set(1, ret_t);
206 if (
auto imm = sigma->immutabilize())
218 const auto& first = doms().front();
219 return first->decl_ = e.world().mut_pi(type, first->is_implicit())->set(
loc());
225 for (
const auto& dom : doms()) dom->
emit_type(e);
227 auto cod = codom() ? codom()->
emit(e) : e.world().type_bot();
228 for (
const auto& dom : doms() | std::ranges::views::reverse) {
233 return doms().front()->pi_;
246 auto c = callee()->emit(e);
247 auto a = arg()->emit(e);
248 return is_explicit() ? e.world().app(c, a) : e.world().iapp(c, a);
252 auto c = callee()->emit(e);
254 auto con = e.world().mut_lam(cn);
255 auto pair = e.world().tuple({arg()->emit(e), con});
256 auto app = e.world().app(c, pair)->set(c->loc() + arg()->
loc());
257 ptrn()->emit_value(e, con->var());
258 con->set(
false, body()->
emit(e));
262 error(c->loc(),
"callee of a ret expression must type as a returning continuation but got '{}' of type '{}'", c,
271 DefVec elems(num_elems(), [&](
size_t i) {
return elem(i)->emit(e); });
272 return e.world().tuple(elems);
276 auto s = shape()->emit_type(e);
277 if (shape()->dbg().is_anon()) {
278 auto b = body()->emit(e);
279 return arr ? e.world().arr(s, b) : e.world().pack(s, b);
282 auto t = e.world().type_infer_univ();
283 auto a = e.world().mut_arr(t);
288 shape()->emit_value(e, var);
289 a->set_body(body()->
emit(e));
290 if (
auto imm = a->immutabilize())
return imm;
293 auto p = e.world().mut_pack(a);
295 shape()->emit_value(e, var);
296 auto b = body()->emit(e);
297 a->set_body(b->type());
299 if (
auto imm = p->immutabilize())
return imm;
308 auto tup = tuple()->emit(e);
309 if (
auto dbg = std::get_if<Dbg>(&index())) {
310 if (
auto sigma = tup->type()->isa_mut<
Sigma>()) {
311 if (
auto i = e.sigma2sym2idx.find(sigma); i != e.sigma2sym2idx.end()) {
312 auto sigma = i->first->as_mut<
Sigma>();
313 const auto& sym2idx = i->second;
314 if (
auto i = sym2idx.find(dbg->sym()); i != sym2idx.end())
315 return e.world().extract(tup, sigma->num_ops(), i->second);
319 if (decl())
return e.world().extract(tup, decl()->def());
320 error(dbg->loc(),
"cannot resolve index '{}' for extraction", dbg);
324 auto i = expr->emit(e);
325 return e.world().extract(tup, i);
329 auto t = tuple()->emit(e);
330 auto i = index()->emit(e);
331 auto v = value()->emit(e);
332 return e.world().insert(t, i, v);
340 mim_type_ = type()->emit(e);
341 auto&
id = annex_->id;
345 if (curry_.lit_u() >
id.curry)
346 error(curry_.loc(),
"curry counter cannot be greater than {}",
id.curry);
348 id.curry = curry_.lit_u();
352 if (trip_.lit_u() >
id.curry)
353 error(trip_.loc(),
"trip counter cannot be greater than curry counter '{}'", (
int)
id.curry);
355 id.trip = trip_.lit_u();
358 auto pi = mim_type_->isa<
Pi>();
361 else if (
bool(pi) ^
bool(*annex_->pi))
362 error(dbg().
loc(),
"all declarations of annex '{}' have to be function types if any is", dbg().sym());
364 if (num_subs() == 0) {
365 auto norm = e.driver().normalizer(
id.plugin,
id.tag, 0);
366 auto axiom = e.world().axiom(norm,
id.curry,
id.trip, mim_type_,
id.plugin,
id.tag, 0)->set(dbg());
368 e.world().register_annex(
id.plugin,
id.tag, 0, axiom);
370 sub_t offset = annex_->subs.size();
371 for (
sub_t i = 0, n = num_subs(); i != n; ++i) {
372 auto& aliases = annex_->subs.emplace_back(std::deque<Sym>());
373 sub_t s = i + offset;
374 auto norm = e.driver().normalizer(
id.plugin,
id.tag, s);
375 auto name = e.world().sym(dbg().sym().str() +
"."s + sub(i).front()->dbg().sym().str());
376 auto axiom = e.world().axiom(norm,
id.curry,
id.trip, mim_type_,
id.plugin,
id.tag, s)->set(name);
377 e.world().register_annex(
id.plugin,
id.tag, s, axiom);
379 for (
const auto& alias : sub(i)) {
381 aliases.emplace_back(alias->dbg().sym());
388 auto v = value()->emit(e);
389 def_ = ptrn()->emit_value(e, v);
390 e.register_annex(annex_, sub_, def_);
394 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_decl(e);
395 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_body(e);
399 auto t = type() ? type()->emit(e) : e.world().type_infer_univ();
400 def_ = body()->emit_decl(e, t);
405 body()->emit_body(e, def_);
407 e.register_annex(annex_, sub_, def_);
411 lam_ = e.world().mut_lam(pi_);
412 auto var = lam_->var();
415 ptrn()->emit_value(e, var->proj(2, 0));
416 ret()->emit_value(e, var->proj(2, 1));
418 ptrn()->emit_value(e, var);
425 auto _ = e.world().push(
loc());
426 bool is_cps = tag_ == Tag::K_cn || tag_ == Tag::K_con || tag_ == Tag::K_fn || tag_ == Tag::K_fun;
429 for (
size_t i = 0, n = num_doms(); i != n; ++i) {
430 for (
const auto& dom : doms() | std::ranges::views::drop(i)) dom->
emit_type(e);
431 auto cod = codom() ? codom()->
emit(e) : is_cps ? e.world().type_bot() : e.world().mut_infer_type();
433 for (
const auto& dom : doms() | std::ranges::views::drop(i) | std::ranges::views::reverse) {
439 auto lam = cur->emit_value(e);
440 auto filter = cur->filter() ? cur->filter()->emit(e)
441 : i + 1 == n && is_cps ? e.world().lit_ff()
442 : e.world().lit_tt();
443 lam->set_filter(filter);
446 def_ = lam->set(dbg().sym());
448 dom(i - 1)->lam_->set_body(lam);
453 doms().back()->lam_->set_body(body()->
emit(e));
454 if (is_external()) doms().front()->lam_->make_external();
455 e.register_annex(annex_, sub_, def_);
460 if (tag() == Tag::K_cfun) {
461 auto ret_t = codom()->
emit(e);
462 def_ = e.world().mut_fun(dom_t, ret_t)->set(dbg());
464 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_(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_type(Emitter &) const override
virtual Ref emit_(Emitter &) const =0
Ref emit(Emitter &) const
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
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
Ref emit_value(Emitter &, Ref) const
virtual Ref emit_type(Emitter &) const =0
virtual void emit_value_(Emitter &, Ref) const
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_type(Emitter &) const override
Ref emit_decl(Emitter &, Ref type) const
void emit_value_(Emitter &, Ref) const override
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