The World represents the whole program and manages creation of MimIR nodes (Defs). More...
#include <mim/world.h>
Classes | |
| struct | CurrLoc |
| World::get_loc together with its interned DbgKey, so pushing/popping a Loc never re-interns it. More... | |
| struct | State |
| class | Externals |
| class | Annexes |
Public Types | |
| using | ScopedLoc = fe::Restore<CurrLoc> |
Public Member Functions | |
Construction & Destruction | |
| World & | operator= (World)=delete |
| World (Driver *, Sym name) | |
| World (Driver *, const State &) | |
| World (World &&other) noexcept | |
| ~World () | |
| std::unique_ptr< World > | inherit () |
| Inherits the State into the new World. | |
Getters/Setters | |
| const State & | state () const |
| Driver & | driver () |
| const Driver & | driver () const |
| fe::Error & | error () |
| const fe::Error & | error () const |
| Zonker & | zonker () |
| Sym | name () const |
| void | set (Sym name) |
| void | set (std::string_view name) |
| u32 | curr_gid () const |
| Manage global identifier - a unique number for each Def. | |
| u32 | next_gid () |
| u32 | curr_run () const |
| Manage run - used to track fixed-point iterations to compute Def::free_vars. | |
| u32 | next_run () |
| Flags & | flags () |
| Retrieve compile Flags. | |
Loc | |
| Loc | get_loc () const |
| DbgKey | dbg_key () const |
| World::get_loc, already interned. | |
| ScopedLoc | push (Loc) |
Sym | |
| Sym | sym (std::string_view) |
| Sym | sym (const char *) |
| Sym | sym (const std::string &) |
| Sym | append_suffix (Sym name, std::string suffix) |
Appends a suffix or an increasing number if the suffix already exists. | |
Freeze | |
In frozen state the World does not create any nodes. Dumping freezes: a dump that allocated gids would perturb the very program you are debugging. So whatever a frozen query cannot answer from what is already there comes back as nullptr. | |
| bool | is_frozen () const |
| auto | freeze () const |
| Freezes the World until the end of the scope and restores the previous frozen state afterwards: | |
Lenient | |
| bool | is_lenient () const |
| auto | lenient () const |
Debugging Features | |
| const auto & | breakpoints () |
| const auto & | watchpoints () |
| const Def * | gid2def (u32 gid) |
Lookup Def by gid. | |
| void | breakpoint (u32 gid) |
Trigger breakpoint in your debugger when creating a Def with this gid. | |
| void | watchpoint (u32 gid) |
Trigger breakpoint in your debugger when Def::setting a Def with this gid. | |
| World & | verify () |
| Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS. | |
Externals & Annexes | |
| const Externals & | externals () const |
| Externals & | externals () |
| Annexes & | annexes () |
| const Annexes & | annexes () const |
| const Def * | annex (Sym sym) |
| Lookup annex by Sym. | |
| const Def * | annex (flags_t flags) |
| Lookup annex by flags. | |
| const Def * | annex (Enum auto id) |
| Lookup annex by Axm::id. | |
| template<annex_without_subs id> | |
| const Def * | annex () |
| Get Axm from a plugin. | |
| const Def * | import (const Def *def) |
Imports def of Driver::library into this World. | |
Level, Type, Var, Proxy, Hole | |
| const Level * | type_level () |
| const Def * | lsucc (const Def *op, level_t offset=1) |
| const Def * | lmax (Defs levels) |
| const Def * | level (Defs types) |
The lmax of the levels of all types, each of which must be a Type level. | |
| const Type * | type (const Def *level) |
| const Level * | type_pending () |
| Placeholder type of a mutable whose sort Def::finalize infers from its ops. | |
| const Type * | type_infer_level () |
| void | postpone (const LMax *lmax, const Def *level) |
Postpones lmax = level as it does not determine the level Holes of lmax yet. | |
| void | solve_levels () |
| Defaults the level Holes of all postponed constraints that are still unknown to 0 and checks them. | |
| template<level_t level = 0> | |
| const Type * | type () |
| const Def * | var (Def *mut) |
| const Def * | inhabitant (const Def *type) |
The sole inhabitant of type, if it has exactly one, nullptr otherwise. | |
| const Proxy * | proxy (const Def *type, Defs ops, u32 tag, bool vars=false, bool muts=false) |
| Hole * | mut_hole (const Def *type) |
| Hole * | mut_hole_level () |
| Hole * | mut_hole_type () |
Axm | |
| const Axm * | axm (NormalizeFn n, u8 curry, u8 trip, const Def *type, plugin_t p, tag_t t, sub_t s) |
| const Axm * | axm (const Def *type, plugin_t p, tag_t t, sub_t s) |
| const Axm * | axm (NormalizeFn n, u8 curry, u8 trip, const Def *type) |
| Builds a fresh Axm with descending Axm::sub. | |
| const Axm * | axm (const Def *type) |
| See above. | |
Pi | |
| const Pi * | pi (const Def *dom, const Def *codom, bool implicit=false) |
| const Pi * | pi (Defs dom, const Def *codom, bool implicit=false) |
| const Pi * | pi (const Def *dom, Defs codom, bool implicit=false) |
| const Pi * | pi (Defs dom, Defs codom, bool implicit=false) |
| Pi * | mut_pi (const Def *type, bool implicit=false) |
Cn | |
| const Pi * | cn () |
| const Pi * | cn (const Def *dom, bool implicit=false) |
| const Pi * | cn (Defs dom, bool implicit=false) |
| const Pi * | fn (const Def *dom, const Def *codom, bool implicit=false) |
| const Pi * | fn (Defs dom, const Def *codom, bool implicit=false) |
| const Pi * | fn (const Def *dom, Defs codom, bool implicit=false) |
| const Pi * | fn (Defs dom, Defs codom, bool implicit=false) |
Lam | |
| const Def * | filter (Lam::Filter filter) |
| const Lam * | lam (const Pi *pi, Lam::Filter f, const Def *body) |
| Lam * | mut_lam (const Pi *pi) |
| const Lam * | con (const Def *dom, Lam::Filter f, const Def *body) |
| const Lam * | con (Defs dom, Lam::Filter f, const Def *body) |
| const Lam * | lam (const Def *dom, const Def *codom, Lam::Filter f, const Def *body) |
| const Lam * | lam (Defs dom, const Def *codom, Lam::Filter f, const Def *body) |
| const Lam * | lam (const Def *dom, Defs codom, Lam::Filter f, const Def *body) |
| const Lam * | lam (Defs dom, Defs codom, Lam::Filter f, const Def *body) |
| const Lam * | fun (const Def *dom, const Def *codom, Lam::Filter f, const Def *body) |
| const Lam * | fun (Defs dom, const Def *codom, Lam::Filter f, const Def *body) |
| const Lam * | fun (const Def *dom, Defs codom, Lam::Filter f, const Def *body) |
| const Lam * | fun (Defs dom, Defs codom, Lam::Filter f, const Def *body) |
| Lam * | mut_con (const Def *dom) |
| Lam * | mut_con (Defs dom) |
| Lam * | mut_lam (const Def *dom, const Def *codom) |
| Lam * | mut_lam (Defs dom, const Def *codom) |
| Lam * | mut_lam (const Def *dom, Defs codom) |
| Lam * | mut_lam (Defs dom, Defs codom) |
| Lam * | mut_fun (const Def *dom, const Def *codom) |
| Lam * | mut_fun (Defs dom, const Def *codom) |
| Lam * | mut_fun (const Def *dom, Defs codom) |
| Lam * | mut_fun (Defs dom, Defs codom) |
Rewrite Rules | |
| const Reform * | reform (const Def *dom) |
| Rule * | mut_rule (const Reform *type) |
| const Rule * | rule (const Reform *type, const Def *lhs, const Def *rhs, const Def *guard) |
App | |
| template<bool Normalize = true> | |
| const Def * | app (const Def *callee, const Def *arg) |
| template<bool Normalize = true> | |
| const Def * | app (const Def *callee, Defs args) |
| const Def * | raw_app (const Axm *axm, u8 curry, u8 trip, const Def *type, const Def *callee, const Def *arg) |
| const Def * | raw_app (const Def *type, const Def *callee, const Def *arg) |
| const Def * | raw_app (const Def *type, const Def *callee, Defs args) |
Sigma | |
| Sigma * | mut_sigma (const Def *type, size_t size) |
| template<level_t level = 0> | |
| Sigma * | mut_sigma (size_t size) |
A mutable Sigma of type level. | |
| const Def * | sigma (Defs ops) |
| const Sigma * | sigma () |
| The unit type within Type 0. | |
Arr & Pack | |
| template<level_t level = 0> | |
| Arr * | mut_arr () |
| Arr * | mut_arr (const Def *type) |
| Pack * | mut_pack (const Def *type) |
| const Def * | arr (Shape shape, const Def *body) |
| const Def * | pack (Shape shape, const Def *body) |
| const Def * | arr (Defs shape, const Def *body) |
| const Def * | pack (Defs shape, const Def *body) |
| const Def * | arr (fe::View< u64 > shape, const Def *body) |
| const Def * | pack (fe::View< u64 > shape, const Def *body) |
| const Def * | arr (u64 n, const Def *body) |
| const Def * | pack (u64 n, const Def *body) |
prod | |
Generic constructor for tuple or sigma. | |
| const Def * | prod (bool term, Defs ops) |
| const Def * | prod (bool term) |
| () or []. | |
Seq | |
| Seq * | mut_seq (bool is_pack, const Def *type) |
| const Def * | seq (bool is_pack, Shape shape, const Def *body) |
| const Def * | seq (bool is_pack, Defs shape, const Def *body) |
| const Def * | seq (bool is_pack, u64 n, const Def *body) |
| const Def * | seq (bool is_pack, fe::View< u64 > shape, const Def *body) |
| const Def * | drop (const Seq *s, nat_t k) |
s without its leading k axes - its body once k covers all of them; nullptr if that isn't a type. | |
| const Def * | fuse (Seq *seq) |
| «i: a; «j: b; T»» -> «v: (a, b); T» - the inverse of World::peel, for a nest that World::seq cannot fuse on construction because its body still binds an index. | |
| const Def * | peel (const Seq *seq, const Def *index) |
seq with the axes covered by index peeled off - the element itself once index covers all of them. | |
| const Def * | type_indices (Shape shape) |
The type of an index into shape: Idx n, a Sigma of those, or «i: r; Idx (s#i)» for a dynamic rank. | |
Tuple | |
| const Def * | tuple (Defs ops) |
| const Def * | tuple (const Def *type, Defs ops) |
Ascribes type to this tuple - needed for dependently typed and mutable Sigmas. | |
| const Tuple * | tuple () |
| the unit value of type [] | |
| const Def * | tuple (Sym sym) |
Converts sym to a tuple of type '«n; I8»'. | |
Extract | |
| const Def * | extract (const Def *d, const Def *i) |
| const Def * | extract (const Def *d, u64 a, u64 i) |
| const Def * | extract (const Def *d, u64 i) |
| const Def * | select (const Def *cond, const Def *t, const Def *f) |
| Builds (f, t)#cond. | |
Insert | |
| const Def * | insert (const Def *d, const Def *i, const Def *val) |
| const Def * | insert (const Def *d, u64 a, u64 i, const Def *val) |
| const Def * | insert (const Def *d, u64 i, const Def *val) |
Lattice | |
| template<bool Up> | |
| const Def * | ext (const Def *type) |
| const Def * | bot (const Def *type) |
| const Def * | top (const Def *type) |
| const Def * | type_bot () |
| const Def * | type_top () |
Join & Variant | |
| const Def * | join (Defs ops) |
| Variant * | mut_variant (const Def *type, size_t size) |
| const Def * | variant (Defs ops) |
| const Def * | inj (const Def *type, const Def *value) |
| const Def * | inj (const Def *type, nat_t index, const Def *value) |
Injects value as case index of a Variant. | |
| const Def * | match (Defs) |
Types | |
| const Nat * | type_nat () |
| const Idx * | type_idx () |
| const Def * | type_idx (const Def *size) |
| const Def * | type_idx (nat_t size) |
| const Def * | type_int (nat_t width) |
| Constructs a type Idx of size 2^width. | |
| const Def * | type_bool () |
| const Def * | type_i1 () |
| const Def * | type_i8 () |
| const Def * | type_i16 () |
| const Def * | type_i32 () |
| const Def * | type_i64 () |
Nominal Newtypes | |
| const Nom * | nom (flags_t key, const Def *type) |
Make type Nominal under key. | |
| const Def * | name (const Def *nom, const Def *struc) |
Name a structural to make it nominal. | |
| const Def * | struc (const Def *nom) |
Get the structural part of a nominal. | |
implicit_app - Cope with implicit Arguments | |
Places Holes as demanded by Pi::is_implicit() and then apps | |
| const Def * | implicit_holes (const Def *callee) |
| Only places the Holes. | |
| template<bool Normalize = true> | |
| const Def * | implicit_app (const Def *callee, const Def *arg) |
| template<bool Normalize = true> | |
| const Def * | implicit_app (const Def *callee, Defs args) |
| template<bool Normalize = true> | |
| const Def * | implicit_app (const Def *callee, nat_t arg) |
| template<bool Normalize = true> requires std::is_same_v<std::underlying_type_t<decltype(arg)>, nat_t> | |
| const Def * | implicit_app (const Def *callee, Enum auto arg) |
call | |
Complete curried call of | |
| template<bool Normalize = true, class... Args> | |
| const Def * | call (const Def *callee, auto &&arg, Args &&... args) |
| template<bool Normalize = true> | |
| const Def * | call (const Def *callee, auto &&arg) |
| Base case. | |
| template<Enum Id, bool Normalize = true, class... Args> | |
| const Def * | call (Id id, Args &&... args) |
| Annex overload with enum instance as first argument. | |
| template<class Id, bool Normalize = true, class... Args> requires std::is_enum_v<Id> | |
| const Def * | call (Args &&... args) |
Annex overload with enum tempalte argument Id for annexes w/o subtag. | |
| template<bool Normalize = true, class... Args> | |
| const Def * | call (flags_t id, Args &&... args) |
| Annex overload with flags_t as first argument. | |
Singletons | |
| const Def * | single (const Def *) |
| Singleton type formation. | |
| const Def * | wrap (const Def *) |
| Singleton term introduction. | |
| const Def * | unwrap (const Def *) |
| Singleton term elimination. | |
Vars & Muts | |
| auto & | vars () |
| auto & | muts () |
| const auto & | vars () const |
| const auto & | muts () const |
| Defs | reduce (const Var *var, const Def *arg) |
| Yields the new body of [mut->var() -> arg]mut. | |
| const Def * | reduce (const Var *var, const Def *arg, size_t i) |
As above but reduces only the i th op. | |
| const Def * | component (const Def *type, Defs parts, size_t n, size_t i) |
The type of component i of the n-ary type, given its leading components parts. | |
for_each | |
Visits all closed mutables in this World. | |
| void | for_each (bool elide_empty, std::function< void(Def *)>, bool schedule=false) |
| template<class M> | |
| void | for_each (bool elide_empty, std::invocable< M * > auto f, bool schedule=false) |
dump/log | |
| const fe::Log & | log () const |
| Log via log().e("...", args) etc.; owned by the Driver. | |
| void | dump (std::ostream &os) |
Dump to os. | |
| void | dump () |
| Dump to std::cout. | |
| void | debug_dump () |
| Dump in Debug build if World::log::level is fe::Log::Level::Debug. | |
| void | write (const char *file) |
Write to a file named file. | |
| void | write () |
| Same above but file name defaults to World::name. | |
dot | |
GraphViz output. | |
| void | dot (std::ostream &os, DotConfig cfg={}) const |
Dumps DOT to os, configured via cfg (see DotConfig). | |
| void | dot (const char *file=nullptr, DotConfig cfg={}) const |
Same as above but write to file or std::cout if file is nullptr. | |
Friends | |
| void | swap (World &w1, World &w2) noexcept |
Lit | |
| static constexpr nat_t | Num_Lit_Nats = 64 |
| Def::arity of a Sigma is lit_nat(num_ops()) and Def::num_projs reads it straight back out, so a plain World::lit would hash-cons a Lit just to launder an integer. | |
| const Lit * | lit (const Def *type, u64 val) |
| const Lit * | lit_level (u64 level) |
| const Lit * | lit_level_0 () |
| const Lit * | lit_level_1 () |
| const Lit * | lit_nat (nat_t a) |
| const Lit * | lit_nat_0 () |
| const Lit * | lit_nat_1 () |
| const Lit * | lit_nat_max () |
| const Lit * | lit_idx_1_0 () |
| const Lit * | lit_i1 () |
| const Lit * | lit_i8 () |
| const Lit * | lit_i16 () |
| const Lit * | lit_i32 () |
| const Lit * | lit_i64 () |
| const Lit * | lit_idx (nat_t size, u64 val) |
Constructs a Lit of type Idx of size size. | |
| const Lit * | lit_idx (std::integral auto val) |
| const Lit * | lit_int (nat_t width, u64 val) |
Constructs a Lit of type Idx of size 2^width. | |
| const Lit * | lit_i1 (bool val) |
| const Lit * | lit_i8 (u8 val) |
| const Lit * | lit_i16 (u16 val) |
| const Lit * | lit_i32 (u32 val) |
| const Lit * | lit_i64 (u64 val) |
| const Lit * | lit_idx_mod (nat_t mod, u64 val) |
Constructs a Lit of type Idx of size mod. | |
| const Lit * | lit_bool (bool val) |
| const Lit * | lit_ff () |
| const Lit * | lit_tt () |
The World represents the whole program and manages creation of MimIR nodes (Defs).
Defs are hashed into an internal HashSet. The World's factory methods just calculate a hash and lookup the Def, if it is already present, or create a new one otherwise. This corresponds to value numbering.
You can create several worlds. All worlds are completely independent from each other.
Note that types are also just Defs and will be hashed as well.
| struct mim::World::CurrLoc |
World::get_loc together with its interned DbgKey, so pushing/popping a Loc never re-interns it.
| Class Members | ||
|---|---|---|
| DbgKey | key = {} | |
| Loc | loc = {} | |
| using mim::World::ScopedLoc = fe::Restore<CurrLoc> |
|
explicit |
Definition at line 181 of file world.cpp.
References driver(), insert(), lit(), lit_idx(), lit_level_0(), lit_level_1(), lit_nat(), Num_Lit_Nats, pi(), sigma(), state(), type(), type_idx(), type_level(), and type_nat().
|
inlinenoexcept |
|
default |
|
inline |
|
inline |
| const Def * mim::World::annex | ( | Sym | sym | ) |
|
inline |
Definition at line 289 of file world.h.
Referenced by annex(), annex(), mim::ast::Emitter::attach(), mim::ast::Emitter::attach_alias(), dump(), mim::Analysis::lookup(), and verify().
Definition at line 416 of file world.cpp.
References axm(), mim::Def::blame(), mim::Check::coerce(), mim::Pi::dom(), flags(), mim::Def::has_var(), is_frozen(), is_lenient(), mim::Def::is_set(), mim::Def::isa_imm(), mim::Def::isa_mut(), mim::Def::isa_type(), lam(), lit_ff(), lit_tt(), mim::Def::loc(), log(), mim::Axm::next(), mim::Axm::normalizer(), pi(), raw_app(), mim::Pi::reduce(), reduce(), type(), mim::type_of(), var(), and mim::Def::zonk().
Referenced by mim::Lam::app(), app(), implicit_app(), implicit_holes(), inhabitant(), match(), mim::plug::autodiff::op_sum(), mim::ADCE::rewrite_imm_App(), mim::EtaConv::rewrite_imm_App(), mim::plug::affine::phase::LowerFor::rewrite_imm_App(), mim::plug::clos::phase::ClosConv::rewrite_imm_App(), mim::plug::clos::phase::LowerTypedClos::rewrite_imm_App(), mim::plug::cps::Conv::rewrite_imm_App(), mim::RWPhase::rewrite_imm_App(), mim::Scalarize::rewrite_imm_App(), mim::SCCP::rewrite_imm_App(), mim::StaticArgOpt::rewrite_imm_App(), mim::SingleErasure::rewrite_imm_Match(), mim::DispatchNormalize::rewrite_mut_Lam(), and type_idx().
| Sym mim::World::append_suffix | ( | Sym | name, |
| std::string | suffix ) |
|
inline |
Builds a fresh Axm with descending Axm::sub.
This is useful during testing to come up with some entity of a specific type. It uses the plugin Axm::Global_Plugin and starts with 0 for Axm::sub and counts up from there. The Axm::tag is set to 0 and the Axm::normalizer to nullptr.
Definition at line 377 of file world.h.
References axm(), mim::Annex::Global_Plugin, and type().
| void mim::World::breakpoint | ( | u32 | gid | ) |
|
inline |
|
inline |
Definition at line 674 of file world.h.
References call(), and implicit_app().
Referenced by call(), call(), call(), call(), mim::plug::affine::phase::LowerFor::rewrite_imm_App(), and mim::plug::clos::phase::LowerTypedClosPrep::rewrite_imm_Tuple().
|
inline |
|
inline |
Definition at line 399 of file world.h.
References pi(), and type_bot().
|
inline |
|
inline |
|
inline |
Manage global identifier - a unique number for each Def.
Definition at line 118 of file world.h.
Referenced by dump(), and mim::RWPhase::start().
|
inline |
Manage run - used to track fixed-point iterations to compute Def::free_vars.
|
inline |
World::get_loc, already interned.
| void mim::World::debug_dump | ( | ) |
Dump in Debug build if World::log::level is fe::Log::Level::Debug.
Definition at line 1550 of file dump.cpp.
References debug_dump(), dump(), level(), and log().
Referenced by debug_dump().
| void mim::World::dot | ( | const char * | file = nullptr, |
| DotConfig | cfg = {} ) const |
| void mim::World::dot | ( | std::ostream & | os, |
| DotConfig | cfg = {} ) const |
Dumps DOT to os, configured via cfg (see DotConfig).
Definition at line 267 of file dot.cpp.
References dot(), externals(), mim::DotConfig::max, and muts().
|
inline |
Definition at line 107 of file world.h.
Referenced by annex(), mim::Def::dbg(), mim::ast::AST::driver(), mim::ast::Emitter::driver(), mim::Def::driver(), mim::Phase::driver(), dump(), mim::plug::ll::Emitter::Emitter(), error(), error(), flags(), inherit(), mim::ast::load_plugins(), log(), mim::plug::compile::normalize_aggr(), mim::plug::compile::normalize_cond(), mim::plug::compile::normalize_is_loaded(), mim::optimize(), push(), mim::plug::gpu::phase::run_stage(), mim::Def::set_dbg(), sym(), sym(), sym(), World(), and World().
s without its leading k axes - its body once k covers all of them; nullptr if that isn't a type.
Definition at line 637 of file world.cpp.
References is_frozen(), and seq().
Referenced by mim::Seq::elem(), and peel().
| void mim::World::dump | ( | ) |
| void mim::World::dump | ( | std::ostream & | os | ) |
Dump to os.
Definition at line 1473 of file dump.cpp.
References mim::Def::All, annexes(), curr_gid(), dot(), driver(), dump(), mim::ast::Lexer::escape(), externals(), mim::file_stem(), flags(), freeze(), mim::ast::Lexer::is_id(), lam(), muts(), name(), nom(), and sym().
Referenced by debug_dump(), dump(), dump(), and write().
| fe::Error & mim::World::error | ( | ) |
| const fe::Error & mim::World::error | ( | ) | const |
|
inline |
Definition at line 286 of file world.h.
Referenced by mim::plug::tensor::count_consumers(), dot(), dump(), mim::Def::externalize(), for_each(), mim::Def::internalize(), mim::optimize(), and verify().
Definition at line 598 of file world.cpp.
References mim::Extract::tuple(), and mim::Def::zonk().
Referenced by insert(), mim::Def::proj(), mim::plug::clos::phase::LowerTypedClos::rewrite_imm(), mim::SingleErasure::rewrite_imm_Extract(), select(), and type_indices().
Definition at line 538 of file world.h.
References mim::Lit::as(), and extract().
Referenced by extract().
|
inline |
| Flags & mim::World::flags | ( | ) |
| void mim::World::for_each | ( | bool | elide_empty, |
| std::function< void(Def *)> | f, | ||
| bool | schedule = false ) |
Definition at line 1220 of file world.cpp.
References externals(), muts(), and mim::post_order().
Referenced by for_each().
|
inline |
Definition at line 739 of file world.h.
References for_each().
|
inlinenodiscard |
Freezes the World until the end of the scope and restores the previous frozen state afterwards:
Definition at line 160 of file world.h.
Referenced by dump(), and mim::Def::operator<<.
|
inline |
|
inline |
|
inline |
|
inline |
«i: a; «j: b; T»» -> «v: (a, b); T» - the inverse of World::peel, for a nest that World::seq cannot fuse on construction because its body still binds an index.
Yields a Def::zonk_mut seq if the nest is ragged, i.e. if the inner extents depend on the outer index.
Definition at line 660 of file world.cpp.
References mim::Seq::body(), mim::Def::has_free_var(), mim::Def::has_var(), mim::Def::node(), seq(), mim::Seq::shape(), var(), mim::Def::zonk(), and mim::Def::zonk_mut().
|
inline |
Definition at line 132 of file world.h.
Referenced by postpone().
| const Def * mim::World::implicit_app | ( | const Def * | callee, |
| const Def * | arg ) |
Definition at line 411 of file world.cpp.
References app(), and implicit_holes().
Referenced by call(), call(), implicit_app(), implicit_app(), and implicit_app().
|
inline |
Definition at line 656 of file world.h.
References implicit_app(), and tuple().
|
inline |
Definition at line 664 of file world.h.
References implicit_app(), and lit_nat().
|
inline |
Definition at line 660 of file world.h.
References implicit_app(), and lit_nat().
Only places the Holes.
Definition at line 401 of file world.cpp.
References app(), mim::Pi::dom(), mim::Pi::isa_implicit(), mut_hole(), pi(), type(), and mim::Def::unfold_type().
Referenced by implicit_app().
Imports def of Driver::library into this World.
Definition at line 314 of file world.h.
Referenced by mim::Driver::move_to_library().
The sole inhabitant of type, if it has exactly one, nullptr otherwise.
Definition at line 342 of file world.h.
References mim::App, app(), mim::Arr, mim::Lit::isa(), lit_idx_1_0(), mim::Sigma, mim::Single, type(), and mim::Variant.
Referenced by mim::eta_callee(), insert(), mim::Analysis::is_singleton(), raw_app(), and var().
|
inline |
Inherits the State into the new World.
World::curr_gid will be offset to not collide with the original World.
Definition at line 97 of file world.h.
References driver(), and state().
Referenced by mim::Driver::move_to_library().
Definition at line 975 of file world.cpp.
References mim::Check::alpha(), mim::Def::blame(), mim::Check::coerce(), mim::Def::is_closed(), join(), name(), mim::Def::op(), mim::Def::ops(), single(), mim::Check::test_alpha(), type(), mim::type_of(), mim::Def::unfold_type(), and mim::Def::zonk().
Injects value as case index of a Variant.
Definition at line 1007 of file world.cpp.
References mim::Def::blame(), mim::Check::coerce(), inj(), nom(), mim::Def::num_ops(), mim::Def::op(), mim::Nom::op(), type(), mim::type_of(), variant(), and mim::Def::zonk().
Definition at line 802 of file world.cpp.
References arr(), mim::Lit::as(), mim::Seq::body(), extract(), flags(), inhabitant(), insert(), is_frozen(), mim::Idx::isa(), mim::Lit::isa(), peel(), mim::Extract::tuple(), tuple(), type(), and mim::Def::zonk().
Referenced by insert(), mut_con(), mut_con(), mut_fun(), mut_fun(), mut_fun(), mut_fun(), mut_hole(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mut_pi(), mut_rule(), mut_seq(), mut_sigma(), mut_variant(), mim::SingleErasure::rewrite_imm_Insert(), and World().
Definition at line 548 of file world.h.
References mim::Lit::as(), and insert().
Referenced by insert().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inlinenodiscard |
Definition at line 168 of file world.h.
Referenced by mim::Analysis::start().
The lmax of the levels of all types, each of which must be a Type level.
Definition at line 349 of file world.cpp.
References mim::Lit::isa(), level(), mim::level_of(), lit_level(), lmax(), and type().
Referenced by debug_dump(), join(), level(), lit_level(), lmax(), postpone(), type(), and type().
Definition at line 919 of file world.cpp.
References mim::Idx::isa(), mim::Lit::isa(), and type().
Referenced by lit_idx(), lit_level(), lit_nat(), and World().
|
inline |
|
inline |
|
inline |
Definition at line 569 of file world.h.
References mim::Idx::bitwidth2size(), and lit_nat().
|
inline |
|
inline |
Definition at line 571 of file world.h.
References mim::Idx::bitwidth2size(), and lit_nat().
|
inline |
Definition at line 572 of file world.h.
References mim::Idx::bitwidth2size(), and lit_nat().
|
inline |
Definition at line 573 of file world.h.
References mim::Idx::bitwidth2size(), and lit_nat().
|
inline |
Definition at line 570 of file world.h.
References mim::Idx::bitwidth2size(), and lit_nat().
Referenced by tuple().
|
inline |
Definition at line 578 of file world.h.
References mim::Idx::bitwidth2size(), and lit_idx().
Referenced by lit_idx().
|
inline |
Definition at line 567 of file world.h.
Referenced by inhabitant().
Definition at line 554 of file world.h.
References level(), lit(), lit_level_0(), lit_level_1(), and type_level().
|
inline |
Definition at line 557 of file world.h.
Referenced by lit_level(), type(), and World().
|
inline |
Definition at line 558 of file world.h.
Referenced by lit_level(), type(), and World().
Definition at line 563 of file world.h.
References lit(), Num_Lit_Nats, and type_nat().
Referenced by mim::Def::arity(), implicit_app(), implicit_app(), lit_i1(), lit_i16(), lit_i32(), lit_i64(), lit_i8(), mim::plug::refly::normalize_gid(), seq(), seq(), type_idx(), type_int(), and World().
|
inline |
Definition at line 565 of file world.h.
Referenced by mim::Def::arity().
|
inline |
Definition at line 260 of file world.cpp.
References mim::Def::blame(), mim::Lit::isa(), mim::Def::isa_type(), level(), lit_level(), push(), mim::type_of(), and mim::Def::zonk().
Referenced by mim::drop_self(), level(), lsucc(), and postpone().
| const fe::Log & mim::World::log | ( | ) | const |
Log via log().e("...", args) etc.; owned by the Driver.
Definition at line 224 of file world.cpp.
References driver(), and mim::Driver::log().
Referenced by app(), mim::Phase::create(), debug_dump(), mim::plug::ll::Emitter::load_rt_module(), mim::optimize(), mim::Phase::run(), mim::Scheduler::smart(), mim::plug::ll::Emit::start(), and mim::plug::nvptx::Emit::start().
Definition at line 247 of file world.cpp.
References mim::Lit::isa(), lit_level(), lmax(), lsucc(), and mim::type_of().
Referenced by lsucc().
Definition at line 1030 of file world.cpp.
References mim::Match::accepts(), mim::Check::alpha(), app(), mim::Def::blame(), mim::Match::cases(), mim::Pi::codom(), mim::Pi::dom(), inj(), mim::Def::isa_type(), join(), mim::Def::num_ops(), mim::Def::op(), pi(), type(), mim::type_of(), variant(), and mim::Def::zonk().
Definition at line 427 of file world.h.
References cn(), and insert().
Referenced by mim::plug::affine::phase::LowerFor::rewrite_imm_App(), and mim::plug::mem::phase::Heap2Stack::rewrite_imm_App().
Definition at line 361 of file world.h.
References insert(), and type().
Referenced by implicit_holes(), mut_hole_level(), mut_hole_type(), and mim::tuple_of_dict().
|
inline |
Definition at line 362 of file world.h.
References mut_hole(), and type_level().
Referenced by type_infer_level().
|
inline |
Definition at line 363 of file world.h.
References mut_hole(), and type_infer_level().
Referenced by mim::tuple_of_dict().
Definition at line 415 of file world.h.
References insert(), and pi().
Referenced by mim::SCCP::rewrite_imm_App(), mim::DispatchNormalize::rewrite_mut_Lam(), mim::plug::clos::phase::Clos2SJLJ::rewrite_mut_Lam(), mim::plug::cps::Conv::rewrite_mut_Lam(), mim::plug::mem::phase::AddMem::rewrite_mut_Lam(), mim::plug::tensor::phase::LowerToMem::rewrite_mut_Lam(), and mim::RetWrap::rewrite_mut_Lam().
Definition at line 464 of file world.h.
References insert(), and type().
Referenced by mut_sigma(), and mim::SingleErasure::rewrite_mut_Sigma().
A mutable Sigma of type level.
Definition at line 467 of file world.h.
References mut_sigma(), and type().
|
inlinenodiscard |
Definition at line 715 of file world.h.
Referenced by mim::Def::collect_locals(), dot(), dump(), for_each(), proxy(), and verify().
|
inline |
Definition at line 113 of file world.h.
Referenced by append_suffix(), dump(), mim::file_stem(), inj(), operator=(), mim::World::Externals::operator[](), set(), set(), mim::plug::ll::Emit::start(), mim::plug::nvptx::Emit::start(), mim::World::State::State(), struc(), and World().
Name a structural to make it nominal.
Definition at line 1140 of file world.cpp.
References mim::Def::blame(), mim::Check::coerce(), nom(), mim::Nom::op(), mim::type_of(), and mim::Def::zonk().
seq with the axes covered by index peeled off - the element itself once index covers all of them.
Definition at line 646 of file world.cpp.
References mim::Seq::body(), drop(), mim::Def::has_var(), is_frozen(), mim::Seq::reduce(), seq(), mim::Shape::Shape(), mim::Seq::shape(), and mim::Def::unfold_type().
Referenced by insert().
|
inline |
Definition at line 497 of file world.h.
References sigma(), and tuple().
Referenced by mim::Rewriter::rewrite_imm_Seq(), mim::SingleErasure::rewrite_imm_Seq(), mim::Rewriter::rewrite_mut_Seq(), mim::SingleErasure::rewrite_mut_Seq(), and seq().
|
inline |
|
nodiscard |
Definition at line 492 of file world.cpp.
References axm(), mim::Axm::next(), raw_app(), type(), and mim::Def::zonk().
Yields the new body of [mut->var() -> arg]mut.
The new body may have fewer elements as mut->num_ops() according to Def::reduction_offset. E.g. a Pi has a Pi::reduction_offset of 1, and only Pi::dom will be reduced - not Pi::codom.
Definition at line 1170 of file world.cpp.
References mim::Var::binder(), mim::Def::reduction_offset(), var(), and mim::VarRewriter::VarRewriter().
Referenced by app(), and component().
As above but reduces only the i th op.
A dependent Sigma is projected while it is still being built - its later ops do not exist yet - so reducing all of them is not an option there.
Definition at line 1201 of file world.cpp.
References mim::Var::binder(), mim::Def::reduction_offset(), var(), and mim::VarRewriter::VarRewriter().
Definition at line 442 of file world.h.
References mim::Reform::infer().
Definition at line 887 of file world.cpp.
References arr(), mim::Shape::extent(), mim::Def::is_intro(), mim::Shape::isa_extents(), mim::Def::isa_imm(), prod(), seq(), mim::type_of(), mim::Def::unfold_type(), and mim::Def::zonk().
Referenced by arr(), arr(), arr(), arr(), drop(), fuse(), pack(), pack(), pack(), pack(), peel(), mim::Rewriter::rewrite_imm_Seq(), seq(), seq(), and seq().
|
inline |
|
inline |
Definition at line 114 of file world.h.
References name().
Referenced by mim::plug::gpu::phase::SplitOffKernels::rewrite_mut_Lam().
|
inline |
Definition at line 506 of file world.cpp.
References arr(), mim::Sigma::infer(), mim::Check::is_uniform(), sigma(), and mim::Def::zonk().
Referenced by cn(), cn(), ext(), fn(), fn(), fn(), mim::is_unit(), pi(), pi(), pi(), prod(), prod(), mim::plug::affine::phase::LowerFor::rewrite_imm_App(), mim::SingleErasure::rewrite_imm_Sigma(), sigma(), tuple(), type_indices(), mim::ast::Emitter::variant_str(), and World().
| void mim::World::solve_levels | ( | ) |
Defaults the level Holes of all postponed constraints that are still unknown to 0 and checks them.
Definition at line 313 of file world.cpp.
References mim::Check::alpha(), mim::default_level(), error(), mim::eval0(), and push().
|
inline |
Get the structural part of a nominal.
Definition at line 1150 of file world.cpp.
References mim::Def::blame(), mim::Def::isa_type(), name(), nom(), mim::Nom::op(), mim::type_of(), and mim::Def::zonk().
| Sym mim::World::sym | ( | const char * | s | ) |
| Sym mim::World::sym | ( | const std::string & | s | ) |
| Sym mim::World::sym | ( | std::string_view | s | ) |
Definition at line 228 of file world.cpp.
References driver().
Referenced by annex(), append_suffix(), mim::World::Annexes::attach(), mim::World::Annexes::attach(), mim::World::Annexes::attach_alias(), mim::World::Annexes::attach_alias(), dump(), mim::file_stem(), mim::optimize(), set(), mim::Def::sym(), mim::Def::sym(), mim::Def::sym(), and tuple().
|
inline |
Definition at line 516 of file world.cpp.
References mim::Check::coerce(), mim::Tuple::infer(), mim::Def::isa_imm(), sigma(), tuple(), mim::type_of(), and mim::Def::zonk().
Referenced by app(), mim::plug::clos::apply_closure(), component(), ext(), implicit_app(), insert(), mim::Rewriter::map(), mim::Rewriter::map(), mim::Rewriter::map(), prod(), prod(), raw_app(), mim::plug::affine::phase::LowerFor::rewrite_imm_App(), mim::plug::mem::phase::SEO::rewrite_imm_App(), mim::RWPhase::rewrite_imm_Tuple(), select(), seq(), tuple(), tuple(), tuple(), and mim::tuple_of_dict().
| const Def * mim::World::tuple | ( | Sym | sym | ) |
Definition at line 332 of file world.h.
References level(), lit_level(), and type().
Definition at line 235 of file world.cpp.
References mim::Def::blame(), mim::Def::isa_type(), level(), lit_level_0(), lit_level_1(), mim::type_of(), and mim::Def::zonk().
Referenced by app(), axm(), axm(), axm(), axm(), bot(), component(), ext(), implicit_holes(), inhabitant(), inj(), inj(), insert(), join(), level(), lit(), match(), mut_arr(), mut_arr(), mut_hole(), mut_pack(), mut_pi(), mut_rule(), mut_seq(), mut_sigma(), mut_sigma(), mut_variant(), nom(), proxy(), raw_app(), raw_app(), raw_app(), rule(), top(), tuple(), type(), type_indices(), type_infer_level(), and World().
|
inline |
|
inline |
Definition at line 636 of file world.h.
References type_int().
|
inline |
Definition at line 637 of file world.h.
References type_int().
|
inline |
Definition at line 638 of file world.h.
References type_int().
Referenced by mim::plug::affine::phase::LowerIndex::rewrite().
|
inline |
Definition at line 635 of file world.h.
References type_int().
|
inline |
Definition at line 623 of file world.h.
Referenced by lit_idx(), type_indices(), type_int(), and World().
Definition at line 625 of file world.h.
References app(), and type_idx().
Referenced by type_idx().
Definition at line 627 of file world.h.
References lit_nat(), and type_idx().
Referenced by type_idx().
The type of an index into shape: Idx n, a Sigma of those, or «i: r; Idx (s#i)» for a dynamic rank.
Definition at line 678 of file world.cpp.
References extract(), mut_arr(), mim::Arr::set_body(), mim::Arr::set_shape(), sigma(), type(), type_idx(), and mim::Def::zonk_mut().
Referenced by mim::Def::var_type().
|
inline |
Definition at line 326 of file world.h.
References mut_hole_level(), and type().
Referenced by mut_hole_type().
Constructs a type Idx of size 2^width.
width = 64 will be automatically converted to size 0 - the encoding for 2^64.
Definition at line 631 of file world.h.
References mim::Idx::bitwidth2size(), lit_nat(), and type_idx().
Referenced by type_i16(), type_i32(), type_i64(), and type_i8().
|
inline |
Definition at line 319 of file world.h.
Referenced by lit_level(), mut_hole_level(), type_pending(), and World().
|
inline |
|
inline |
Placeholder type of a mutable whose sort Def::finalize infers from its ops.
Definition at line 325 of file world.h.
References type_level().
Singleton term elimination.
Definition at line 1128 of file world.cpp.
References mim::Def::op(), single(), and mim::type_of().
Definition at line 392 of file world.cpp.
References inhabitant(), var(), and mim::Def::var_type().
Referenced by app(), component(), fuse(), reduce(), reduce(), mim::EtaConv::rewrite_imm_Var(), mim::Def::var(), and var().
Definition at line 1023 of file world.cpp.
References bot(), mim::Variant::infer(), and mim::Def::zonk().
|
inlinenodiscard |
Definition at line 714 of file world.h.
Referenced by mim::Rewriter::bind_new(), mim::Rewriter::bind_old(), mim::Def::collect_locals(), mim::plug::clos::phase::ClosConv::finalize(), mim::Def::free_vars(), mim::Rewriter::map(), and proxy().
| World & mim::World::verify | ( | ) |
Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.
Definition at line 1262 of file world.cpp.
References annexes(), externals(), muts(), and World().
Referenced by mim::Phase::run().
| void mim::World::watchpoint | ( | u32 | gid | ) |
| void mim::World::write | ( | ) |
Same above but file name defaults to World::name.
Definition at line 1559 of file dump.cpp.
References mim::file_stem(), and write().
| void mim::World::write | ( | const char * | file | ) |
|
inline |
Definition at line 111 of file world.h.
Referenced by mim::Def::zonk(), and mim::Def::zonk_mut().
|
staticconstexpr |
Def::arity of a Sigma is lit_nat(num_ops()) and Def::num_projs reads it straight back out, so a plain World::lit would hash-cons a Lit just to launder an integer.
Worth ~4% of an -Og Debug compile.