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