MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
def.cpp
Go to the documentation of this file.
1#include "mim/def.h"
2
3#include <algorithm>
4
5#include <absl/container/fixed_array.h>
6#include <fe/assert.h>
7
8#include "mim/world.h"
9
10#include "mim/util/hash.h"
11
12using namespace std::literals;
13
14namespace mim {
15
16template void Sets<const Var>::dot();
17template void Sets<Def>::dot();
18
19/*
20 * constructors
21 */
22
23Def::Def(World* world, Node node, const Def* type, Defs ops, flags_t flags)
24 : world_(world)
25 , flags_(flags)
26 , node_(node)
27 , mut_(false)
28 , external_(false)
29 , dep_(node == Node::Hole ? unsigned(Dep::Hole)
30 : node == Node::Proxy ? unsigned(Dep::Proxy)
31 : node == Node::Var ? (Dep::Var | Dep::Mut)
32 : 0)
33 , num_ops_(ops.size())
34 , type_(type) {
35 if (node == Node::Univ) {
36 gid_ = world->next_gid();
38 } else if (auto var = isa<Var>()) {
39 assert(flags_ == 0); // if we ever need flags here, we need to hash that
40 gid_ = type->world().next_gid();
41 vars_ = Vars(var);
42 dep_ |= type->dep_;
43 auto op = ops[0];
44 ops_ptr()[0] = op;
45 hash_ = hash_begin(node_t(Node::Var));
46 hash_ = hash_combine(hash_, type->gid());
47 hash_ = hash_combine(hash_, op->gid());
48 } else {
50 Sets<Def>* muts;
51 hash_ = hash_begin(u8(node));
52 hash_ = hash_combine(hash_, flags_);
53
54 if (type) {
55 world = &type->world();
56 vars = &world->vars();
57 muts = &world->muts();
58 dep_ |= type->dep_;
59 vars_ = vars->merge(vars_, type->local_vars());
60 muts_ = muts->merge(muts_, type->local_muts());
61 hash_ = hash_combine(hash_, type->gid());
62 } else {
63 world = &ops[0]->world();
64 vars = &world->vars();
65 muts = &world->muts();
66 }
67
68 gid_ = world->next_gid();
69 auto ptr = ops_ptr();
70 for (size_t i = 0, e = ops.size(); i != e; ++i) {
71 auto op = ops[i];
72 ptr[i] = op;
73 dep_ |= op->dep_;
74 vars_ = vars->merge(vars_, op->local_vars());
75 muts_ = muts->merge(muts_, op->local_muts());
76 hash_ = hash_combine(hash_, op->gid());
77 }
78 }
79}
80
81Def::Def(Node n, const Def* type, Defs ops, flags_t flags)
82 : Def(nullptr, n, type, ops, flags) {}
83
84Def::Def(Node node, const Def* type, size_t num_ops, flags_t flags)
85 : flags_(flags)
86 , node_(node)
87 , mut_(true)
88 , external_(false)
89 , dep_(Dep::Mut | (node == Node::Hole ? Dep::Hole : Dep::None))
90 , num_ops_(num_ops)
91 , type_(type) {
92 gid_ = world().next_gid();
93 hash_ = mim::hash(gid());
94 var_ = nullptr;
95 std::fill_n(ops_ptr(), num_ops, nullptr);
96}
97
98Nat::Nat(World& world)
99 : Def(Node, world.type(), Defs{}, 0) {}
100
101UMax::UMax(World& world, Defs ops)
102 : Def(Node, world.univ(), ops, 0) {}
103
104// clang-format off
105
106/*
107 * rebuild
108 */
109
110const Def* Hole ::rebuild_(World&, const Def*, Defs ) const { fe::unreachable(); }
111const Def* Global ::rebuild_(World&, const Def*, Defs ) const { fe::unreachable(); }
112const Def* Idx ::rebuild_(World& w, const Def* , Defs ) const { return w.type_idx(); }
113const Def* Nat ::rebuild_(World& w, const Def* , Defs ) const { return w.type_nat(); }
114const Def* Univ ::rebuild_(World& w, const Def* , Defs ) const { return w.univ(); }
115const Def* App ::rebuild_(World& w, const Def* , Defs o) const { return w.app(o[0], o[1]); }
116const Def* Arr ::rebuild_(World& w, const Def* , Defs o) const { return w.arr(o[0], o[1]); }
117const Def* Extract::rebuild_(World& w, const Def* , Defs o) const { return w.extract(o[0], o[1]); }
118const Def* Inj ::rebuild_(World& w, const Def* t, Defs o) const { return w.inj(t, o[0])->set(dbg()); }
119const Def* Insert ::rebuild_(World& w, const Def* , Defs o) const { return w.insert(o[0], o[1], o[2]); }
120const Def* Lam ::rebuild_(World& w, const Def* t, Defs o) const { return w.lam(t->as<Pi>(), o[0], o[1]); }
121const Def* Lit ::rebuild_(World& w, const Def* t, Defs ) const { return w.lit(t, get()); }
122const Def* Merge ::rebuild_(World& w, const Def* t, Defs o) const { return w.merge(t, o); }
123const Def* Pack ::rebuild_(World& w, const Def* t, Defs o) const { return w.pack(t->arity(), o[0]); }
124const Def* Pi ::rebuild_(World& w, const Def* , Defs o) const { return w.pi(o[0], o[1], is_implicit()); }
125const Def* Proxy ::rebuild_(World& w, const Def* t, Defs o) const { return w.proxy(t, o, pass(), tag()); }
126const Def* Sigma ::rebuild_(World& w, const Def* , Defs o) const { return w.sigma(o); }
127const Def* Split ::rebuild_(World& w, const Def* t, Defs o) const { return w.split(t, o[0]); }
128const Def* Match ::rebuild_(World& w, const Def* , Defs o) const { return w.match(o); }
129const Def* Tuple ::rebuild_(World& w, const Def* t, Defs o) const { return w.tuple(t, o); }
130const Def* Type ::rebuild_(World& w, const Def* , Defs o) const { return w.type(o[0]); }
131const Def* UInc ::rebuild_(World& w, const Def* , Defs o) const { return w.uinc(o[0], offset()); }
132const Def* UMax ::rebuild_(World& w, const Def* , Defs o) const { return w.umax(o); }
133const Def* Uniq ::rebuild_(World& w, const Def* , Defs o) const { return w.uniq(o[0]); }
134const Def* Var ::rebuild_(World& w, const Def* t, Defs o) const { return w.var(t, o[0]->as_mut()); }
135
136const Def* Axm ::rebuild_(World& w, const Def* t, Defs ) const {
137 if (&w != &world()) return w.axm(normalizer(), curry(), trip(), t, plugin(), tag(), sub())->set(dbg());
139 return this;
140}
141
142template<bool up> const Def* TExt <up>::rebuild_(World& w, const Def* t, Defs ) const { return w.ext <up>(t)->set(dbg()); }
143template<bool up> const Def* TBound<up>::rebuild_(World& w, const Def* , Defs o) const { return w.bound<up>(o)->set(dbg()); }
144
145/*
146 * stub
147 */
148
149Arr* Arr ::stub_(World& w, const Def* t) { return w.mut_arr (t); }
150Global* Global::stub_(World& w, const Def* t) { return w.global (t, is_mutable()); }
151Hole* Hole ::stub_(World& w, const Def* t) { return w.mut_hole(t); }
152Lam* Lam ::stub_(World& w, const Def* t) { return w.mut_lam (t->as<Pi>()); }
153Pack* Pack ::stub_(World& w, const Def* t) { return w.mut_pack (t); }
154Pi* Pi ::stub_(World& w, const Def* t) { return w.mut_pi (t, is_implicit()); }
155Sigma* Sigma ::stub_(World& w, const Def* t) { return w.mut_sigma(t, num_ops()); }
156
157/*
158 * instantiate templates
159 */
160
161#ifndef DOXYGEN
162template const Def* TExt<false> ::rebuild_(World&, const Def*, Defs) const;
163template const Def* TExt<true > ::rebuild_(World&, const Def*, Defs) const;
164template const Def* TBound<false>::rebuild_(World&, const Def*, Defs) const;
165template const Def* TBound<true >::rebuild_(World&, const Def*, Defs) const;
166#endif
167
168// clang-format on
169
170/*
171 * immutabilize
172 */
173
175 if (auto v = has_var()) {
176 for (auto op : deps())
177 if (op->free_vars().contains(v)) return false;
178 }
179 for (auto op : deps()) {
180 for (auto mut : op->local_muts())
181 if (mut == this) return false; // recursion
182 }
183 return true;
184}
185
187 if (is_immutabilizable()) return world().pi(dom(), codom());
188 return nullptr;
189}
190
192 if (is_immutabilizable()) return static_cast<const Sigma*>(world().sigma(ops()));
193 return nullptr;
194}
195
196const Def* Arr::immutabilize() {
197 auto& w = world();
198 if (is_immutabilizable()) return w.arr(shape(), body());
199
200 if (auto n = Lit::isa(shape()); n && *n < w.flags().scalarize_threshold)
201 return w.sigma(DefVec(*n, [&](size_t i) { return reduce(w.lit_idx(*n, i)); }));
202
203 return nullptr;
204}
205
206const Def* Pack::immutabilize() {
207 auto& w = world();
208 if (is_immutabilizable()) return w.pack(shape(), body());
209
210 if (auto n = Lit::isa(shape()); n && *n < w.flags().scalarize_threshold)
211 return w.tuple(DefVec(*n, [&](size_t i) { return reduce(w.lit_idx(*n, i)); }));
212
213 return nullptr;
214}
215
216/*
217 * reduce
218 */
219
220Defs Def::reduce_(const Def* arg) const {
221 if (auto var = has_var()) return world().reduce(var, arg);
222 return {ops().begin() + reduction_offset(), num_ops() - reduction_offset()};
223}
224
225const Def* Def::refine(size_t i, const Def* new_op) const {
226 auto new_ops = absl::FixedArray<const Def*>(num_ops());
227 for (size_t j = 0, e = num_ops(); j != e; ++j) new_ops[j] = i == j ? new_op : op(j);
228 return rebuild(type(), new_ops);
229}
230
231/*
232 * Def - set
233 */
234
236 assert(ops.size() == num_ops());
237 for (size_t i = 0, e = num_ops(); i != e; ++i) set(i, ops[i]);
238 return this;
239}
240
241Def* Def::set(size_t i, const Def* def) {
242 def = check(i, def);
243 assert(def && !op(i) && curr_op_++ == i);
244 ops_ptr()[i] = def;
245
246 if (i + 1 == num_ops()) { // set last op, so check kind
247 if (auto t = check()->zonk(); t != type()) type_ = t;
248 }
249
250 return this;
251}
252
254 invalidate();
255#ifndef NDEBUG
256 curr_op_ = 0;
257#endif
258 std::ranges::fill(ops_ptr(), ops_ptr() + num_ops(), nullptr);
259 return this;
260}
261
262bool Def::is_set() const {
263 if (num_ops() == 0) return true;
264 bool result = ops().back();
265 assert((!result || std::ranges::all_of(ops().rsubspan(1), [](auto op) { return op; }))
266 && "the last operand is set but others in front of it aren't");
267 return result;
268}
269
270/*
271 * free_vars
272 */
273
275 if (auto mut = isa_mut()) return Muts(mut);
276 return muts_;
277}
278
280 if (auto mut = isa_mut()) return mut->free_vars();
281
282 auto& vars = world().vars();
283 auto fvs = local_vars();
284 for (auto mut : local_muts()) fvs = vars.merge(fvs, mut->free_vars());
285
286 return fvs;
287}
288
289Vars Def::local_vars() const { return mut_ ? Vars() : vars_; }
290
292 if (!is_set()) return {};
293
294 if (mark_ == 0) {
295 // fixed-point iteration to recompute free vars:
296 // (run - 1) identifies the previous iteration; so make sure to offset run by 2 for the first iteration
297 auto& w = world();
298 w.next_run();
299 for (bool todo = true, cyclic = false; todo;) {
300 todo = false;
301 free_vars(todo, cyclic, w.next_run());
302 if (!cyclic) break; // triggers either immediately or never
303 }
304 }
305
306 return vars_;
307}
308
309Vars Def::free_vars(bool& todo, bool& cyclic, uint32_t run) {
310 // Recursively recompute free vars. If
311 // * mark_ == 0: invalid - need to recompute
312 // * mark_ == run - 1: Previous iteration - need to recompute
313 // * mark_ == run: We are running in cycles within the *current* iteration of our fixed-point loop
314 // * all other values for mark_: valid!
315 if (mark_ != 0 && mark_ != run - 1) return cyclic |= mark_ == run, vars_;
316 mark_ = run;
317
318 auto fvs0 = vars_;
319 auto fvs = fvs0;
320 auto& w = world();
321 auto& muts = w.muts();
322 auto& vars = w.vars();
323
324 for (auto op : deps()) {
325 fvs = vars.merge(fvs, op->local_vars());
326
327 for (auto mut : op->local_muts()) {
328 mut->muts_ = muts.insert(mut->muts_, this); // register "this" as user of local_mut
329 fvs = vars.merge(fvs, mut->free_vars(todo, cyclic, run));
330 }
331 }
332
333 if (auto var = has_var()) fvs = vars.erase(fvs, var); // FV(λx.e) = FV(e) \ {x}
334
335 todo |= fvs0 != fvs;
336 return vars_ = fvs;
337}
338
339void Def::invalidate() {
340 if (mark_ != 0) {
341 mark_ = 0;
342 if (vars_) { // only necessary, if the cached free vars are non-empty
343 for (auto mut : users()) mut->invalidate();
344 vars_ = Vars();
345 }
346 muts_ = Muts();
347 }
348}
349
350bool Def::is_closed() const {
351 if (local_vars().empty() && local_muts().empty()) return true;
352#ifdef MIM_ENABLE_CHECKS
353 assert(!is_external() || free_vars().empty());
354#endif
355 return free_vars().empty();
356}
357
358bool Def::is_open() const {
359 if (!local_vars().empty()) return true;
360 return !free_vars().empty();
361}
362
363/*
364 * Def - misc
365 */
366
367Sym Def::sym(const char* s) const { return world().sym(s); }
368Sym Def::sym(std::string_view s) const { return world().sym(s); }
369Sym Def::sym(std::string s) const { return world().sym(std::move(s)); }
370
371World& Def::world() const noexcept {
372 for (auto def = this;; def = def->type()) {
373 if (def->isa<Univ>()) return *def->world_;
374 if (auto type = def->isa<Type>()) return *type->level()->type()->as<Univ>()->world_;
375 }
376}
377
378const Def* Def::unfold_type() const {
379 if (!type_) {
380 auto& w = world();
381 if (auto t = isa<Type>()) return w.type(w.uinc(t->level()));
382 assert(isa<Univ>());
383 return nullptr;
384 }
385
386 return type_;
387}
388
389std::string_view Def::node_name() const {
390 switch (node()) {
391#define CODE(name, _, __) \
392 case Node::name: return #name;
394#undef CODE
395 default: fe::unreachable();
396 }
397}
398
399Defs Def::deps() const noexcept {
400 if (isa<Type>() || isa<Univ>()) return Defs();
401 assert(type());
402 return Defs(ops_ptr() - 1, (is_set() ? num_ops_ : 0) + 1);
403}
404
405u32 Def::judge() const noexcept {
406 switch (node()) {
407#define CODE(n, _, j) \
408 case Node::n: return u32(j);
410#undef CODE
411 default: fe::unreachable();
412 }
413}
414
415bool Def::is_term() const {
416 if (auto t = type()) {
417 if (auto u = t->type()) {
418 if (auto type = u->isa<Type>()) {
419 if (auto level = Lit::isa(type->level())) return *level == 0;
420 }
421 }
422 }
423 return false;
424}
425
426#ifndef NDEBUG
427const Def* Def::debug_prefix(std::string prefix) const { return dbg_.set(world().sym(prefix + sym().str())), this; }
428const Def* Def::debug_suffix(std::string suffix) const { return dbg_.set(world().sym(sym().str() + suffix)), this; }
429#endif
430
431// clang-format off
432
433const Def* Def::var() {
434 if (var_) return var_;
435 auto& w = world();
436
437 if (w.is_frozen()) return nullptr;
438 if (auto lam = isa<Lam >()) return w.var(lam ->dom(), lam);
439 if (auto pi = isa<Pi >()) return w.var(pi ->dom(), pi);
440 if (auto sig = isa<Sigma>()) return w.var(sig, sig);
441 if (auto arr = isa<Arr >()) return w.var(w.type_idx(arr ->shape()), arr ); // TODO shapes like (2, 3)
442 if (auto pack = isa<Pack >()) return w.var(w.type_idx(pack->shape()), pack); // TODO shapes like (2, 3)
443 if (isa<Bound >()) return w.var(this, this);
444 if (isa<Hole >()) return nullptr;
445 if (isa<Global>()) return nullptr;
446 fe::unreachable();
447}
448
449const Def* Def::arity() const {
450 if (auto sigma = isa<Sigma>()) return world().lit_nat(sigma->num_ops());
451 if (auto arr = isa<Arr >()) return arr->shape();
452 if (auto t = type()) return t->arity();
453 return world().lit_nat_1();
454}
455
456std::optional<nat_t> Def::isa_lit_arity() const {
457 if (auto sigma = isa<Sigma>()) return sigma->num_ops();
458 if (auto arr = isa<Arr >()) return Lit::isa(arr->shape());
459 if (auto t = type()) return t->isa_lit_arity();
460 return 1;
461}
462
463// clang-format on
464
465bool Def::equal(const Def* other) const {
466 if (isa<Univ>() || this->isa_mut() || other->isa_mut()) return this == other;
467
468 bool result = this->node() == other->node() && this->flags() == other->flags()
469 && this->num_ops() == other->num_ops() && this->type() == other->type();
470
471 for (size_t i = 0, e = num_ops(); result && i != e; ++i) result &= this->op(i) == other->op(i);
472
473 return result;
474}
475
476void Def::make_external() { return world().make_external(this); }
477void Def::make_internal() { return world().make_internal(this); }
478
479std::string Def::unique_name() const { return sym().str() + "_"s + std::to_string(gid()); }
480
482 if (auto a = isa_lit_arity(); a && *a < world().flags().scalarize_threshold) return *a;
483 return 1;
484}
485
486const Def* Def::proj(nat_t a, nat_t i) const {
487 World& w = world();
488
489 if (auto arr = isa<Arr>()) {
490 if (arr->arity()->isa<Top>()) return arr->body();
491 return arr->reduce(w.lit_idx(a, i));
492 } else if (auto pack = isa<Pack>()) {
493 if (pack->arity()->isa<Top>()) return pack->body();
494 assert(!w.is_frozen() && "TODO");
495 return pack->reduce(w.lit_idx(a, i));
496 }
497
498 if (a == 1) {
499 if (!type()) return this;
500 if (!isa_mut<Sigma>() && !type()->isa_mut<Sigma>()) return this;
501 }
502
503 if (isa<Tuple>() || isa<Sigma>()) return op(i);
504 if (w.is_frozen()) return nullptr;
505
506 return w.extract(this, a, i);
507}
508
509/*
510 * Idx
511 */
512
513const Def* Idx::isa(const Def* def) {
514 if (auto app = def->isa<App>()) {
515 if (app->callee()->isa<Idx>()) return app->arg();
516 }
517
518 return nullptr;
519}
520
521std::optional<nat_t> Idx::isa_lit(const Def* def) {
522 if (auto size = Idx::isa(def))
523 if (auto l = Lit::isa(size)) return l;
524 return {};
525}
526
527std::optional<nat_t> Idx::size2bitwidth(const Def* size) {
528 if (size->isa<Top>()) return 64;
529 if (auto s = Lit::isa(size)) return size2bitwidth(*s);
530 return {};
531}
532
533/*
534 * Global
535 */
536
537const App* Global::type() const { return Def::type()->as<App>(); }
538const Def* Global::alloced_type() const { return type()->arg(0); }
539
540} // namespace mim
friend class World
Definition lam.h:246
const Def * arg() const
Definition lam.h:230
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:196
const Def * body() const
Definition tuple.h:85
friend class World
Definition tuple.h:117
const Def * shape() const
Definition tuple.h:84
const Def * reduce(const Def *arg) const
Definition tuple.h:101
tag_t tag() const
Definition axm.h:55
u8 trip() const
Definition axm.h:38
friend class World
Definition axm.h:136
NormalizeFn normalizer() const
Definition axm.h:36
sub_t sub() const
Definition axm.h:56
plugin_t plugin() const
Definition axm.h:54
u8 curry() const
Definition axm.h:37
static bool alpha(const Def *d1, const Def *d2)
Definition check.h:63
Base class for all Defs.
Definition def.h:198
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:262
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:486
constexpr Node node() const noexcept
Definition def.h:221
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:241
void make_internal()
Definition def.cpp:477
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Definition def.h:433
Defs deps() const noexcept
Definition def.cpp:399
nat_t num_tprojs() const
As above but yields 1, if Flags::scalarize_threshold is exceeded.
Definition def.cpp:481
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
Definition check.cpp:35
World & world() const noexcept
Definition def.cpp:371
virtual const Def * check()
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
Definition def.h:521
const Def * refine(size_t i, const Def *new_op) const
Definition def.cpp:225
std::string_view node_name() const
Definition def.cpp:389
constexpr auto ops() const noexcept
Definition def.h:261
Vars local_vars() const
Vars reachable by following immutable deps().
Definition def.cpp:289
void make_external()
Definition def.cpp:476
constexpr flags_t flags() const noexcept
Definition def.h:216
Dbg dbg_
Definition def.h:572
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:425
auto vars() noexcept
Definition def.h:374
bool is_term() const
Definition def.cpp:415
const Def * debug_prefix(std::string) const
Definition def.cpp:427
const Def * op(size_t i) const noexcept
Definition def.h:264
bool is_immutabilizable()
Definition def.cpp:174
const Def * var(nat_t a, nat_t i) noexcept
Definition def.h:374
bool is_external() const
Definition def.h:409
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
Definition def.cpp:378
bool is_open() const
Has free_vars()?
Definition def.cpp:358
friend class World
Definition def.h:601
Muts local_muts() const
Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }...
Definition def.cpp:274
const Def * debug_suffix(std::string) const
Definition def.cpp:428
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:242
auto vars(F f) noexcept
Definition def.h:374
const Def * rebuild(World &w, const Def *type, Defs ops) const
Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
Definition def.h:487
const Def * var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
Definition def.cpp:433
virtual constexpr size_t reduction_offset() const noexcept
First Def::op that needs to be dealt with during reduction; e.g.
Definition def.h:507
Sym sym() const
Definition def.h:446
std::optional< nat_t > isa_lit_arity() const
Definition def.cpp:456
flags_t flags_
Definition def.h:579
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
Definition def.h:217
const Def * arity() const
Definition def.cpp:449
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
Definition def.cpp:253
std::string unique_name() const
name + "_" + Def::gid
Definition def.cpp:479
Muts users()
Set of mutables where this mutable is locally referenced.
Definition def.h:402
bool is_closed() const
Has no free_vars()?
Definition def.cpp:350
Vars free_vars() const
Compute a global solution by transitively following mutables as well.
Definition def.cpp:279
Dbg dbg() const
Definition def.h:444
u32 judge() const noexcept
Definition def.cpp:405
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
Definition def.h:378
constexpr size_t num_ops() const noexcept
Definition def.h:265
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:117
friend class World
Definition tuple.h:182
const Def * alloced_type() const
Definition def.cpp:538
friend class World
Definition def.h:855
bool is_mutable() const
Definition def.h:841
const App * type() const
Definition def.cpp:537
Global * stub_(World &, const Def *) override
Definition def.cpp:150
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:10
friend class World
Definition check.h:43
static constexpr nat_t size2bitwidth(nat_t n)
Definition def.h:781
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Definition def.cpp:513
friend class World
Definition def.h:791
static std::optional< nat_t > isa_lit(const Def *def)
Definition def.cpp:521
friend class World
Definition lattice.h:83
friend class World
Definition tuple.h:209
friend class World
Definition lam.h:196
static std::optional< T > isa(const Def *def)
Definition def.h:719
friend class World
Definition def.h:732
friend class World
Definition lattice.h:129
friend class World
Definition lattice.h:60
friend class World
Definition def.h:745
const Def * body() const
Definition tuple.h:132
const Def * shape() const
Definition tuple.cpp:40
friend class World
Definition tuple.h:159
const Def * reduce(const Def *arg) const
Definition tuple.h:149
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:206
A dependent function type.
Definition lam.h:11
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Definition lam.h:14
bool is_implicit() const
Definition lam.h:23
const Def * dom() const
Definition lam.h:32
friend class World
Definition lam.h:101
const Def * codom() const
Definition lam.h:33
const Pi * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:186
friend class World
Definition def.h:813
u32 pass() const
IPass::index within PassMan.
Definition def.h:804
u32 tag() const
Definition def.h:805
constexpr bool empty() const noexcept
Is empty?
Definition sets.h:235
void dot()
Definition sets.h:553
Set merge(Set s1, Set s2)
Yields .
Definition sets.h:481
Set insert(Set s, D *d)
Yields .
Definition sets.h:415
const TExt< Up > * set(Loc l) const
Definition def.h:150
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:191
friend class World
Definition tuple.h:51
friend class World
Definition lattice.h:105
friend class World
Definition lattice.h:44
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:143
Extremum. Either Top (Up) or Bottom.
Definition lattice.h:140
friend class World
Definition lattice.h:153
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:142
friend class World
Definition tuple.h:68
friend class World
Definition def.h:694
friend class World
Definition def.h:673
level_t offset() const
Definition def.h:665
friend class World
Definition def.h:651
friend class World
Definition lattice.h:185
friend class World
Definition def.h:638
friend class World
Definition def.h:624
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:33
auto & muts()
Definition world.h:504
void make_external(Def *)
Definition world.cpp:87
const Def * sigma(Defs ops)
Definition world.cpp:258
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:251
Flags & flags()
Retrieve compile Flags.
Definition world.cpp:71
u32 next_gid()
Definition world.h:89
Sym sym(std::string_view)
Definition world.cpp:74
void make_internal(Def *)
Definition world.cpp:94
const Lit * lit_nat(nat_t a)
Definition world.h:384
auto & vars()
Definition world.h:503
Defs reduce(const Var *var, const Def *arg)
Yields the new body of [mut->var() -> arg]mut.
Definition world.cpp:618
const Lit * lit_nat_1()
Definition world.h:386
#define MIM_NODE(m)
Definition def.h:17
Definition ast.h:14
View< const Def * > Defs
Definition def.h:49
u64 nat_t
Definition types.h:43
Vector< const Def * > DefVec
Definition def.h:50
Dep
Tracks a dependency to certain Defs transitively through the Def::deps() up to but excliding mutables...
Definition def.h:97
@ None
Definition def.h:98
@ Mut
Definition def.h:99
u64 flags_t
Definition types.h:45
uint64_t scalarize_threshold
Definition flags.h:13
u8 node_t
Definition types.h:44
constexpr size_t hash_combine(size_t seed, T v) noexcept
Definition hash.h:58
Sets< Def >::Set Muts
Definition def.h:59
TExt< true > Top
Definition lattice.h:159
constexpr decltype(auto) get(Span< T, N > span) noexcept
Definition span.h:107
consteval size_t hash_begin() noexcept
Definition hash.h:71
constexpr size_t hash(size_t h) noexcept
Definition hash.h:32
Sets< const Var >::Set Vars
Definition def.h:68
uint32_t u32
Definition types.h:34
uint8_t u8
Definition types.h:34
Node
Definition def.h:83
@ Univ
Definition def.h:85
@ Var
Definition def.h:85
CODE(node, name, _)
Definition def.h:84