MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
world.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
4#include <string>
5#include <string_view>
6#include <type_traits>
7
8#include <absl/container/btree_map.h>
9#include <absl/container/btree_set.h>
10#include <fe/arena.h>
11
12#include "mim/axm.h"
13#include "mim/check.h"
14#include "mim/flags.h"
15#include "mim/lam.h"
16#include "mim/lattice.h"
17#include "mim/rule.h"
18#include "mim/tuple.h"
19
20#include "mim/util/dbg.h"
21#include "mim/util/log.h"
22
23namespace mim {
24
25class Driver;
26
27/// The World represents the whole program and manages creation of MimIR nodes (Def%s).
28/// Def%s are hashed into an internal HashSet.
29/// The World's factory methods just calculate a hash and lookup the Def, if it is already present, or create a new one
30/// otherwise. This corresponds to value numbering.
31///
32/// You can create several worlds.
33/// All worlds are completely independent from each other.
34///
35/// Note that types are also just Def%s and will be hashed as well.
36class World {
37public:
38 /// @name State
39 ///@{
40 struct State {
41 State() = default;
42
43 /// [Plain Old Data](https://en.cppreference.com/w/cpp/named_req/PODType)
44 struct POD {
47 Loc loc;
48 Sym name;
49 mutable bool frozen = false;
50 } pod;
51
52#ifdef MIM_ENABLE_CHECKS
53 absl::flat_hash_set<uint32_t> breakpoints;
54 absl::flat_hash_set<uint32_t> watchpoints;
55#endif
56 friend void swap(State& s1, State& s2) noexcept {
57 using std::swap;
58 assert((!s1.pod.loc || !s2.pod.loc) && "Why is get_loc() still set?");
59 swap(s1.pod, s2.pod);
60#ifdef MIM_ENABLE_CHECKS
61 swap(s1.breakpoints, s2.breakpoints);
62 swap(s1.watchpoints, s2.watchpoints);
63#endif
64 }
65 };
66
67 /// @name Construction & Destruction
68 ///@{
69 World& operator=(World) = delete;
70
71 explicit World(Driver*);
72 World(Driver*, const State&);
73 World(World&& other) noexcept
74 : World(&other.driver(), other.state()) {
75 swap(*this, other);
76 }
77 ~World();
78
79 World inherit() { return freeze(), World(&driver(), state()); } ///< Inherits the @p state into the new World.
80 std::unique_ptr<World> inherit_ptr() { return std::make_unique<World>(&driver(), state()); } ///< As above.
81 ///@}
82
83 /// @name Getters/Setters
84 ///@{
85 const State& state() const { return state_; }
86
87 const Driver& driver() const { return *driver_; }
88 Driver& driver() { return *driver_; }
89
90 Sym name() const { return state_.pod.name; }
91 void set(Sym name) { state_.pod.name = name; }
92 void set(std::string_view name) { state_.pod.name = sym(name); }
93
94 /// Manage global identifier - a unique number for each Def.
95 u32 curr_gid() const { return state_.pod.curr_gid; }
96 u32 next_gid() { return ++state_.pod.curr_gid; }
97 u32 next_run() { return ++data_.curr_run; }
98
99 /// Retrieve compile Flags.
100 Flags& flags();
101 ///@}
102
103 /// @name Loc
104 ///@{
105 struct ScopedLoc {
106 ScopedLoc(World& world, Loc old_loc)
107 : world_(world)
108 , old_loc_(old_loc) {}
109 ~ScopedLoc() { world_.set_loc(old_loc_); }
110
111 private:
112 World& world_;
113 Loc old_loc_;
114 };
115
116 Loc get_loc() const { return state_.pod.loc; }
117 void set_loc(Loc loc = {}) { state_.pod.loc = loc; }
118 ScopedLoc push(Loc loc) {
119 auto sl = ScopedLoc(*this, get_loc());
120 set_loc(loc);
121 return sl;
122 }
123 ///@}
124
125 /// @name Sym
126 ///@{
127 Sym sym(std::string_view);
128 Sym sym(const char*);
129 Sym sym(const std::string&);
130 /// Appends a @p suffix or an increasing number if the suffix already exists.
131 Sym append_suffix(Sym name, std::string suffix);
132 ///@}
133
134 /// @name Freeze
135 /// In frozen state the World does not create any nodes.
136 ///@{
137 bool is_frozen() const { return state_.pod.frozen; }
138
139 /// Yields old frozen state.
140 bool freeze(bool on = true) const {
141 bool old = state_.pod.frozen;
142 state_.pod.frozen = on;
143 return old;
144 }
145
146 /// Use to World::freeze and automatically unfreeze at the end of scope.
147 struct Freezer {
149 : world(world)
150 , old(world.freeze(true)) {}
151 ~Freezer() { world.freeze(old); }
152
153 const World& world;
154 bool old;
155 };
156 ///@}
157
158 /// @name Debugging Features
159 ///@{
160#ifdef MIM_ENABLE_CHECKS
161 const auto& breakpoints() { return state_.breakpoints; }
162 const auto& watchpoints() { return state_.watchpoints; }
163
164 const Def* gid2def(u32 gid); ///< Lookup Def by @p gid.
165 void breakpoint(u32 gid); ///< Trigger breakpoint in your debugger when creating a Def with this @p gid.
166 void watchpoint(u32 gid); ///< Trigger breakpoint in your debugger when Def::set%ting a Def with this @p gid.
167
168 World& verify(); ///< Verifies that all externals() and annexes() are Def::is_closed(), if `MIM_ENABLE_CHECKS`.
169#else
170 World& verify() { return *this; }
171#endif
172 ///@}
173
174 /// @name Annexes
175 ///@{
176 const auto& flags2annex() const { return move_.flags2annex; }
177 auto annexes() const { return move_.flags2annex | std::views::values; }
178
179 /// Lookup annex by Axm::id.
180 template<class Id>
181 const Def* annex(Id id) {
182 auto flags = static_cast<flags_t>(id);
183 if (auto i = move_.flags2annex.find(flags); i != move_.flags2annex.end()) return i->second;
184 error("Axm with ID '{x}' not found; demangled plugin name is '{}'", flags, Annex::demangle(driver(), flags));
185 }
186
187 /// Get Axm from a plugin.
188 /// Can be used to get an Axm without sub-tags.
189 /// E.g. use `w.annex<mem::M>();` to get the `%mem.M` Axm.
190 template<annex_without_subs id>
191 const Def* annex() {
192 return annex(Annex::Base<id>);
193 }
194
195 const Def* register_annex(flags_t f, const Def*);
196 const Def* register_annex(plugin_t p, tag_t t, sub_t s, const Def* def) {
197 return register_annex(p | (flags_t(t) << 8_u64) | flags_t(s), def);
198 }
199 ///@}
200
201 /// @name Externals
202 ///@{
203 const auto& sym2external() const { return move_.sym2external; }
204 Def* external(Sym name) { return mim::lookup(move_.sym2external, name); } ///< Lookup by @p name.
205 auto externals() const { return move_.sym2external | std::views::values; }
206 Vector<Def*> copy_externals() const { return {externals().begin(), externals().end()}; }
207 void make_external(Def*);
208 void make_internal(Def*);
209 ///@}
210
211 /// @name Univ, Type, Var, Proxy, Hole
212 ///@{
213 const Univ* univ() { return data_.univ; }
214 const Def* uinc(const Def* op, level_t offset = 1);
215 template<int sort = UMax::Univ>
216 const Def* umax(Defs);
217 const Type* type(const Def* level);
218 const Type* type_infer_univ() { return type(mut_hole_univ()); }
219 template<level_t level = 0>
220 const Type* type() {
221 if constexpr (level == 0)
222 return data_.type_0;
223 else if constexpr (level == 1)
224 return data_.type_1;
225 else
226 return type(lit_univ(level));
227 }
228 const Def* var(const Def* type, Def* mut);
229 const Proxy* proxy(const Def* type, Defs ops, u32 index, u32 tag) { return unify<Proxy>(type, index, tag, ops); }
230
231 Hole* mut_hole(const Def* type) { return insert<Hole>(type); }
232 Hole* mut_hole_univ() { return mut_hole(univ()); }
234
235 /// Either a value `?:?:Type ?` or a type `?:Type ?:Type ?`.
237 auto t = type_infer_univ();
238 auto res = mut_hole(mut_hole(t));
239 assert(this == &res->world());
240 return res;
241 }
242 ///@}
243
244 /// @name Axm
245 ///@{
246 const Axm* axm(NormalizeFn n, u8 curry, u8 trip, const Def* type, plugin_t p, tag_t t, sub_t s) {
247 return unify<Axm>(n, curry, trip, type, p, t, s);
248 }
249 const Axm* axm(const Def* type, plugin_t p, tag_t t, sub_t s) { return axm(nullptr, 0, 0, type, p, t, s); }
250
251 /// Builds a fresh Axm with descending Axm::sub.
252 /// This is useful during testing to come up with some entity of a specific type.
253 /// It uses the plugin Axm::Global_Plugin and starts with `0` for Axm::sub and counts up from there.
254 /// The Axm::tag is set to `0` and the Axm::normalizer to `nullptr`.
255 const Axm* axm(NormalizeFn n, u8 curry, u8 trip, const Def* type) {
256 return axm(n, curry, trip, type, Annex::Global_Plugin, 0, state_.pod.curr_sub++);
257 }
258 const Axm* axm(const Def* type) { return axm(nullptr, 0, 0, type); } ///< See above.
259 ///@}
260
261 /// @name Pi
262 ///@{
263 // clang-format off
264 const Pi* pi(const Def* dom, const Def* codom, bool implicit = false) { return unify<Pi>(Pi::infer(dom, codom), dom, codom, implicit); }
265 const Pi* pi(Defs dom, const Def* codom, bool implicit = false) { return pi(sigma(dom), codom, implicit); }
266 const Pi* pi(const Def* dom, Defs codom, bool implicit = false) { return pi(dom, sigma(codom), implicit); }
267 const Pi* pi(Defs dom, Defs codom, bool implicit = false) { return pi(sigma(dom), sigma(codom), implicit); }
268 Pi* mut_pi(const Def* type, bool implicit = false) { return insert<Pi>(type, implicit); }
269 // clang-format on
270 ///@}
271
272 /// @name Cn
273 /// Pi with codom mim::Bot%tom
274 ///@{
275 // clang-format off
276 const Pi* cn( ) { return cn(sigma( ), false); }
277 const Pi* cn(const Def* dom, bool implicit = false) { return pi( dom , type_bot(), implicit); }
278 const Pi* cn(Defs dom, bool implicit = false) { return cn(sigma(dom), implicit); }
279 const Pi* fn(const Def* dom, const Def* codom, bool implicit = false) { return cn({ dom , cn(codom)}, implicit); }
280 const Pi* fn(Defs dom, const Def* codom, bool implicit = false) { return fn(sigma(dom), codom, implicit); }
281 const Pi* fn(const Def* dom, Defs codom, bool implicit = false) { return fn( dom , sigma(codom), implicit); }
282 const Pi* fn(Defs dom, Defs codom, bool implicit = false) { return fn(sigma(dom), sigma(codom), implicit); }
283 // clang-format on
284 ///@}
285
286 /// @name Lam
287 ///@{
289 if (auto b = std::get_if<bool>(&filter)) return lit_bool(*b);
290 return std::get<const Def*>(filter);
291 }
292 const Lam* lam(const Pi* pi, Lam::Filter f, const Def* body) { return unify<Lam>(pi, filter(f), body); }
293 Lam* mut_lam(const Pi* pi) { return insert<Lam>(pi); }
294 // clang-format off
295 const Lam* con(const Def* dom, Lam::Filter f, const Def* body) { return unify<Lam>(cn(dom ), filter(f), body); }
296 const Lam* con(Defs dom, Lam::Filter f, const Def* body) { return unify<Lam>(cn(dom ), filter(f), body); }
297 const Lam* lam(const Def* dom, const Def* codom, Lam::Filter f, const Def* body) { return unify<Lam>(pi(dom, codom), filter(f), body); }
298 const Lam* lam(Defs dom, const Def* codom, Lam::Filter f, const Def* body) { return unify<Lam>(pi(dom, codom), filter(f), body); }
299 const Lam* lam(const Def* dom, Defs codom, Lam::Filter f, const Def* body) { return unify<Lam>(pi(dom, codom), filter(f), body); }
300 const Lam* lam(Defs dom, Defs codom, Lam::Filter f, const Def* body) { return unify<Lam>(pi(dom, codom), filter(f), body); }
301 const Lam* fun(const Def* dom, const Def* codom, Lam::Filter f, const Def* body) { return unify<Lam>(fn(dom, codom), filter(f), body); }
302 const Lam* fun(Defs dom, const Def* codom, Lam::Filter f, const Def* body) { return unify<Lam>(fn(dom, codom), filter(f), body); }
303 const Lam* fun(const Def* dom, Defs codom, Lam::Filter f, const Def* body) { return unify<Lam>(fn(dom, codom), filter(f), body); }
304 const Lam* fun(Defs dom, Defs codom, Lam::Filter f, const Def* body) { return unify<Lam>(fn(dom, codom), filter(f), body); }
305 Lam* mut_con(const Def* dom ) { return insert<Lam>(cn(dom )); }
306 Lam* mut_con(Defs dom ) { return insert<Lam>(cn(dom )); }
307 Lam* mut_lam(const Def* dom, const Def* codom) { return insert<Lam>(pi(dom, codom)); }
308 Lam* mut_lam(Defs dom, const Def* codom) { return insert<Lam>(pi(dom, codom)); }
309 Lam* mut_lam(const Def* dom, Defs codom) { return insert<Lam>(pi(dom, codom)); }
310 Lam* mut_lam(Defs dom, Defs codom) { return insert<Lam>(pi(dom, codom)); }
311 Lam* mut_fun(const Def* dom, const Def* codom) { return insert<Lam>(fn(dom, codom)); }
312 Lam* mut_fun(Defs dom, const Def* codom) { return insert<Lam>(fn(dom, codom)); }
313 Lam* mut_fun(const Def* dom, Defs codom) { return insert<Lam>(fn(dom, codom)); }
314 Lam* mut_fun(Defs dom, Defs codom) { return insert<Lam>(fn(dom, codom)); }
315 // clang-format on
316 ///@}
317
318 /// @name Rewrite Rules
319 ///@{
320 const Reform* reform(const Def* meta_type) { return unify<Reform>(Reform::infer(meta_type), meta_type); }
321 Rule* mut_rule(const Reform* type) { return insert<Rule>(type); }
322 const Rule* rule(const Reform* type, const Def* lhs, const Def* rhs, const Def* guard) {
323 return mut_rule(type)->set(lhs, rhs, guard);
324 }
325 const Rule* rule(const Def* meta_type, const Def* lhs, const Def* rhs, const Def* guard) {
326 return rule(reform(meta_type), lhs, rhs, guard);
327 }
328 ///@}
329
330 /// @name App
331 ///@{
332 template<bool Normalize = true>
333 const Def* app(const Def* callee, const Def* arg);
334 template<bool Normalize = true>
335 const Def* app(const Def* callee, Defs args) {
336 return app<Normalize>(callee, tuple(args));
337 }
338 const Def* raw_app(const Axm* axm, u8 curry, u8 trip, const Def* type, const Def* callee, const Def* arg);
339 const Def* raw_app(const Def* type, const Def* callee, const Def* arg);
340 const Def* raw_app(const Def* type, const Def* callee, Defs args) { return raw_app(type, callee, tuple(args)); }
341 ///@}
342
343 /// @name Sigma
344 ///@{
345 Sigma* mut_sigma(const Def* type, size_t size) { return insert<Sigma>(type, size); }
346 /// A *mutable* Sigma of type @p level.
347 template<level_t level = 0>
348 Sigma* mut_sigma(size_t size) {
349 return mut_sigma(type<level>(), size);
350 }
351 const Def* sigma(Defs ops);
352 const Sigma* sigma() { return data_.sigma; } ///< The unit type within Type 0.
353 ///@}
354
355 /// @name Arr
356 ///@{
357 // clang-format off
358 const Def* unit(bool term) { return term ? (const Def*)tuple() : sigma(); }
359
360 Seq* mut_seq(bool term, const Def* type) { return term ? (Seq*)insert<Pack>(type) : insert<Arr>(type); }
361 const Def* seq(bool term, const Def* arity, const Def* body);
362 const Def* seq(bool term, Defs shape, const Def* body);
363 const Def* seq(bool term, u64 n, const Def* body) { return seq(term, lit_nat(n), body); }
364 const Def* seq(bool term, View<u64> shape, const Def* body) { return seq(term, DefVec(shape.size(), [&](size_t i) { return lit_nat(shape[i]); }), body); }
365 const Def* seq_unsafe(bool term, const Def* body) { return seq(term, top_nat(), body); }
366
367 template<level_t level = 0>
369 return mut_arr(type<level>());
370 }
371
372 Arr * mut_arr (const Def* type) { return mut_seq(false, type)->as<Arr >(); }
373 Pack* mut_pack(const Def* type) { return mut_seq(true , type)->as<Pack>(); }
374 const Def* arr (const Def* arity, const Def* body) { return seq(false, arity, body); }
375 const Def* pack(const Def* arity, const Def* body) { return seq(true , arity, body); }
376 const Def* arr (Defs shape, const Def* body) { return seq(false, shape, body); }
377 const Def* pack(Defs shape, const Def* body) { return seq(true , shape, body); }
378 const Def* arr (u64 n, const Def* body) { return seq(false, n, body); }
379 const Def* pack(u64 n, const Def* body) { return seq(true , n, body); }
380 const Def* arr (View<u64> shape, const Def* body) { return seq(false, shape, body); }
381 const Def* pack(View<u64> shape, const Def* body) { return seq(true , shape, body); }
382 const Def* arr_unsafe( const Def* body) { return seq_unsafe(false, body); }
383 const Def* pack_unsafe( const Def* body) { return seq_unsafe(true , body); }
384
385 const Def* prod(bool term, Defs ops) { return term ? tuple(ops) : sigma(ops); }
386 const Def* prod(bool term) { return term ? (const Def*)tuple() : (const Def*)sigma(); }
387 // clang-format on
388 ///@}
389
390 /// @name Tuple
391 ///@{
392 const Def* tuple(Defs ops);
393 /// Ascribes @p type to this tuple - needed for dependently typed and mutable Sigma%s.
394 const Def* tuple(const Def* type, Defs ops);
395 const Tuple* tuple() { return data_.tuple; } ///< the unit value of type `[]`
396 const Def* tuple(Sym sym); ///< Converts @p sym to a tuple of type '«n; I8»'.
397 ///@}
398
399 /// @name Extract
400 /// @see core::extract_unsafe
401 ///@{
402 const Def* extract(const Def* d, const Def* i);
403 const Def* extract(const Def* d, u64 a, u64 i) { return extract(d, lit_idx(a, i)); }
404 const Def* extract(const Def* d, u64 i) { return extract(d, Lit::as(d->arity()), i); }
405
406 /// Builds `(f, t)#cond`.
407 /// @note Expects @p cond as first, @p t as second, and @p f as third argument.
408 const Def* select(const Def* cond, const Def* t, const Def* f) { return extract(tuple({f, t}), cond); }
409 ///@}
410
411 /// @name Insert
412 /// @see core::insert_unsafe
413 ///@{
414 const Def* insert(const Def* d, const Def* i, const Def* val);
415 const Def* insert(const Def* d, u64 a, u64 i, const Def* val) { return insert(d, lit_idx(a, i), val); }
416 const Def* insert(const Def* d, u64 i, const Def* val) { return insert(d, Lit::as(d->arity()), i, val); }
417 ///@}
418
419 /// @name Lit
420 ///@{
421 const Lit* lit(const Def* type, u64 val);
422 const Lit* lit_univ(u64 level) { return lit(univ(), level); }
423 const Lit* lit_univ_0() { return data_.lit_univ_0; }
424 const Lit* lit_univ_1() { return data_.lit_univ_1; }
425 const Lit* lit_nat(nat_t a) { return lit(type_nat(), a); }
426 const Lit* lit_nat_0() { return data_.lit_nat_0; }
427 const Lit* lit_nat_1() { return data_.lit_nat_1; }
428 const Lit* lit_nat_max() { return data_.lit_nat_max; }
429 const Lit* lit_idx_1_0() { return data_.lit_idx_1_0; }
430 // clang-format off
431 const Lit* lit_i1() { return lit_nat(Idx::bitwidth2size( 1)); };
432 const Lit* lit_i8() { return lit_nat(Idx::bitwidth2size( 8)); };
433 const Lit* lit_i16() { return lit_nat(Idx::bitwidth2size(16)); };
434 const Lit* lit_i32() { return lit_nat(Idx::bitwidth2size(32)); };
435 const Lit* lit_i64() { return lit_nat(Idx::bitwidth2size(64)); };
436 /// Constructs a Lit of type Idx of size @p size.
437 /// @note `size = 0` means `2^64`.
438 const Lit* lit_idx(nat_t size, u64 val) { return lit(type_idx(size), val); }
439 const Lit* lit_idx_unsafe(u64 val) { return lit(type_idx(top(type_nat())), val); }
440
441 template<class I> const Lit* lit_idx(I val) {
442 static_assert(std::is_integral<I>());
443 return lit_idx(Idx::bitwidth2size(sizeof(I) * 8), val);
444 }
445
446 /// Constructs a Lit @p of type Idx of size 2^width.
447 /// `val = 64` will be automatically converted to size `0` - the encoding for 2^64.
448 const Lit* lit_int(nat_t width, u64 val) { return lit_idx(Idx::bitwidth2size(width), val); }
449 const Lit* lit_i1 (bool val) { return lit_int( 1, u64(val)); }
450 const Lit* lit_i2 (u8 val) { return lit_int( 2, u64(val)); }
451 const Lit* lit_i4 (u8 val) { return lit_int( 4, u64(val)); }
452 const Lit* lit_i8 (u8 val) { return lit_int( 8, u64(val)); }
453 const Lit* lit_i16(u16 val) { return lit_int(16, u64(val)); }
454 const Lit* lit_i32(u32 val) { return lit_int(32, u64(val)); }
455 const Lit* lit_i64(u64 val) { return lit_int(64, u64(val)); }
456 // clang-format on
457
458 /// Constructs a Lit of type Idx of size @p mod.
459 /// The value @p val will be adjusted modulo @p mod.
460 /// @note `mod == 0` is the special case for 2^64 and no modulo will be performed on @p val.
461 const Lit* lit_idx_mod(nat_t mod, u64 val) { return lit_idx(mod, mod == 0 ? val : (val % mod)); }
462
463 const Lit* lit_bool(bool val) { return data_.lit_bool[size_t(val)]; }
464 const Lit* lit_ff() { return data_.lit_bool[0]; }
465 const Lit* lit_tt() { return data_.lit_bool[1]; }
466 ///@}
467
468 /// @name Lattice
469 ///@{
470 template<bool Up>
471 const Def* ext(const Def* type);
472 const Def* bot(const Def* type) { return ext<false>(type); }
473 const Def* top(const Def* type) { return ext<true>(type); }
474 const Def* type_bot() { return data_.type_bot; }
475 const Def* type_top() { return data_.type_top; }
476 const Def* top_nat() { return data_.top_nat; }
477 template<bool Up>
478 const Def* bound(Defs ops);
479 const Def* join(Defs ops) { return bound<true>(ops); }
480 const Def* meet(Defs ops) { return bound<false>(ops); }
481 const Def* merge(const Def* type, Defs ops);
482 const Def* merge(Defs ops); ///< Infers the type using a Meet.
483 const Def* inj(const Def* type, const Def* value);
484 const Def* split(const Def* type, const Def* value);
485 const Def* match(Defs);
486 const Def* uniq(const Def* inhabitant);
487 ///@}
488
489 /// @name Globals
490 /// @deprecated Will be removed.
491 ///@{
492 Global* global(const Def* type, bool is_mutable = true) { return insert<Global>(type, is_mutable); }
493 ///@}
494
495 /// @name Types
496 ///@{
497 const Nat* type_nat() { return data_.type_nat; }
498 const Idx* type_idx() { return data_.type_idx; }
499 /// @note `size = 0` means `2^64`.
500 const Def* type_idx(const Def* size) { return app(type_idx(), size); }
501 /// @note `size = 0` means `2^64`.
502 const Def* type_idx(nat_t size) { return type_idx(lit_nat(size)); }
503
504 /// Constructs a type Idx of size 2^width.
505 /// `width = 64` will be automatically converted to size `0` - the encoding for 2^64.
506 const Def* type_int(nat_t width) { return type_idx(lit_nat(Idx::bitwidth2size(width))); }
507 // clang-format off
508 const Def* type_bool() { return data_.type_bool; }
509 const Def* type_i1() { return data_.type_bool; }
510 const Def* type_i2() { return type_int( 2); };
511 const Def* type_i4() { return type_int( 4); };
512 const Def* type_i8() { return type_int( 8); };
513 const Def* type_i16() { return type_int(16); };
514 const Def* type_i32() { return type_int(32); };
515 const Def* type_i64() { return type_int(64); };
516 // clang-format on
517 ///@}
518
519 /// @name Cope with implicit Arguments
520 ///@{
521
522 /// Places Hole%s as demanded by Pi::is_implicit() and then apps @p arg.
523 template<bool Normalize = true>
524 const Def* implicit_app(const Def* callee, const Def* arg);
525 template<bool Normalize = true>
526 const Def* implicit_app(const Def* callee, Defs args) {
527 return implicit_app<Normalize>(callee, tuple(args));
528 }
529 template<bool Normalize = true>
530 const Def* implicit_app(const Def* callee, nat_t arg) {
531 return implicit_app<Normalize>(callee, lit_nat(arg));
532 }
533 template<bool Normalize = true, class E>
534 const Def* implicit_app(const Def* callee, E arg)
535 requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>
536 {
537 return implicit_app<Normalize>(callee, lit_nat((nat_t)arg));
538 }
539
540 /// Complete curried call of annexes obeying implicits.
541 // clang-format off
542 template<class Id, bool Normalize = true, class... Args> const Def* call(Id id, Args&&... args) { return call_<Normalize>(annex(id), std::forward<Args>(args)...); }
543 template<class Id, bool Normalize = true, class... Args> const Def* call( Args&&... args) { return call_<Normalize>(annex<Id>(), std::forward<Args>(args)...); }
544 // clang-format on
545 ///@}
546
547 /// @name Vars & Muts
548 /// Manges sets of Vars and Muts.
549 ///@{
550 [[nodiscard]] auto& vars() { return move_.vars; }
551 [[nodiscard]] auto& muts() { return move_.muts; }
552 [[nodiscard]] const auto& vars() const { return move_.vars; }
553 [[nodiscard]] const auto& muts() const { return move_.muts; }
554
555 /// Yields the new body of `[mut->var() -> arg]mut`.
556 /// The new body may have fewer elements as `mut->num_ops()` according to Def::reduction_offset.
557 /// E.g. a Pi has a Pi::reduction_offset of 1, and only Pi::dom will be reduced - *not* Pi::codom.
558 Defs reduce(const Var* var, const Def* arg);
559 ///@}
560
561 /// @name dump/log
562 ///@{
563 Log& log();
564 void dummy() {}
565 void dump(std::ostream& os); ///< Dump to @p os.
566 void dump(); ///< Dump to `std::cout`.
567 void debug_dump(); ///< Dump in Debug build if World::log::level is Log::Level::Debug.
568 void write(const char* file); ///< Write to a file named @p file.
569 void write(); ///< Same above but file name defaults to World::name.
570 ///@}
571
572 /// @name dot
573 /// GraphViz output.
574 ///@{
575
576 /// Dumps DOT to @p os.
577 /// @param os Output stream
578 /// @param annexes If `true`, include all annexes - even if unused.
579 /// @param types Follow type dependencies?
580 void dot(std::ostream& os, bool annexes = false, bool types = false) const;
581 /// Same as above but write to @p file or `std::cout` if @p file is `nullptr`.
582 void dot(const char* file = nullptr, bool annexes = false, bool types = false) const;
583 ///@}
584
585private:
586 /// @name call_
587 /// Helpers to unwind World::call with variadic templates.
588 ///@{
589 template<bool Normalize = true, class T, class... Args>
590 const Def* call_(const Def* callee, T arg, Args&&... args) {
591 return call_<Normalize>(implicit_app(callee, arg), std::forward<Args>(args)...);
592 }
593 template<bool Normalize = true, class T>
594 const Def* call_(const Def* callee, T arg) {
595 return implicit_app<Normalize>(callee, arg);
596 }
597 ///@}
598
599 /// @name Put into Sea of Nodes
600 ///@{
601 template<class T, class... Args>
602 const T* unify(Args&&... args) {
603 auto num_ops = T::Num_Ops;
604 if constexpr (T::Num_Ops == std::dynamic_extent) {
605 auto&& last = std::get<sizeof...(Args) - 1>(std::forward_as_tuple(std::forward<Args>(args)...));
606 num_ops = last.size();
607 }
608
609 auto state = move_.arena.defs.state();
610 auto def = allocate<T>(num_ops, std::forward<Args&&>(args)...);
611 if (auto loc = get_loc()) def->set(loc);
612 assert(!def->isa_mut());
613#ifdef MIM_ENABLE_CHECKS
614 if (flags().trace_gids) outln("{}: {} - {}", def->node_name(), def->gid(), def->flags());
615 if (flags().reeval_breakpoints && breakpoints().contains(def->gid())) fe::breakpoint();
616#endif
617 if (is_frozen()) {
618 auto i = move_.defs.find(def);
619 deallocate<T>(state, def);
620 if (i != move_.defs.end()) return static_cast<const T*>(*i);
621 return nullptr;
622 }
623
624 if (auto [i, ins] = move_.defs.emplace(def); !ins) {
625 deallocate<T>(state, def);
626 return static_cast<const T*>(*i);
627 }
628#ifdef MIM_ENABLE_CHECKS
629 if (!flags().reeval_breakpoints && breakpoints().contains(def->gid())) fe::breakpoint();
630#endif
631 return def;
632 }
633
634 template<class T>
635 void deallocate(fe::Arena::State state, const T* ptr) {
636 --state_.pod.curr_gid;
637 ptr->~T();
638 move_.arena.defs.deallocate(state);
639 }
640
641 template<class T, class... Args>
642 T* insert(Args&&... args) {
643 auto num_ops = T::Num_Ops;
644 if constexpr (T::Num_Ops == std::dynamic_extent)
645 num_ops = std::get<sizeof...(Args) - 1>(std::forward_as_tuple(std::forward<Args>(args)...));
646
647 auto def = allocate<T>(num_ops, std::forward<Args>(args)...);
648 if (auto loc = get_loc()) def->set(loc);
649#ifdef MIM_ENABLE_CHECKS
650 if (flags().trace_gids) outln("{}: {} - {}", def->node_name(), def->gid(), def->flags());
651 if (breakpoints().contains(def->gid())) fe::breakpoint();
652#endif
653 assert_emplace(move_.defs, def);
654 return def;
655 }
656
657#if (!defined(_MSC_VER) && defined(NDEBUG))
658 struct Lock {
659 Lock() { assert((guard_ = !guard_) && "you are not allowed to recursively invoke allocate"); }
660 ~Lock() { guard_ = !guard_; }
661 static bool guard_;
662 };
663#else
664 struct Lock {
665 ~Lock() {}
666 };
667#endif
668
669 template<class T, class... Args>
670 T* allocate(size_t num_ops, Args&&... args) {
671 static_assert(sizeof(Def) == sizeof(T),
672 "you are not allowed to introduce any additional data in subclasses of Def");
673 auto lock = Lock();
674 auto num_bytes = sizeof(Def) + sizeof(uintptr_t) * num_ops;
675 auto ptr = move_.arena.defs.allocate(num_bytes, alignof(T));
676 auto res = new (ptr) T(std::forward<Args>(args)...);
677 assert(res->num_ops() == num_ops);
678 return res;
679 }
680 ///@}
681
682 Driver* driver_;
683 State state_;
684
685 struct SeaHash {
686 size_t operator()(const Def* def) const { return def->hash(); }
687 };
688
689 struct SeaEq {
690 bool operator()(const Def* d1, const Def* d2) const { return d1->equal(d2); }
691 };
692
693 class Reduct {
694 public:
695 constexpr Reduct(size_t size) noexcept
696 : size_(size) {}
697
698 template<size_t N = std::dynamic_extent>
699 constexpr auto defs() const noexcept {
700 return View<const Def*, N>{defs_, size_};
701 }
702
703 private:
704 size_t size_;
705 const Def* defs_[];
706
707 friend class World;
708 };
709
710 struct Move {
711 struct {
712 fe::Arena defs, substs;
713 } arena;
714
715 absl::btree_map<flags_t, const Def*> flags2annex;
716 absl::btree_map<Sym, Def*> sym2external;
717 absl::flat_hash_set<const Def*, SeaHash, SeaEq> defs;
720 absl::flat_hash_map<std::pair<const Var*, const Def*>, const Reduct*> substs;
721
722 friend void swap(Move& m1, Move& m2) noexcept {
723 using std::swap;
724 // clang-format off
725 swap(m1.arena.defs, m2.arena.defs);
726 swap(m1.arena.substs, m2.arena.substs);
727 swap(m1.defs, m2.defs);
728 swap(m1.substs, m2.substs);
729 swap(m1.vars, m2.vars);
730 swap(m1.muts, m2.muts);
731 swap(m1.flags2annex, m2.flags2annex);
732 swap(m1.sym2external, m2.sym2external);
733 // clang-format on
734 }
735 } move_;
736
737 struct {
738 const Univ* univ;
739 const Type* type_0;
740 const Type* type_1;
741 const Bot* type_bot;
742 const Top* type_top;
743 const Def* type_bool;
744 const Top* top_nat;
745 const Sigma* sigma;
746 const Tuple* tuple;
747 const Nat* type_nat;
748 const Idx* type_idx;
749 const Def* table_id;
750 const Def* table_not;
751 const Lit* lit_univ_0;
752 const Lit* lit_univ_1;
753 const Lit* lit_nat_0;
754 const Lit* lit_nat_1;
755 const Lit* lit_nat_max;
756 const Lit* lit_idx_1_0;
757 std::array<const Lit*, 2> lit_bool;
758 u32 curr_run = 0;
759 } data_;
760
761 friend void swap(World& w1, World& w2) noexcept {
762 using std::swap;
763 // clang-format off
764 swap(w1.state_, w2.state_);
765 swap(w1.data_, w2.data_ );
766 swap(w1.move_, w2.move_ );
767 // clang-format on
768
769 swap(w1.data_.univ->world_, w2.data_.univ->world_);
770 assert(&w1.univ()->world() == &w1);
771 assert(&w2.univ()->world() == &w2);
772 }
773};
774
775} // namespace mim
A (possibly paramterized) Array.
Definition tuple.h:117
Definition axm.h:9
Base class for all Defs.
Definition def.h:251
Some "global" variables needed all over the place.
Definition driver.h:17
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:14
A built-in constant of type Nat -> *.
Definition def.h:845
static constexpr nat_t bitwidth2size(nat_t n)
Definition def.h:876
A function.
Definition lam.h:109
std::variant< bool, const Def * > Filter
Definition lam.h:117
static T as(const Def *def)
Definition def.h:816
Facility to log what you are doing.
Definition log.h:17
A (possibly paramterized) Tuple.
Definition tuple.h:166
A dependent function type.
Definition lam.h:13
static const Def * infer(const Def *dom, const Def *codom)
Definition check.cpp:365
Type formation of a rewrite Rule.
Definition rule.h:9
static const Def * infer(const Def *meta_type)
Definition check.cpp:402
A rewrite rule.
Definition rule.h:38
Rule * set(const Def *lhs, const Def *rhs)
Definition rule.h:62
Base class for Arr and Pack.
Definition tuple.h:84
A dependent tuple type.
Definition tuple.h:20
Data constructor for a Sigma.
Definition tuple.h:68
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
const Lit * lit_idx(nat_t size, u64 val)
Constructs a Lit of type Idx of size size.
Definition world.h:438
const Lit * lit_idx(I val)
Definition world.h:441
const Def * arr(Defs shape, const Def *body)
Definition world.h:376
const Def * insert(const Def *d, const Def *i, const Def *val)
Definition world.cpp:425
const Def * type_i16()
Definition world.h:513
const Pi * fn(Defs dom, const Def *codom, bool implicit=false)
Definition world.h:280
const Def * meet(Defs ops)
Definition world.h:480
const auto & flags2annex() const
Definition world.h:176
const Lam * con(Defs dom, Lam::Filter f, const Def *body)
Definition world.h:296
const Def * uinc(const Def *op, level_t offset=1)
Definition world.cpp:115
const Pi * cn()
Definition world.h:276
const Lit * lit(const Def *type, u64 val)
Definition world.cpp:508
const Def * arr(u64 n, const Def *body)
Definition world.h:378
u32 next_run()
Definition world.h:97
friend void swap(World &w1, World &w2) noexcept
Definition world.h:761
Log & log()
Definition world.cpp:71
const Def * implicit_app(const Def *callee, nat_t arg)
Definition world.h:530
const Def * extract(const Def *d, u64 a, u64 i)
Definition world.h:403
auto & muts()
Definition world.h:551
const Def * type_i4()
Definition world.h:511
const Lit * lit_i8()
Definition world.h:432
Hole * mut_hole_infer_entity()
Either a value ?:?:Type ? or a type ?:Type ?:Type ?.
Definition world.h:236
const Pi * cn(const Def *dom, bool implicit=false)
Definition world.h:277
const Def * type_int(nat_t width)
Constructs a type Idx of size 2^width.
Definition world.h:506
World & operator=(World)=delete
const Lit * lit_i16(u16 val)
Definition world.h:453
void watchpoint(u32 gid)
Trigger breakpoint in your debugger when Def::setting a Def with this gid.
Definition world.cpp:679
const Lit * lit_i1(bool val)
Definition world.h:449
const Def * arr(View< u64 > shape, const Def *body)
Definition world.h:380
const Lit * lit_i32()
Definition world.h:434
Driver & driver()
Definition world.h:88
Lam * mut_fun(const Def *dom, Defs codom)
Definition world.h:313
const Type * type(const Def *level)
Definition world.cpp:106
void make_external(Def *)
Definition world.cpp:88
const Driver & driver() const
Definition world.h:87
const Lam * lam(const Def *dom, const Def *codom, Lam::Filter f, const Def *body)
Definition world.h:297
Lam * mut_lam(const Def *dom, Defs codom)
Definition world.h:309
const Lit * lit_tt()
Definition world.h:465
const Def * filter(Lam::Filter filter)
Definition world.h:288
World(Driver *)
Definition world.cpp:59
const auto & watchpoints()
Definition world.h:162
const auto & sym2external() const
Definition world.h:203
const Def * type_idx(nat_t size)
Definition world.h:502
const Def * pack(const Def *arity, const Def *body)
Definition world.h:375
const Def * unit(bool term)
Definition world.h:358
void set(std::string_view name)
Definition world.h:92
const Def * app(const Def *callee, const Def *arg)
Definition world.cpp:196
u32 curr_gid() const
Manage global identifier - a unique number for each Def.
Definition world.h:95
const Def * seq(bool term, View< u64 > shape, const Def *body)
Definition world.h:364
const Axm * axm(const Def *type)
See above.
Definition world.h:258
const Def * match(Defs)
Definition world.cpp:595
World inherit()
Inherits the state into the new World.
Definition world.h:79
const Def * type_bot()
Definition world.h:474
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:264
const Def * pack(u64 n, const Def *body)
Definition world.h:379
const Def * seq(bool term, const Def *arity, const Def *body)
Definition world.cpp:474
const Def * insert(const Def *d, u64 a, u64 i, const Def *val)
Definition world.h:415
const auto & muts() const
Definition world.h:553
const Univ * univ()
Definition world.h:213
const Lam * lam(Defs dom, const Def *codom, Lam::Filter f, const Def *body)
Definition world.h:298
const Def * seq_unsafe(bool term, const Def *body)
Definition world.h:365
const Lam * fun(Defs dom, const Def *codom, Lam::Filter f, const Def *body)
Definition world.h:302
Rule * mut_rule(const Reform *type)
Definition world.h:321
const Def * type_i8()
Definition world.h:512
World & verify()
Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.
Definition world.cpp:687
const Def * bot(const Def *type)
Definition world.h:472
const Lit * lit_i64()
Definition world.h:435
Arr * mut_arr(const Def *type)
Definition world.h:372
const Rule * rule(const Def *meta_type, const Def *lhs, const Def *rhs, const Def *guard)
Definition world.h:325
const Lam * lam(const Def *dom, Defs codom, Lam::Filter f, const Def *body)
Definition world.h:299
const Lit * lit_idx_mod(nat_t mod, u64 val)
Constructs a Lit of type Idx of size mod.
Definition world.h:461
const Idx * type_idx()
Definition world.h:498
const Def * type_i1()
Definition world.h:509
Pi * mut_pi(const Def *type, bool implicit=false)
Definition world.h:268
const Lit * lit_univ_0()
Definition world.h:423
const Def * annex(Id id)
Lookup annex by Axm::id.
Definition world.h:181
void set_loc(Loc loc={})
Definition world.h:117
const Def * implicit_app(const Def *callee, E arg)
Definition world.h:534
Sym name() const
Definition world.h:90
const Pi * cn(Defs dom, bool implicit=false)
Definition world.h:278
void dump()
Dump to std::cout.
Definition dump.cpp:491
const Lam * fun(const Def *dom, Defs codom, Lam::Filter f, const Def *body)
Definition world.h:303
const Lit * lit_univ_1()
Definition world.h:424
const Reform * reform(const Def *meta_type)
Definition world.h:320
void write()
Same above but file name defaults to World::name.
Definition dump.cpp:502
const Lam * lam(Defs dom, Defs codom, Lam::Filter f, const Def *body)
Definition world.h:300
const Def * register_annex(plugin_t p, tag_t t, sub_t s, const Def *def)
Definition world.h:196
Lam * mut_fun(Defs dom, const Def *codom)
Definition world.h:312
Lam * mut_fun(const Def *dom, const Def *codom)
Definition world.h:311
const Lit * lit_i1()
Definition world.h:431
const Axm * axm(NormalizeFn n, u8 curry, u8 trip, const Def *type)
Builds a fresh Axm with descending Axm::sub.
Definition world.h:255
const Nat * type_nat()
Definition world.h:497
const Pi * fn(const Def *dom, Defs codom, bool implicit=false)
Definition world.h:281
Hole * mut_hole(const Def *type)
Definition world.h:231
const Axm * axm(const Def *type, plugin_t p, tag_t t, sub_t s)
Definition world.h:249
const Lam * lam(const Pi *pi, Lam::Filter f, const Def *body)
Definition world.h:292
const Lam * fun(Defs dom, Defs codom, Lam::Filter f, const Def *body)
Definition world.h:304
Lam * mut_lam(const Def *dom, const Def *codom)
Definition world.h:307
const Def * gid2def(u32 gid)
Lookup Def by gid.
Definition world.cpp:681
Flags & flags()
Retrieve compile Flags.
Definition world.cpp:72
const Def * implicit_app(const Def *callee, const Def *arg)
Places Holes as demanded by Pi::is_implicit() and then apps arg.
Definition world.cpp:189
std::unique_ptr< World > inherit_ptr()
As above.
Definition world.h:80
ScopedLoc push(Loc loc)
Definition world.h:118
const Def * implicit_app(const Def *callee, Defs args)
Definition world.h:526
void debug_dump()
Dump in Debug build if World::log::level is Log::Level::Debug.
Definition dump.cpp:493
u32 next_gid()
Definition world.h:96
const Def * extract(const Def *d, u64 i)
Definition world.h:404
Seq * mut_seq(bool term, const Def *type)
Definition world.h:360
const Lam * fun(const Def *dom, const Def *codom, Lam::Filter f, const Def *body)
Definition world.h:301
const Def * inj(const Def *type, const Def *value)
Definition world.cpp:580
const Def * call(Args &&... args)
Definition world.h:543
const auto & breakpoints()
Definition world.h:161
const Type * type()
Definition world.h:220
const Axm * axm(NormalizeFn n, u8 curry, u8 trip, const Def *type, plugin_t p, tag_t t, sub_t s)
Definition world.h:246
const Def * pack(Defs shape, const Def *body)
Definition world.h:377
const Def * var(const Def *type, Def *mut)
Definition world.cpp:177
const Def * seq(bool term, u64 n, const Def *body)
Definition world.h:363
void set(Sym name)
Definition world.h:91
const Def * app(const Def *callee, Defs args)
Definition world.h:335
const Def * pack(View< u64 > shape, const Def *body)
Definition world.h:381
Lam * mut_fun(Defs dom, Defs codom)
Definition world.h:314
const Lit * lit_i2(u8 val)
Definition world.h:450
const Def * extract(const Def *d, const Def *i)
Definition world.cpp:346
Pack * mut_pack(const Def *type)
Definition world.h:373
bool is_frozen() const
Definition world.h:137
const Lit * lit_idx_unsafe(u64 val)
Definition world.h:439
Loc get_loc() const
Definition world.h:116
auto externals() const
Definition world.h:205
const Lit * lit_nat_0()
Definition world.h:426
const Def * arr(const Def *arity, const Def *body)
Definition world.h:374
Sym sym(std::string_view)
Definition world.cpp:75
const Lit * lit_i16()
Definition world.h:433
Global * global(const Def *type, bool is_mutable=true)
Definition world.h:492
Lam * mut_lam(Defs dom, const Def *codom)
Definition world.h:308
const Lit * lit_ff()
Definition world.h:464
const Lit * lit_nat_max()
Definition world.h:428
const Def * raw_app(const Def *type, const Def *callee, Defs args)
Definition world.h:340
const Pi * pi(Defs dom, const Def *codom, bool implicit=false)
Definition world.h:265
Def * external(Sym name)
Lookup by name.
Definition world.h:204
const Def * bound(Defs ops)
Definition world.cpp:539
const Def * join(Defs ops)
Definition world.h:479
const Def * ext(const Def *type)
Definition world.cpp:529
Sym append_suffix(Sym name, std::string suffix)
Appends a suffix or an increasing number if the suffix already exists.
Definition world.cpp:636
void make_internal(Def *)
Definition world.cpp:95
const Proxy * proxy(const Def *type, Defs ops, u32 index, u32 tag)
Definition world.h:229
const Lit * lit_i32(u32 val)
Definition world.h:454
const Lit * lit_i8(u8 val)
Definition world.h:452
Lam * mut_lam(Defs dom, Defs codom)
Definition world.h:310
const Def * type_top()
Definition world.h:475
const Lit * lit_idx_1_0()
Definition world.h:429
Sigma * mut_sigma(size_t size)
A mutable Sigma of type level.
Definition world.h:348
const Lit * lit_univ(u64 level)
Definition world.h:422
const Pi * pi(Defs dom, Defs codom, bool implicit=false)
Definition world.h:267
const Tuple * tuple()
the unit value of type []
Definition world.h:395
const Type * type_infer_univ()
Definition world.h:218
const Def * call(Id id, Args &&... args)
Complete curried call of annexes obeying implicits.
Definition world.h:542
const Def * type_bool()
Definition world.h:508
const Def * uniq(const Def *inhabitant)
Definition world.cpp:631
void dummy()
Definition world.h:564
const Def * raw_app(const Axm *axm, u8 curry, u8 trip, const Def *type, const Def *callee, const Def *arg)
Definition world.cpp:274
const Def * prod(bool term, Defs ops)
Definition world.h:385
const Def * prod(bool term)
Definition world.h:386
const Def * umax(Defs)
Definition world.cpp:135
Vector< Def * > copy_externals() const
Definition world.h:206
const Lam * con(const Def *dom, Lam::Filter f, const Def *body)
Definition world.h:295
const Def * type_i2()
Definition world.h:510
const Def * arr_unsafe(const Def *body)
Definition world.h:382
const Def * merge(const Def *type, Defs ops)
Definition world.cpp:562
const Lit * lit_i64(u64 val)
Definition world.h:455
const Def * type_i64()
Definition world.h:515
const Sigma * sigma()
The unit type within Type 0.
Definition world.h:352
const Lit * lit_nat(nat_t a)
Definition world.h:425
const State & state() const
Definition world.h:85
Hole * mut_hole_type()
Definition world.h:233
const Def * pack_unsafe(const Def *body)
Definition world.h:383
const auto & vars() const
Definition world.h:552
const Def * register_annex(flags_t f, const Def *)
Definition world.cpp:78
const Def * top(const Def *type)
Definition world.h:473
const Def * type_idx(const Def *size)
Definition world.h:500
Lam * mut_con(const Def *dom)
Definition world.h:305
Arr * mut_arr()
Definition world.h:368
auto & vars()
Definition world.h:550
Defs reduce(const Var *var, const Def *arg)
Yields the new body of [mut->var() -> arg]mut.
Definition world.cpp:656
const Lit * lit_int(nat_t width, u64 val)
Constructs a Lit of type Idx of size 2^width.
Definition world.h:448
const Lit * lit_bool(bool val)
Definition world.h:463
void breakpoint(u32 gid)
Trigger breakpoint in your debugger when creating a Def with this gid.
Definition world.cpp:678
const Def * select(const Def *cond, const Def *t, const Def *f)
Builds (f, t)#cond.
Definition world.h:408
Sigma * mut_sigma(const Def *type, size_t size)
Definition world.h:345
Hole * mut_hole_univ()
Definition world.h:232
Lam * mut_con(Defs dom)
Definition world.h:306
const Def * split(const Def *type, const Def *value)
Definition world.cpp:588
const Def * top_nat()
Definition world.h:476
const Pi * fn(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:279
const Rule * rule(const Reform *type, const Def *lhs, const Def *rhs, const Def *guard)
Definition world.h:322
auto annexes() const
Definition world.h:177
World(World &&other) noexcept
Definition world.h:73
const Lit * lit_nat_1()
Definition world.h:427
const Pi * pi(const Def *dom, Defs codom, bool implicit=false)
Definition world.h:266
bool freeze(bool on=true) const
Yields old frozen state.
Definition world.h:140
const Def * type_i32()
Definition world.h:514
const Lit * lit_i4(u8 val)
Definition world.h:451
void dot(std::ostream &os, bool annexes=false, bool types=false) const
Dumps DOT to os.
Definition dot.cpp:146
const Def * insert(const Def *d, u64 i, const Def *val)
Definition world.h:416
const Pi * fn(Defs dom, Defs codom, bool implicit=false)
Definition world.h:282
Lam * mut_lam(const Pi *pi)
Definition world.h:293
const Def * annex()
Get Axm from a plugin.
Definition world.h:191
Definition ast.h:14
View< const Def * > Defs
Definition def.h:76
u64 nat_t
Definition types.h:43
Vector< const Def * > DefVec
Definition def.h:77
u8 sub_t
Definition types.h:48
auto assert_emplace(C &container, Args &&... args)
Invokes emplace on container, asserts that insertion actually happened, and returns the iterator.
Definition util.h:110
u64 flags_t
Definition types.h:45
auto lookup(const C &container, const K &key)
Yields pointer to element (or the element itself if it is already a pointer), if found and nullptr ot...
Definition util.h:100
Span< const T, N > View
Definition span.h:98
void error(Loc loc, const char *f, Args &&... args)
Definition dbg.h:125
u64 level_t
Definition types.h:42
TExt< true > Top
Definition lattice.h:172
std::ostream & outln(const char *fmt, Args &&... args)
Definition print.h:200
const Def *(*)(const Def *, const Def *, const Def *) NormalizeFn
Definition def.h:100
u64 plugin_t
Definition types.h:46
uint32_t u32
Definition types.h:34
TExt< false > Bot
Definition lattice.h:171
uint64_t u64
Definition types.h:34
u8 tag_t
Definition types.h:47
uint8_t u8
Definition types.h:34
@ Nat
Definition def.h:114
@ Univ
Definition def.h:114
@ Idx
Definition def.h:114
@ Sigma
Definition def.h:114
@ Type
Definition def.h:114
@ Tuple
Definition def.h:114
@ Lit
Definition def.h:114
uint16_t u16
Definition types.h:34
Compiler switches that must be saved and looked up in later phases of compilation.
Definition flags.h:11
static constexpr plugin_t Global_Plugin
Definition plugin.h:61
static Sym demangle(Driver &, plugin_t plugin)
Reverts an Axm::mangled string to a Sym.
Definition plugin.cpp:37
static constexpr flags_t Base
Definition plugin.h:123
Freezer(const World &world)
Definition world.h:148
const World & world
Definition world.h:153
ScopedLoc(World &world, Loc old_loc)
Definition world.h:106
absl::flat_hash_set< uint32_t > watchpoints
Definition world.h:54
friend void swap(State &s1, State &s2) noexcept
Definition world.h:56
struct mim::World::State::POD pod
absl::flat_hash_set< uint32_t > breakpoints
Definition world.h:53
Plain Old Data
Definition world.h:44