6using namespace std::literals;
23 const auto&
id = annex->
id;
44 auto _ = e.world().push(
loc());
47 for (
const auto&
import :
imports())
49 for (
const auto& decl :
decls())
73 auto _ = e.world().push(
loc());
75 for (
size_t i = 0, n =
num_ptrns(); i != n; ++i)
87 auto _ = e.world().push(
loc());
88 return type() ?
type()->
emit(e) : e.world().mut_hole_type();
98 auto _ = e.world().push(
loc());
104 auto type = e.world().type_infer_univ();
105 sigma = e.world().mut_sigma(type, n);
107 auto var = sigma->
var();
108 auto& sym2idx = e.sigma2sym2idx[sigma];
110 for (
size_t i = 0; i != n; ++i) {
113 if (
auto id =
ptrn(i)->isa<IdPtrn>()) sym2idx[
id->dbg().sym()] = i;
121 auto _ = e.world().push(
loc());
122 type = type ? type : e.world().type_infer_univ();
123 return e.world().mut_sigma(type,
num_ptrns());
131 auto _ = e.world().push(
loc());
145 return e.world().type(l);
151 case Tag::K_Univ:
return e.world().univ();
152 case Tag::K_Nat:
return e.world().type_nat();
153 case Tag::K_Idx:
return e.world().type_idx();
154 case Tag::K_Bool:
return e.world().type_bool();
155 case Tag::K_ff:
return e.world().lit_ff();
156 case Tag::K_tt:
return e.world().lit_tt();
157 case Tag::K_i1:
return e.world().lit_i1();
158 case Tag::K_i8:
return e.world().lit_i8();
159 case Tag::K_i16:
return e.world().lit_i16();
160 case Tag::K_i32:
return e.world().lit_i32();
161 case Tag::K_i64:
return e.world().lit_i64();
162 case Tag::K_I1:
return e.world().type_i1();
163 case Tag::K_I8:
return e.world().type_i8();
164 case Tag::K_I16:
return e.world().type_i16();
165 case Tag::K_I32:
return e.world().type_i32();
166 case Tag::K_I64:
return e.world().type_i64();
167 case Tag::T_star:
return e.world().type<0>();
168 case Tag::T_box:
return e.world().type<1>();
169 default: fe::unreachable();
180 case Tag::L_u:
return t ? e.world().lit(t,
tok().lit_u()) : e.world().lit_nat(
tok().lit_u());
181 case Tag::L_i:
return tok().
lit_i();
182 case Tag::L_c:
return e.world().lit_i8(
tok().lit_c());
183 case Tag::L_str:
return e.world().tuple(
tok().sym());
184 case Tag::T_bot:
return t ? e.world().bot(t) : e.world().type_bot();
185 case Tag::T_top:
return t ? e.world().top(t) : e.world().type_top();
186 default: fe::unreachable();
193 for (
const auto& decl :
decls() | std::ranges::views::reverse)
196 for (
const auto& decl :
decls())
202 return decl_ = e.world().mut_pi(type,
false)->set(
loc());
206 decl_->set_dom(dom()->
emit(e));
207 decl_->set_codom(codom()->
emit(e));
211 auto d = dom()->emit(e);
212 auto c = codom()->emit(e);
213 return e.world().pi(d, c);
218 for (
auto& t :
types())
219 etypes.emplace_back(t->emit(e));
220 return e.world().join(etypes);
226 return e.world().inj(t, v);
230 auto _ = e.world().push(
loc());
232 auto pi = e.world().pi(dom_t, e.world().mut_hole_type());
233 auto lam = e.world().mut_lam(pi);
242 res.emplace_back(
arm->emit(e));
243 return e.world().match(res);
248 auto dom_t =
ptrn()->emit_type(e);
251 auto sigma = e.world().mut_sigma(2)->set(
loc());
252 auto var = sigma->var()->set(
ret()->
loc().anew_begin());
253 sigma->set(0, dom_t);
254 ptrn()->emit_value(e, var->proj(2, 0));
256 sigma->set(1, ret_t);
258 if (
auto imm = sigma->immutabilize())
265 ptrn()->emit_value(e,
pi_->var());
270 return dom()->decl_ = e.world().mut_pi(type, dom()->is_implicit())->set(
loc());
277 auto cod = codom() ? codom()->emit(e) : e.world().type_bot();
278 return dom()->pi_->set_codom(cod);
291 auto c =
callee()->emit(e);
292 auto a =
arg()->emit(e);
293 return is_explicit() ? e.world().app(c, a) : e.world().implicit_app(c, a);
297 auto c =
callee()->emit(e);
299 auto con = e.world().mut_lam(cn);
300 auto pair = e.world().tuple({
arg()->emit(e), con});
301 auto app = e.world().app(c, pair)->set(c->loc() +
arg()->
loc());
302 ptrn()->emit_value(e, con->var());
307 error(c->loc(),
"callee of a ret expression must type as a returning continuation but got '{}' of type '{}'", c,
317 return e.world().tuple(
elems);
321 auto s =
arity()->emit_type(e);
322 if (
arity()->dbg().is_anon()) {
323 auto b =
body()->emit(e);
324 return is_arr() ? e.world().arr(s, b) : e.world().pack(s, b);
327 auto t = e.world().type_infer_univ();
328 auto a = e.world().mut_arr(t);
333 arity()->emit_value(e, var);
335 if (
auto imm = a->immutabilize())
return imm;
338 auto p = e.world().mut_pack(a);
340 arity()->emit_value(e, var);
341 auto b =
body()->emit(e);
342 a->set_body(b->type());
344 if (
auto imm = p->immutabilize())
return imm;
350 auto tup =
tuple()->emit(e);
351 if (
auto dbg = std::get_if<Dbg>(&
index())) {
352 if (
auto sigma = tup->type()->isa_mut<
Sigma>()) {
353 if (
auto i = e.sigma2sym2idx.find(sigma); i != e.sigma2sym2idx.end()) {
354 auto sigma = i->first->as_mut<
Sigma>();
355 const auto& sym2idx = i->second;
356 if (
auto i = sym2idx.find(dbg->sym()); i != sym2idx.end())
357 return e.world().extract(tup, sigma->num_ops(), i->second);
361 if (
decl())
return e.world().extract(tup,
decl()->def());
362 error(dbg->loc(),
"cannot resolve index '{}' for extraction", *dbg);
365 auto expr = std::get<Ptr<Expr>>(
index()).
get();
366 auto i = expr->emit(e);
367 return e.world().extract(tup, i);
371 auto t =
tuple()->emit(e);
372 auto i =
index()->emit(e);
373 auto v =
value()->emit(e);
374 return e.world().insert(t, i, v);
384 mim_type_ =
type()->emit(e);
385 auto&
id = annex_->id;
389 if (curry_.lit_u() >
id.curry)
390 error(curry_.loc(),
"curry counter cannot be greater than {}",
id.curry);
392 id.curry = curry_.lit_u();
396 if (trip_.lit_u() >
id.curry)
397 error(trip_.loc(),
"trip counter cannot be greater than curry counter '{}'", (
int)
id.curry);
399 id.trip = trip_.lit_u();
403 auto norm = e.driver().normalizer(
id.plugin,
id.tag, 0);
404 auto axm = e.world().axm(norm,
id.
curry,
id.
trip, mim_type_,
id.plugin,
id.tag, 0)->set(
dbg());
406 e.world().register_annex(
id.plugin,
id.tag, 0, axm);
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))
422 auto v =
value()->emit(e);
424 e.register_annex(annex_, sub_,
def_);
428 for (
auto curr =
this; curr; curr = curr->next())
430 for (
auto curr =
this; curr; curr = curr->next())
435 auto t =
type() ?
type()->emit(e) : e.world().type_infer_univ();
443 e.register_annex(annex_, sub_,
def_);
447 lam_ = e.world().mut_lam(
pi_);
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))
469 auto cod =
codom() ?
codom()->emit(e) : is_cps ? e.world().type_bot() : e.world().mut_hole_type();
470 for (
const auto&
dom :
doms() | std::ranges::views::drop(i) | std::ranges::views::reverse)
471 cod =
dom->pi_->set_codom(cod);
474 auto lam = cur->emit_value(e);
475 auto filter = cur->filter() ? cur->filter()->emit(e)
476 : i + 1 == n && is_cps ? e.world().lit_ff()
477 : e.world().lit_tt();
478 lam->set_filter(filter);
483 dom(i - 1)->lam_->set_body(lam);
488 auto b =
body()->emit(e);
489 doms().back()->lam_->set_body(b);
492 for (
size_t i = 0, n =
num_doms(); i != n; ++i) {
494 auto lam =
dom(i)->lam_;
495 auto pi = lam->type()->as_mut<
Pi>();
496 for (
const auto&
dom :
doms() | std::ranges::views::drop(i)) {
497 if (
auto var = pi->has_var()) rw.add(
dom->lam_->var()->as<
Var>(), var);
498 auto cod = pi->codom();
499 if (!cod || !cod->isa_mut<
Pi>())
break;
500 pi = cod->as_mut<
Pi>();
503 if (
auto cod = pi->codom(); cod && cod->has_dep(
Dep::Hole)) pi->
set(pi->dom(), rw.rewrite(cod));
506 for (
const auto&
dom :
doms() | std::ranges::views::reverse) {
507 if (
auto imm =
dom->pi_->immutabilize()) {
508 auto f =
dom->lam_->filter();
509 auto b =
dom->lam_->body();
510 dom->lam_->unset()->set_type(imm)->as<
Lam>()->set(f, b);
515 e.register_annex(annex_, sub_,
def_);
519 auto dom_t =
dom()->emit_type(e);
520 if (
tag() == Tag::K_cfun) {
521 auto ret_t =
codom()->emit(e);
522 def_ = e.world().mut_fun(dom_t, ret_t)->set(
dbg());
524 def_ = e.world().mut_con(dom_t)->set(
dbg());
529 auto _ = e.world().push(
loc());
530 auto meta_t = e.world().reform(
var()->emit_type(e));
531 auto rule_ = e.world().mut_rule(meta_t);
532 var()->emit_value(e, rule_->var());
533 auto l =
lhs()->emit(e);
534 auto r =
rhs()->emit(e);
535 auto c =
guard()->emit(e);
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.
Pi * set(const Def *dom, const Def *codom)
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 * guard() const
void emit(Emitter &) const override
const Expr * body() const
const IdPtrn * arity() 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