MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
def.h
Go to the documentation of this file.
1#pragma once
2
3#include <optional>
4#include <span>
5
6#include <fe/assert.h>
7#include <fe/cast.h>
8#include <fe/enum.h>
9
10#include "mim/config.h"
11
12#include "mim/util/dbg.h"
13#include "mim/util/sets.h"
14#include "mim/util/util.h"
15#include "mim/util/vector.h"
16
17// clang-format off
18#define MIM_NODE(m) \
19 m(Lit, Judge::Intro) /* keep this first - causes Lit to appear left in Def::less/Def::greater*/ \
20 m(Axm, Judge::Intro) \
21 m(Var, Judge::Intro) \
22 m(Global, Judge::Intro) \
23 m(Proxy, Judge::Intro) \
24 m(Hole, Judge::Hole ) \
25 m(Type, Judge::Meta ) m(Univ, Judge::Meta ) m(UMax, Judge::Meta) m(UInc, (Judge::Meta )) \
26 m(Pi, Judge::Form ) m(Lam, Judge::Intro) m(App, Judge::Elim) \
27 m(Sigma, Judge::Form ) m(Tuple, Judge::Intro) m(Extract, Judge::Elim) m(Insert, (Judge::Intro | Judge::Elim)) \
28 m(Arr, Judge::Form ) m(Pack, Judge::Intro) \
29 m(Join, Judge::Form ) m(Inj, Judge::Intro) m(Match, Judge::Elim) m(Top, (Judge::Intro )) \
30 m(Meet, Judge::Form ) m(Merge, Judge::Intro) m(Split, Judge::Elim) m(Bot, (Judge::Intro )) \
31 m(Reform, Judge::Form ) m(Rule, Judge::Intro) \
32 m(Uniq, Judge::Form ) \
33 m(Nat, Judge::Form ) \
34 m(Idx, Judge::Intro)
35
36#define MIM_IMM_NODE(m) \
37 m(Lit) \
38 m(Axm) \
39 m(Var) \
40 m(Proxy) \
41 m(Type) m(Univ) m(UMax) m(UInc) \
42 m(Pi) m(Lam) m(App) \
43 m(Sigma) m(Tuple) m(Extract) m(Insert) \
44 m(Arr) m(Pack) \
45 m(Join) m(Inj) m(Match) m(Top) \
46 m(Meet) m(Merge) m(Split) m(Bot) \
47 m(Rule) \
48 m(Uniq) \
49 m(Nat) \
50 m(Idx)
51
52#define MIM_MUT_NODE(m) \
53 m(Global) \
54 m(Hole) \
55 m(Pi) m(Lam) \
56 m(Sigma) \
57 m(Arr) m(Pack) \
58 m(Rule)
59// clang-format on
60
61namespace mim {
62
63class App;
64class Axm;
65class Var;
66class Def;
67class World;
68
69/// @name Def
70/// GIDSet / GIDMap keyed by Def::gid of `conset Def*`.
71///@{
72template<class To>
78///@}
79
80/// @name Def (Mutable)
81/// GIDSet / GIDMap keyed by Def::gid of `Def*`.
82///@{
83template<class To>
88///@}
89
90/// @name Var
91/// GIDSet / GIDMap keyed by Var::gid of `const Var*`.
92///@{
93template<class To>
98///@}
99
100using NormalizeFn = const Def* (*)(const Def*, const Def*, const Def*);
101
102using fe::operator&;
103using fe::operator|;
104using fe::operator^;
105using fe::operator<=>;
106using fe::operator==;
107using fe::operator!=;
108
109/// @name Enums that classify certain aspects of Def%s.
110///@{
111
112enum class Node : node_t {
113#define CODE(node, _) node,
115#undef CODE
116};
117
118#define CODE(node, _) +size_t(1)
119static constexpr size_t Num_Nodes = size_t(0) MIM_NODE(CODE);
120#undef CODE
121
122/// Tracks a dependency to certain Def%s transitively through the Def::deps() up to but excliding *mutables*.
123enum class Dep : unsigned {
124 None = 0,
125 Mut = 1 << 0,
126 Var = 1 << 1,
127 Hole = 1 << 2,
128 Proxy = 1 << 3,
129};
130
131/// [Judgement](https://ncatlab.org/nlab/show/judgment).
132enum class Judge : u32 {
133 // clang-format off
134 Form = 1 << 0, ///< [Type Formation](https://ncatlab.org/nlab/show/type+formation) like `T -> T`.
135 Intro = 1 << 1, ///< [Term Introduction](https://ncatlab.org/nlab/show/natural+deduction) like `λ(x: Nat): Nat = x`.
136 Elim = 1 << 2, ///< [Term Elimination](https://ncatlab.org/nlab/show/term+elimination) like `f a`.
137 Meta = 1 << 3, ///< Meta rules for Univ%erse and Type levels.
138 Hole = 1 << 4, ///< Special rule for Hole.
139 // clang-format on
140};
141
142/// [Judgement](https://ncatlab.org/nlab/show/judgment).
143enum class Mut {
144 // clang-format off
145 Mut = 1 << 0, ///< Node may be mutable.
146 Imm = 1 << 1, ///< Node may be immmutable.
147 // clang-format on
148};
149///@}
150
151} // namespace mim
152
153#ifndef DOXYGEN
154// clang-format off
155template<> struct fe::is_bit_enum<mim::Dep> : std::true_type {};
156template<> struct fe::is_bit_enum<mim::Judge> : std::true_type {};
157template<> struct fe::is_bit_enum<mim::Mut> : std::true_type {};
158// clang-format on
159#endif
160
161namespace mim {
162
163/// Use as mixin to wrap all kind of Def::proj and Def::projs variants.
164#define MIM_PROJ(NAME, CONST) \
165 nat_t num_##NAME##s() CONST noexcept { return ((const Def*)NAME())->num_projs(); } \
166 nat_t num_t##NAME##s() CONST noexcept { return ((const Def*)NAME())->num_tprojs(); } \
167 const Def* NAME(nat_t a, nat_t i) CONST noexcept { return ((const Def*)NAME())->proj(a, i); } \
168 const Def* NAME(nat_t i) CONST noexcept { return ((const Def*)NAME())->proj(i); } \
169 const Def* t##NAME(nat_t i) CONST noexcept { return ((const Def*)NAME())->tproj(i); } \
170 template<nat_t A = std::dynamic_extent, class F> \
171 auto NAME##s(F f) CONST noexcept { \
172 return ((const Def*)NAME())->projs<A, F>(f); \
173 } \
174 template<class F> \
175 auto t##NAME##s(F f) CONST noexcept { \
176 return ((const Def*)NAME())->tprojs<F>(f); \
177 } \
178 template<nat_t A = std::dynamic_extent> \
179 auto NAME##s() CONST noexcept { \
180 return ((const Def*)NAME())->projs<A>(); \
181 } \
182 auto t##NAME##s() CONST noexcept { return ((const Def*)NAME())->tprojs(); } \
183 template<class F> \
184 auto NAME##s(nat_t a, F f) CONST noexcept { \
185 return ((const Def*)NAME())->projs<F>(a, f); \
186 } \
187 auto NAME##s(nat_t a) CONST noexcept { return ((const Def*)NAME())->projs(a); }
188
189/// CRTP-based mixin to declare setters for Def::loc \& Def::name using a *covariant* return type.
190template<class P, class D = Def>
191class // D is only needed to make the resolution `D::template set` lazy
192#ifdef _MSC_VER
193 __declspec(empty_bases)
194#endif
195 Setters {
196private:
197 P* super() { return static_cast<P*>(this); }
198 const P* super() const { return static_cast<const P*>(this); }
199
200public:
201 // clang-format off
202 template<bool Ow = false> const P* set(Loc l ) const { super()->D::template set<Ow>(l); return super(); }
203 template<bool Ow = false> P* set(Loc l ) { super()->D::template set<Ow>(l); return super(); }
204 template<bool Ow = false> const P* set( Sym s ) const { super()->D::template set<Ow>(s); return super(); }
205 template<bool Ow = false> P* set( Sym s ) { super()->D::template set<Ow>(s); return super(); }
206 template<bool Ow = false> const P* set( std::string s) const { super()->D::template set<Ow>(std::move(s)); return super(); }
207 template<bool Ow = false> P* set( std::string s) { super()->D::template set<Ow>(std::move(s)); return super(); }
208 template<bool Ow = false> const P* set(Loc l, Sym s ) const { super()->D::template set<Ow>(l, s); return super(); }
209 template<bool Ow = false> P* set(Loc l, Sym s ) { super()->D::template set<Ow>(l, s); return super(); }
210 template<bool Ow = false> const P* set(Loc l, std::string s) const { super()->D::template set<Ow>(l, std::move(s)); return super(); }
211 template<bool Ow = false> P* set(Loc l, std::string s) { super()->D::template set<Ow>(l, std::move(s)); return super(); }
212 template<bool Ow = false> const P* set(Dbg d ) const { super()->D::template set<Ow>(d); return super(); }
213 template<bool Ow = false> P* set(Dbg d ) { super()->D::template set<Ow>(d); return super(); }
214 // clang-format on
215};
216
217/// Base class for all Def%s.
218///
219/// These are the most important subclasses:
220/// | Type Formation | Term Introduction | Term Elimination |
221/// | ----------------- | ----------------- | ----------------- |
222/// | Pi | Lam | App |
223/// | Sigma / Arr | Tuple / Pack | Extract |
224/// | | Insert | Insert |
225/// | Uniq | Wrap | Unwrap |
226/// | Join | Inj | Match |
227/// | Meet | Merge | Split |
228/// | Reform | Rule | |
229/// | Nat | Lit | |
230/// | Idx | Lit | |
231/// In addition there is:
232/// * Var: A variable. Currently the following Def%s may be binders:
233/// * Pi, Lam, Sigma, Arr, Pack
234/// * Axm: To introduce new entities.
235/// * Proxy: Used for intermediate values during optimizations.
236/// * Hole: A metavariable filled in by the type inference (always mutable as holes are filled in later).
237/// * Type, Univ, UMax, UInc: To keep track of type levels.
238///
239/// The data layout (see World::alloc and Def::deps) looks like this:
240/// ```
241/// Def| type | op(0) ... op(num_ops-1) |
242/// |-----------ops-----------|
243/// deps
244/// |--------------------------------| if type() != nullptr && is_set()
245/// |-------------------------| if type() == nullptr && is_set()
246/// |------| if type() != nullptr && !is_set()
247/// || if type() == nullptr && !is_set()
248/// ```
249/// @attention This means that any subclass of Def **must not** introduce additional members.
250/// @see @ref mut
251class Def : public fe::RuntimeCast<Def> {
252private:
253 Def& operator=(const Def&) = delete;
254 Def(const Def&) = delete;
255
256protected:
257 /// @name C'tors and D'tors
258 ///@{
259 Def(World*, Node, const Def* type, Defs ops, flags_t flags); ///< Constructor for an *immutable* Def.
260 Def(Node, const Def* type, Defs ops, flags_t flags); ///< As above but World retrieved from @p type.
261 Def(Node, const Def* type, size_t num_ops, flags_t flags); ///< Constructor for a *mutable* Def.
262 virtual ~Def() = default;
263 ///@}
264
265public:
266 /// @name Getters
267 ///@{
268 World& world() const noexcept;
269 constexpr flags_t flags() const noexcept { return flags_; }
270 constexpr u32 gid() const noexcept { return gid_; } ///< Global id - *unique* number for this Def.
271 constexpr u32 tid() const noexcept { return tid_; } ///< Trie id - only used in Trie.
272 constexpr u32 mark() const noexcept { return mark_; } ///< Used internally by free_vars().
273 constexpr size_t hash() const noexcept { return hash_; }
274 constexpr Node node() const noexcept { return node_; }
275 std::string_view node_name() const;
276 ///@}
277
278 /// @name Judgement
279 /// What kind of Judge%ment represents this Def?
280 ///@{
281 u32 judge() const noexcept;
282 // clang-format off
283 bool is_form() const noexcept { return judge() & Judge::Form; }
284 bool is_intro() const noexcept { return judge() & Judge::Intro; }
285 bool is_elim() const noexcept { return judge() & Judge::Elim; }
286 bool is_meta() const noexcept { return judge() & Judge::Meta; }
287 // clang-format on
288 ///@}
289
290 /// @name type
291 ///@{
292
293 /// Yields the "raw" type of this Def (maybe `nullptr`).
294 /// @see Def::unfold_type.
295 const Def* type() const noexcept;
296 /// Yields the type of this Def and builds a new `Type (UInc n)` if necessary.
297 const Def* unfold_type() const;
298 bool is_term() const;
299 virtual const Def* arity() const;
300 ///@}
301
302 /// @name ops
303 ///@{
304 template<size_t N = std::dynamic_extent>
305 constexpr auto ops() const noexcept {
306 return View<const Def*, N>(ops_ptr(), num_ops_);
307 }
308 const Def* op(size_t i) const noexcept { return ops()[i]; }
309 constexpr size_t num_ops() const noexcept { return num_ops_; }
310 ///@}
311
312 /// @name Setting Ops (Mutables Only)
313 /// @anchor set_ops
314 /// You can set and change the Def::ops of a mutable after construction.
315 /// However, you have to obey the following rules:
316 /// If Def::is_set() is ...
317 /// * `false`, [set](@ref Def::set) the [operands](@ref Def::ops) from left to right.
318 /// * `true`, Def::unset() the operands first and then start over:
319 /// ```
320 /// mut->unset()->set({a, b, c});
321 /// ```
322 ///
323 /// MimIR assumes that a mutable is *final*, when its last operand is set.
324 /// Then, Def::check() will be invoked.
325 ///@{
326 bool is_set() const; ///< Yields `true` if empty or the last op is set.
327 Def* set(size_t i, const Def*); ///< Successively set from left to right.
328 Def* set(Defs ops); ///< Set @p ops all at once (no Def::unset necessary beforehand).
329 Def* unset(); ///< Unsets all Def::ops; works even, if not set at all or only partially set.
330
331 /// Update type.
332 /// @warning Only make type-preserving updates such as removing Hole%s.
333 /// Do this even before updating all other ops()!
334 Def* set_type(const Def*);
335 ///@}
336
337 /// @name deps
338 /// All *dependencies* of a Def and includes:
339 /// * Def::type() (if not `nullptr`) and
340 /// * the other Def::ops() (only included, if Def::is_set()) in this order.
341 ///@{
342 Defs deps() const noexcept;
343 const Def* dep(size_t i) const noexcept { return deps()[i]; }
344 size_t num_deps() const noexcept { return deps().size(); }
345 ///@}
346
347 /// @name has_dep
348 /// Checks whether one Def::deps() contains specific elements defined in Dep.
349 /// This works up to the next *mutable*.
350 /// For example, consider the Tuple `tup`: `(?, lam (x: Nat) = y)`:
351 /// ```
352 /// bool has_hole = tup->has_dep(Dep::Hole); // true
353 /// bool has_mut = tup->has_dep(Dep::Mut); // true
354 /// bool has_var = tup->has_dep(Dep::Var); // false - y is contained in another mutable
355 /// ```
356 ///@{
357 bool has_dep() const { return dep_ != 0; }
358 bool has_dep(Dep d) const { return has_dep(unsigned(d)); }
359 bool has_dep(unsigned u) const { return dep_ & u; }
360 ///@}
361
362 /// @name proj
363 /// @anchor proj
364 /// Splits this Def via Extract%s or directly accessing the Def::ops in the case of Sigma%s or Arr%ays.
365 /// ```
366 /// std::array<const Def*, 2> ab = def->projs<2>();
367 /// std::array<u64, 2> xy = def->projs<2>([](auto def) { return Lit::as(def); });
368 /// auto [a, b] = def->projs<2>();
369 /// auto [x, y] = def->projs<2>([](auto def) { return Lit::as(def); });
370 /// Vector<const Def*> projs1 = def->projs(); // "projs1" has def->num_projs() many elements
371 /// Vector<const Def*> projs2 = def->projs(n);// "projs2" has n elements - asserts if incorrect
372 /// // same as above but applies Lit::as<nat_t>(def) to each element
373 /// Vector<const Lit*> lits1 = def->projs( [](auto def) { return Lit::as(def); });
374 /// Vector<const Lit*> lits2 = def->projs(n, [](auto def) { return Lit::as(def); });
375 /// ```
376 ///@{
377
378 /// Yields Def::arity(), if it is a Lit, or `1` otherwise.
379 nat_t num_projs() const;
380 nat_t num_tprojs() const; ///< As above but yields 1, if Flags::scalarize_threshold is exceeded.
381
382 /// Similar to World::extract while assuming an arity of @p a, but also works on Sigma%s and Arr%ays.
383 const Def* proj(nat_t a, nat_t i) const;
384 const Def* proj(nat_t i) const { return proj(num_projs(), i); } ///< As above but takes Def::num_projs as arity.
385 const Def* tproj(nat_t i) const { return proj(num_tprojs(), i); } ///< As above but takes Def::num_tprojs.
386
387 /// Splits this Def via Def::proj%ections into an Array (if `A == std::dynamic_extent`) or `std::array` (otherwise).
388 /// Applies @p f to each element.
389 template<nat_t A = std::dynamic_extent, class F>
390 auto projs(F f) const {
391 using R = std::decay_t<decltype(f(this))>;
392 if constexpr (A == std::dynamic_extent) {
393 return projs(num_projs(), f);
394 } else {
395 std::array<R, A> array;
396 for (nat_t i = 0; i != A; ++i)
397 array[i] = f(proj(A, i));
398 return array;
399 }
400 }
401
402 template<class F>
403 auto tprojs(F f) const {
404 return projs(num_tprojs(), f);
405 }
406
407 template<class F>
408 auto projs(nat_t a, F f) const {
409 using R = std::decay_t<decltype(f(this))>;
410 return Vector<R>(a, [&](nat_t i) { return f(proj(a, i)); });
411 }
412 template<nat_t A = std::dynamic_extent>
413 auto projs() const {
414 return projs<A>([](const Def* def) { return def; });
415 }
416 auto tprojs() const {
417 return tprojs([](const Def* def) { return def; });
418 }
419 auto projs(nat_t a) const {
420 return projs(a, [](const Def* def) { return def; });
421 }
422 ///@}
423
424 /// @name var
425 /// @anchor var
426 /// Retrieve Var for *mutables*.
427 /// @see @ref proj
428 ///@{
430 /// Not necessarily a Var: E.g., if the return type is `[]`, this will yield `()`.
431 const Def* var();
432 /// Only returns not `nullptr`, if Var of this mutable has ever been created.
433 const Var* has_var() { return var_; }
434 /// As above if `this` is a *mutable*.
435 const Var* has_var() const {
436 if (auto mut = isa_mut()) return mut->has_var();
437 return nullptr;
438 }
439
440 /// If `this` is a binder, compute the type of its Var%iable.
441 const Def* var_type();
442 ///@}
443
444 /// @name Free Vars and Muts
445 /// * local_muts() / local_vars() are cached and hash-consed.
446 /// * free_vars() are computed on demand and cached in mutables.
447 /// They will be transitively invalidated by following users(), if a mutable is mutated.
448 ///@{
449
450 /// Mutables reachable by following *immutable* deps(); `mut->local_muts()` is by definition the set `{ mut }`.
451 Muts local_muts() const;
452
453 /// Var%s reachable by following *immutable* deps().
454 /// @note `var->local_vars()` is by definition the set `{ var }`.
455 Vars local_vars() const;
456
457 /// Compute a global solution by transitively following *mutables* as well.
458 Vars free_vars() const;
459 Vars free_vars();
460 Muts users() { return muts_; } ///< Set of mutables where this mutable is locally referenced.
461 bool is_open() const; ///< Has free_vars()?
462 bool is_closed() const; ///< Has no free_vars()?
463 ///@}
464
465 /// @name external
466 ///@{
467 bool is_external() const noexcept { return external_; }
468 void make_external();
469 void make_internal();
470 void transfer_external(Def* to);
471 ///@}
472
473 /// @name Casts
474 /// @see @ref cast_builtin
475 ///@{
476 bool is_mutable() const noexcept { return mut_; }
477
478 // clang-format off
479 template<class T = Def> const T* isa_imm() const { return isa_mut<T, true>(); }
480 template<class T = Def> const T* as_imm() const { return as_mut<T, true>(); }
481 // clang-format on
482
483 /// If `this` is *mutable*, it will cast `const`ness away and perform a `dynamic_cast` to @p T.
484 template<class T = Def, bool invert = false>
485 T* isa_mut() const {
486 if constexpr (std::is_same<T, Def>::value)
487 return mut_ ^ invert ? const_cast<Def*>(this) : nullptr;
488 else
489 return mut_ ^ invert ? const_cast<Def*>(this)->template isa<T>() : nullptr;
490 }
491
492 /// Asserts that `this` is a *mutable*, casts `const`ness away and performs a `static_cast` to @p T.
493 template<class T = Def, bool invert = false>
494 T* as_mut() const {
495 assert(mut_ ^ invert);
496 if constexpr (std::is_same<T, Def>::value)
497 return const_cast<Def*>(this);
498 else
499 return const_cast<Def*>(this)->template as<T>();
500 }
501 ///@}
502
503 /// @name Dbg Getters
504 ///@{
505 Dbg dbg() const { return dbg_; }
506 Loc loc() const { return dbg_.loc(); }
507 Sym sym() const { return dbg_.sym(); }
508 std::string unique_name() const; ///< name + "_" + Def::gid
509 ///@}
510
511 /// @name Dbg Setters
512 /// Every subclass `S` of Def has the same setters that return `S*`/`const S*` via the mixin Setters.
513 ///@{
514 // clang-format off
515 template<bool Ow = false> const Def* set(Loc l) const { if (Ow || !dbg_.loc()) dbg_.set(l); return this; }
516 template<bool Ow = false> Def* set(Loc l) { if (Ow || !dbg_.loc()) dbg_.set(l); return this; }
517 template<bool Ow = false> const Def* set(Sym s) const { if (Ow || !dbg_.sym()) dbg_.set(s); return this; }
518 template<bool Ow = false> Def* set(Sym s) { if (Ow || !dbg_.sym()) dbg_.set(s); return this; }
519 template<bool Ow = false> const Def* set( std::string s) const { set<Ow>(sym(std::move(s))); return this; }
520 template<bool Ow = false> Def* set( std::string s) { set<Ow>(sym(std::move(s))); return this; }
521 template<bool Ow = false> const Def* set(Loc l, Sym s ) const { set<Ow>(l); set<Ow>(s); return this; }
522 template<bool Ow = false> Def* set(Loc l, Sym s ) { set<Ow>(l); set<Ow>(s); return this; }
523 template<bool Ow = false> const Def* set(Loc l, std::string s) const { set<Ow>(l); set<Ow>(sym(std::move(s))); return this; }
524 template<bool Ow = false> Def* set(Loc l, std::string s) { set<Ow>(l); set<Ow>(sym(std::move(s))); return this; }
525 template<bool Ow = false> const Def* set(Dbg d) const { set<Ow>(d.loc(), d.sym()); return this; }
526 template<bool Ow = false> Def* set(Dbg d) { set<Ow>(d.loc(), d.sym()); return this; }
527 // clang-format on
528 ///@}
529
530 /// @name debug_prefix/suffix
531 /// Prepends/Appends a prefix/suffix to Def::name - but only in `Debug` build.
532 ///@{
533#ifndef NDEBUG
534 const Def* debug_prefix(std::string) const;
535 const Def* debug_suffix(std::string) const;
536#else
537 const Def* debug_prefix(std::string) const { return this; }
538 const Def* debug_suffix(std::string) const { return this; }
539#endif
540 ///@}
541
542 /// @name Rebuild
543 ///@{
544 Def* stub(World& w, const Def* type) { return stub_(w, type)->set(dbg()); }
545 Def* stub(const Def* type) { return stub(world(), type); }
546
547 /// Def::rebuild%s this Def while using @p new_op as substitute for its @p i'th Def::op
548 const Def* rebuild(World& w, const Def* type, Defs ops) const {
549 assert(isa_imm());
550 return rebuild_(w, type, ops)->set(dbg());
551 }
552 const Def* rebuild(const Def* type, Defs ops) const { return rebuild(world(), type, ops); }
553
554 /// Tries to make an immutable from a mutable.
555 /// This usually works if the mutable isn't recursive and its var isn't used.
556 virtual const Def* immutabilize() { return nullptr; }
557 bool is_immutabilizable();
558
559 const Def* refine(size_t i, const Def* new_op) const;
560
561 /// @see World::reduce
562 template<size_t N = std::dynamic_extent>
563 constexpr auto reduce(const Def* arg) const {
564 return reduce_(arg).span<N>();
565 }
566
567 /// First Def::op that needs to be dealt with during reduction; e.g. for a Pi we don't reduce the Pi::dom.
568 /// @see World::reduce
569 virtual constexpr size_t reduction_offset() const noexcept { return size_t(-1); }
570 ///@}
571
572 /// @name Type Checking
573 ///@{
574
575 /// Checks whether the `i`th operand can be set to `def`.
576 /// The method returns a possibly updated version of `def` (e.g. where Hole%s have been resolved).
577 /// This is the actual `def` that will be set as the `i`th operand.
578 virtual const Def* check([[maybe_unused]] size_t i, const Def* def) { return def; }
579
580 /// After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
581 /// The method returns a possibly updated version of its type (e.g. where Hole%s have been resolved).
582 /// If different from Def::type, it will update its Def::type to a Def::zonk%ed version of that.
583 virtual const Def* check() { return type(); }
584
585 /// Yields `true`, if Def::local_muts() contain a Hole that is set.
586 /// Rewriting (Def::zonk%ing) will resolve the Hole to its operand.
587 bool needs_zonk() const;
588
589 /// If Hole%s have been filled, reconstruct the program without them.
590 /// Only goes up to but excluding other mutables.
591 /// @see https://stackoverflow.com/questions/31889048/what-does-the-ghc-source-mean-by-zonk
592 const Def* zonk() const;
593
594 /// If *mutable, zonk%s all ops and tries to immutabilize it; otherwise just zonk.
595 const Def* zonk_mut() const;
596 ///@}
597
598 /// zonk%s all @p defs and retuns a new DefVec.
599 static DefVec zonk(Defs defs);
600
601 /// @name dump
602 ///@{
603 void dump() const;
604 void dump(int max) const;
605 void write(int max) const;
606 void write(int max, const char* file) const;
607 std::ostream& stream(std::ostream&, int max) const;
608 ///@}
609
610 /// @name Syntactic Comparison
611 ///
612 enum class Cmp {
613 L, ///< Less
614 G, ///< Greater
615 E, ///< Equal
616 U, ///< Unknown
617 };
618 [[nodiscard]] static Cmp cmp(const Def* a, const Def* b);
619 [[nodiscard]] static bool less(const Def* a, const Def* b);
620 [[nodiscard]] static bool greater(const Def* a, const Def* b);
621
622 /// @name dot
623 /// Dumps DOT to @p os while obeying maximum recursion depth of @p max.
624 /// If @p types is `true`, Def::type() dependencies will be followed as well.
625 ///@{
626 void dot(std::ostream& os, uint32_t max = 0xFFFFFF, bool types = false) const;
627 /// Same as above but write to @p file or `std::cout` if @p file is `nullptr`.
628 void dot(const char* file = nullptr, uint32_t max = 0xFFFFFF, bool types = false) const;
629 void dot(const std::string& file, uint32_t max = 0xFFFFFF, bool types = false) const {
630 return dot(file.c_str(), max, types);
631 }
632 ///@}
633
634protected:
635 /// @name Wrappers for World::sym
636 /// These are here to have Def::set%ters inline without including `mim/world.h`.
637 ///@{
638 Sym sym(const char*) const;
639 Sym sym(std::string_view) const;
640 Sym sym(std::string) const;
641 ///@}
642
643private:
644 Defs reduce_(const Def* arg) const;
645 virtual Def* stub_(World&, const Def*) { fe::unreachable(); }
646 virtual const Def* rebuild_(World& w, const Def* type, Defs ops) const = 0;
647
648 template<bool init>
649 Vars free_vars(bool&, uint32_t);
650 void invalidate();
651 const Def** ops_ptr() const {
652 return reinterpret_cast<const Def**>(reinterpret_cast<char*>(const_cast<Def*>(this + 1)));
653 }
654 bool equal(const Def* other) const;
655
656 template<Cmp>
657 [[nodiscard]] static bool cmp_(const Def* a, const Def* b);
658
659protected:
660 mutable Dbg dbg_;
661 union {
662 NormalizeFn normalizer_; ///< Axm only: Axm%s use this member to store their normalizer.
663 const Axm* axm_; ///< App only: Curried App%s of Axm%s use this member to propagate the Axm.
664 const Var* var_; ///< Mutable only: Var of a mutable.
665 mutable World* world_;
666 };
670
671private:
672 Node node_;
673 bool mut_ : 1;
674 bool external_ : 1;
675 unsigned dep_ : 6;
676 u32 mark_ = 0;
677#ifndef NDEBUG
678 size_t curr_op_ = 0;
679#endif
680 u32 gid_;
681 u32 num_ops_;
682 size_t hash_;
683 Vars vars_; // Mutable: local vars; Immutable: free vars.
684 Muts muts_; // Immutable: local_muts; Mutable: users;
685 mutable u32 tid_ = 0;
686 mutable const Def* type_;
687
688 template<class D, size_t N>
689 friend class Sets;
690 friend class World;
691 friend void swap(World&, World&) noexcept;
692 friend std::ostream& operator<<(std::ostream&, const Def*);
693};
694
695/// A variable introduced by a binder (mutable).
696/// @note Var will keep its type_ field as `nullptr`.
697/// Instead, Def::type() and Var::type() will compute the type via Def::var_type().
698/// The reason is that the type could need a Def::zonk().
699/// But we don't want to have several Var%s that belong to the same binder.
700class Var : public Def, public Setters<Var> {
701private:
702 Var(Def* mut)
703 : Def(Node, nullptr, Defs{mut}, 0) {}
704
705public:
706 using Setters<Var>::set;
707
708 const Def* type() const { return mut()->var_type(); }
709
710 /// @name ops
711 ///@{
712 Def* mut() const { return op(0)->as_mut(); }
713 ///@}
714
715 static constexpr auto Node = mim::Node::Var;
716 static constexpr size_t Num_Ops = 1;
717
718private:
719 const Def* rebuild_(World&, const Def*, Defs) const final;
720
721 friend class World;
722};
723
724class Univ : public Def, public Setters<Univ> {
725public:
726 using Setters<Univ>::set;
727 static constexpr auto Node = mim::Node::Univ;
728 static constexpr size_t Num_Ops = 0;
729
730private:
732 : Def(&world, Node, nullptr, Defs{}, 0) {}
733
734 const Def* rebuild_(World&, const Def*, Defs) const final;
735
736 friend class World;
737};
738
739class UMax : public Def, public Setters<UMax> {
740public:
741 using Setters<UMax>::set;
742 static constexpr auto Node = mim::Node::UMax;
743 static constexpr size_t Num_Ops = std::dynamic_extent;
744
745 enum Sort { Univ, Kind, Type, Term };
746
747private:
748 UMax(World&, Defs ops);
749
750 const Def* rebuild_(World&, const Def*, Defs) const final;
751
752 friend class World;
753};
754
755class UInc : public Def, public Setters<UInc> {
756private:
757 UInc(const Def* op, level_t offset)
758 : Def(Node, op->type()->as<Univ>(), {op}, offset) {}
759
760public:
761 using Setters<UInc>::set;
762
763 /// @name ops
764 ///@{
765 const Def* op() const { return Def::op(0); }
766 level_t offset() const { return flags(); }
767 ///@}
768
769 static constexpr auto Node = mim::Node::UInc;
770 static constexpr size_t Num_Ops = 1;
771
772private:
773 const Def* rebuild_(World&, const Def*, Defs) const final;
774
775 friend class World;
776};
777
778class Type : public Def, public Setters<Type> {
779private:
780 Type(const Def* level)
781 : Def(Node, nullptr, {level}, 0) {}
782
783public:
784 using Setters<Type>::set;
785
786 /// @name ops
787 ///@{
788 const Def* level() const { return op(0); }
789 ///@}
790
791 static constexpr auto Node = mim::Node::Type;
792 static constexpr size_t Num_Ops = 1;
793
794private:
795 const Def* rebuild_(World&, const Def*, Defs) const final;
796
797 friend class World;
798};
799
800class Lit : public Def, public Setters<Lit> {
801private:
802 Lit(const Def* type, flags_t val)
803 : Def(Node, type, Defs{}, val) {}
804
805public:
806 using Setters<Lit>::set;
807
808 /// @name Get actual Constant
809 ///@{
810 template<class T = flags_t>
811 T get() const {
812 static_assert(sizeof(T) <= 8);
813 return bitcast<T>(flags_);
814 }
815 ///@}
816
817 using Def::as;
818 using Def::isa;
819
820 /// @name Casts
821 ///@{
822 /// @see @ref cast_lit
823 template<class T = nat_t>
824 static std::optional<T> isa(const Def* def) {
825 if (!def) return {};
826 if (auto lit = def->isa<Lit>()) return lit->get<T>();
827 return {};
828 }
829 template<class T = nat_t>
830 static T as(const Def* def) {
831 return def->as<Lit>()->get<T>();
832 }
833 ///@}
834
835 static constexpr auto Node = mim::Node::Lit;
836 static constexpr size_t Num_Ops = 0;
837
838private:
839 const Def* rebuild_(World&, const Def*, Defs) const final;
840
841 friend class World;
842};
843
844class Nat : public Def, public Setters<Nat> {
845public:
846 using Setters<Nat>::set;
847 static constexpr auto Node = mim::Node::Nat;
848 static constexpr size_t Num_Ops = 0;
849
850private:
851 Nat(World& world);
852
853 const Def* rebuild_(World&, const Def*, Defs) const final;
854
855 friend class World;
856};
857
858/// A built-in constant of type `Nat -> *`.
859class Idx : public Def, public Setters<Idx> {
860private:
861 Idx(const Def* type)
862 : Def(Node, type, Defs{}, 0) {}
863
864public:
865 using Setters<Idx>::set;
866 using Def::as;
867 using Def::isa;
868
869 /// @name isa
870 ///@{
871
872 /// Checks if @p def is a `Idx s` and returns `s` or `nullptr` otherwise.
873 static const Def* isa(const Def* def);
874 static const Def* as(const Def* def) {
875 auto res = isa(def);
876 assert(res);
877 return res;
878 }
879 static std::optional<nat_t> isa_lit(const Def* def);
880 static nat_t as_lit(const Def* def) {
881 auto res = isa_lit(def);
882 assert(res.has_value());
883 return *res;
884 }
885 ///@}
886
887 /// @name Convert between Idx::isa and bitwidth and vice versa
888 ///@{
889 // clang-format off
890 static constexpr nat_t bitwidth2size(nat_t n) { assert(n != 0); return n == 64 ? 0 : (1_n << n); }
891 static constexpr nat_t size2bitwidth(nat_t n) { return n == 0 ? 64 : std::bit_width(n - 1_n); }
892 // clang-format on
893 static std::optional<nat_t> size2bitwidth(const Def* size);
894 ///@}
895
896 static constexpr auto Node = mim::Node::Idx;
897 static constexpr size_t Num_Ops = 0;
898
899private:
900 const Def* rebuild_(World&, const Def*, Defs) const final;
901
902 friend class World;
903};
904
905class Proxy : public Def, public Setters<Proxy> {
906private:
907 Proxy(const Def* type, u32 pass, u32 tag, Defs ops)
908 : Def(Node, type, ops, (u64(pass) << 32_u64) | u64(tag)) {}
909
910public:
911 using Setters<Proxy>::set;
912
913 /// @name Getters
914 ///@{
915 u32 pass() const { return u32(flags() >> 32_u64); } ///< IPass::index within PassMan.
916 u32 tag() const { return u32(flags()); }
917 ///@}
918
919 static constexpr auto Node = mim::Node::Proxy;
920 static constexpr size_t Num_Ops = std::dynamic_extent;
921
922private:
923 const Def* rebuild_(World&, const Def*, Defs) const final;
924
925 friend class World;
926};
927
928/// @deprecated A global variable in the data segment.
929/// A Global may be mutable or immutable.
930/// @deprecated Will be removed.
931class Global : public Def, public Setters<Global> {
932private:
933 Global(const Def* type, bool is_mutable)
934 : Def(Node, type, 1, is_mutable) {}
935
936public:
937 using Setters<Global>::set;
938
939 /// @name ops
940 ///@{
941 const Def* init() const { return op(0); }
942 void set(const Def* init) { Def::set(0, init); }
943 ///@}
944
945 /// @name type
946 ///@{
947 const App* type() const;
948 const Def* alloced_type() const;
949 ///@}
950
951 /// @name Getters
952 ///@{
953 bool is_mutable() const { return flags(); }
954 ///@}
955
956 /// @name Rebuild
957 ///@{
958 Global* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
959 ///@}
960
961 static constexpr auto Node = mim::Node::Global;
962 static constexpr size_t Num_Ops = 1;
963
964private:
965 const Def* rebuild_(World&, const Def*, Defs) const final;
966 Global* stub_(World&, const Def*) final;
967
968 friend class World;
969};
970
971} // namespace mim
Definition axm.h:9
Base class for all Defs.
Definition def.h:251
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:295
size_t num_deps() const noexcept
Definition def.h:344
const Def * zonk_mut() const
If *mutable, zonks all ops and tries to immutabilize it; otherwise just zonk.
Definition check.cpp:23
const Def * set(Dbg d) const
Definition def.h:525
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:588
constexpr Node node() const noexcept
Definition def.h:274
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:263
void dot(std::ostream &os, uint32_t max=0xFFFFFF, bool types=false) const
Definition dot.cpp:126
void make_internal()
Definition def.cpp:571
virtual const Def * check(size_t i, const Def *def)
Checks whether the ith operand can be set to def.
Definition def.h:578
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Definition def.h:494
const Var * has_var() const
As above if this is a mutable.
Definition def.h:435
void dump() const
Definition dump.cpp:452
Defs deps() const noexcept
Definition def.cpp:470
auto projs() const
Definition def.h:413
u8 trip_
Definition def.h:669
bool has_dep(Dep d) const
Definition def.h:358
bool is_elim() const noexcept
Definition def.h:285
nat_t num_tprojs() const
As above but yields 1, if Flags::scalarize_threshold is exceeded.
Definition def.cpp:583
virtual ~Def()=default
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
Definition check.cpp:21
bool has_dep(unsigned u) const
Definition def.h:359
World & world() const noexcept
Definition def.cpp:439
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:583
const Def * refine(size_t i, const Def *new_op) const
Definition def.cpp:229
Def * set_type(const Def *)
Update type.
Definition def.cpp:280
void dot(const std::string &file, uint32_t max=0xFFFFFF, bool types=false) const
Definition def.h:629
std::string_view node_name() const
Definition def.cpp:460
auto projs(nat_t a, F f) const
Definition def.h:408
bool is_intro() const noexcept
Definition def.h:284
constexpr auto ops() const noexcept
Definition def.h:305
Vars local_vars() const
Vars reachable by following immutable deps().
Definition def.cpp:348
void make_external()
Definition def.cpp:570
constexpr flags_t flags() const noexcept
Definition def.h:269
Dbg dbg_
Definition def.h:660
virtual Def * stub_(World &, const Def *)
Definition def.h:645
const Def * set(std::string s) const
Definition def.h:519
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:485
Vars free_vars()
Definition def.cpp:350
constexpr u32 mark() const noexcept
Used internally by free_vars().
Definition def.h:272
constexpr u32 tid() const noexcept
Trie id - only used in Trie.
Definition def.h:271
auto projs(nat_t a) const
Definition def.h:419
u8 curry_
Definition def.h:668
auto tprojs() const
Definition def.h:416
friend std::ostream & operator<<(std::ostream &, const Def *)
This will stream def as an operand.
Definition dump.cpp:423
bool is_term() const
Definition def.cpp:487
const Def * debug_prefix(std::string) const
Definition def.cpp:499
const Def * op(size_t i) const noexcept
Definition def.h:308
bool is_immutabilizable()
Definition def.cpp:174
virtual const Def * rebuild_(World &w, const Def *type, Defs ops) const =0
const Def * var(nat_t a, nat_t i) noexcept
Definition def.h:429
void transfer_external(Def *to)
Definition def.cpp:573
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
Definition def.cpp:452
const Def * proj(nat_t i) const
As above but takes Def::num_projs as arity.
Definition def.h:384
auto projs(F f) const
Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (other...
Definition def.h:390
bool is_open() const
Has free_vars()?
Definition def.cpp:426
constexpr size_t hash() const noexcept
Definition def.h:273
friend class World
Definition def.h:690
virtual const Def * immutabilize()
Tries to make an immutable from a mutable.
Definition def.h:556
bool is_form() const noexcept
Definition def.h:283
Def * set(Dbg d)
Definition def.h:526
Muts local_muts() const
Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }...
Definition def.cpp:332
Def * set(Sym s)
Definition def.h:518
const Def * debug_suffix(std::string) const
Definition def.cpp:500
const Def * set(Sym s) const
Definition def.h:517
Def * set(Loc l)
Definition def.h:516
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.cpp:447
const Def * dep(size_t i) const noexcept
Definition def.h:343
bool is_mutable() const noexcept
Definition def.h:476
bool is_external() const noexcept
Definition def.h:467
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:548
const Def * set(Loc l, Sym s) const
Definition def.h:521
static bool less(const Def *a, const Def *b)
Definition def.cpp:549
Def * set(std::string s)
Definition def.h:520
bool is_meta() const noexcept
Definition def.h:286
static bool greater(const Def *a, const Def *b)
Definition def.cpp:550
bool has_dep() const
Definition def.h:357
const Def * set(Loc l) const
Definition def.h:515
Loc loc() const
Definition def.h:506
void write(int max) const
Definition dump.cpp:460
auto tprojs(F f) const
Definition def.h:403
Def * set(Loc l, std::string s)
Definition def.h:524
friend class Sets
Definition def.h:689
const T * as_imm() const
Definition def.h:480
Def * stub(const Def *type)
Definition def.h:545
static Cmp cmp(const Def *a, const Def *b)
Definition def.cpp:507
virtual constexpr size_t reduction_offset() const noexcept
First Def::op that needs to be dealt with during reduction; e.g.
Definition def.h:569
Sym sym() const
Definition def.h:507
nat_t num_projs() const
Yields Def::arity(), if it is a Lit, or 1 otherwise.
Definition def.cpp:581
std::ostream & stream(std::ostream &, int max) const
Definition dump.cpp:432
flags_t flags_
Definition def.h:667
friend void swap(World &, World &) noexcept
const Def * var_type()
If this is a binder, compute the type of its Variable.
Definition def.cpp:314
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
Definition def.h:270
virtual const Def * arity() const
Definition def.cpp:553
Def * unset()
Unsets all Def::ops; works even, if not set at all or only partially set.
Definition def.cpp:286
std::string unique_name() const
name + "_" + Def::gid
Definition def.cpp:579
constexpr auto reduce(const Def *arg) const
Definition def.h:563
const Def * set(Loc l, std::string s) const
Definition def.h:523
const T * isa_imm() const
Definition def.h:479
bool needs_zonk() const
Yields true, if Def::local_muts() contain a Hole that is set.
Definition check.cpp:12
Muts users()
Set of mutables where this mutable is locally referenced.
Definition def.h:460
bool is_closed() const
Has no free_vars()?
Definition def.cpp:418
const Def * rebuild(const Def *type, Defs ops) const
Definition def.h:552
Def * set(Loc l, Sym s)
Definition def.h:522
Dbg dbg() const
Definition def.h:505
Def * stub(World &w, const Def *type)
Definition def.h:544
u32 judge() const noexcept
Definition def.cpp:477
const Def * tproj(nat_t i) const
As above but takes Def::num_tprojs.
Definition def.h:385
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
Definition def.h:433
constexpr size_t num_ops() const noexcept
Definition def.h:309
@ E
Equal.
Definition def.h:615
@ U
Unknown.
Definition def.h:616
@ L
Less.
Definition def.h:613
@ G
Greater.
Definition def.h:614
const Def * init() const
Definition def.h:941
void set(const Def *init)
Definition def.h:942
Global * stub(const Def *type)
Definition def.h:958
const Def * alloced_type() const
Definition def.cpp:638
friend class World
Definition def.h:968
bool is_mutable() const
Definition def.h:953
const App * type() const
Definition def.cpp:637
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:108
static constexpr size_t Num_Ops
Definition def.h:962
Global * stub_(World &, const Def *) final
Definition def.cpp:149
static constexpr auto Node
Definition def.h:961
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:14
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:109
static constexpr auto Node
Definition def.h:896
static nat_t as_lit(const Def *def)
Definition def.h:880
static constexpr nat_t size2bitwidth(nat_t n)
Definition def.h:891
static constexpr nat_t bitwidth2size(nat_t n)
Definition def.h:890
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Definition def.cpp:613
friend class World
Definition def.h:902
static std::optional< nat_t > isa_lit(const Def *def)
Definition def.cpp:621
static constexpr size_t Num_Ops
Definition def.h:897
static const Def * as(const Def *def)
Definition def.h:874
static constexpr auto Node
Definition def.h:835
static std::optional< T > isa(const Def *def)
Definition def.h:824
friend class World
Definition def.h:841
T get() const
Definition def.h:811
static T as(const Def *def)
Definition def.h:830
static constexpr size_t Num_Ops
Definition def.h:836
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:118
friend class World
Definition def.h:855
static constexpr auto Node
Definition def.h:847
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:110
static constexpr size_t Num_Ops
Definition def.h:848
static constexpr size_t Num_Ops
Definition def.h:920
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:122
friend class World
Definition def.h:925
static constexpr auto Node
Definition def.h:919
u32 pass() const
IPass::index within PassMan.
Definition def.h:915
u32 tag() const
Definition def.h:916
CRTP-based mixin to declare setters for Def::loc & Def::name using a covariant return type.
Definition def.h:195
P * set(Loc l, Sym s)
Definition def.h:209
P * set(std::string s)
Definition def.h:207
const P * set(Sym s) const
Definition def.h:204
const P * set(Loc l, Sym s) const
Definition def.h:208
const P * set(Loc l) const
Definition def.h:202
P * set(Loc l)
Definition def.h:203
const P * set(Dbg d) const
Definition def.h:212
const P * set(Loc l, std::string s) const
Definition def.h:210
P * set(Sym s)
Definition def.h:205
P * set(Dbg d)
Definition def.h:213
P * set(Loc l, std::string s)
Definition def.h:211
const P * set(std::string s) const
Definition def.h:206
friend class World
Definition def.h:797
static constexpr size_t Num_Ops
Definition def.h:792
static constexpr auto Node
Definition def.h:791
const Def * level() const
Definition def.h:788
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:129
const Def * op() const
Definition def.h:765
static constexpr auto Node
Definition def.h:769
friend class World
Definition def.h:775
level_t offset() const
Definition def.h:766
static constexpr size_t Num_Ops
Definition def.h:770
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:130
@ Type
Definition def.h:745
@ Univ
Definition def.h:745
@ Term
Definition def.h:745
@ Kind
Definition def.h:745
static constexpr auto Node
Definition def.h:742
friend class World
Definition def.h:752
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:131
static constexpr size_t Num_Ops
Definition def.h:743
static constexpr size_t Num_Ops
Definition def.h:728
static constexpr auto Node
Definition def.h:727
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:111
friend class World
Definition def.h:736
A variable introduced by a binder (mutable).
Definition def.h:700
const Def * type() const
Definition def.h:708
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:133
static constexpr auto Node
Definition def.h:715
friend class World
Definition def.h:721
static constexpr size_t Num_Ops
Definition def.h:716
Def * mut() const
Definition def.h:712
This is a thin wrapper for absl::InlinedVector<T, N, A> which is a drop-in replacement for std::vecto...
Definition vector.h:18
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:32
#define MIM_NODE(m)
Definition def.h:18
#define MIM_PROJ(NAME, CONST)
Use as mixin to wrap all kind of Def::proj and Def::projs variants.
Definition def.h:164
Definition ast.h:14
View< const Def * > Defs
Definition def.h:76
u64 nat_t
Definition types.h:43
DefMap< const Def * > Def2Def
Definition def.h:75
Vector< const Def * > DefVec
Definition def.h:77
D bitcast(const S &src)
A bitcast from src of type S to D.
Definition util.h:23
Dep
Tracks a dependency to certain Defs transitively through the Def::deps() up to but excliding mutables...
Definition def.h:123
@ None
Definition def.h:124
u64 flags_t
Definition types.h:45
u8 node_t
Definition types.h:44
Span< const T, N > View
Definition span.h:98
absl::flat_hash_map< K, V, GIDHash< K > > GIDMap
Definition util.h:195
GIDSet< const Var * > VarSet
Definition def.h:95
GIDMap< const Var *, To > VarMap
Definition def.h:94
Sets< Def >::Set Muts
Definition def.h:87
u64 level_t
Definition types.h:42
GIDMap< const Def *, To > DefMap
Definition def.h:73
GIDSet< Def * > MutSet
Definition def.h:85
MutMap< Def * > Mut2Mut
Definition def.h:86
GIDSet< const Def * > DefSet
Definition def.h:74
static constexpr size_t Num_Nodes
Definition def.h:119
const Def *(*)(const Def *, const Def *, const Def *) NormalizeFn
Definition def.h:100
Sets< const Var >::Set Vars
Definition def.h:97
uint32_t u32
Definition types.h:34
Mut
Judgement.
Definition def.h:143
@ Imm
Node may be immmutable.
Definition def.h:146
uint64_t u64
Definition types.h:34
Judge
Judgement.
Definition def.h:132
@ Intro
Term Introduction like λ(x: Nat): Nat = x.
Definition def.h:135
@ Meta
Meta rules for Universe and Type levels.
Definition def.h:137
@ Form
Type Formation like T -> T.
Definition def.h:134
@ Elim
Term Elimination like f a.
Definition def.h:136
absl::flat_hash_set< K, GIDHash< K > > GIDSet
Definition util.h:196
uint8_t u8
Definition types.h:34
Node
Definition def.h:112
@ Nat
Definition def.h:114
@ Univ
Definition def.h:114
CODE(node, _)
Definition def.h:113
@ Idx
Definition def.h:114
@ UInc
Definition def.h:114
@ Global
Definition def.h:114
@ Var
Definition def.h:114
@ Axm
Definition def.h:114
@ Type
Definition def.h:114
@ App
Definition def.h:114
@ Lit
Definition def.h:114
@ Proxy
Definition def.h:114
@ UMax
Definition def.h:114
Vector(I, I, A=A()) -> Vector< typename std::iterator_traits< I >::value_type, Default_Inlined_Size< typename std::iterator_traits< I >::value_type >, A >
GIDMap< Def *, To > MutMap
Definition def.h:84
VarMap< const Var * > Var2Var
Definition def.h:96
Definition span.h:122