6using namespace std::literals;
23 const auto&
id = annex->
id;
44 auto _ = e.world().push(
loc());
46 for (
const auto&
import :
imports())
import->emit(e);
47 for (
const auto& decl :
decls()) decl->emit(e);
70 auto _ = e.world().push(
loc());
83 auto _ = e.world().push(
loc());
84 return type() ?
type()->
emit(e) : e.world().mut_hole_type();
94 auto _ = e.world().push(
loc());
100 auto type = e.world().type_infer_univ();
101 sigma = e.world().mut_sigma(type, n);
103 auto var = sigma->
var();
104 auto& sym2idx = e.sigma2sym2idx[sigma];
106 for (
size_t i = 0; i != n; ++i) {
109 if (
auto id =
ptrn(i)->isa<IdPtrn>()) sym2idx[
id->dbg().sym()] = i;
117 auto _ = e.world().push(
loc());
118 type = type ? type : e.world().type_infer_univ();
119 return e.world().mut_sigma(type,
num_ptrns());
127 auto _ = e.world().push(
loc());
141 return e.world().type(l);
147 case Tag::K_Univ:
return e.world().univ();
148 case Tag::K_Nat:
return e.world().type_nat();
149 case Tag::K_Idx:
return e.world().type_idx();
150 case Tag::K_Bool:
return e.world().type_bool();
151 case Tag::K_ff:
return e.world().lit_ff();
152 case Tag::K_tt:
return e.world().lit_tt();
153 case Tag::K_i1:
return e.world().lit_i1();
154 case Tag::K_i8:
return e.world().lit_i8();
155 case Tag::K_i16:
return e.world().lit_i16();
156 case Tag::K_i32:
return e.world().lit_i32();
157 case Tag::K_i64:
return e.world().lit_i64();
158 case Tag::K_I1:
return e.world().type_i1();
159 case Tag::K_I8:
return e.world().type_i8();
160 case Tag::K_I16:
return e.world().type_i16();
161 case Tag::K_I32:
return e.world().type_i32();
162 case Tag::K_I64:
return e.world().type_i64();
163 case Tag::T_star:
return e.world().type<0>();
164 case Tag::T_box:
return e.world().type<1>();
165 default: fe::unreachable();
176 case Tag::L_u:
return t ? e.world().lit(t,
tok().lit_u()) : e.world().lit_nat(
tok().lit_u());
177 case Tag::L_i:
return tok().
lit_i();
178 case Tag::L_c:
return e.world().lit_i8(
tok().lit_c());
179 case Tag::L_str:
return e.world().tuple(
tok().sym());
180 case Tag::T_bot:
return t ? e.world().bot(t) : e.world().type_bot();
181 case Tag::T_top:
return t ? e.world().top(t) : e.world().type_top();
182 default: fe::unreachable();
189 for (
const auto& decl :
decls() | std::ranges::views::reverse) decl->emit(e);
191 for (
const auto& decl :
decls()) decl->emit(e);
196 return decl_ = e.world().mut_pi(type,
false)->set(
loc());
200 decl_->set_dom(dom()->
emit(e));
201 decl_->set_codom(codom()->
emit(e));
205 auto d = dom()->emit(e);
206 auto c = codom()->emit(e);
207 return e.world().pi(d, c);
212 for (
auto& t :
types()) etypes.emplace_back(t->emit(e));
213 return e.world().join(etypes);
219 return e.world().inj(t, v);
223 auto _ = e.world().push(
loc());
225 auto pi = e.world().pi(dom_t, e.world().mut_hole_type());
226 auto lam = e.world().mut_lam(pi);
234 for (
const auto&
arm :
arms()) res.emplace_back(
arm->emit(e));
235 return e.world().match(res);
240 auto dom_t =
ptrn()->emit_type(e);
243 auto sigma = e.world().mut_sigma(2)->set(
loc());
244 auto var = sigma->var()->set(
ret()->
loc().anew_begin());
245 sigma->set(0, dom_t);
246 ptrn()->emit_value(e, var->proj(2, 0));
248 sigma->set(1, ret_t);
250 if (
auto imm = sigma->immutabilize())
257 ptrn()->emit_value(e,
pi_->var());
262 return dom()->decl_ = e.world().mut_pi(type, dom()->is_implicit())->set(
loc());
269 auto cod = codom() ? codom()->emit(e) : e.world().type_bot();
270 return dom()->set_codom(cod);
283 auto c =
callee()->emit(e);
284 auto a =
arg()->emit(e);
285 return is_explicit() ? e.world().app(c, a) : e.world().implicit_app(c, a);
289 auto c =
callee()->emit(e);
291 auto con = e.world().mut_lam(cn);
292 auto pair = e.world().tuple({
arg()->emit(e), con});
293 auto app = e.world().app(c, pair)->set(c->loc() +
arg()->
loc());
294 ptrn()->emit_value(e, con->var());
299 error(c->loc(),
"callee of a ret expression must type as a returning continuation but got '{}' of type '{}'", c,
309 return e.world().tuple(
elems);
313 auto s =
shape()->emit_type(e);
314 if (
shape()->dbg().is_anon()) {
315 auto b =
body()->emit(e);
316 return is_arr() ? e.world().arr(s, b) : e.world().pack(s, b);
319 auto t = e.world().type_infer_univ();
320 auto a = e.world().mut_arr(t);
325 shape()->emit_value(e, var);
327 if (
auto imm = a->immutabilize())
return imm;
330 auto p = e.world().mut_pack(a);
332 shape()->emit_value(e, var);
333 auto b =
body()->emit(e);
334 a->set_body(b->type());
336 if (
auto imm = p->immutabilize())
return imm;
342 auto tup =
tuple()->emit(e);
343 if (
auto dbg = std::get_if<Dbg>(&
index())) {
344 if (
auto sigma = tup->type()->isa_mut<
Sigma>()) {
345 if (
auto i = e.sigma2sym2idx.find(sigma); i != e.sigma2sym2idx.end()) {
346 auto sigma = i->first->as_mut<
Sigma>();
347 const auto& sym2idx = i->second;
348 if (
auto i = sym2idx.find(dbg->sym()); i != sym2idx.end())
349 return e.world().extract(tup, sigma->num_ops(), i->second);
353 if (
decl())
return e.world().extract(tup,
decl()->def());
354 error(dbg->loc(),
"cannot resolve index '{}' for extraction", *dbg);
357 auto expr = std::get<Ptr<Expr>>(
index()).
get();
358 auto i = expr->emit(e);
359 return e.world().extract(tup, i);
363 auto t =
tuple()->emit(e);
364 auto i =
index()->emit(e);
365 auto v =
value()->emit(e);
366 return e.world().insert(t, i, v);
376 mim_type_ =
type()->emit(e);
377 auto&
id = annex_->id;
381 if (curry_.lit_u() >
id.curry)
382 error(curry_.loc(),
"curry counter cannot be greater than {}",
id.curry);
384 id.curry = curry_.lit_u();
388 if (trip_.lit_u() >
id.curry)
389 error(trip_.loc(),
"trip counter cannot be greater than curry counter '{}'", (
int)
id.curry);
391 id.trip = trip_.lit_u();
394 auto pi = mim_type_->isa<
Pi>();
397 else if (
bool(pi) ^
bool(*annex_->pi))
398 error(
dbg().
loc(),
"all declarations of annex '{}' have to be function types if any is",
dbg().sym());
401 auto norm = e.driver().normalizer(
id.plugin,
id.tag, 0);
402 auto axm = e.world().axm(norm,
id.
curry,
id.
trip, mim_type_,
id.plugin,
id.tag, 0)->set(
dbg());
404 e.world().register_annex(
id.plugin,
id.tag, 0, axm);
406 sub_t offset = annex_->subs.size();
408 auto& aliases = annex_->subs.emplace_back(std::deque<Sym>());
409 sub_t s = i + offset;
410 auto norm = e.driver().normalizer(
id.plugin,
id.tag, s);
411 auto name = e.world().sym(
dbg().sym().str() +
"."s +
sub(i).front()->
dbg().sym().str());
412 auto axm = e.world().axm(norm,
id.
curry,
id.
trip, mim_type_,
id.plugin,
id.tag, s)->set(name);
413 e.world().register_annex(
id.plugin,
id.tag, s, axm);
415 for (
const auto& alias :
sub(i)) {
417 aliases.emplace_back(alias->dbg().sym());
424 auto v =
value()->emit(e);
426 e.register_annex(annex_, sub_,
def_);
430 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_decl(e);
431 for (
auto curr =
this; curr; curr = curr->next()) curr->emit_body(e);
435 auto t =
type() ?
type()->emit(e) : e.world().type_infer_univ();
443 e.register_annex(annex_, sub_,
def_);
448 auto var = lam_->var();
451 ptrn()->emit_value(e, var->proj(2, 0));
452 ret()->emit_value(e, var->proj(2, 1));
454 ptrn()->emit_value(e, var);
461 auto _ = e.world().push(
loc());
462 bool is_cps = tag_ == Tag::K_cn || tag_ == Tag::K_con || tag_ == Tag::K_fn || tag_ == Tag::K_fun;
465 for (
size_t i = 0, n =
num_doms(); i != n; ++i) {
466 for (
const auto&
dom :
doms() | std::ranges::views::drop(i))
dom->emit_type(e);
467 auto cod =
codom() ?
codom()->emit(e) : is_cps ? e.world().type_bot() : e.world().mut_hole_type();
469 for (
const auto&
dom :
doms() | std::ranges::views::drop(i) | std::ranges::views::reverse)
470 cod =
dom->set_codom(cod);
473 auto lam = cur->emit_value(e);
474 auto filter = cur->filter() ? cur->filter()->emit(e)
475 : i + 1 == n && is_cps ? e.world().lit_ff()
476 : e.world().lit_tt();
477 lam->set_filter(filter);
482 dom(i - 1)->lam_->set_body(lam);
489 e.register_annex(annex_, sub_,
def_);
493 auto dom_t =
dom()->emit_type(e);
494 if (
tag() == Tag::K_cfun) {
495 auto ret_t =
codom()->emit(e);
496 def_ = e.world().mut_fun(dom_t, ret_t)->set(
dbg());
498 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 *)
Successively set from left to right.
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
const Def * var(nat_t a, nat_t i) noexcept
Some "global" variables needed all over the place.
A dependent function type.
static const Pi * has_ret_pi(const Def *d)
Yields the Pi::ret_pi() of d, if it is in fact a Pi.
const Def * immutabilize() final
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 *)
const Def * emit_value(Emitter &, const Def *) const override
const Def * emit_type(Emitter &) const override
const Ptrn * ptrn() const
const Def * emit_(Emitter &) const override
const Expr * callee() const
void emit_body(Emitter &, const Def *decl) const override
const Def * emit_decl(Emitter &, const Def *type) const override
const Def * emit_(Emitter &) const override
void emit(Emitter &) const override
const Expr * type() const
const auto & sub(size_t i) const
void emit(Emitter &) const override
const Expr * codom() const
const Expr * expr() const
const Def * emit_(Emitter &) const override
const auto & decls() const
void register_annex(AnnexInfo *annex, sub_t sub, const Def *def)
absl::node_hash_map< Sigma *, fe::SymMap< size_t >, GIDHash< const Def * > > sigma2sym2idx
const Def * emit_(Emitter &) const override
const Def * emit_type(Emitter &) const override
const Def * emit_value(Emitter &, const Def *) const override
const Def * emit(Emitter &) const
virtual void emit_body(Emitter &, const Def *) const
virtual const Def * emit_(Emitter &) const =0
virtual const Def * emit_decl(Emitter &, const Def *) const
const Def * emit_type(Emitter &) const override
const Def * emit_value(Emitter &, const Def *) const override
const IdPtrn * id() const
const Def * emit_(Emitter &) const override
const Def * emit_(Emitter &) const override
const Decl * decl() const
const Def * emit_type(Emitter &) const override
const Def * emit_value(Emitter &, const Def *) const override
const Expr * type() const
void emit(Emitter &) const
const Module * module() const
const Def * emit_(Emitter &) const override
const Expr * type() const
const Expr * value() const
const Expr * index() const
const Expr * tuple() const
const Def * emit_(Emitter &) const override
const Expr * value() const
Lam * emit_value(Emitter &) const
const Ptrs< Dom > & doms() const
const Expr * codom() const
void emit_decl(Emitter &) const override
void emit_body(Emitter &) const override
const Dom * dom(size_t i) const
void emit_body(Emitter &, const Def *decl) const override
const Def * emit_(Emitter &) const override
const LamDecl * lam() const
const Def * emit_decl(Emitter &, const Def *type) const override
const Expr * value() const
const Ptrn * ptrn() const
void emit(Emitter &) const override
const Expr * type() const
const Def * emit_(Emitter &) const override
Lam * emit(Emitter &) const
const Expr * body() const
const Ptrn * ptrn() const
const Def * emit_(Emitter &) const override
const Expr * scrutinee() const
const Arm * arm(size_t i) const
const auto & arms() const
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
const Def * emit_(Emitter &) const override
const Def * emit_decl(Emitter &, const Def *type) const override
void emit_body(Emitter &, const Def *decl) const override
virtual const Def * emit_value(Emitter &, const Def *) const =0
virtual const Def * emit_type(Emitter &) const =0
void emit(Emitter &) const override
virtual void emit_body(Emitter &) const
virtual void emit_decl(Emitter &) const
const Expr * body() const
const Expr * type() const
const Ptrn * ptrn() const
const Def * emit_(Emitter &) const override
const Expr * body() const
const Expr * callee() const
const Expr * body() const
const IdPtrn * shape() const
const Def * emit_(Emitter &) const override
const TuplePtrn * ptrn() const
const Def * emit_(Emitter &) const override
void emit_body(Emitter &, const Def *decl) const override
const Def * emit_decl(Emitter &, const Def *type) const override
const Lit * lit_i() const
const Expr * elem(size_t i) const
const Def * emit_(Emitter &) const override
const auto & elems() const
const Ptrn * ptrn(size_t i) const
const Def * emit_type(Emitter &) const override
const Def * emit_decl(Emitter &, const Def *type) const
const Def * emit_value(Emitter &, const Def *) const override
const Def * emit_body(Emitter &, const Def *decl) const
const Def * emit_(Emitter &) const override
const Expr * level() const
const auto & types() const
const Def * emit_(Emitter &) const override
const Expr * inhabitant() const
const Def * emit_(Emitter &) const override
Vector< const Def * > DefVec
void error(Loc loc, const char *f, Args &&... args)
constexpr decltype(auto) get(Span< T, N > span) noexcept
struct mim::ast::AnnexInfo::@177100250272201136376142224053244231100060214216 id