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