MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
emit.cpp
Go to the documentation of this file.
1#include "mim/ast/ast.h"
2
3using namespace std::literals;
4
5namespace mim::ast {
6
7using Tag = Tok::Tag;
8
9class Emitter {
10public:
12 : ast_(ast) {}
13
14 AST& ast() const { return ast_; }
15 World& world() { return ast().world(); }
16 Driver& driver() { return world().driver(); }
17
18 void register_annex(AnnexInfo* annex, sub_t sub, Ref def) {
19 if (annex) {
20 const auto& id = annex->id;
21 world().register_annex(id.plugin | (id.tag << 8) | sub, def);
22 }
23 }
24
25 absl::node_hash_map<Sigma*, fe::SymMap<size_t>, GIDHash<const Def*>, GIDEq<const Def*>> sigma2sym2idx;
26
27private:
28 AST& ast_;
29};
30
31/*
32 * Module
33 */
34
35void Module::emit(AST& ast) const {
36 auto emitter = Emitter(ast);
37 emit(emitter);
38}
39
40void Module::emit(Emitter& e) const {
41 auto _ = e.world().push(loc());
42 for (const auto& import : implicit_imports()) import->emit(e);
43 for (const auto& import : imports()) import->emit(e);
44 for (const auto& decl : decls()) decl->emit(e);
45}
46
47void Import::emit(Emitter& e) const { module()->emit(e); }
48
49/*
50 * Ptrn::emit_value
51 */
52
54 auto _ = e.world().push(loc());
55 emit_type(e);
56 emit_value_(e, def);
57 return def_ = def->set(dbg());
58}
59
60void TuplePtrn::emit_value_(Emitter& e, Ref def) const {
61 for (size_t i = 0, n = num_ptrns(); i != n; ++i) ptrn(i)->emit_value(e, def->proj(n, i));
62}
63
64/*
65 * Ptrn::emit_Type
66 */
67
68Ref ErrorPtrn::emit_type(Emitter&) const { fe::unreachable(); }
69
71 auto _ = e.world().push(loc());
72 return type() ? type()->emit(e) : e.world().mut_infer_type();
73}
74
75Ref GrpPtrn::emit_type(Emitter& e) const { return id()->emit_type(e); }
76
77Ref TuplePtrn::emit_type(Emitter& e) const { return emit_body(e, {}); }
78
80 auto _ = e.world().push(loc());
81 auto n = num_ptrns();
82 Sigma* sigma;
83 if (decl) {
84 sigma = decl->as_mut<Sigma>();
85 } else {
86 auto type = e.world().type_infer_univ();
87 sigma = e.world().mut_sigma(type, n)->set(dbg().sym());
88 }
89 auto var = sigma->var()->set(dbg());
90 auto& sym2idx = e.sigma2sym2idx[sigma];
91
92 for (size_t i = 0; i != n; ++i) {
93 sigma->set(i, ptrn(i)->emit_type(e));
94 ptrn(i)->emit_value(e, var->proj(n, i));
95 sym2idx[ptrn(i)->dbg().sym()] = i;
96 }
97
98 if (auto imm = sigma->immutabilize()) return imm;
99 return sigma;
100}
101
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());
106}
107
108/*
109 * Expr
110 */
111
113 auto _ = e.world().push(loc());
114 return emit_(e);
115}
116
117Ref ErrorExpr::emit_(Emitter&) const { fe::unreachable(); }
118Ref InferExpr::emit_(Emitter& e) const { return e.world().mut_infer_type(); }
119
121 assert(decl());
122 return decl()->def();
123}
124
126 auto l = level()->emit(e);
127 return e.world().type(l);
128}
129
130Ref PrimaryExpr ::emit_(Emitter& e) const {
131 // clang-format off
132 switch (tag()) {
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();
152 }
153 // clang-format on
154}
155
157 auto t = type() ? type()->emit(e) : nullptr;
158 // clang-format off
159 switch (tag()) {
160 case Tag::L_f:
161 case Tag::L_s:
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();
169 }
170 // clang-format on
171}
172
174 if (is_where())
175 for (const auto& decl : decls() | std::ranges::views::reverse) decl->emit(e);
176 else
177 for (const auto& decl : decls()) decl->emit(e);
178 return expr()->emit(e);
179}
180
181Ref ArrowExpr::emit_decl(Emitter& e, Ref type) const { return decl_ = e.world().mut_pi(type, false)->set(loc()); }
182
184 decl_->set_dom(dom()->emit(e));
185 decl_->set_codom(codom()->emit(e));
186}
187
189 auto d = dom()->emit(e);
190 auto c = codom()->emit(e);
191 return e.world().pi(d, c);
192}
193
195 pi_ = decl_ ? decl_ : e.world().mut_pi(e.world().type_infer_univ(), is_implicit());
196 auto dom_t = ptrn()->emit_type(e);
197
198 if (ret()) {
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);
202 ptrn()->emit_value(e, var->proj(2, 0));
203 auto ret_t = e.world().cn(ret()->emit_type(e));
204 sigma->set(1, ret_t);
205
206 if (auto imm = sigma->immutabilize())
207 dom_t = imm;
208 else
209 dom_t = sigma;
210 pi_->set_dom(dom_t);
211 } else {
212 pi_->set_dom(dom_t);
213 ptrn()->emit_value(e, pi_->var());
214 }
215}
216
218 const auto& first = doms().front();
219 return first->decl_ = e.world().mut_pi(type, first->is_implicit())->set(loc());
220}
221
222void PiExpr::emit_body(Emitter& e, Ref) const { emit(e); }
223
225 for (const auto& dom : doms()) dom->emit_type(e);
226
227 auto cod = codom() ? codom()->emit(e) : e.world().type_bot();
228 for (const auto& dom : doms() | std::ranges::views::reverse) {
229 dom->pi_->set_codom(cod);
230 cod = dom->pi_;
231 }
232
233 return doms().front()->pi_;
234}
235
236Ref LamExpr::emit_decl(Emitter& e, Ref) const { return lam()->emit_decl(e), lam()->def(); }
237void LamExpr::emit_body(Emitter& e, Ref) const { lam()->emit_body(e); }
238
240 auto res = emit_decl(e, {});
241 emit_body(e, {});
242 return res;
243}
244
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);
249}
250
252 auto c = callee()->emit(e);
253 if (auto cn = Pi::ret_pi(c->type())) {
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));
259 return app;
260 }
261
262 error(c->loc(), "callee of a ret expression must type as a returning continuation but got '{}' of type '{}'", c,
263 c->type());
264}
265
266Ref SigmaExpr::emit_decl(Emitter& e, Ref type) const { return ptrn()->emit_decl(e, type); }
267void SigmaExpr::emit_body(Emitter& e, Ref decl) const { ptrn()->emit_body(e, decl); }
268Ref SigmaExpr::emit_(Emitter& e) const { return ptrn()->emit_type(e); }
269
271 DefVec elems(num_elems(), [&](size_t i) { return elem(i)->emit(e); });
272 return e.world().tuple(elems);
273}
274
275template<bool arr> Ref ArrOrPackExpr<arr>::emit_(Emitter& e) const {
276 auto s = shape()->emit_type(e);
277 if (shape()->dbg().is_anon()) { // immutable
278 auto b = body()->emit(e);
279 return arr ? e.world().arr(s, b) : e.world().pack(s, b);
280 }
281
282 auto t = e.world().type_infer_univ();
283 auto a = e.world().mut_arr(t);
284 a->set_shape(s);
285
286 if (arr) {
287 auto var = a->var();
288 shape()->emit_value(e, var);
289 a->set_body(body()->emit(e));
290 if (auto imm = a->immutabilize()) return imm;
291 return a;
292 } else {
293 auto p = e.world().mut_pack(a);
294 auto var = p->var();
295 shape()->emit_value(e, var);
296 auto b = body()->emit(e);
297 a->set_body(b->type());
298 p->set(b);
299 if (auto imm = p->immutabilize()) return imm;
300 return p;
301 }
302}
303
304template Ref ArrOrPackExpr<true>::emit_(Emitter&) const;
306
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);
316 }
317 }
318
319 if (decl()) return e.world().extract(tup, decl()->def());
320 error(dbg->loc(), "cannot resolve index '{}' for extraction", dbg);
321 }
322
323 auto expr = std::get<Ptr<Expr>>(index()).get();
324 auto i = expr->emit(e);
325 return e.world().extract(tup, i);
326}
327
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);
333}
334
335/*
336 * Decl
337 */
338
339void AxiomDecl::emit(Emitter& e) const {
340 mim_type_ = type()->emit(e);
341 auto& id = annex_->id;
342
343 std::tie(id.curry, id.trip) = Axiom::infer_curry_and_trip(mim_type_);
344 if (curry_) {
345 if (curry_.lit_u() > id.curry)
346 error(curry_.loc(), "curry counter cannot be greater than {}", id.curry);
347 else
348 id.curry = curry_.lit_u();
349 }
350
351 if (trip_) {
352 if (trip_.lit_u() > id.curry)
353 error(trip_.loc(), "trip counter cannot be greater than curry counter '{}'", (int)id.curry);
354 else
355 id.trip = trip_.lit_u();
356 }
357
358 auto pi = mim_type_->isa<Pi>();
359 if (!annex_->pi)
360 annex_->pi = 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());
363
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());
367 def_ = axiom;
368 e.world().register_annex(id.plugin, id.tag, 0, axiom);
369 } else {
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);
378
379 for (const auto& alias : sub(i)) {
380 alias->def_ = axiom;
381 aliases.emplace_back(alias->dbg().sym());
382 }
383 }
384 }
385}
386
387void LetDecl::emit(Emitter& e) const {
388 auto v = value()->emit(e);
389 def_ = ptrn()->emit_value(e, v);
390 e.register_annex(annex_, sub_, def_);
391}
392
393void RecDecl::emit(Emitter& e) const {
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);
396}
397
399 auto t = type() ? type()->emit(e) : e.world().type_infer_univ();
400 def_ = body()->emit_decl(e, t);
401 def_->set(dbg());
402}
403
405 body()->emit_body(e, def_);
406 // TODO immutabilize?
407 e.register_annex(annex_, sub_, def_);
408}
409
411 lam_ = e.world().mut_lam(pi_);
412 auto var = lam_->var();
413
414 if (ret()) {
415 ptrn()->emit_value(e, var->proj(2, 0));
416 ret()->emit_value(e, var->proj(2, 1));
417 } else {
418 ptrn()->emit_value(e, var);
419 }
420
421 return lam_;
422}
423
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;
427
428 // Iterate over all doms: Build a Lam for cur dom, by first building a curried Pi for the remaining doms.
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();
432
433 for (const auto& dom : doms() | std::ranges::views::drop(i) | std::ranges::views::reverse) {
434 dom->pi_->set_codom(cod);
435 cod = dom->pi_;
436 }
437
438 auto cur = dom(i);
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);
444
445 if (i == 0)
446 def_ = lam->set(dbg().sym());
447 else
448 dom(i - 1)->lam_->set_body(lam);
449 }
450}
451
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_);
456}
457
458void CDecl::emit(Emitter& e) const {
459 auto dom_t = dom()->emit_type(e);
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());
463 } else {
464 def_ = e.world().mut_con(dom_t)->set(dbg());
465 }
466}
467
468} // namespace mim::ast
static std::pair< u8, u8 > infer_curry_and_trip(const Def *type)
Definition axiom.cpp:14
Def * set(size_t i, const Def *def)
Successively set from left to right.
Definition def.cpp:246
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.
Definition def.cpp:518
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Definition def.h:455
Ref var(nat_t a, nat_t i)
Definition def.h:401
Some "global" variables needed all over the place.
Definition driver.h:17
A function.
Definition lam.h:103
A dependent function type.
Definition lam.h:11
Pi * set_codom(Ref codom)
Definition lam.h:76
const Pi * ret_pi() const
Yields the last Pi::dom, if it Pi::isa_basicblock.
Definition lam.cpp:13
Pi * set_dom(Ref dom)
Definition lam.h:74
Helper class to retrieve Infer::arg if present.
Definition def.h:86
A dependent tuple type.
Definition tuple.h:9
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:166
Sigma * set(size_t i, const Def *def)
Definition tuple.h:21
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:33
const Driver & driver() const
Definition world.h:81
const Def * register_annex(flags_t f, const Def *)
Definition world.cpp:80
World & world()
Definition ast.h:61
Ref emit_(Emitter &) const override
Definition emit.cpp:245
Ref emit_(Emitter &) const override
Definition emit.cpp:275
Ref emit_(Emitter &) const override
Definition emit.cpp:188
void emit_body(Emitter &, Ref decl) const override
Definition emit.cpp:183
Ref emit_decl(Emitter &, Ref type) const override
Definition emit.cpp:181
void emit(Emitter &) const override
Definition emit.cpp:339
void emit(Emitter &) const override
Definition emit.cpp:458
const Expr * expr() const
Definition ast.h:379
const auto & decls() const
Definition ast.h:377
Ref emit_(Emitter &) const override
Definition emit.cpp:173
bool is_where() const
Definition ast.h:378
Ref def() const
Definition ast.h:151
AST & ast() const
Definition emit.cpp:14
absl::node_hash_map< Sigma *, fe::SymMap< size_t >, GIDHash< const Def * >, GIDEq< const Def * > > sigma2sym2idx
Definition emit.cpp:25
World & world()
Definition emit.cpp:15
Emitter(AST &ast)
Definition emit.cpp:11
void register_annex(AnnexInfo *annex, sub_t sub, Ref def)
Definition emit.cpp:18
Driver & driver()
Definition emit.cpp:16
Ref emit_(Emitter &) const override
Definition emit.cpp:117
Ref emit_type(Emitter &) const override
Definition emit.cpp:68
virtual Ref emit_(Emitter &) const =0
Ref emit(Emitter &) const
Definition emit.cpp:112
Ref emit_(Emitter &) const override
Definition emit.cpp:307
Ref emit_type(Emitter &) const override
Definition emit.cpp:75
const IdPtrn * id() const
Definition ast.h:238
const Decl * decl() const
Definition ast.h:314
Ref emit_(Emitter &) const override
Definition emit.cpp:120
Ref emit_type(Emitter &) const override
Definition emit.cpp:70
const Expr * type() const
Definition ast.h:212
void emit(Emitter &) const
Definition emit.cpp:47
const Module * module() const
Definition ast.h:909
Ref emit_(Emitter &) const override
Definition emit.cpp:118
Ref emit_(Emitter &) const override
Definition emit.cpp:328
Lam * emit_value(Emitter &) const
Definition emit.cpp:410
void emit_decl(Emitter &) const override
Definition emit.cpp:424
void emit_body(Emitter &) const override
Definition emit.cpp:452
Ref emit_decl(Emitter &, Ref type) const override
Definition emit.cpp:236
void emit_body(Emitter &, Ref decl) const override
Definition emit.cpp:237
Ref emit_(Emitter &) const override
Definition emit.cpp:239
void emit(Emitter &) const override
Definition emit.cpp:387
Tok tok() const
Definition ast.h:354
const Expr * type() const
Definition ast.h:356
Tok::Tag tag() const
Definition ast.h:355
Ref emit_(Emitter &) const override
Definition emit.cpp:156
const auto & decls() const
Definition ast.h:937
void emit(AST &) const
Definition emit.cpp:35
const auto & implicit_imports() const
Definition ast.h:935
const auto & imports() const
Definition ast.h:936
Loc loc() const
Definition ast.h:121
virtual void emit_type(Emitter &) const
Definition emit.cpp:194
const IdPtrn * ret() const
Definition ast.h:452
bool is_implicit() const
Definition ast.h:450
const Ptrn * ptrn() const
Definition ast.h:451
void emit_body(Emitter &, Ref decl) const override
Definition emit.cpp:222
Ref emit_(Emitter &) const override
Definition emit.cpp:224
Ref emit_decl(Emitter &, Ref type) const override
Definition emit.cpp:217
Ref emit_value(Emitter &, Ref) const
Definition emit.cpp:53
virtual Ref emit_type(Emitter &) const =0
Dbg dbg() const
Definition ast.h:179
virtual void emit_value_(Emitter &, Ref) const
Definition ast.h:189
void emit(Emitter &) const override
Definition emit.cpp:393
virtual void emit_body(Emitter &) const
Definition emit.cpp:404
virtual void emit_decl(Emitter &) const
Definition emit.cpp:398
Ref emit_(Emitter &) const override
Definition emit.cpp:251
void emit_body(Emitter &, Ref decl) const override
Definition emit.cpp:267
Ref emit_(Emitter &) const override
Definition emit.cpp:268
Ref emit_decl(Emitter &, Ref type) const override
Definition emit.cpp:266
const Lit * lit_i() const
Definition tok.h:174
Ref emit_(Emitter &) const override
Definition emit.cpp:270
const Ptrn * ptrn(size_t i) const
Definition ast.h:262
Ref emit_type(Emitter &) const override
Definition emit.cpp:77
Ref emit_decl(Emitter &, Ref type) const
Definition emit.cpp:102
size_t num_ptrns() const
Definition ast.h:263
void emit_value_(Emitter &, Ref) const override
Definition emit.cpp:60
Ref emit_body(Emitter &, Ref decl) const
Definition emit.cpp:79
const Expr * level() const
Definition ast.h:399
Ref emit_(Emitter &) const override
Definition emit.cpp:125
Definition ast.h:14
u8 sub_t
Definition types.h:48
void error(Loc loc, const char *f, Args &&... args)
Definition dbg.h:122
constexpr decltype(auto) get(mim::Span< T, N > span)
Definition span.h:113
Sym sym() const
Definition dbg.h:145
struct mim::ast::AnnexInfo::@1 id