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());
69 auto _ = e.world().push(
loc());
70 return type() ?
type()->
emit(e) : e.world().mut_infer_type();
78 auto _ = e.world().push(
loc());
84 auto type = e.world().type_infer_univ();
85 sigma = e.world().mut_sigma(type, n)->set(
dbg().
sym());
88 auto& sym2idx = e.sigma2sym2idx[sigma];
90 for (
size_t i = 0; i != n; ++i) {
101 auto _ = e.world().push(
loc());
102 type = type ? type : e.world().type_infer_univ();
103 return e.world().mut_sigma(type,
num_ptrns())->set(
dbg().sym());
111 auto _ = e.world().push(
loc());
125 return e.world().type(l);
131 case Tag::K_Univ:
return e.world().univ();
132 case Tag::K_Nat:
return e.world().type_nat();
133 case Tag::K_Idx:
return e.world().type_idx();
134 case Tag::K_Bool:
return e.world().type_bool();
135 case Tag::K_ff:
return e.world().lit_ff();
136 case Tag::K_tt:
return e.world().lit_tt();
137 case Tag::K_i1:
return e.world().lit_i1();
138 case Tag::K_i8:
return e.world().lit_i8();
139 case Tag::K_i16:
return e.world().lit_i16();
140 case Tag::K_i32:
return e.world().lit_i32();
141 case Tag::K_i64:
return e.world().lit_i64();
142 case Tag::K_I1:
return e.world().type_i1();
143 case Tag::K_I8:
return e.world().type_i8();
144 case Tag::K_I16:
return e.world().type_i16();
145 case Tag::K_I32:
return e.world().type_i32();
146 case Tag::K_I64:
return e.world().type_i64();
147 case Tag::T_star:
return e.world().type<0>();
148 case Tag::T_box:
return e.world().type<1>();
149 default: fe::unreachable();
160 case Tag::L_u:
return t ? e.world().lit(t,
tok().lit_u()) : e.world().lit_nat(
tok().lit_u());
161 case Tag::L_i:
return tok().
lit_i();
162 case Tag::L_c:
return e.world().lit_i8(
tok().lit_c());
163 case Tag::L_str:
return e.world().tuple(
tok().sym());
164 case Tag::T_bot:
return t ? e.world().bot(t) : e.world().type_bot();
165 case Tag::T_top:
return t ? e.world().top(t) : e.world().type_top();
166 default: fe::unreachable();
173 for (
const auto& decl :
decls() | std::ranges::views::reverse) decl->emit(e);
175 for (
const auto& decl :
decls()) decl->emit(e);
182 auto d = dom()->
emit(e);
183 auto c = codom()->
emit(e);
184 return e.world().pi(d, c);
192 auto sigma = e.world().mut_sigma(2)->set(
loc());
193 auto var = sigma->var()->set(
ret()->
loc().anew_begin());
194 sigma->set(0, dom_t);
197 sigma->set(1, ret_t);
199 if (
auto imm = sigma->immutabilize())
211 const auto& first = doms().front();
212 return first->decl_ = e.world().mut_pi(type, first->is_implicit())->set(
loc());
218 for (
const auto& dom : doms()) dom->
emit_type(e);
220 auto cod = codom() ? codom()->
emit(e) : e.world().type_bot();
221 for (
const auto& dom : doms() | std::ranges::views::reverse) {
226 return doms().front()->pi_;
239 auto c = callee()->emit(e);
240 auto a = arg()->emit(e);
241 return is_explicit() ? e.world().app(c, a) : e.world().iapp(c, a);
245 auto c = callee()->emit(e);
247 auto con = e.world().mut_lam(cn);
248 auto pair = e.world().tuple({arg()->emit(e), con});
249 auto app = e.world().app(c, pair)->set(c->loc() + arg()->loc());
250 ptrn()->emit_value(e, con->var());
251 con->set(
false, body()->
emit(e));
255 error(c->loc(),
"callee of a .ret expression must type as a returning continuation but got '{}' of type '{}'", c,
264 DefVec elems(num_elems(), [&](
size_t i) {
return elem(i)->emit(e); });
265 return e.world().tuple(elems);
269 auto s = shape()->emit_type(e);
270 if (shape()->dbg().is_anon()) {
271 auto b = body()->emit(e);
272 return arr ? e.world().arr(s, b) : e.world().pack(s, b);
275 auto t = e.world().type_infer_univ();
276 auto a = e.world().mut_arr(t);
281 shape()->emit_value(e, var);
282 a->set_body(body()->
emit(e));
283 if (
auto imm = a->immutabilize())
return imm;
286 auto p = e.world().mut_pack(a);
288 shape()->emit_value(e, var);
289 auto b = body()->emit(e);
290 a->set_body(b->type());
292 if (
auto imm = p->immutabilize())
return imm;
301 auto tup = tuple()->emit(e);
302 if (
auto dbg = std::get_if<Dbg>(&index())) {
303 if (
auto sigma = tup->type()->isa_mut<
Sigma>()) {
304 if (
auto i = e.sigma2sym2idx.find(sigma); i != e.sigma2sym2idx.end()) {
306 const auto& sym2idx = i->second;
307 if (
auto i = sym2idx.find(dbg->sym()); i != sym2idx.end())
308 return e.world().extract(tup, sigma->num_ops(), i->second);
312 if (decl())
return e.world().extract(tup, decl()->def());
313 error(dbg->loc(),
"cannot resolve index '{}' for extraction", dbg);
316 auto expr = std::get<Ptr<Expr>>(index()).get();
317 auto i = expr->emit(e);
318 return e.world().extract(tup, i);
322 auto t = tuple()->emit(e);
323 auto i = index()->emit(e);
324 auto v = value()->emit(e);
325 return e.world().insert(t, i, v);
333 thorin_type_ = type()->emit(e);
334 auto&
id = annex_->id;
338 if (curry_.lit_u() >
id.curry)
339 error(curry_.loc(),
"curry counter cannot be greater than {}",
id.curry);
341 id.curry = curry_.lit_u();
345 if (trip_.lit_u() >
id.curry)
346 error(trip_.loc(),
"trip counter cannot be greater than curry counter '{}'", (
int)
id.curry);
348 id.trip = trip_.lit_u();
351 auto pi = thorin_type_->isa<
Pi>();
354 else if (
bool(pi) ^ bool(*annex_->pi))
355 error(dbg().loc(),
"all declarations of annex '{}' have to be function types if any is", dbg().sym());
357 if (num_subs() == 0) {
358 auto norm = e.driver().normalizer(
id.plugin,
id.tag, 0);
359 auto axiom = e.world().axiom(norm,
id.curry,
id.trip, thorin_type_,
id.plugin,
id.tag, 0)->set(dbg());
361 e.world().register_annex(
id.plugin,
id.tag, 0, axiom);
363 sub_t offset = annex_->subs.size();
364 for (
sub_t i = 0, n = num_subs(); i != n; ++i) {
365 auto& aliases = annex_->subs.emplace_back(std::deque<Sym>());
366 sub_t s = i + offset;
367 auto norm = e.driver().normalizer(
id.plugin,
id.tag, s);
368 auto name = e.world().sym(dbg().sym().str() +
"."s + sub(i).front()->dbg().sym().str());
369 auto axiom = e.world().axiom(norm,
id.curry,
id.trip, thorin_type_,
id.plugin,
id.tag, s)->set(name);
370 e.world().register_annex(
id.plugin,
id.tag, s, axiom);
372 for (
const auto& alias : sub(i)) {
374 aliases.emplace_back(alias->dbg().sym());
381 auto v = value()->emit(e);
382 def_ = ptrn()->emit_value(e, v);
383 e.register_annex(annex_, sub_, def_);
387 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_decl(e);
388 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_body(e);
392 auto t = type() ? type()->emit(e) : e.world().type_infer_univ();
393 def_ = body()->emit_decl(e, t);
398 body()->emit_body(e, def_);
400 e.register_annex(annex_, sub_, def_);
404 lam_ = e.world().mut_lam(pi_);
405 auto var = lam_->var();
408 ptrn()->emit_value(e, var->proj(2, 0));
409 ret()->emit_value(e, var->proj(2, 1));
411 ptrn()->emit_value(e, var);
418 auto _ = e.world().push(
loc());
419 bool is_cps = tag_ == Tag::K_cn || tag_ == Tag::K_con || tag_ == Tag::K_fn || tag_ == Tag::K_fun;
422 for (
size_t i = 0, n = num_doms(); i != n; ++i) {
423 for (
const auto& dom : doms() | std::ranges::views::drop(i)) dom->
emit_type(e);
424 auto cod = codom() ? codom()->
emit(e) : is_cps ? e.world().type_bot() : e.world().mut_infer_type();
426 for (
const auto& dom : doms() | std::ranges::views::drop(i) | std::ranges::views::reverse) {
432 auto lam = cur->emit_value(e);
433 auto filter = cur->filter() ? cur->filter()->emit(e)
434 : i + 1 == n && is_cps ? e.world().lit_ff()
435 : e.world().lit_tt();
436 lam->set_filter(filter);
439 def_ = lam->set(dbg().sym());
441 dom(i - 1)->lam_->set_body(lam);
446 doms().back()->lam_->set_body(body()->
emit(e));
447 if (is_external()) doms().front()->lam_->make_external();
448 e.register_annex(annex_, sub_, def_);
453 if (tag() == Tag::K_cfun) {
454 auto ret_t = codom()->
emit(e);
455 def_ = e.world().mut_fun(dom_t, ret_t)->set(dbg());
457 def_ = e.world().mut_con(dom_t)->set(dbg());
static std::pair< u8, u8 > infer_curry_and_trip(const Def *type)
Ref var(nat_t a, nat_t i)
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, 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.
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.
Sigma * set(size_t i, const Def *def)
const Def * immutabilize() override
Tries to make an immutable from a mutable.
The World represents the whole program and manages creation of Thorin 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(Emitter &) const override
const Expr * expr() const
Ref emit_(Emitter &) const override
void emit(Emitter &) const override
const auto & decls() const
Ref emit_(Emitter &) const override
const Expr * expr() const
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
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
const Expr * type() const
Ref emit_type(Emitter &) const override
const Module * module() const
void emit(Emitter &) 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_(Emitter &) const override
void emit_body(Emitter &, Ref decl) const override
Ref emit_decl(Emitter &, Ref type) const override
void emit(Emitter &) const override
Ref emit_(Emitter &) const override
const Expr * type() const
const auto & decls() const
const auto & imports() const
const auto & implicit_imports() const
const IdPtrn * ret() const
const Ptrn * ptrn() const
virtual void emit_type(Emitter &) const
void emit_body(Emitter &, Ref decl) const override
Ref emit_decl(Emitter &, Ref type) const override
Ref emit_(Emitter &) const override
virtual Ref emit_type(Emitter &) const =0
Ref emit_value(Emitter &, Ref) const
virtual void emit_value_(Emitter &, Ref) const
virtual void emit_body(Emitter &) const
void emit(Emitter &) const override
virtual void emit_decl(Emitter &) const
Ref emit_(Emitter &) const override
Ref emit_(Emitter &) const override
Ref emit_decl(Emitter &, Ref type) const override
void emit_body(Emitter &, Ref decl) const override
const Lit * lit_i() const
Ref emit_(Emitter &) const override
Ref emit_decl(Emitter &, Ref type) const
Ref emit_type(Emitter &) const override
const Ptrn * ptrn(size_t i) const
Ref emit_body(Emitter &, Ref decl) const
void emit_value_(Emitter &, Ref) const override
const Expr * level() const
Ref emit_(Emitter &) const override
void error(Loc loc, const char *f, Args &&... args)
struct thorin::ast::AnnexInfo::@1 id