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 { return type_; }
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
441 /// @name Free Vars and Muts
442 /// * local_muts() / local_vars() are cached and hash-consed.
443 /// * free_vars() are computed on demand and cached in mutables.
444 /// They will be transitively invalidated by following users(), if a mutable is mutated.
445 ///@{
446
447 /// Mutables reachable by following *immutable* deps(); `mut->local_muts()` is by definition the set `{ mut }`.
448 Muts local_muts() const;
449
450 /// Var%s reachable by following *immutable* deps().
451 /// @note `var->local_vars()` is by definition the set `{ var }`.
452 Vars local_vars() const;
453
454 /// Compute a global solution by transitively following *mutables* as well.
455 Vars free_vars() const;
456 Vars free_vars();
457 Muts users() { return muts_; } ///< Set of mutables where this mutable is locally referenced.
458 bool is_open() const; ///< Has free_vars()?
459 bool is_closed() const; ///< Has no free_vars()?
460 ///@}
461
462 /// @name external
463 ///@{
464 bool is_external() const noexcept { return external_; }
465 void make_external();
466 void make_internal();
467 void transfer_external(Def* to);
468 ///@}
469
470 /// @name Casts
471 /// @see @ref cast_builtin
472 ///@{
473 bool is_mutable() const noexcept { return mut_; }
474
475 // clang-format off
476 template<class T = Def> const T* isa_imm() const { return isa_mut<T, true>(); }
477 template<class T = Def> const T* as_imm() const { return as_mut<T, true>(); }
478 // clang-format on
479
480 /// If `this` is *mutable*, it will cast `const`ness away and perform a `dynamic_cast` to @p T.
481 template<class T = Def, bool invert = false>
482 T* isa_mut() const {
483 if constexpr (std::is_same<T, Def>::value)
484 return mut_ ^ invert ? const_cast<Def*>(this) : nullptr;
485 else
486 return mut_ ^ invert ? const_cast<Def*>(this)->template isa<T>() : nullptr;
487 }
488
489 /// Asserts that `this` is a *mutable*, casts `const`ness away and performs a `static_cast` to @p T.
490 template<class T = Def, bool invert = false>
491 T* as_mut() const {
492 assert(mut_ ^ invert);
493 if constexpr (std::is_same<T, Def>::value)
494 return const_cast<Def*>(this);
495 else
496 return const_cast<Def*>(this)->template as<T>();
497 }
498 ///@}
499
500 /// @name Dbg Getters
501 ///@{
502 Dbg dbg() const { return dbg_; }
503 Loc loc() const { return dbg_.loc(); }
504 Sym sym() const { return dbg_.sym(); }
505 std::string unique_name() const; ///< name + "_" + Def::gid
506 ///@}
507
508 /// @name Dbg Setters
509 /// Every subclass `S` of Def has the same setters that return `S*`/`const S*` via the mixin Setters.
510 ///@{
511 // clang-format off
512 template<bool Ow = false> const Def* set(Loc l) const { if (Ow || !dbg_.loc()) dbg_.set(l); return this; }
513 template<bool Ow = false> Def* set(Loc l) { if (Ow || !dbg_.loc()) dbg_.set(l); return this; }
514 template<bool Ow = false> const Def* set(Sym s) const { if (Ow || !dbg_.sym()) dbg_.set(s); return this; }
515 template<bool Ow = false> Def* set(Sym s) { if (Ow || !dbg_.sym()) dbg_.set(s); return this; }
516 template<bool Ow = false> const Def* set( std::string s) const { set<Ow>(sym(std::move(s))); return this; }
517 template<bool Ow = false> Def* set( std::string s) { set<Ow>(sym(std::move(s))); return this; }
518 template<bool Ow = false> const Def* set(Loc l, Sym s ) const { set<Ow>(l); set<Ow>(s); return this; }
519 template<bool Ow = false> Def* set(Loc l, Sym s ) { set<Ow>(l); set<Ow>(s); return this; }
520 template<bool Ow = false> const Def* set(Loc l, std::string s) const { set<Ow>(l); set<Ow>(sym(std::move(s))); return this; }
521 template<bool Ow = false> Def* set(Loc l, std::string s) { set<Ow>(l); set<Ow>(sym(std::move(s))); return this; }
522 template<bool Ow = false> const Def* set(Dbg d) const { set<Ow>(d.loc(), d.sym()); return this; }
523 template<bool Ow = false> Def* set(Dbg d) { set<Ow>(d.loc(), d.sym()); return this; }
524 // clang-format on
525 ///@}
526
527 /// @name debug_prefix/suffix
528 /// Prepends/Appends a prefix/suffix to Def::name - but only in `Debug` build.
529 ///@{
530#ifndef NDEBUG
531 const Def* debug_prefix(std::string) const;
532 const Def* debug_suffix(std::string) const;
533#else
534 const Def* debug_prefix(std::string) const { return this; }
535 const Def* debug_suffix(std::string) const { return this; }
536#endif
537 ///@}
538
539 /// @name Rebuild
540 ///@{
541 Def* stub(World& w, const Def* type) { return stub_(w, type)->set(dbg()); }
542 Def* stub(const Def* type) { return stub(world(), type); }
543
544 /// Def::rebuild%s this Def while using @p new_op as substitute for its @p i'th Def::op
545 const Def* rebuild(World& w, const Def* type, Defs ops) const {
546 assert(isa_imm());
547 return rebuild_(w, type, ops)->set(dbg());
548 }
549 const Def* rebuild(const Def* type, Defs ops) const { return rebuild(world(), type, ops); }
550
551 /// Tries to make an immutable from a mutable.
552 /// This usually works if the mutable isn't recursive and its var isn't used.
553 virtual const Def* immutabilize() { return nullptr; }
554 bool is_immutabilizable();
555
556 const Def* refine(size_t i, const Def* new_op) const;
557
558 /// @see World::reduce
559 template<size_t N = std::dynamic_extent>
560 constexpr auto reduce(const Def* arg) const {
561 return reduce_(arg).span<N>();
562 }
563
564 /// First Def::op that needs to be dealt with during reduction; e.g. for a Pi we don't reduce the Pi::dom.
565 /// @see World::reduce
566 virtual constexpr size_t reduction_offset() const noexcept { return size_t(-1); }
567 ///@}
568
569 /// @name Type Checking
570 ///@{
571
572 /// Checks whether the `i`th operand can be set to `def`.
573 /// The method returns a possibly updated version of `def` (e.g. where Hole%s have been resolved).
574 /// This is the actual `def` that will be set as the `i`th operand.
575 virtual const Def* check([[maybe_unused]] size_t i, const Def* def) { return def; }
576
577 /// After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
578 /// The method returns a possibly updated version of its type (e.g. where Hole%s have been resolved).
579 /// If different from Def::type, it will update its Def::type to a Def::zonk%ed version of that.
580 virtual const Def* check() { return type(); }
581
582 /// If Hole%s have been filled, reconstruct the program without them.
583 /// Only gues up to but excluding other mutables.
584 /// @see https://stackoverflow.com/questions/31889048/what-does-the-ghc-source-mean-by-zonk
585 const Def* zonk() const;
586
587 /// If *mutable, zonk%s all ops and tries to immutabilize it; otherwise just zonk.
588 const Def* zonk_mut() const;
589 ///@}
590
591 /// zonk%s all @p defs and retuns a new DefVec.
592 static DefVec zonk(Defs defs);
593
594 /// @name dump
595 ///@{
596 void dump() const;
597 void dump(int max) const;
598 void write(int max) const;
599 void write(int max, const char* file) const;
600 std::ostream& stream(std::ostream&, int max) const;
601 ///@}
602
603 /// @name Syntactic Comparison
604 ///
605 enum class Cmp {
606 L, ///< Less
607 G, ///< Greater
608 E, ///< Equal
609 U, ///< Unknown
610 };
611 [[nodiscard]] static Cmp cmp(const Def* a, const Def* b);
612 [[nodiscard]] static bool less(const Def* a, const Def* b);
613 [[nodiscard]] static bool greater(const Def* a, const Def* b);
614
615 /// @name dot
616 /// Dumps DOT to @p os while obeying maximum recursion depth of @p max.
617 /// If @p types is `true`, Def::type() dependencies will be followed as well.
618 ///@{
619 void dot(std::ostream& os, uint32_t max = 0xFFFFFF, bool types = false) const;
620 /// Same as above but write to @p file or `std::cout` if @p file is `nullptr`.
621 void dot(const char* file = nullptr, uint32_t max = 0xFFFFFF, bool types = false) const;
622 void dot(const std::string& file, uint32_t max = 0xFFFFFF, bool types = false) const {
623 return dot(file.c_str(), max, types);
624 }
625 ///@}
626
627protected:
628 /// @name Wrappers for World::sym
629 /// These are here to have Def::set%ters inline without including `mim/world.h`.
630 ///@{
631 Sym sym(const char*) const;
632 Sym sym(std::string_view) const;
633 Sym sym(std::string) const;
634 ///@}
635
636private:
637 Defs reduce_(const Def* arg) const;
638 virtual Def* stub_(World&, const Def*) { fe::unreachable(); }
639 virtual const Def* rebuild_(World& w, const Def* type, Defs ops) const = 0;
640
641 template<bool init>
642 Vars free_vars(bool&, uint32_t);
643 void invalidate();
644 const Def** ops_ptr() const {
645 return reinterpret_cast<const Def**>(reinterpret_cast<char*>(const_cast<Def*>(this + 1)));
646 }
647 bool equal(const Def* other) const;
648
649 template<Cmp>
650 [[nodiscard]] static bool cmp_(const Def* a, const Def* b);
651
652protected:
653 mutable Dbg dbg_;
654 union {
655 NormalizeFn normalizer_; ///< Axm only: Axm%s use this member to store their normalizer.
656 const Axm* axm_; ///< App only: Curried App%s of Axm%s use this member to propagate the Axm.
657 const Var* var_; ///< Mutable only: Var of a mutable.
658 mutable World* world_;
659 };
663
664private:
665 Node node_;
666 bool mut_ : 1;
667 bool external_ : 1;
668 unsigned dep_ : 6;
669 u32 mark_ = 0;
670#ifndef NDEBUG
671 size_t curr_op_ = 0;
672#endif
673 u32 gid_;
674 u32 num_ops_;
675 size_t hash_;
676 Vars vars_; // Mutable: local vars; Immutable: free vars.
677 Muts muts_; // Immutable: local_muts; Mutable: users;
678 mutable u32 tid_ = 0;
679 const Def* type_;
680
681 template<class D, size_t N>
682 friend class Sets;
683 friend class World;
684 friend void swap(World&, World&) noexcept;
685 friend std::ostream& operator<<(std::ostream&, const Def*);
686};
687
688class Var : public Def, public Setters<Var> {
689private:
690 Var(const Def* type, Def* mut)
691 : Def(Node, type, Defs{mut}, 0) {}
692
693public:
694 using Setters<Var>::set;
695
696 /// @name ops
697 ///@{
698 Def* mut() const { return op(0)->as_mut(); }
699 ///@}
700
701 static constexpr auto Node = mim::Node::Var;
702 static constexpr size_t Num_Ops = 1;
703
704private:
705 const Def* rebuild_(World&, const Def*, Defs) const final;
706
707 friend class World;
708};
709
710class Univ : public Def, public Setters<Univ> {
711public:
712 using Setters<Univ>::set;
713 static constexpr auto Node = mim::Node::Univ;
714 static constexpr size_t Num_Ops = 0;
715
716private:
718 : Def(&world, Node, nullptr, Defs{}, 0) {}
719
720 const Def* rebuild_(World&, const Def*, Defs) const final;
721
722 friend class World;
723};
724
725class UMax : public Def, public Setters<UMax> {
726public:
727 using Setters<UMax>::set;
728 static constexpr auto Node = mim::Node::UMax;
729 static constexpr size_t Num_Ops = std::dynamic_extent;
730
731 enum Sort { Univ, Kind, Type, Term };
732
733private:
734 UMax(World&, Defs ops);
735
736 const Def* rebuild_(World&, const Def*, Defs) const final;
737
738 friend class World;
739};
740
741class UInc : public Def, public Setters<UInc> {
742private:
743 UInc(const Def* op, level_t offset)
744 : Def(Node, op->type()->as<Univ>(), {op}, offset) {}
745
746public:
747 using Setters<UInc>::set;
748
749 /// @name ops
750 ///@{
751 const Def* op() const { return Def::op(0); }
752 level_t offset() const { return flags(); }
753 ///@}
754
755 static constexpr auto Node = mim::Node::UInc;
756 static constexpr size_t Num_Ops = 1;
757
758private:
759 const Def* rebuild_(World&, const Def*, Defs) const final;
760
761 friend class World;
762};
763
764class Type : public Def, public Setters<Type> {
765private:
766 Type(const Def* level)
767 : Def(Node, nullptr, {level}, 0) {}
768
769public:
770 using Setters<Type>::set;
771
772 /// @name ops
773 ///@{
774 const Def* level() const { return op(0); }
775 ///@}
776
777 static constexpr auto Node = mim::Node::Type;
778 static constexpr size_t Num_Ops = 1;
779
780private:
781 const Def* rebuild_(World&, const Def*, Defs) const final;
782
783 friend class World;
784};
785
786class Lit : public Def, public Setters<Lit> {
787private:
788 Lit(const Def* type, flags_t val)
789 : Def(Node, type, Defs{}, val) {}
790
791public:
792 using Setters<Lit>::set;
793
794 /// @name Get actual Constant
795 ///@{
796 template<class T = flags_t>
797 T get() const {
798 static_assert(sizeof(T) <= 8);
799 return bitcast<T>(flags_);
800 }
801 ///@}
802
803 using Def::as;
804 using Def::isa;
805
806 /// @name Casts
807 ///@{
808 /// @see @ref cast_lit
809 template<class T = nat_t>
810 static std::optional<T> isa(const Def* def) {
811 if (!def) return {};
812 if (auto lit = def->isa<Lit>()) return lit->get<T>();
813 return {};
814 }
815 template<class T = nat_t>
816 static T as(const Def* def) {
817 return def->as<Lit>()->get<T>();
818 }
819 ///@}
820
821 static constexpr auto Node = mim::Node::Lit;
822 static constexpr size_t Num_Ops = 0;
823
824private:
825 const Def* rebuild_(World&, const Def*, Defs) const final;
826
827 friend class World;
828};
829
830class Nat : public Def, public Setters<Nat> {
831public:
832 using Setters<Nat>::set;
833 static constexpr auto Node = mim::Node::Nat;
834 static constexpr size_t Num_Ops = 0;
835
836private:
837 Nat(World& world);
838
839 const Def* rebuild_(World&, const Def*, Defs) const final;
840
841 friend class World;
842};
843
844/// A built-in constant of type `Nat -> *`.
845class Idx : public Def, public Setters<Idx> {
846private:
847 Idx(const Def* type)
848 : Def(Node, type, Defs{}, 0) {}
849
850public:
851 using Setters<Idx>::set;
852 using Def::as;
853 using Def::isa;
854
855 /// @name isa
856 ///@{
857
858 /// Checks if @p def is a `Idx s` and returns `s` or `nullptr` otherwise.
859 static const Def* isa(const Def* def);
860 static const Def* as(const Def* def) {
861 auto res = isa(def);
862 assert(res);
863 return res;
864 }
865 static std::optional<nat_t> isa_lit(const Def* def);
866 static nat_t as_lit(const Def* def) {
867 auto res = isa_lit(def);
868 assert(res.has_value());
869 return *res;
870 }
871 ///@}
872
873 /// @name Convert between Idx::isa and bitwidth and vice versa
874 ///@{
875 // clang-format off
876 static constexpr nat_t bitwidth2size(nat_t n) { assert(n != 0); return n == 64 ? 0 : (1_n << n); }
877 static constexpr nat_t size2bitwidth(nat_t n) { return n == 0 ? 64 : std::bit_width(n - 1_n); }
878 // clang-format on
879 static std::optional<nat_t> size2bitwidth(const Def* size);
880 ///@}
881
882 static constexpr auto Node = mim::Node::Idx;
883 static constexpr size_t Num_Ops = 0;
884
885private:
886 const Def* rebuild_(World&, const Def*, Defs) const final;
887
888 friend class World;
889};
890
891class Proxy : public Def, public Setters<Proxy> {
892private:
893 Proxy(const Def* type, u32 pass, u32 tag, Defs ops)
894 : Def(Node, type, ops, (u64(pass) << 32_u64) | u64(tag)) {}
895
896public:
897 using Setters<Proxy>::set;
898
899 /// @name Getters
900 ///@{
901 u32 pass() const { return u32(flags() >> 32_u64); } ///< IPass::index within PassMan.
902 u32 tag() const { return u32(flags()); }
903 ///@}
904
905 static constexpr auto Node = mim::Node::Proxy;
906 static constexpr size_t Num_Ops = std::dynamic_extent;
907
908private:
909 const Def* rebuild_(World&, const Def*, Defs) const final;
910
911 friend class World;
912};
913
914/// @deprecated A global variable in the data segment.
915/// A Global may be mutable or immutable.
916/// @deprecated Will be removed.
917class Global : public Def, public Setters<Global> {
918private:
919 Global(const Def* type, bool is_mutable)
920 : Def(Node, type, 1, is_mutable) {}
921
922public:
923 using Setters<Global>::set;
924
925 /// @name ops
926 ///@{
927 const Def* init() const { return op(0); }
928 void set(const Def* init) { Def::set(0, init); }
929 ///@}
930
931 /// @name type
932 ///@{
933 const App* type() const;
934 const Def* alloced_type() const;
935 ///@}
936
937 /// @name Getters
938 ///@{
939 bool is_mutable() const { return flags(); }
940 ///@}
941
942 /// @name Rebuild
943 ///@{
944 Global* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
945 ///@}
946
947 static constexpr auto Node = mim::Node::Global;
948 static constexpr size_t Num_Ops = 1;
949
950private:
951 const Def* rebuild_(World&, const Def*, Defs) const final;
952 Global* stub_(World&, const Def*) final;
953
954 friend class World;
955};
956
957} // 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:298
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:63
const Def * set(Dbg d) const
Definition def.h:522
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:581
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:266
void dot(std::ostream &os, uint32_t max=0xFFFFFF, bool types=false) const
Definition dot.cpp:126
void make_internal()
Definition def.cpp:564
virtual const Def * check(size_t i, const Def *def)
Checks whether the ith operand can be set to def.
Definition def.h:575
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Definition def.h:491
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:464
auto projs() const
Definition def.h:413
u8 trip_
Definition def.h:662
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:576
virtual ~Def()=default
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
Definition check.cpp:61
bool has_dep(unsigned u) const
Definition def.h:359
World & world() const noexcept
Definition def.cpp:436
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:580
const Def * refine(size_t i, const Def *new_op) const
Definition def.cpp:232
Def * set_type(const Def *)
Update type.
Definition def.cpp:283
void dot(const std::string &file, uint32_t max=0xFFFFFF, bool types=false) const
Definition def.h:622
std::string_view node_name() const
Definition def.cpp:454
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:345
void make_external()
Definition def.cpp:563
constexpr flags_t flags() const noexcept
Definition def.h:269
Dbg dbg_
Definition def.h:653
virtual Def * stub_(World &, const Def *)
Definition def.h:638
const Def * set(std::string s) const
Definition def.h:516
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:482
Vars free_vars()
Definition def.cpp:347
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:661
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:480
const Def * debug_prefix(std::string) const
Definition def.cpp:492
const Def * op(size_t i) const noexcept
Definition def.h:308
bool is_immutabilizable()
Definition def.cpp:177
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:566
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
Definition def.cpp:443
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:423
constexpr size_t hash() const noexcept
Definition def.h:273
friend class World
Definition def.h:683
virtual const Def * immutabilize()
Tries to make an immutable from a mutable.
Definition def.h:553
bool is_form() const noexcept
Definition def.h:283
Def * set(Dbg d)
Definition def.h:523
Muts local_muts() const
Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }...
Definition def.cpp:329
Def * set(Sym s)
Definition def.h:515
const Def * debug_suffix(std::string) const
Definition def.cpp:493
const Def * set(Sym s) const
Definition def.h:514
Def * set(Loc l)
Definition def.h:513
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:295
const Def * dep(size_t i) const noexcept
Definition def.h:343
bool is_mutable() const noexcept
Definition def.h:473
bool is_external() const noexcept
Definition def.h:464
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:545
const Def * set(Loc l, Sym s) const
Definition def.h:518
static bool less(const Def *a, const Def *b)
Definition def.cpp:542
Def * set(std::string s)
Definition def.h:517
bool is_meta() const noexcept
Definition def.h:286
static bool greater(const Def *a, const Def *b)
Definition def.cpp:543
bool has_dep() const
Definition def.h:357
const Def * set(Loc l) const
Definition def.h:512
Loc loc() const
Definition def.h:503
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:521
friend class Sets
Definition def.h:682
const T * as_imm() const
Definition def.h:477
Def * stub(const Def *type)
Definition def.h:542
static Cmp cmp(const Def *a, const Def *b)
Definition def.cpp:500
virtual constexpr size_t reduction_offset() const noexcept
First Def::op that needs to be dealt with during reduction; e.g.
Definition def.h:566
Sym sym() const
Definition def.h:504
nat_t num_projs() const
Yields Def::arity(), if it is a Lit, or 1 otherwise.
Definition def.cpp:574
std::ostream & stream(std::ostream &, int max) const
Definition dump.cpp:432
flags_t flags_
Definition def.h:660
friend void swap(World &, World &) noexcept
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
Definition def.h:270
virtual const Def * arity() const
Definition def.cpp:546
Def * unset()
Unsets all Def::ops; works even, if not set at all or only partially set.
Definition def.cpp:289
std::string unique_name() const
name + "_" + Def::gid
Definition def.cpp:572
constexpr auto reduce(const Def *arg) const
Definition def.h:560
const Def * set(Loc l, std::string s) const
Definition def.h:520
const T * isa_imm() const
Definition def.h:476
Muts users()
Set of mutables where this mutable is locally referenced.
Definition def.h:457
bool is_closed() const
Has no free_vars()?
Definition def.cpp:415
const Def * rebuild(const Def *type, Defs ops) const
Definition def.h:549
Def * set(Loc l, Sym s)
Definition def.h:519
Dbg dbg() const
Definition def.h:502
Def * stub(World &w, const Def *type)
Definition def.h:541
u32 judge() const noexcept
Definition def.cpp:470
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:608
@ U
Unknown.
Definition def.h:609
@ L
Less.
Definition def.h:606
@ G
Greater.
Definition def.h:607
const Def * init() const
Definition def.h:927
void set(const Def *init)
Definition def.h:928
Global * stub(const Def *type)
Definition def.h:944
const Def * alloced_type() const
Definition def.cpp:630
friend class World
Definition def.h:954
bool is_mutable() const
Definition def.h:939
const App * type() const
Definition def.cpp:629
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:111
static constexpr size_t Num_Ops
Definition def.h:948
Global * stub_(World &, const Def *) final
Definition def.cpp:152
static constexpr auto Node
Definition def.h:947
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:112
static constexpr auto Node
Definition def.h:882
static nat_t as_lit(const Def *def)
Definition def.h:866
static constexpr nat_t size2bitwidth(nat_t n)
Definition def.h:877
static constexpr nat_t bitwidth2size(nat_t n)
Definition def.h:876
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Definition def.cpp:605
friend class World
Definition def.h:888
static std::optional< nat_t > isa_lit(const Def *def)
Definition def.cpp:613
static constexpr size_t Num_Ops
Definition def.h:883
static const Def * as(const Def *def)
Definition def.h:860
static constexpr auto Node
Definition def.h:821
static std::optional< T > isa(const Def *def)
Definition def.h:810
friend class World
Definition def.h:827
T get() const
Definition def.h:797
static T as(const Def *def)
Definition def.h:816
static constexpr size_t Num_Ops
Definition def.h:822
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:121
friend class World
Definition def.h:841
static constexpr auto Node
Definition def.h:833
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:113
static constexpr size_t Num_Ops
Definition def.h:834
static constexpr size_t Num_Ops
Definition def.h:906
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:125
friend class World
Definition def.h:911
static constexpr auto Node
Definition def.h:905
u32 pass() const
IPass::index within PassMan.
Definition def.h:901
u32 tag() const
Definition def.h:902
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:783
static constexpr size_t Num_Ops
Definition def.h:778
static constexpr auto Node
Definition def.h:777
const Def * level() const
Definition def.h:774
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:132
const Def * op() const
Definition def.h:751
static constexpr auto Node
Definition def.h:755
friend class World
Definition def.h:761
level_t offset() const
Definition def.h:752
static constexpr size_t Num_Ops
Definition def.h:756
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:133
@ Type
Definition def.h:731
@ Univ
Definition def.h:731
@ Term
Definition def.h:731
@ Kind
Definition def.h:731
static constexpr auto Node
Definition def.h:728
friend class World
Definition def.h:738
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:134
static constexpr size_t Num_Ops
Definition def.h:729
static constexpr size_t Num_Ops
Definition def.h:714
static constexpr auto Node
Definition def.h:713
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:114
friend class World
Definition def.h:722
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:136
static constexpr auto Node
Definition def.h:701
friend class World
Definition def.h:707
static constexpr size_t Num_Ops
Definition def.h:702
Def * mut() const
Definition def.h:698
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:36
#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:187
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:188
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