MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
Classes | Friends | List of all members
mim::World Class Reference

The World represents the whole program and manages creation of MimIR nodes (Defs). More...

#include <mim/world.h>

Classes

struct  Freezer
 Use to World::freeze and automatically unfreeze at the end of scope. More...
 
struct  ScopedLoc
 
struct  State
 

Public Member Functions

C'tor and D'tor
World & operator= (World)=delete
 
 World (Driver *)
 Inherits the state into the new World.
 
 World (Driver *, const State &)
 
 World (World &&other) noexcept
 
World inherit ()
 
 ~World ()
 
Getters/Setters
const State & state () const
 
const Driver & driver () const
 
Driver & driver ()
 
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 ()
 
Flags & flags ()
 Retrive compile Flags.
 
Loc
Loc get_loc () const
 
void set_loc (Loc loc={})
 
ScopedLoc push (Loc 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.

bool is_frozen () const
 
bool freeze (bool on=true) const
 Yields old frozen state.
 
Debugging Features
const auto & breakpoints ()
 
Ref gid2def (u32 gid)
 Lookup Def by gid.
 
void breakpoint (u32 gid)
 Trigger breakpoint in your debugger when creating Def with Def::gid gid.
 
World & verify ()
 Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.
 
Manage Nodes
const auto & annexes () const
 
const auto & externals () const
 
void make_external (Def *def)
 
void make_internal (Def *def)
 
Def * external (Sym name)
 Lookup by name.
 
template<class Id >
const Def * annex (Id id)
 Lookup annex by Axiom::id.
 
template<annex_without_subs id>
const Def * annex ()
 Get Axiom from a plugin.
 
const Def * register_annex (flags_t f, const Def *)
 
const Def * register_annex (plugin_t p, tag_t t, sub_t s, const Def *def)
 
Univ, Type, Var, Proxy, Infer
const Univ * univ ()
 
Ref uinc (Ref op, level_t offset=1)
 
template<Sort = Sort::Univ>
Ref umax (Defs)
 
const Type * type (Ref level)
 
const Type * type_infer_univ ()
 
template<level_t level = 0>
const Type * type ()
 
Ref var (Ref type, Def *mut)
 
const Proxy * proxy (Ref type, Defs ops, u32 index, u32 tag)
 
Infer * mut_infer (Ref type)
 
Infer * mut_infer_univ ()
 
Infer * mut_infer_type ()
 
Infer * mut_infer_entity ()
 Either a value ?:?:Type ? or a type ?:Type ?:Type ?.
 
Axiom
const Axiom * axiom (NormalizeFn n, u8 curry, u8 trip, Ref type, plugin_t p, tag_t t, sub_t s)
 
const Axiom * axiom (Ref type, plugin_t p, tag_t t, sub_t s)
 
const Axiom * axiom (NormalizeFn n, u8 curry, u8 trip, Ref type)
 Builds a fresh Axiom with descending Axiom::sub.
 
const Axiom * axiom (Ref type)
 See above.
 
Pi
const Pi * pi (Ref dom, Ref codom, bool implicit=false)
 
const Pi * pi (Defs dom, Ref codom, bool implicit=false)
 
const Pi * pi (Ref dom, Defs codom, bool implicit=false)
 
const Pi * pi (Defs dom, Defs codom, bool implicit=false)
 
Pi * mut_pi (Ref type, bool implicit=false)
 
Cn

Pi with codom mim::Bottom

const Pi * cn ()
 
const Pi * cn (Ref dom, bool implicit=false)
 
const Pi * cn (Defs dom, bool implicit=false)
 
const Pi * fn (Ref dom, Ref codom, bool implicit=false)
 
const Pi * fn (Defs dom, Ref codom, bool implicit=false)
 
const Pi * fn (Ref dom, Defs codom, bool implicit=false)
 
const Pi * fn (Defs dom, Defs codom, bool implicit=false)
 
Lam
Ref filter (Lam::Filter filter)
 
const Lam * lam (const Pi *pi, Lam::Filter f, Ref body)
 
Lam * mut_lam (const Pi *pi)
 
const Lam * con (Ref dom, Lam::Filter f, Ref body)
 
const Lam * con (Defs dom, Lam::Filter f, Ref body)
 
const Lam * lam (Ref dom, Ref codom, Lam::Filter f, Ref body)
 
const Lam * lam (Defs dom, Ref codom, Lam::Filter f, Ref body)
 
const Lam * lam (Ref dom, Defs codom, Lam::Filter f, Ref body)
 
const Lam * lam (Defs dom, Defs codom, Lam::Filter f, Ref body)
 
const Lam * fun (Ref dom, Ref codom, Lam::Filter f, Ref body)
 
const Lam * fun (Defs dom, Ref codom, Lam::Filter f, Ref body)
 
const Lam * fun (Ref dom, Defs codom, Lam::Filter f, Ref body)
 
const Lam * fun (Defs dom, Defs codom, Lam::Filter f, Ref body)
 
Lam * mut_con (Ref dom)
 
Lam * mut_con (Defs dom)
 
Lam * mut_lam (Ref dom, Ref codom)
 
Lam * mut_lam (Defs dom, Ref codom)
 
Lam * mut_lam (Ref dom, Defs codom)
 
Lam * mut_lam (Defs dom, Defs codom)
 
Lam * mut_fun (Ref dom, Ref codom)
 
Lam * mut_fun (Defs dom, Ref codom)
 
Lam * mut_fun (Ref dom, Defs codom)
 
Lam * mut_fun (Defs dom, Defs codom)
 
Lam * exit ()
 Used as a dummy exit node within Scope.
 
App
template<bool Normalize = true>
Ref app (Ref callee, Ref arg)
 
template<bool Normalize = true>
Ref app (Ref callee, Defs args)
 
Ref raw_app (const Axiom *axiom, u8 curry, u8 trip, Ref type, Ref callee, Ref arg)
 
Ref raw_app (Ref type, Ref callee, Ref arg)
 
Ref raw_app (Ref type, Ref callee, Defs args)
 
Sigma
Sigma * mut_sigma (Ref type, size_t size)
 
template<level_t level = 0>
Sigma * mut_sigma (size_t size)
 A *mut*able Sigma of type level.
 
Ref sigma (Defs ops)
 
const Sigma * sigma ()
 The unit type within Type 0.
 
Arr
Arr * mut_arr (Ref type)
 
template<level_t level = 0>
Arr * mut_arr ()
 
Ref arr (Ref shape, Ref body)
 
Ref arr (Defs shape, Ref body)
 
Ref arr (u64 n, Ref body)
 
Ref arr (View< u64 > shape, Ref body)
 
Ref arr_unsafe (Ref body)
 
Tuple
Ref tuple (Defs ops)
 
Ref tuple (Ref type, Defs ops)
 Ascribes type to this tuple - needed for dependently typed and mutable Sigmas.
 
const Tuple * tuple ()
 the unit value of type []
 
Ref tuple (Sym sym)
 Converts sym to a tuple of type '«n; I8»'.
 
Pack
Pack * mut_pack (Ref type)
 
Ref pack (Ref arity, Ref body)
 
Ref pack (Defs shape, Ref body)
 
Ref pack (u64 n, Ref body)
 
Ref pack (View< u64 > shape, Ref body)
 
Extract
See also
core::extract_unsafe
Ref extract (Ref d, Ref i)
 
Ref extract (Ref d, u64 a, u64 i)
 
Ref extract (Ref d, u64 i)
 
Ref select (Ref cond, Ref t, Ref f)
 Builds (f, t)#cond.
 
Insert
See also
core::insert_unsafe
Ref insert (Ref d, Ref i, Ref val)
 
Ref insert (Ref d, u64 a, u64 i, Ref val)
 
Ref insert (Ref d, u64 i, Ref val)
 
Lit
const Lit * lit (Ref type, u64 val)
 
const Lit * lit_univ (u64 level)
 
const Lit * lit_univ_0 ()
 
const Lit * lit_univ_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_0_1 ()
 
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.
 
template<class I >
const Lit * lit_idx (I 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_i2 (u8 val)
 
const Lit * lit_i4 (u8 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 ()
 
Lattice
template<bool Up>
Ref ext (Ref type)
 
Ref bot (Ref type)
 
Ref top (Ref type)
 
Ref type_bot ()
 
Ref type_top ()
 
Ref top_nat ()
 
template<bool Up>
TBound< Up > * mut_bound (Ref type, size_t size)
 
template<bool Up, level_t l = 0>
TBound< Up > * mut_bound (size_t size)
 A *mut*able Bound of Type level.
 
template<bool Up>
Ref bound (Defs ops)
 
Join * mut_join (Ref type, size_t size)
 
Meet * mut_meet (Ref type, size_t size)
 
template<level_t l = 0>
Join * mut_join (size_t size)
 
template<level_t l = 0>
Meet * mut_meet (size_t size)
 
Ref join (Defs ops)
 
Ref meet (Defs ops)
 
Ref ac (Ref type, Defs ops)
 
Ref ac (Defs ops)
 Infers the type using an immutable Meet.
 
Ref vel (Ref type, Ref value)
 
Ref pick (Ref type, Ref value)
 
Ref test (Ref value, Ref probe, Ref match, Ref clash)
 
Ref uniq (Ref inhabitant)
 
Globals
Deprecated
Will be removed.
Global * global (Ref type, bool is_mutable=true)
 
Types
const Nat * type_nat ()
 
const Idx * type_idx ()
 
Ref type_idx (Ref size)
 
Ref type_idx (nat_t size)
 
Ref type_int (nat_t width)
 Constructs a type Idx of size $2^width$.
 
Ref type_bool ()
 
Ref type_i1 ()
 
Ref type_i2 ()
 
Ref type_i4 ()
 
Ref type_i8 ()
 
Ref type_i16 ()
 
Ref type_i32 ()
 
Ref type_i64 ()
 
Cope with implicit Arguments
template<bool Normalize = true>
Ref implicit_app (Ref callee, Ref arg)
 
template<bool Normalize = true>
Ref implicit_app (Ref callee, Defs args)
 
template<bool Normalize = true>
Ref implicit_app (Ref callee, nat_t arg)
 
template<bool Normalize = true, class E >
requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>
Ref implicit_app (Ref callee, E arg)
 
template<class Id , bool Normalize = true, class... Args>
const Def * call (Id id, Args &&... args)
 Complete curried call of annexes obeying implicits.
 
template<class Id , bool Normalize = true, class... Args>
const Def * call (Args &&... args)
 
Vars & Muts

Manges sets of Vars and Muts.

auto & vars ()
 
auto & muts ()
 
const auto & vars () const
 
const auto & muts () const
 
dump/log
Log & log ()
 
void dummy ()
 
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 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

Dumps DOT to os.

void dot (std::ostream &os, bool annexes=false, bool types=false) const
 
void dot (const char *file=nullptr, bool annexes=false, bool types=false) const
 Same as above but write to file or std::cout if file is nullptr.
 

Friends

void swap (World &w1, World &w2) noexcept
 
DefVec Def::reduce (Ref)
 

Detailed Description

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.

Definition at line 33 of file world.h.

Constructor & Destructor Documentation

◆ World() [1/3]

mim::World::World ( Driver * driver)
explicit

Inherits the state into the new World.

Definition at line 62 of file world.cpp.

Referenced by inherit().

◆ World() [2/3]

mim::World::World ( Driver * driver,
const State & state )

Definition at line 37 of file world.cpp.

References cn(), insert(), lit_idx(), lit_nat(), lit_univ(), lit_univ_0(), lit_univ_1(), mut_lam(), pi(), mim::Lam::set(), sigma(), sym(), type(), type_bot(), type_idx(), and type_nat().

◆ World() [3/3]

mim::World::World ( World && other)
inlinenoexcept

Definition at line 69 of file world.h.

References swap.

◆ ~World()

mim::World::~World ( )

Definition at line 65 of file world.cpp.

Member Function Documentation

◆ ac() [1/2]

Ref mim::World::ac ( Defs ops)

Infers the type using an immutable Meet.

Definition at line 506 of file world.cpp.

References ac(), and umax().

◆ ac() [2/2]

Ref mim::World::ac ( Ref type,
Defs ops )

Definition at line 496 of file world.cpp.

References meet(), and type().

Referenced by ac().

◆ annex() [1/2]

template<annex_without_subs id>
const Def * mim::World::annex ( )
inline

Get Axiom from a plugin.

Can be used to get an Axiom without sub-tags. E.g. use w.annex<mem::M>(); to get the mem.M Axiom.

Definition at line 194 of file world.h.

References annex(), and mim::Annex::Base.

Referenced by annex(), call(), call(), dot(), and verify().

◆ annex() [2/2]

template<class Id >
const Def * mim::World::annex ( Id id)
inline

Lookup annex by Axiom::id.

Definition at line 185 of file world.h.

References mim::Annex::demangle(), driver(), mim::error(), and flags().

Referenced by mim::plug::matrix::LowerMatrixMediumLevel::rewrite_().

◆ annexes()

const auto & mim::World::annexes ( ) const
inline

Definition at line 167 of file world.h.

Referenced by dot(), dot(), and verify().

◆ app() [1/2]

template<bool Normalize = true>
Ref mim::World::app ( Ref callee,
Defs args )
inline

Definition at line 313 of file world.h.

References app(), and tuple().

◆ app() [2/2]

template<bool Normalize>
Ref mim::World::app ( Ref callee,
Ref arg )

Definition at line 170 of file world.cpp.

References mim::Checker::assignable(), axiom(), mim::Lam::body(), DLOG, mim::Pi::dom(), mim::Error::error(), mim::Lam::filter(), mim::Axiom::get(), mim::Def::is_set(), mim::Def::isa_imm(), mim::Def::isa_mut(), lam(), lit_ff(), lit_tt(), mim::Def::loc(), mim::Axiom::normalizer(), mim::Error::note(), pi(), raw_app(), mim::Pi::reduce(), mim::Rewriter::rewrite(), mim::Axiom::Trip_End, mim::Def::type(), type(), mim::Def::var(), and mim::Def::zonk().

Referenced by app(), mim::plug::autodiff::AutoDiffEval::augment_app(), mim::plug::autodiff::AutoDiffEval::augment_pack(), implicit_app(), mim::plug::autodiff::op_sum(), mim::LamSpec::rewrite(), mim::plug::affine::LowerFor::rewrite(), mim::plug::direct::DS2CPS::rewrite(), mim::plug::mem::CopyProp::rewrite(), mim::TailRecElim::rewrite(), mim::plug::matrix::LowerMatrixHighLevelMapRed::rewrite_(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), and type_idx().

◆ append_suffix()

Sym mim::World::append_suffix ( Sym name,
std::string suffix )

Appends a suffix or an increasing number if the suffix already exists.

Definition at line 531 of file world.cpp.

References name(), and sym().

◆ arr() [1/4]

Ref mim::World::arr ( Defs shape,
Ref body )

Definition at line 439 of file world.cpp.

References arr().

◆ arr() [2/4]

Ref mim::World::arr ( Ref shape,
Ref body )

Definition at line 392 of file world.cpp.

References arr(), mim::error(), extract(), mim::Lit::isa(), mim::Def::ops(), pack(), sigma(), tuple(), and mim::Def::unfold_type().

Referenced by arr(), arr(), arr(), arr_unsafe(), ext(), extract(), pack(), and sigma().

◆ arr() [3/4]

Ref mim::World::arr ( u64 n,
Ref body )
inline

Definition at line 334 of file world.h.

References arr(), and lit_nat().

Referenced by arr().

◆ arr() [4/4]

Ref mim::World::arr ( View< u64 > shape,
Ref body )
inline

Definition at line 335 of file world.h.

References arr().

◆ arr_unsafe()

Ref mim::World::arr_unsafe ( Ref body)
inline

Definition at line 338 of file world.h.

References arr(), and top_nat().

◆ axiom() [1/4]

const Axiom * mim::World::axiom ( NormalizeFn n,
u8 curry,
u8 trip,
Ref type )
inline

Builds a fresh Axiom with descending Axiom::sub.

This is useful during testing to come up with some entitiy of a specific type. It uses the plugin Axiom::Global_Plugin and starts with 0 for Axiom::sub and counts up from there. The Axiom::tag is set to 0 and the Axiom::normalizer to nullptr.

Definition at line 246 of file world.h.

References axiom(), mim::World::State::POD::curr_sub, mim::Annex::Global_Plugin, mim::World::State::pod, and type().

◆ axiom() [2/4]

const Axiom * mim::World::axiom ( NormalizeFn n,
u8 curry,
u8 trip,
Ref type,
plugin_t p,
tag_t t,
sub_t s )
inline

Definition at line 237 of file world.h.

References type().

Referenced by app(), axiom(), raw_app(), and raw_app().

◆ axiom() [3/4]

const Axiom * mim::World::axiom ( Ref type)
inline

See above.

Definition at line 249 of file world.h.

References axiom(), and type().

Referenced by axiom().

◆ axiom() [4/4]

const Axiom * mim::World::axiom ( Ref type,
plugin_t p,
tag_t t,
sub_t s )
inline

Definition at line 240 of file world.h.

References axiom(), and type().

Referenced by axiom().

◆ bot()

Ref mim::World::bot ( Ref type)
inline

Definition at line 434 of file world.h.

References ext(), and type().

Referenced by mim::plug::autodiff::AutoDiffZeroCleanup::rewrite(), and mim::plug::clos::LowerTypedClos::start().

◆ bound()

template<bool Up>
Ref mim::World::bound ( Defs ops)

Definition at line 472 of file world.cpp.

References ext(), and umax().

Referenced by join(), and meet().

◆ breakpoint()

void mim::World::breakpoint ( u32 gid)

Trigger breakpoint in your debugger when creating Def with Def::gid gid.

Definition at line 557 of file world.cpp.

References mim::World::State::breakpoints.

Referenced by main().

◆ breakpoints()

const auto & mim::World::breakpoints ( )
inline

Definition at line 154 of file world.h.

References mim::World::State::breakpoints.

◆ call() [1/2]

template<class Id , bool Normalize = true, class... Args>
const Def * mim::World::call ( Args &&... args)
inline

Definition at line 508 of file world.h.

References annex().

◆ call() [2/2]

template<class Id , bool Normalize = true, class... Args>
const Def * mim::World::call ( Id id,
Args &&... args )
inline

Complete curried call of annexes obeying implicits.

Definition at line 507 of file world.h.

References annex().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_lam(), mim::plug::clos::ClosConvPrep::eta_wrap(), mim::plug::compile::normalize_single_pass_phase(), mim::plug::affine::LowerFor::rewrite(), mim::plug::clos::LowerTypedClosPrep::rewrite(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), and mim::plug::matrix::LowerMatrixLowLevel::rewrite_imm().

◆ cn() [1/3]

const Pi * mim::World::cn ( )
inline

Definition at line 267 of file world.h.

References cn(), and sigma().

Referenced by cn(), con(), con(), fn(), mut_con(), mut_con(), and World().

◆ cn() [2/3]

const Pi * mim::World::cn ( Defs dom,
bool implicit = false )
inline

Definition at line 269 of file world.h.

References cn(), and sigma().

Referenced by cn().

◆ cn() [3/3]

const Pi * mim::World::cn ( Ref dom,
bool implicit = false )
inline

Definition at line 268 of file world.h.

References pi(), and type_bot().

◆ con() [1/2]

const Lam * mim::World::con ( Defs dom,
Lam::Filter f,
Ref body )
inline

Definition at line 287 of file world.h.

References cn(), and filter().

◆ con() [2/2]

const Lam * mim::World::con ( Ref dom,
Lam::Filter f,
Ref body )
inline

Definition at line 286 of file world.h.

References cn(), and filter().

◆ curr_gid()

u32 mim::World::curr_gid ( ) const
inline

Manage global identifier - a unique number for each Def.

Definition at line 89 of file world.h.

References mim::World::State::POD::curr_gid, and mim::World::State::pod.

◆ debug_dump()

void mim::World::debug_dump ( )

Dump in Debug build if World::log::level is Log::Level::Debug.

Definition at line 491 of file dump.cpp.

References mim::Log::Debug.

Referenced by mim::plug::autodiff::AutoDiffEval::augment_app(), DebugDump::prepare(), and mim::PassMan::run().

◆ dot() [1/2]

void mim::World::dot ( const char * file = nullptr,
bool annexes = false,
bool types = false ) const

Same as above but write to file or std::cout if file is nullptr.

Definition at line 134 of file dot.cpp.

References annexes(), and dot().

◆ dot() [2/2]

void mim::World::dot ( std::ostream & os,
bool annexes = false,
bool types = false ) const
Parameters
osOutput stream
annexesIf true, include all annexes - even if unused.
typesFollow type dependencies?

Definition at line 143 of file dot.cpp.

References annex(), annexes(), dot(), external(), and externals().

Referenced by dot(), dot(), and main().

◆ driver() [1/2]

Driver & mim::World::driver ( )
inline

Definition at line 82 of file world.h.

◆ driver() [2/2]

const Driver & mim::World::driver ( ) const
inline

Definition at line 81 of file world.h.

Referenced by annex(), mim::ast::AST::driver(), mim::ast::Emitter::driver(), flags(), inherit(), mim::ast::load_plugins(), log(), mim::optimize(), register_annex(), sym(), sym(), and sym().

◆ dummy()

void mim::World::dummy ( )
inline

Definition at line 524 of file world.h.

◆ dump() [1/2]

void mim::World::dump ( )

Dump to std::cout.

Definition at line 489 of file dump.cpp.

◆ dump() [2/2]

void mim::World::dump ( std::ostream & os)

Dump to os.

Definition at line 469 of file dump.cpp.

References assertf, and mim::print().

Referenced by main().

◆ exit()

Lam * mim::World::exit ( )
inline

Used as a dummy exit node within Scope.

Definition at line 307 of file world.h.

◆ ext()

template<bool Up>
Ref mim::World::ext ( Ref type)

Definition at line 465 of file world.cpp.

References arr(), ext(), mim::Def::num_ops(), pack(), sigma(), tuple(), and type().

Referenced by bot(), bound(), ext(), and top().

◆ external()

Def * mim::World::external ( Sym name)
inline

Lookup by name.

Definition at line 182 of file world.h.

References mim::lookup(), and name().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_(), dot(), mim::optimize(), and mim::plug::matrix::LowerMatrixHighLevelMapRed::rewrite_().

◆ externals()

const auto & mim::World::externals ( ) const
inline

Definition at line 168 of file world.h.

Referenced by dot(), mim::optimize(), mim::PassMan::run(), mim::RWPhase::start(), and verify().

◆ extract() [1/3]

Ref mim::World::extract ( Ref d,
Ref i )

Definition at line 286 of file world.cpp.

References mim::Checker::alpha(), mim::Def::arity(), arr(), mim::Lit::as(), mim::Def::as_lit_arity(), mim::error(), extract(), insert(), mim::Idx::isa(), mim::Lit::isa(), mim::Def::isa_mut(), mim::Def::loc(), mut_sigma(), mim::Def::num_ops(), mim::Def::op(), mim::Def::ops(), pack(), mim::Def::reduce(), mim::Rewriter::rewrite(), sigma(), tuple(), mim::Def::type(), type(), mim::Def::var(), and WLOG.

Referenced by arr(), mim::plug::autodiff::AutoDiffEval::augment_extract(), extract(), select(), and tuple().

◆ extract() [2/3]

Ref mim::World::extract ( Ref d,
u64 a,
u64 i )
inline

Definition at line 365 of file world.h.

References extract(), and lit_idx().

Referenced by extract().

◆ extract() [3/3]

Ref mim::World::extract ( Ref d,
u64 i )
inline

Definition at line 366 of file world.h.

References extract().

Referenced by extract().

◆ filter()

Ref mim::World::filter ( Lam::Filter filter)
inline

Definition at line 279 of file world.h.

References filter(), std::get(), and lit_bool().

Referenced by con(), con(), filter(), fun(), fun(), fun(), fun(), lam(), lam(), lam(), lam(), and lam().

◆ flags()

Flags & mim::World::flags ( )

Retrive compile Flags.

Definition at line 74 of file world.cpp.

References driver(), and mim::Driver::flags().

Referenced by annex(), insert(), and mim::Def::num_tprojs().

◆ fn() [1/4]

const Pi * mim::World::fn ( Defs dom,
Defs codom,
bool implicit = false )
inline

Definition at line 273 of file world.h.

References fn(), and sigma().

Referenced by fn().

◆ fn() [2/4]

const Pi * mim::World::fn ( Defs dom,
Ref codom,
bool implicit = false )
inline

Definition at line 271 of file world.h.

References fn(), and sigma().

Referenced by fn().

◆ fn() [3/4]

const Pi * mim::World::fn ( Ref dom,
Defs codom,
bool implicit = false )
inline

Definition at line 272 of file world.h.

References fn(), and sigma().

Referenced by fn().

◆ fn() [4/4]

const Pi * mim::World::fn ( Ref dom,
Ref codom,
bool implicit = false )
inline

Definition at line 270 of file world.h.

References cn().

Referenced by fun(), fun(), fun(), fun(), mut_fun(), mut_fun(), mut_fun(), and mut_fun().

◆ freeze()

bool mim::World::freeze ( bool on = true) const
inline

Yields old frozen state.

Definition at line 133 of file world.h.

References mim::World::State::POD::frozen, and mim::World::State::pod.

Referenced by mim::World::Freezer::~Freezer().

◆ fun() [1/4]

const Lam * mim::World::fun ( Defs dom,
Defs codom,
Lam::Filter f,
Ref body )
inline

Definition at line 295 of file world.h.

References filter(), and fn().

◆ fun() [2/4]

const Lam * mim::World::fun ( Defs dom,
Ref codom,
Lam::Filter f,
Ref body )
inline

Definition at line 293 of file world.h.

References filter(), and fn().

◆ fun() [3/4]

const Lam * mim::World::fun ( Ref dom,
Defs codom,
Lam::Filter f,
Ref body )
inline

Definition at line 294 of file world.h.

References filter(), and fn().

◆ fun() [4/4]

const Lam * mim::World::fun ( Ref dom,
Ref codom,
Lam::Filter f,
Ref body )
inline

Definition at line 292 of file world.h.

References filter(), and fn().

◆ get_loc()

Loc mim::World::get_loc ( ) const
inline

Definition at line 109 of file world.h.

References mim::World::State::POD::loc, and mim::World::State::pod.

Referenced by push().

◆ gid2def()

Ref mim::World::gid2def ( u32 gid)

Lookup Def by gid.

Definition at line 559 of file world.cpp.

◆ global()

Global * mim::World::global ( Ref type,
bool is_mutable = true )
inline

Definition at line 461 of file world.h.

References insert(), and type().

◆ implicit_app() [1/4]

template<bool Normalize = true>
Ref mim::World::implicit_app ( Ref callee,
Defs args )
inline

Definition at line 493 of file world.h.

References implicit_app(), and tuple().

◆ implicit_app() [2/4]

template<bool Normalize = true, class E >
requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>
Ref mim::World::implicit_app ( Ref callee,
E arg )
inline

Definition at line 500 of file world.h.

References implicit_app(), and lit_nat().

◆ implicit_app() [3/4]

template<bool Normalize = true>
Ref mim::World::implicit_app ( Ref callee,
nat_t arg )
inline

Definition at line 496 of file world.h.

References implicit_app(), and lit_nat().

◆ implicit_app() [4/4]

template<bool Normalize>
Ref mim::World::implicit_app ( Ref callee,
Ref arg )

Places Infer arguments as demanded by Pi::implicit and then apps arg.

Definition at line 165 of file world.cpp.

References app(), mim::Pi::dom(), mim::Pi::isa_implicit(), mut_infer(), pi(), and mim::Def::type().

Referenced by implicit_app(), implicit_app(), and implicit_app().

◆ inherit()

World mim::World::inherit ( )
inline

Definition at line 73 of file world.h.

References driver(), state(), and World().

Referenced by mim::Cleanup::start().

◆ insert() [1/3]

Ref mim::World::insert ( Ref d,
Ref i,
Ref val )

Definition at line 348 of file world.cpp.

References mim::Checker::alpha(), mim::Def::arity(), mim::Checker::assignable(), mim::error(), mim::Error::error(), flags(), insert(), mim::Idx::isa(), mim::Lit::isa(), mim::Def::isa_lit_arity(), mim::Def::loc(), mim::Error::note(), pack(), mim::Def::proj(), tuple(), mim::Def::type(), and type().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_extract(), extract(), global(), insert(), mut_arr(), mut_bound(), mut_con(), mut_con(), mut_fun(), mut_fun(), mut_fun(), mut_fun(), mut_infer(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mut_pack(), mut_pi(), mut_sigma(), and World().

◆ insert() [2/3]

Ref mim::World::insert ( Ref d,
u64 a,
u64 i,
Ref val )
inline

Definition at line 377 of file world.h.

References insert(), and lit_idx().

Referenced by insert().

◆ insert() [3/3]

Ref mim::World::insert ( Ref d,
u64 i,
Ref val )
inline

Definition at line 378 of file world.h.

References insert().

Referenced by insert().

◆ is_frozen()

bool mim::World::is_frozen ( ) const
inline

Definition at line 130 of file world.h.

References mim::World::State::POD::frozen, and mim::World::State::pod.

◆ join()

Ref mim::World::join ( Defs ops)
inline

Definition at line 447 of file world.h.

References bound().

Referenced by test().

◆ lam() [1/5]

const Lam * mim::World::lam ( const Pi * pi,
Lam::Filter f,
Ref body )
inline

Definition at line 283 of file world.h.

References filter(), and pi().

Referenced by app().

◆ lam() [2/5]

const Lam * mim::World::lam ( Defs dom,
Defs codom,
Lam::Filter f,
Ref body )
inline

Definition at line 291 of file world.h.

References filter(), and pi().

◆ lam() [3/5]

const Lam * mim::World::lam ( Defs dom,
Ref codom,
Lam::Filter f,
Ref body )
inline

Definition at line 289 of file world.h.

References filter(), and pi().

◆ lam() [4/5]

const Lam * mim::World::lam ( Ref dom,
Defs codom,
Lam::Filter f,
Ref body )
inline

Definition at line 290 of file world.h.

References filter(), and pi().

◆ lam() [5/5]

const Lam * mim::World::lam ( Ref dom,
Ref codom,
Lam::Filter f,
Ref body )
inline

Definition at line 288 of file world.h.

References filter(), and pi().

◆ lit()

const Lit * mim::World::lit ( Ref type,
u64 val )

Definition at line 449 of file world.cpp.

References mim::error(), mim::Idx::isa(), mim::Lit::isa(), mim::Def::loc(), and type().

Referenced by lit_idx(), lit_nat(), lit_univ(), and mim::plug::demo::normalize_const().

◆ lit_0_1()

const Lit * mim::World::lit_0_1 ( )
inline

Definition at line 391 of file world.h.

Referenced by var().

◆ lit_bool()

const Lit * mim::World::lit_bool ( bool val)
inline

Definition at line 424 of file world.h.

Referenced by filter().

◆ lit_ff()

const Lit * mim::World::lit_ff ( )
inline

Definition at line 425 of file world.h.

Referenced by app().

◆ lit_i1() [1/2]

const Lit * mim::World::lit_i1 ( )
inline

Definition at line 393 of file world.h.

References mim::Idx::bitwidth2size(), and lit_nat().

◆ lit_i1() [2/2]

const Lit * mim::World::lit_i1 ( bool val)
inline

Definition at line 410 of file world.h.

References lit_int().

◆ lit_i16() [1/2]

const Lit * mim::World::lit_i16 ( )
inline

Definition at line 395 of file world.h.

References mim::Idx::bitwidth2size(), and lit_nat().

◆ lit_i16() [2/2]

const Lit * mim::World::lit_i16 ( u16 val)
inline

Definition at line 414 of file world.h.

References lit_int().

◆ lit_i2()

const Lit * mim::World::lit_i2 ( u8 val)
inline

Definition at line 411 of file world.h.

References lit_int().

◆ lit_i32() [1/2]

const Lit * mim::World::lit_i32 ( )
inline

Definition at line 396 of file world.h.

References mim::Idx::bitwidth2size(), and lit_nat().

◆ lit_i32() [2/2]

const Lit * mim::World::lit_i32 ( u32 val)
inline

Definition at line 415 of file world.h.

References lit_int().

◆ lit_i4()

const Lit * mim::World::lit_i4 ( u8 val)
inline

Definition at line 412 of file world.h.

References lit_int().

◆ lit_i64() [1/2]

const Lit * mim::World::lit_i64 ( )
inline

Definition at line 397 of file world.h.

References mim::Idx::bitwidth2size(), and lit_nat().

Referenced by mim::plug::mem::op_lea_unsafe().

◆ lit_i64() [2/2]

const Lit * mim::World::lit_i64 ( u64 val)
inline

Definition at line 416 of file world.h.

References lit_int().

◆ lit_i8() [1/2]

const Lit * mim::World::lit_i8 ( )
inline

Definition at line 394 of file world.h.

References mim::Idx::bitwidth2size(), and lit_nat().

Referenced by tuple().

◆ lit_i8() [2/2]

const Lit * mim::World::lit_i8 ( u8 val)
inline

Definition at line 413 of file world.h.

References lit_int().

◆ lit_idx() [1/2]

template<class I >
const Lit * mim::World::lit_idx ( I val)
inline

Definition at line 402 of file world.h.

References mim::Idx::bitwidth2size(), and lit_idx().

◆ lit_idx() [2/2]

const Lit * mim::World::lit_idx ( nat_t size,
u64 val )
inline

Constructs a Lit of type Idx of size size.

Note
size = 0 means 2^64.

Definition at line 400 of file world.h.

References lit(), and type_idx().

Referenced by extract(), insert(), lit_idx(), lit_idx_mod(), lit_int(), and World().

◆ lit_idx_mod()

const Lit * mim::World::lit_idx_mod ( nat_t mod,
u64 val )
inline

Constructs a Lit of type Idx of size mod.

The value val will be adjusted modulo mod.

Note
mod == 0 is the special case for $2^64$ and no modulo will be performed on val.

Definition at line 422 of file world.h.

References lit_idx().

◆ lit_int()

const Lit * mim::World::lit_int ( nat_t width,
u64 val )
inline

Constructs a Lit of type Idx of size $2^width$.

val = 64 will be automatically converted to size 0 - the encoding for $2^64$.

Definition at line 409 of file world.h.

References mim::Idx::bitwidth2size(), and lit_idx().

Referenced by lit_i1(), lit_i16(), lit_i2(), lit_i32(), lit_i4(), lit_i64(), and lit_i8().

◆ lit_nat()

const Lit * mim::World::lit_nat ( nat_t a)
inline

Definition at line 387 of file world.h.

References lit(), and type_nat().

Referenced by mim::Def::arity(), arr(), implicit_app(), implicit_app(), lit_i1(), lit_i16(), lit_i32(), lit_i64(), lit_i8(), mim::plug::refly::normalize_gid(), pack(), type_idx(), type_int(), and World().

◆ lit_nat_0()

const Lit * mim::World::lit_nat_0 ( )
inline

Definition at line 388 of file world.h.

Referenced by mim::plug::matrix::LowerMatrixLowLevel::rewrite_imm(), and mim::Pack::shape().

◆ lit_nat_1()

const Lit * mim::World::lit_nat_1 ( )
inline

Definition at line 389 of file world.h.

Referenced by mim::Def::arity(), and mim::Pack::shape().

◆ lit_nat_max()

const Lit * mim::World::lit_nat_max ( )
inline

Definition at line 390 of file world.h.

◆ lit_tt()

const Lit * mim::World::lit_tt ( )
inline

Definition at line 426 of file world.h.

Referenced by app(), and mim::plug::core::normalize_ncmp().

◆ lit_univ()

const Lit * mim::World::lit_univ ( u64 level)
inline

Definition at line 384 of file world.h.

References lit(), and univ().

Referenced by type(), uinc(), umax(), and World().

◆ lit_univ_0()

const Lit * mim::World::lit_univ_0 ( )
inline

Definition at line 385 of file world.h.

Referenced by World().

◆ lit_univ_1()

const Lit * mim::World::lit_univ_1 ( )
inline

Definition at line 386 of file world.h.

Referenced by World().

◆ log()

Log & mim::World::log ( )

Definition at line 73 of file world.cpp.

References driver(), and mim::Driver::log().

◆ make_external()

void mim::World::make_external ( Def * def)
inline

Definition at line 169 of file world.h.

References mim::assert_emplace(), mim::Def::is_closed(), mim::Def::is_external(), and mim::Def::sym().

Referenced by mim::Def::make_external().

◆ make_internal()

void mim::World::make_internal ( Def * def)
inline

Definition at line 175 of file world.h.

References mim::Def::is_external(), and mim::Def::sym().

Referenced by mim::Def::make_internal().

◆ meet()

Ref mim::World::meet ( Defs ops)
inline

Definition at line 448 of file world.h.

References bound().

Referenced by ac().

◆ mut_arr() [1/2]

template<level_t level = 0>
Arr * mim::World::mut_arr ( )
inline

Definition at line 331 of file world.h.

References mut_arr(), and type().

Referenced by mut_arr().

◆ mut_arr() [2/2]

Arr * mim::World::mut_arr ( Ref type)
inline

Definition at line 330 of file world.h.

References insert(), and type().

◆ mut_bound() [1/2]

template<bool Up>
TBound< Up > * mim::World::mut_bound ( Ref type,
size_t size )
inline

Definition at line 439 of file world.h.

References insert(), and type().

Referenced by mut_bound(), mut_join(), and mut_meet().

◆ mut_bound() [2/2]

template<bool Up, level_t l = 0>
TBound< Up > * mim::World::mut_bound ( size_t size)
inline

A *mut*able Bound of Type level.

Definition at line 441 of file world.h.

References mut_bound(), and type().

◆ mut_con() [1/2]

Lam * mim::World::mut_con ( Defs dom)
inline

Definition at line 297 of file world.h.

References cn(), and insert().

◆ mut_con() [2/2]

Lam * mim::World::mut_con ( Ref dom)
inline

Definition at line 296 of file world.h.

References cn(), and insert().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_lam(), and mim::plug::affine::LowerFor::rewrite().

◆ mut_fun() [1/4]

Lam * mim::World::mut_fun ( Defs dom,
Defs codom )
inline

Definition at line 305 of file world.h.

References fn(), and insert().

◆ mut_fun() [2/4]

Lam * mim::World::mut_fun ( Defs dom,
Ref codom )
inline

Definition at line 303 of file world.h.

References fn(), and insert().

◆ mut_fun() [3/4]

Lam * mim::World::mut_fun ( Ref dom,
Defs codom )
inline

Definition at line 304 of file world.h.

References fn(), and insert().

◆ mut_fun() [4/4]

Lam * mim::World::mut_fun ( Ref dom,
Ref codom )
inline

Definition at line 302 of file world.h.

References fn(), and insert().

Referenced by mim::plug::matrix::LowerMatrixMediumLevel::rewrite_().

◆ mut_infer()

Infer * mim::World::mut_infer ( Ref type)
inline

Definition at line 222 of file world.h.

References insert(), and type().

Referenced by implicit_app(), mut_infer_entity(), mut_infer_type(), mut_infer_univ(), and mim::Infer::tuplefy().

◆ mut_infer_entity()

Infer * mim::World::mut_infer_entity ( )
inline

Either a value ?:?:Type ? or a type ?:Type ?:Type ?.

Definition at line 227 of file world.h.

References mut_infer(), and type_infer_univ().

◆ mut_infer_type()

Infer * mim::World::mut_infer_type ( )
inline

Definition at line 224 of file world.h.

References mut_infer(), and type_infer_univ().

◆ mut_infer_univ()

Infer * mim::World::mut_infer_univ ( )
inline

Definition at line 223 of file world.h.

References mut_infer(), and univ().

Referenced by type_infer_univ().

◆ mut_join() [1/2]

Join * mim::World::mut_join ( Ref type,
size_t size )
inline

Definition at line 443 of file world.h.

References mut_bound(), and type().

◆ mut_join() [2/2]

template<level_t l = 0>
Join * mim::World::mut_join ( size_t size)
inline

Definition at line 445 of file world.h.

References mut_join(), and type().

Referenced by mut_join().

◆ mut_lam() [1/5]

Lam * mim::World::mut_lam ( const Pi * pi)
inline

Definition at line 284 of file world.h.

References insert(), and pi().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_app(), mim::plug::autodiff::AutoDiffEval::augment_extract(), mim::plug::autodiff::AutoDiffEval::augment_pack(), mim::plug::autodiff::AutoDiffEval::augment_tuple(), mim::plug::autodiff::AutoDiffEval::derive_(), mim::RetWrap::enter(), and World().

◆ mut_lam() [2/5]

Lam * mim::World::mut_lam ( Defs dom,
Defs codom )
inline

Definition at line 301 of file world.h.

References insert(), and pi().

◆ mut_lam() [3/5]

Lam * mim::World::mut_lam ( Defs dom,
Ref codom )
inline

Definition at line 299 of file world.h.

References insert(), and pi().

◆ mut_lam() [4/5]

Lam * mim::World::mut_lam ( Ref dom,
Defs codom )
inline

Definition at line 300 of file world.h.

References insert(), and pi().

◆ mut_lam() [5/5]

Lam * mim::World::mut_lam ( Ref dom,
Ref codom )
inline

Definition at line 298 of file world.h.

References insert(), and pi().

◆ mut_meet() [1/2]

Meet * mim::World::mut_meet ( Ref type,
size_t size )
inline

Definition at line 444 of file world.h.

References mut_bound(), and type().

◆ mut_meet() [2/2]

template<level_t l = 0>
Meet * mim::World::mut_meet ( size_t size)
inline

Definition at line 446 of file world.h.

References mut_meet(), and type().

Referenced by mut_meet().

◆ mut_pack()

Pack * mim::World::mut_pack ( Ref type)
inline

Definition at line 352 of file world.h.

References insert(), and type().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_pack().

◆ mut_pi()

Pi * mim::World::mut_pi ( Ref type,
bool implicit = false )
inline

Definition at line 259 of file world.h.

References insert(), and type().

◆ mut_sigma() [1/2]

Sigma * mim::World::mut_sigma ( Ref type,
size_t size )
inline

Definition at line 321 of file world.h.

References insert(), and type().

Referenced by extract().

◆ mut_sigma() [2/2]

template<level_t level = 0>
Sigma * mim::World::mut_sigma ( size_t size)
inline

A *mut*able Sigma of type level.

Definition at line 323 of file world.h.

References mut_sigma(), and type().

Referenced by mut_sigma().

◆ muts() [1/2]

auto & mim::World::muts ( )
inlinenodiscard

Definition at line 516 of file world.h.

Referenced by mim::Def::Def(), and mim::Def::local_muts().

◆ muts() [2/2]

const auto & mim::World::muts ( ) const
inlinenodiscard

Definition at line 518 of file world.h.

◆ name()

Sym mim::World::name ( ) const
inline

Definition at line 84 of file world.h.

References mim::World::State::POD::name, and mim::World::State::pod.

Referenced by append_suffix(), external(), set(), and set().

◆ next_gid()

u32 mim::World::next_gid ( )
inline

Definition at line 90 of file world.h.

References mim::World::State::POD::curr_gid, and mim::World::State::pod.

Referenced by mim::Def::Def(), and mim::Def::Def().

◆ operator=()

World & mim::World::operator= ( World )
delete

◆ pack() [1/4]

Ref mim::World::pack ( Defs shape,
Ref body )

Definition at line 444 of file world.cpp.

References pack().

◆ pack() [2/4]

Ref mim::World::pack ( Ref arity,
Ref body )

Definition at line 419 of file world.cpp.

References arr(), mim::error(), mim::Lit::isa(), mim::Def::ops(), pack(), tuple(), mim::Def::type(), and type().

Referenced by arr(), mim::plug::autodiff::AutoDiffEval::augment_pack(), ext(), extract(), insert(), pack(), pack(), pack(), and tuple().

◆ pack() [3/4]

Ref mim::World::pack ( u64 n,
Ref body )
inline

Definition at line 355 of file world.h.

References lit_nat(), and pack().

Referenced by pack().

◆ pack() [4/4]

Ref mim::World::pack ( View< u64 > shape,
Ref body )
inline

Definition at line 356 of file world.h.

References pack().

◆ pi() [1/4]

const Pi * mim::World::pi ( Defs dom,
Defs codom,
bool implicit = false )
inline

Definition at line 258 of file world.h.

References pi(), and sigma().

Referenced by pi().

◆ pi() [2/4]

const Pi * mim::World::pi ( Defs dom,
Ref codom,
bool implicit = false )
inline

Definition at line 256 of file world.h.

References pi(), and sigma().

Referenced by pi().

◆ pi() [3/4]

const Pi * mim::World::pi ( Ref dom,
Defs codom,
bool implicit = false )
inline

Definition at line 257 of file world.h.

References pi(), and sigma().

Referenced by pi().

◆ pi() [4/4]

const Pi * mim::World::pi ( Ref dom,
Ref codom,
bool implicit = false )
inline

Definition at line 255 of file world.h.

References mim::Pi::infer().

Referenced by app(), cn(), mim::Pi::immutabilize(), implicit_app(), lam(), lam(), lam(), lam(), lam(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mim::plug::mem::CopyProp::rewrite(), test(), and World().

◆ pick()

Ref mim::World::pick ( Ref type,
Ref value )

Definition at line 513 of file world.cpp.

References type().

◆ proxy()

const Proxy * mim::World::proxy ( Ref type,
Defs ops,
u32 index,
u32 tag )
inline

Definition at line 218 of file world.h.

References type().

Referenced by mim::Pass::proxy().

◆ push()

ScopedLoc mim::World::push ( Loc loc)
inline

Definition at line 111 of file world.h.

References get_loc(), and set_loc().

◆ raw_app() [1/3]

Ref mim::World::raw_app ( const Axiom * axiom,
u8 curry,
u8 trip,
Ref type,
Ref callee,
Ref arg )

Definition at line 221 of file world.cpp.

References axiom(), and type().

Referenced by app(), and raw_app().

◆ raw_app() [2/3]

Ref mim::World::raw_app ( Ref type,
Ref callee,
Defs args )
inline

Definition at line 316 of file world.h.

References raw_app(), tuple(), and type().

Referenced by raw_app().

◆ raw_app() [3/3]

Ref mim::World::raw_app ( Ref type,
Ref callee,
Ref arg )

Definition at line 211 of file world.cpp.

References axiom(), mim::Axiom::get(), raw_app(), mim::Axiom::Trip_End, and type().

◆ register_annex() [1/2]

const Def * mim::World::register_annex ( flags_t f,
const Def * def )

Definition at line 80 of file world.cpp.

References mim::assert_emplace(), mim::Annex::demangle(), and driver().

Referenced by mim::ast::Emitter::register_annex(), and register_annex().

◆ register_annex() [2/2]

const Def * mim::World::register_annex ( plugin_t p,
tag_t t,
sub_t s,
const Def * def )
inline

Definition at line 197 of file world.h.

References register_annex().

◆ select()

Ref mim::World::select ( Ref cond,
Ref t,
Ref f )
inline

Builds (f, t)#cond.

Note
Expects cond as first, t as second, and f as third argument.

Definition at line 370 of file world.h.

References extract(), and tuple().

◆ set() [1/2]

void mim::World::set ( std::string_view name)
inline

Definition at line 86 of file world.h.

References name(), mim::World::State::POD::name, mim::World::State::pod, and sym().

◆ set() [2/2]

void mim::World::set ( Sym name)
inline

Definition at line 85 of file world.h.

References name(), mim::World::State::POD::name, and mim::World::State::pod.

Referenced by main().

◆ set_loc()

void mim::World::set_loc ( Loc loc = {})
inline

Definition at line 110 of file world.h.

Referenced by push(), and mim::World::ScopedLoc::~ScopedLoc().

◆ sigma() [1/2]

const Sigma * mim::World::sigma ( )
inline

The unit type within Type 0.

Definition at line 325 of file world.h.

Referenced by arr(), cn(), cn(), ext(), extract(), fn(), fn(), fn(), pi(), pi(), pi(), sigma(), tuple(), and World().

◆ sigma() [2/2]

Ref mim::World::sigma ( Defs ops)

Definition at line 225 of file world.cpp.

References arr(), mim::Sigma::infer(), mim::Checker::is_uniform(), and sigma().

Referenced by mim::flatten(), mim::Sigma::immutabilize(), mim::is_unit(), mim::merge_sigma(), mim::plug::affine::LowerFor::rewrite(), and mim::plug::mem::CopyProp::rewrite().

◆ state()

const State & mim::World::state ( ) const
inline

Definition at line 79 of file world.h.

Referenced by inherit().

◆ sym() [1/3]

Sym mim::World::sym ( const char * s)

Definition at line 76 of file world.cpp.

References driver().

◆ sym() [2/3]

Sym mim::World::sym ( const std::string & s)

Definition at line 78 of file world.cpp.

References driver().

◆ sym() [3/3]

Sym mim::World::sym ( std::string_view s)

Definition at line 77 of file world.cpp.

References driver().

Referenced by append_suffix(), mim::plug::autodiff::AutoDiffEval::augment_(), main(), mim::optimize(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), set(), mim::Def::sym(), mim::Def::sym(), mim::Def::sym(), tuple(), and World().

◆ test()

Ref mim::World::test ( Ref value,
Ref probe,
Ref match,
Ref clash )

Definition at line 515 of file world.cpp.

References mim::Checker::alpha(), mim::Pi::codom(), mim::Pi::dom(), join(), mim::match(), pi(), and mim::Def::type().

◆ top()

Ref mim::World::top ( Ref type)
inline

Definition at line 435 of file world.h.

References ext(), and type().

◆ top_nat()

Ref mim::World::top_nat ( )
inline

Definition at line 438 of file world.h.

Referenced by arr_unsafe().

◆ tuple() [1/4]

const Tuple * mim::World::tuple ( )
inline

the unit value of type []

Definition at line 346 of file world.h.

Referenced by app(), arr(), ext(), extract(), implicit_app(), insert(), pack(), raw_app(), select(), tuple(), tuple(), and tuple().

◆ tuple() [2/4]

Ref mim::World::tuple ( Defs ops)

Definition at line 233 of file world.cpp.

References mim::Checker::assignable(), mim::error(), sigma(), and tuple().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_tuple(), mim::plug::matrix::counting_for(), mim::plug::autodiff::AutoDiffEval::derive_(), mim::RetWrap::enter(), mim::flatten(), mim::merge_tuple(), mim::plug::affine::LowerFor::rewrite(), mim::plug::mem::SSAConstr::rewrite(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), mim::plug::matrix::LowerMatrixLowLevel::rewrite_imm(), and mim::Infer::tuplefy().

◆ tuple() [3/4]

Ref mim::World::tuple ( Ref type,
Defs ops )

Ascribes type to this tuple - needed for dependently typed and mutable Sigmas.

Definition at line 245 of file world.cpp.

References extract(), mim::Checker::is_uniform(), mim::Lit::isa(), mim::Def::isa_mut(), pack(), tuple(), mim::Def::type(), and type().

◆ tuple() [4/4]

Ref mim::World::tuple ( Sym sym)

Converts sym to a tuple of type '«n; I8»'.

Definition at line 280 of file world.cpp.

References lit_i8(), sym(), and tuple().

◆ type() [1/2]

template<level_t level = 0>
const Type * mim::World::type ( )
inline

Definition at line 209 of file world.h.

References lit_univ(), and type().

Referenced by ac(), app(), axiom(), axiom(), axiom(), axiom(), bot(), ext(), extract(), global(), insert(), lit(), mut_arr(), mut_arr(), mut_bound(), mut_bound(), mut_infer(), mut_join(), mut_join(), mut_meet(), mut_meet(), mut_pack(), mut_pi(), mut_sigma(), mut_sigma(), pack(), pick(), proxy(), raw_app(), raw_app(), raw_app(), top(), tuple(), type(), type_infer_univ(), umax(), var(), vel(), and World().

◆ type() [2/2]

const Type * mim::World::type ( Ref level)

Definition at line 94 of file world.cpp.

References mim::error(), mim::Def::loc(), and mim::Def::type().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_app(), mim::plug::affine::LowerFor::rewrite(), and mim::Def::unfold_type().

◆ type_bool()

Ref mim::World::type_bool ( )
inline

Definition at line 478 of file world.h.

◆ type_bot()

Ref mim::World::type_bot ( )
inline

Definition at line 436 of file world.h.

Referenced by cn(), and World().

◆ type_i1()

Ref mim::World::type_i1 ( )
inline

Definition at line 479 of file world.h.

◆ type_i16()

Ref mim::World::type_i16 ( )
inline

Definition at line 483 of file world.h.

References type_int().

◆ type_i2()

Ref mim::World::type_i2 ( )
inline

Definition at line 480 of file world.h.

References type_int().

◆ type_i32()

Ref mim::World::type_i32 ( )
inline

Definition at line 484 of file world.h.

References type_int().

Referenced by mim::plug::matrix::LowerMatrixMediumLevel::rewrite_().

◆ type_i4()

Ref mim::World::type_i4 ( )
inline

Definition at line 481 of file world.h.

References type_int().

◆ type_i64()

Ref mim::World::type_i64 ( )
inline

Definition at line 485 of file world.h.

References type_int().

◆ type_i8()

Ref mim::World::type_i8 ( )
inline

Definition at line 482 of file world.h.

References type_int().

◆ type_idx() [1/3]

const Idx * mim::World::type_idx ( )
inline

Definition at line 468 of file world.h.

Referenced by lit_idx(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), type_int(), and World().

◆ type_idx() [2/3]

Ref mim::World::type_idx ( nat_t size)
inline
Note
size = 0 means 2^64.

Definition at line 472 of file world.h.

References lit_nat(), and type_idx().

Referenced by type_idx().

◆ type_idx() [3/3]

Ref mim::World::type_idx ( Ref size)
inline
Note
size = 0 means 2^64.

Definition at line 470 of file world.h.

References app(), and type_idx().

Referenced by type_idx().

◆ type_infer_univ()

const Type * mim::World::type_infer_univ ( )
inline

Definition at line 208 of file world.h.

References mut_infer_univ(), and type().

Referenced by mut_infer_entity(), and mut_infer_type().

◆ type_int()

Ref mim::World::type_int ( nat_t width)
inline

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 476 of file world.h.

References mim::Idx::bitwidth2size(), lit_nat(), and type_idx().

Referenced by type_i16(), type_i2(), type_i32(), type_i4(), type_i64(), and type_i8().

◆ type_nat()

const Nat * mim::World::type_nat ( )
inline

Definition at line 467 of file world.h.

Referenced by lit_nat(), and World().

◆ type_top()

Ref mim::World::type_top ( )
inline

Definition at line 437 of file world.h.

◆ uinc()

Ref mim::World::uinc ( Ref op,
level_t offset = 1 )

Definition at line 101 of file world.cpp.

References mim::error(), mim::Lit::isa(), lit_univ(), mim::Def::loc(), and mim::Def::type().

◆ umax()

template<Sort sort>
Ref mim::World::umax ( Defs ops_)

Definition at line 110 of file world.cpp.

References mim::error(), mim::Lit::isa(), mim::Kind, mim::Type::level(), lit_univ(), mim::Term, mim::Type, type(), and mim::Univ.

Referenced by ac(), and bound().

◆ uniq()

Ref mim::World::uniq ( Ref inhabitant)

Definition at line 529 of file world.cpp.

References mim::Def::type(), and mim::Def::unfold_type().

◆ univ()

const Univ * mim::World::univ ( )
inline

Definition at line 204 of file world.h.

Referenced by lit_univ(), mut_infer_univ(), and mim::Rewriter::rewrite().

◆ var()

Ref mim::World::var ( Ref type,
Def * mut )

Definition at line 156 of file world.cpp.

References mim::Idx::isa(), mim::Lit::isa(), lit_0_1(), type(), and var().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_extract(), mim::plug::autodiff::AutoDiffEval::augment_tuple(), mim::plug::affine::LowerFor::rewrite(), and var().

◆ vars() [1/2]

auto & mim::World::vars ( )
inlinenodiscard

Definition at line 515 of file world.h.

Referenced by mim::Def::Def(), mim::Def::free_vars(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), mim::VarRewriter::rewrite_mut(), and mim::VarRewriter::VarRewriter().

◆ vars() [2/2]

const auto & mim::World::vars ( ) const
inlinenodiscard

Definition at line 517 of file world.h.

◆ vel()

Ref mim::World::vel ( Ref type,
Ref value )

Definition at line 508 of file world.cpp.

References type().

◆ verify()

World & mim::World::verify ( )

Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.

Definition at line 565 of file world.cpp.

References annex(), annexes(), externals(), and mim::Def::is_closed().

Referenced by mim::PassMan::run(), and mim::Phase::run().

◆ write() [1/2]

void mim::World::write ( )

Same above but file name defaults to World::name.

Definition at line 500 of file dump.cpp.

◆ write() [2/2]

void mim::World::write ( const char * file)

Write to a file named file.

Definition at line 495 of file dump.cpp.

Friends And Related Symbol Documentation

◆ Def::reduce

DefVec Def::reduce ( Ref )
friend

◆ swap

void swap ( World & w1,
World & w2 )
friend

Definition at line 684 of file world.h.

Referenced by World().

The documentation for this class was generated from the following files: