mim::World Class Reference

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

#include <mim/world.h>

Classes
struct	State
struct	ScopedLoc
struct	Freezer
	Use to World::freeze and automatically unfreeze at the end of scope. More...
class	Externals
struct	Move.arena

Public Member Functions
Construction & Destruction
World &	operator= (World)=delete
	World (Driver *)
	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
const Driver &	driver () const
Driver &	driver ()
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
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	do_freeze (bool on=true) const
	Yields old frozen state.
Freezer	freeze ()
	Use like this to freeze and automatically unfreeze:
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.
Annexes
const auto &	flags2annex () const
auto	annexes () const
template<class Id>
const Def *	annex (Id id)
	Lookup annex by Axm::id.
template<annex_without_subs id>
const Def *	annex ()
	Get Axm 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)
Externals
const Externals &	externals () const
Externals &	externals ()
Univ, Type, Var, Proxy, Hole
const Univ *	univ ()
const Def *	uinc (const Def *op, level_t offset=1)
template<int sort = UMax::Univ>
const Def *	umax (Defs)
const Type *	type (const Def *level)
const Type *	type_infer_univ ()
template<level_t level = 0>
const Type *	type ()
const Def *	var (Def *mut)
const Proxy *	proxy (const Def *type, Defs ops, u32 index, u32 tag)
Hole *	mut_hole (const Def *type)
Hole *	mut_hole_univ ()
Hole *	mut_hole_type ()
Hole *	mut_hole_infer_entity ()
	Either a value ?:?:Type ? or a type ?:Type ?: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
Pi with codom mim::Bottom
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 *meta_type)
Rule *	mut_rule (const Reform *type)
const Rule *	rule (const Reform *type, const Def *lhs, const Def *rhs, const Def *guard)
const Rule *	rule (const Def *meta_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 (const Def *arity, const Def *body)
const Def *	pack (const Def *arity, const Def *body)
const Def *	arr (Defs shape, const Def *body)
const Def *	pack (Defs shape, const Def *body)
const Def *	arr (u64 n, const Def *body)
const Def *	pack (u64 n, const Def *body)
const Def *	arr (View< u64 > shape, const Def *body)
const Def *	pack (View< u64 > shape, const Def *body)
const Def *	arr_unsafe (const Def *body)
const Def *	pack_unsafe (const Def *body)
const Def *	prod (bool term, Defs ops)
const Def *	prod (bool term)
Seq
These either build a Pack or an Arr depending on the first argument. Oftentimes, the logic for Packs and Arrays can be quite similar; these methods help factoring such code.
const Def *	unit (bool is_pack)
Seq *	mut_seq (bool is_pack, const Def *type)
const Def *	seq (bool is_pack, const Def *arity, 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, View< u64 > shape, const Def *body)
const Def *	seq_unsafe (bool is_pack, const Def *body)
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
See also core::extract_unsafe
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
See also core::insert_unsafe
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)
Lit
const Lit *	lit (const Def *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_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_unsafe (u64 val)
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>
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 ()
const Def *	top_nat ()
template<bool Up>
const Def *	bound (Defs ops)
const Def *	join (Defs ops)
const Def *	meet (Defs ops)
const Def *	merge (const Def *type, Defs ops)
const Def *	merge (Defs ops)
	Infers the type using a Meet.
const Def *	inj (const Def *type, const Def *value)
const Def *	split (const Def *type, const Def *value)
const Def *	match (Defs)
const Def *	uniq (const Def *inhabitant)
Globals
Deprecated Will be removed.
Global *	global (const Def *type, bool is_mutable=true)
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_i2 ()
const Def *	type_i4 ()
const Def *	type_i8 ()
const Def *	type_i16 ()
const Def *	type_i32 ()
const Def *	type_i64 ()
implicit_app - Cope with implicit Arguments
Places Holes as demanded by Pi::is_implicit() and then apps arg.
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, class E> requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>
const Def *	implicit_app (const Def *callee, E arg)
call
Complete curried call of callee obeying implicits.
template<bool Normalize = true, class T, class... Args>
const Def *	call (const Def *callee, T &&arg, Args &&... args)
template<bool Normalize = true, class T>
const Def *	call (const Def *callee, T &&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>
const Def *	call (Args &&... args)
	Annex overload with enum tempalte argument Id for annexes w/o subtag.
Vars & Muts
Manges sets of Vars and 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.
for_each
Visits all closed mutables in this World.
void	for_each (bool elide_empty, std::function< void(Def *)>)
template<class M>
void	for_each (bool elide_empty, std::function< void(M *)> f)
dump/log
Log &	log () const
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
GraphViz output.
void	dot (std::ostream &os, bool annexes=false, bool types=false) const
	Dumps DOT to os.
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

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

---

Class Documentation

mim::World::Move.arena

struct mim::World::Move.arena

Definition at line 789 of file world.h.

Class Members
Arena	defs
Arena	substs

Constructor & Destructor Documentation

World() [1/3]

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

explicit

Definition at line 74 of file world.cpp.

References driver(), and World().

Referenced by mim::World::Freezer::Freezer(), operator=(), mim::World::ScopedLoc::ScopedLoc(), swap, verify(), World(), and World().

World() [2/3]

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

Definition at line 49 of file world.cpp.

References driver(), insert(), lit_idx(), lit_nat(), lit_univ(), lit_univ_0(), lit_univ_1(), pi(), sigma(), state(), type(), type_idx(), and type_nat().

World() [3/3]

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

inlinenoexcept

Definition at line 71 of file world.h.

References swap, and World().

~World()

mim::World::~World

(

)

Definition at line 77 of file world.cpp.

Member Function Documentation

annex() [1/2]

template<annex_without_subs id>

const Def * mim::World::annex ( )

inline

Get Axm from a plugin.

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

Definition at line 206 of file world.h.

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

Referenced by annex(), and call().

annex() [2/2]

template<class Id>

const Def * mim::World::annex ( Id id )

inline

Lookup annex by Axm::id.

Definition at line 196 of file world.h.

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

Referenced by call(), and dot().

annexes()

auto mim::World::annexes ( ) const

inline

Definition at line 192 of file world.h.

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

app() [1/2]

template<bool Normalize>

const Def * mim::World::app	(	const Def *	callee,
		const Def *	arg )

Definition at line 201 of file world.cpp.

References mim::assert_emplace(), mim::Checker::assignable(), axm(), DLOG, mim::Error::error(), filter(), mim::Axm::get(), mim::Def::isa_imm(), mim::Def::isa_mut(), lam(), lit_ff(), lit_tt(), mim::Def::loc(), mim::Error::note(), pi(), raw_app(), mim::Axm::Trip_End, mim::Def::type(), type(), var(), and mim::Def::zonk().

Referenced by mim::Lam::app(), app(), mim::plug::autodiff::Eval::augment_app(), mim::plug::autodiff::Eval::augment_pack(), implicit_app(), mim::plug::autodiff::op_sum(), mim::LamSpec::rewrite(), mim::TailRecElim::rewrite(), mim::plug::matrix::LowerMatrixHighLevelMapRed::rewrite_(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), mim::EtaExpPhase::rewrite_imm_App(), mim::plug::affine::phase::LowerFor::rewrite_imm_App(), mim::plug::direct::DS2CPS::rewrite_imm_App(), and type_idx().

app() [2/2]

template<bool Normalize = true>

const Def * mim::World::app ( const Def * callee, Defs args )

inline

Definition at line 380 of file world.h.

References app(), and tuple().

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 655 of file world.cpp.

References name(), and sym().

arr() [1/4]

const Def * mim::World::arr ( const Def * arity, const Def * body )

inline

Definition at line 409 of file world.h.

References seq().

Referenced by ext(), extract(), seq(), and sigma().

arr() [2/4]

const Def * mim::World::arr ( Defs shape, const Def * body )

inline

Definition at line 411 of file world.h.

References seq().

arr() [3/4]

const Def * mim::World::arr ( u64 n, const Def * body )

inline

Definition at line 413 of file world.h.

References seq().

arr() [4/4]

const Def * mim::World::arr ( View< u64 > shape, const Def * body )

inline

Definition at line 415 of file world.h.

References seq().

arr_unsafe()

const Def * mim::World::arr_unsafe ( const Def * body )

inline

Definition at line 417 of file world.h.

References seq_unsafe().

axm() [1/4]

const Axm * mim::World::axm ( const Def * type )

inline

See above.

Definition at line 303 of file world.h.

References axm(), and type().

Referenced by axm().

axm() [2/4]

const Axm * mim::World::axm ( const Def * type, plugin_t p, tag_t t, sub_t s )

inline

Definition at line 294 of file world.h.

References axm(), and type().

Referenced by axm().

axm() [3/4]

const Axm * mim::World::axm ( NormalizeFn n, u8 curry, u8 trip, const Def * type )

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

References axm(), mim::Annex::Global_Plugin, and type().

axm() [4/4]

const Axm * mim::World::axm ( NormalizeFn n, u8 curry, u8 trip, const Def * type, plugin_t p, tag_t t, sub_t s )

inline

Definition at line 291 of file world.h.

References type().

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

bot()

const Def * mim::World::bot ( const Def * type )

inline

Definition at line 522 of file world.h.

References ext(), and type().

Referenced by mim::plug::clos::LowerTypedClos::start().

bound()

template<bool Up>

const Def * mim::World::bound

(

Defs

ops

)

Definition at line 558 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 a Def with this gid.

Definition at line 712 of file world.cpp.

Referenced by main().

breakpoints()

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

inline

Definition at line 176 of file world.h.

call() [1/4]

template<class Id, bool Normalize = true, class... Args>

const Def * mim::World::call ( Args &&... args )

inline

Annex overload with enum tempalte argument Id for annexes w/o subtag.

Definition at line 613 of file world.h.

References annex(), and call().

call() [2/4]

template<bool Normalize = true, class T>

const Def * mim::World::call ( const Def * callee, T && arg )

inline

Base case.

Definition at line 600 of file world.h.

References implicit_app().

call() [3/4]

template<bool Normalize = true, class T, class... Args>

const Def * mim::World::call ( const Def * callee, T && arg, Args &&... args )

inline

Definition at line 594 of file world.h.

References call(), and implicit_app().

Referenced by mim::plug::autodiff::Eval::augment_lam(), call(), call(), call(), mim::plug::clos::ClosConvPrep::eta_wrap(), mim::plug::clos::LowerTypedClosPrep::rewrite(), mim::plug::mem::pass::SSA::rewrite(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), and mim::plug::affine::phase::LowerFor::rewrite_imm_App().

call() [4/4]

template<Enum Id, bool Normalize = true, class... Args>

const Def * mim::World::call ( Id id, Args &&... args )

inline

Annex overload with enum instance as first argument.

Definition at line 606 of file world.h.

References annex(), and call().

cn() [1/3]

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

inline

Definition at line 321 of file world.h.

References cn(), and sigma().

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

cn() [2/3]

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

inline

Definition at line 322 of file world.h.

References pi(), and type_bot().

cn() [3/3]

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

inline

Definition at line 323 of file world.h.

References cn(), and sigma().

Referenced by cn().

con() [1/2]

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

inline

Definition at line 340 of file world.h.

References cn(), and filter().

con() [2/2]

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

inline

Definition at line 341 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 98 of file world.h.

Referenced by dump().

curr_run()

u32 mim::World::curr_run ( ) const

inline

Manage run - used to track fixed-point iterations to compute Def::free_vars.

Definition at line 102 of file world.h.

debug_dump()

void mim::World::debug_dump

(

)

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

Definition at line 555 of file dump.cpp.

References mim::Log::Debug, dump(), and log().

Referenced by mim::plug::autodiff::Eval::augment_app(), mim::PassMan::run(), mim::plug::direct::CPS2DSPhase::start(), and mim::ReplManPhase::start().

do_freeze()

bool mim::World::do_freeze ( bool on = true ) const

inline

Yields old frozen state.

Definition at line 157 of file world.h.

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

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 166 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

Dumps DOT to os.

Parameters

os	Output stream
annexes	If true, include all annexes - even if unused.
types	Follow type dependencies?

Definition at line 175 of file dot.cpp.

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

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

driver() [1/2]

Driver & mim::World::driver ( )

inline

Definition at line 90 of file world.h.

driver() [2/2]

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

inline

Definition at line 89 of file world.h.

Referenced by annex(), mim::ast::AST::driver(), mim::ast::Emitter::driver(), mim::Stage::driver(), dump(), flags(), inherit(), mim::ast::load_plugins(), log(), mim::plug::compile::normalize_is_loaded(), mim::optimize(), register_annex(), sym(), sym(), sym(), World(), and World().

dump() [1/2]

void mim::World::dump

(

)

Dump to std::cout.

Definition at line 553 of file dump.cpp.

References dump().

dump() [2/2]

void mim::World::dump

(

std::ostream &

os

)

Dump to os.

Definition at line 531 of file dump.cpp.

References assertf, curr_gid(), driver(), externals(), flags(), muts(), mim::print(), and sym().

Referenced by debug_dump(), dump(), main(), and write().

ext()

template<bool Up>

const Def * mim::World::ext

(

const Def *

type

)

Definition at line 548 of file world.cpp.

References arr(), ext(), pack(), sigma(), tuple(), and type().

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

externals() [1/2]

Externals & mim::World::externals ( )

inline

Definition at line 253 of file world.h.

externals() [2/2]

const Externals & mim::World::externals ( ) const

inline

Definition at line 252 of file world.h.

Referenced by mim::plug::autodiff::Eval::augment_(), dot(), dump(), mim::Def::externalize(), for_each(), mim::Def::internalize(), mim::optimize(), mim::plug::matrix::LowerMatrixHighLevelMapRed::rewrite_(), and verify().

extract() [1/3]

const Def * mim::World::extract	(	const Def *	d,
		const Def *	i )

Definition at line 358 of file world.cpp.

References mim::Checker::alpha(), mim::Def::arity(), arr(), mim::Idx::as_lit(), mim::error(), extract(), insert(), is_frozen(), mim::Idx::isa(), mim::Lit::isa(), mim::isa_indicies(), mim::Hole::isa_unset(), join(), lit_idx(), mim::Def::loc(), mut_hole(), mim::Def::ops(), pack(), mim::VarRewriter::rewrite(), sigma(), tuple(), mim::Def::type(), type(), var(), WLOG, and mim::Def::zonk().

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

extract() [2/3]

const Def * mim::World::extract ( const Def * d, u64 a, u64 i )

inline

Definition at line 453 of file world.h.

References extract(), and lit_idx().

Referenced by extract().

extract() [3/3]

const Def * mim::World::extract ( const Def * d, u64 i )

inline

Definition at line 454 of file world.h.

References mim::Lit::as(), and extract().

Referenced by extract().

filter()

const Def * mim::World::filter ( Lam::Filter filter )

inline

Definition at line 333 of file world.h.

References filter(), and lit_bool().

Referenced by mim::Lam::app(), app(), con(), con(), filter(), fun(), fun(), fun(), fun(), lam(), lam(), lam(), lam(), lam(), and mim::Lam::set().

flags()

Flags & mim::World::flags

(

)

Retrieve compile Flags.

Definition at line 87 of file world.cpp.

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

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

flags2annex()

const auto & mim::World::flags2annex ( ) const

inline

Definition at line 191 of file world.h.

fn() [1/4]

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

inline

Definition at line 324 of file world.h.

References cn().

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

fn() [2/4]

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

inline

Definition at line 326 of file world.h.

References fn(), and sigma().

Referenced by fn().

fn() [3/4]

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

inline

Definition at line 325 of file world.h.

References fn(), and sigma().

Referenced by fn().

fn() [4/4]

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

inline

Definition at line 327 of file world.h.

References fn(), and sigma().

Referenced by fn().

for_each() [1/2]

void mim::World::for_each	(	bool	elide_empty,
		std::function< void(Def *)>	f )

Definition at line 691 of file world.cpp.

References mim::Def::deps(), mim::unique_queue< Set >::empty(), externals(), mim::Def::local_muts(), muts(), mim::unique_queue< Set >::pop(), and mim::unique_queue< Set >::push().

Referenced by for_each(), and mim::plug::direct::CPS2DSPhase::start().

for_each() [2/2]

template<class M>

void mim::World::for_each ( bool elide_empty, std::function< void(M *)> f )

inline

Definition at line 638 of file world.h.

References for_each(), and M.

freeze()

Freezer mim::World::freeze ( )

inline

Use like this to freeze and automatically unfreeze:

{
    auto _ = world.freeze();
    // do stuff
}

Definition at line 170 of file world.h.

Referenced by mim::Def::operator<<.

fun() [1/4]

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

inline

Definition at line 346 of file world.h.

References filter(), and fn().

fun() [2/4]

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

inline

Definition at line 348 of file world.h.

References filter(), and fn().

fun() [3/4]

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

inline

Definition at line 347 of file world.h.

References filter(), and fn().

fun() [4/4]

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

inline

Definition at line 349 of file world.h.

References filter(), and fn().

get_loc()

Loc mim::World::get_loc ( ) const

inline

Definition at line 122 of file world.h.

Referenced by push().

gid2def()

const Def * mim::World::gid2def

(

u32

gid

)

Lookup Def by gid.

Definition at line 715 of file world.cpp.

global()

Global * mim::World::global ( const Def * type, bool is_mutable = true )

inline

Definition at line 542 of file world.h.

References insert(), and type().

implicit_app() [1/4]

template<bool Normalize>

const Def * mim::World::implicit_app	(	const Def *	callee,
		const Def *	arg )

Definition at line 194 of file world.cpp.

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

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

implicit_app() [2/4]

template<bool Normalize = true>

const Def * mim::World::implicit_app ( const Def * callee, Defs args )

inline

Definition at line 575 of file world.h.

References implicit_app(), and tuple().

implicit_app() [3/4]

template<bool Normalize = true, class E>
requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>

const Def * mim::World::implicit_app ( const Def * callee, E arg )

inline

Definition at line 583 of file world.h.

References implicit_app(), and lit_nat().

implicit_app() [4/4]

template<bool Normalize = true>

const Def * mim::World::implicit_app ( const Def * callee, nat_t arg )

inline

Definition at line 579 of file world.h.

References implicit_app(), and lit_nat().

inherit()

std::unique_ptr< World > mim::World::inherit ( )

inline

Inherits the State into the new World.

World::curr_gid will be offset to not collide with the original World.

Definition at line 79 of file world.h.

References driver(), and state().

inj()

const Def * mim::World::inj	(	const Def *	type,
		const Def *	value )

Definition at line 599 of file world.cpp.

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

insert() [1/3]

const Def * mim::World::insert	(	const Def *	d,
		const Def *	i,
		const Def *	val )

Definition at line 443 of file world.cpp.

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

Referenced by mim::plug::autodiff::Eval::augment_extract(), extract(), global(), 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(), and World().

insert() [2/3]

const Def * mim::World::insert ( const Def * d, u64 a, u64 i, const Def * val )

inline

Definition at line 465 of file world.h.

References insert(), and lit_idx().

Referenced by insert().

insert() [3/3]

const Def * mim::World::insert ( const Def * d, u64 i, const Def * val )

inline

Definition at line 466 of file world.h.

References mim::Lit::as(), and insert().

Referenced by insert().

is_frozen()

bool mim::World::is_frozen ( ) const

inline

Definition at line 143 of file world.h.

Referenced by extract().

join()

const Def * mim::World::join ( Defs ops )

inline

Definition at line 529 of file world.h.

References bound().

Referenced by extract(), and match().

lam() [1/5]

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

inline

Definition at line 342 of file world.h.

References filter(), and pi().

lam() [2/5]

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

inline

Definition at line 344 of file world.h.

References filter(), and pi().

lam() [3/5]

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

inline

Definition at line 337 of file world.h.

References filter(), and pi().

Referenced by app().

lam() [4/5]

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

inline

Definition at line 343 of file world.h.

References filter(), and pi().

lam() [5/5]

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

inline

Definition at line 345 of file world.h.

References filter(), and pi().

lit()

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

Definition at line 526 of file world.cpp.

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

Referenced by lit_idx(), lit_idx_unsafe(), lit_nat(), and lit_univ().

lit_bool()

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

inline

Definition at line 513 of file world.h.

Referenced by filter().

lit_ff()

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

inline

Definition at line 514 of file world.h.

Referenced by app().

lit_i1() [1/2]

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

inline

Definition at line 481 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 499 of file world.h.

References lit_int().

lit_i16() [1/2]

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

inline

Definition at line 483 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 503 of file world.h.

References lit_int().

lit_i2()

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

inline

Definition at line 500 of file world.h.

References lit_int().

lit_i32() [1/2]

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

inline

Definition at line 484 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 504 of file world.h.

References lit_int().

lit_i4()

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

inline

Definition at line 501 of file world.h.

References lit_int().

lit_i64() [1/2]

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

inline

Definition at line 485 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 505 of file world.h.

References lit_int().

lit_i8() [1/2]

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

inline

Definition at line 482 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 502 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 491 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 488 of file world.h.

References lit(), and type_idx().

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

lit_idx_1_0()

const Lit * mim::World::lit_idx_1_0 ( )

inline

Definition at line 479 of file world.h.

Referenced by var().

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

References lit_idx().

lit_idx_unsafe()

const Lit * mim::World::lit_idx_unsafe ( u64 val )

inline

Definition at line 489 of file world.h.

References lit(), top(), type_idx(), and type_nat().

Referenced by mim::plug::core::normalize_idx_unsafe().

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

References lit(), and type_nat().

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

lit_nat_0()

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

inline

Definition at line 476 of file world.h.

Referenced by mim::Pack::arity().

lit_nat_1()

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

inline

Definition at line 477 of file world.h.

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

lit_nat_max()

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

inline

Definition at line 478 of file world.h.

lit_tt()

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

inline

Definition at line 515 of file world.h.

Referenced by app().

lit_univ()

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

inline

Definition at line 472 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 473 of file world.h.

Referenced by World().

lit_univ_1()

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

inline

Definition at line 474 of file world.h.

Referenced by World().

log()

Log & mim::World::log

(

)

const

Definition at line 86 of file world.cpp.

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

Referenced by debug_dump().

match()

const Def * mim::World::match

(

Defs

ops_

)

Definition at line 614 of file world.cpp.

References mim::Checker::alpha(), mim::error(), mim::Def::gid(), join(), pi(), mim::Def::type(), type(), and mim::Def::zonk().

meet()

const Def * mim::World::meet ( Defs ops )

inline

Definition at line 530 of file world.h.

References bound().

Referenced by merge().

merge() [1/2]

const Def * mim::World::merge	(	const Def *	type,
		Defs	ops )

Definition at line 581 of file world.cpp.

References meet(), type(), and mim::Def::zonk().

Referenced by merge().

merge() [2/2]

const Def * mim::World::merge

(

Defs

ops

)

Infers the type using a Meet.

Definition at line 594 of file world.cpp.

References merge(), umax(), and mim::Def::zonk().

mut_arr() [1/2]

template<level_t level = 0>

Arr * mim::World::mut_arr ( )

inline

Definition at line 404 of file world.h.

References mut_arr(), and type().

Referenced by mut_arr().

mut_arr() [2/2]

Arr * mim::World::mut_arr ( const Def * type )

inline

Definition at line 407 of file world.h.

References mut_seq(), and type().

mut_con() [1/2]

Lam * mim::World::mut_con ( const Def * dom )

inline

Definition at line 350 of file world.h.

References cn(), and insert().

Referenced by mim::plug::autodiff::Eval::augment_lam(), and mim::plug::affine::phase::LowerFor::rewrite_imm_App().

mut_con() [2/2]

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

inline

Definition at line 351 of file world.h.

References cn(), and insert().

mut_fun() [1/4]

Lam * mim::World::mut_fun ( const Def * dom, const Def * codom )

inline

Definition at line 356 of file world.h.

References fn(), and insert().

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

mut_fun() [2/4]

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

inline

Definition at line 358 of file world.h.

References fn(), and insert().

mut_fun() [3/4]

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

inline

Definition at line 357 of file world.h.

References fn(), and insert().

mut_fun() [4/4]

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

inline

Definition at line 359 of file world.h.

References fn(), and insert().

mut_hole()

Hole * mim::World::mut_hole ( const Def * type )

inline

Definition at line 276 of file world.h.

References insert(), and type().

Referenced by extract(), implicit_app(), mut_hole_infer_entity(), mut_hole_type(), mut_hole_univ(), and mim::tuple_of_dict().

mut_hole_infer_entity()

Hole * mim::World::mut_hole_infer_entity ( )

inline

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

Definition at line 281 of file world.h.

References mut_hole(), and type_infer_univ().

mut_hole_type()

Hole * mim::World::mut_hole_type ( )

inline

Definition at line 278 of file world.h.

References mut_hole(), and type_infer_univ().

Referenced by mim::tuple_of_dict().

mut_hole_univ()

Hole * mim::World::mut_hole_univ ( )

inline

Definition at line 277 of file world.h.

References mut_hole(), and univ().

Referenced by type_infer_univ().

mut_lam() [1/5]

Lam * mim::World::mut_lam ( const Def * dom, const Def * codom )

inline

Definition at line 352 of file world.h.

References insert(), and pi().

mut_lam() [2/5]

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

inline

Definition at line 354 of file world.h.

References insert(), and pi().

mut_lam() [3/5]

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

inline

Definition at line 338 of file world.h.

References insert(), and pi().

Referenced by mim::plug::autodiff::Eval::augment_app(), mim::plug::autodiff::Eval::augment_extract(), mim::plug::autodiff::Eval::augment_pack(), mim::plug::autodiff::Eval::augment_tuple(), mim::plug::autodiff::Eval::derive_(), mim::SymExprOpt::rewrite_imm_App(), and mim::RetWrap::rewrite_mut_Lam().

mut_lam() [4/5]

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

inline

Definition at line 353 of file world.h.

References insert(), and pi().

mut_lam() [5/5]

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

inline

Definition at line 355 of file world.h.

References insert(), and pi().

mut_pack()

Pack * mim::World::mut_pack ( const Def * type )

inline

Definition at line 408 of file world.h.

References mut_seq(), and type().

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

mut_pi()

Pi * mim::World::mut_pi ( const Def * type, bool implicit = false )

inline

Definition at line 313 of file world.h.

References insert(), and type().

mut_rule()

Rule * mim::World::mut_rule ( const Reform * type )

inline

Definition at line 366 of file world.h.

References insert(), and type().

Referenced by rule().

mut_seq()

Seq * mim::World::mut_seq ( bool is_pack, const Def * type )

inline

Definition at line 430 of file world.h.

References insert(), and type().

Referenced by mut_arr(), and mut_pack().

mut_sigma() [1/2]

Sigma * mim::World::mut_sigma ( const Def * type, size_t size )

inline

Definition at line 390 of file world.h.

References insert(), and type().

Referenced by mut_sigma().

mut_sigma() [2/2]

template<level_t level = 0>

Sigma * mim::World::mut_sigma ( size_t size )

inline

A mutable Sigma of type level.

Definition at line 393 of file world.h.

References mut_sigma(), and type().

muts() [1/2]

auto & mim::World::muts ( )

inlinenodiscard

Definition at line 622 of file world.h.

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

muts() [2/2]

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

inlinenodiscard

Definition at line 624 of file world.h.

name()

Sym mim::World::name ( ) const

inline

Definition at line 93 of file world.h.

Referenced by append_suffix(), mim::World::Externals::operator[](), set(), set(), and write().

next_gid()

u32 mim::World::next_gid ( )

inline

Definition at line 99 of file world.h.

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

next_run()

u32 mim::World::next_run ( )

inline

Definition at line 103 of file world.h.

operator=()

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

delete

References World().

pack() [1/4]

const Def * mim::World::pack ( const Def * arity, const Def * body )

inline

Definition at line 410 of file world.h.

References seq().

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

pack() [2/4]

const Def * mim::World::pack ( Defs shape, const Def * body )

inline

Definition at line 412 of file world.h.

References seq().

pack() [3/4]

const Def * mim::World::pack ( u64 n, const Def * body )

inline

Definition at line 414 of file world.h.

References seq().

pack() [4/4]

const Def * mim::World::pack ( View< u64 > shape, const Def * body )

inline

Definition at line 416 of file world.h.

References seq().

pack_unsafe()

const Def * mim::World::pack_unsafe ( const Def * body )

inline

Definition at line 418 of file world.h.

References seq_unsafe().

pi() [1/4]

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

inline

Definition at line 309 of file world.h.

References mim::Pi::infer().

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

pi() [2/4]

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

inline

Definition at line 311 of file world.h.

References pi(), and sigma().

Referenced by pi().

pi() [3/4]

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

inline

Definition at line 310 of file world.h.

References pi(), and sigma().

Referenced by pi().

pi() [4/4]

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

inline

Definition at line 312 of file world.h.

References pi(), and sigma().

Referenced by pi().

prod() [1/2]

const Def * mim::World::prod ( bool term )

inline

Definition at line 421 of file world.h.

References sigma(), and tuple().

prod() [2/2]

const Def * mim::World::prod ( bool term, Defs ops )

inline

Definition at line 420 of file world.h.

References sigma(), and tuple().

Referenced by mim::Rewriter::rewrite_imm_Seq(), and mim::Rewriter::rewrite_mut_Seq().

proxy()

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

inline

Definition at line 274 of file world.h.

References type().

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

push()

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

inline

Definition at line 124 of file world.h.

References get_loc(), and set_loc().

raw_app() [1/3]

const Def * mim::World::raw_app	(	const Axm *	axm,
		u8	curry,
		u8	trip,
		const Def *	type,
		const Def *	callee,
		const Def *	arg )

Definition at line 279 of file world.cpp.

References axm(), and type().

Referenced by app(), and raw_app().

raw_app() [2/3]

const Def * mim::World::raw_app	(	const Def *	type,
		const Def *	callee,
		const Def *	arg )

Definition at line 265 of file world.cpp.

References axm(), mim::Axm::get(), raw_app(), mim::Axm::Trip_End, type(), and mim::Def::zonk().

raw_app() [3/3]

const Def * mim::World::raw_app ( const Def * type, const Def * callee, Defs args )

inline

Definition at line 385 of file world.h.

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

Referenced by raw_app().

reduce()

Defs mim::World::reduce	(	const Var *	var,
		const Def *	arg )

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 675 of file world.cpp.

References mim::assert_emplace(), and var().

reform()

const Reform * mim::World::reform ( const Def * meta_type )

inline

Definition at line 365 of file world.h.

References mim::Reform::infer().

Referenced by rule().

register_annex() [1/2]

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

Definition at line 93 of file world.cpp.

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

Referenced by mim::ast::Emitter::register_annex(), register_annex(), mim::EtaExpPhase::rewrite_annex(), and mim::RWPhase::rewrite_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 211 of file world.h.

References register_annex().

rule() [1/2]

const Rule * mim::World::rule ( const Def * meta_type, const Def * lhs, const Def * rhs, const Def * guard )

inline

Definition at line 370 of file world.h.

References reform(), and rule().

rule() [2/2]

const Rule * mim::World::rule ( const Reform * type, const Def * lhs, const Def * rhs, const Def * guard )

inline

Definition at line 367 of file world.h.

References mut_rule(), mim::Rule::set(), and type().

Referenced by rule().

select()

const Def * mim::World::select ( const Def * cond, const Def * t, const Def * f )

inline

Builds (f, t)#cond.

Note

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

Definition at line 458 of file world.h.

References extract(), and tuple().

seq() [1/4]

const Def * mim::World::seq	(	bool	is_pack,
		const Def *	arity,
		const Def *	body )

Definition at line 492 of file world.cpp.

References arr(), mim::error(), mim::Lit::isa(), mim::Def::loc(), mim::Def::proj(), seq(), tuple(), mim::Def::type(), type(), mim::Def::unfold_type(), unit(), and mim::Def::zonk().

Referenced by arr(), arr(), arr(), arr(), pack(), pack(), pack(), pack(), mim::Rewriter::rewrite_imm_Seq(), seq(), seq(), seq(), and seq_unsafe().

seq() [2/4]

const Def * mim::World::seq	(	bool	is_pack,
		Defs	shape,
		const Def *	body )

Definition at line 521 of file world.cpp.

References seq().

seq() [3/4]

const Def * mim::World::seq ( bool is_pack, u64 n, const Def * body )

inline

Definition at line 433 of file world.h.

References lit_nat(), and seq().

Referenced by seq().

seq() [4/4]

const Def * mim::World::seq ( bool is_pack, View< u64 > shape, const Def * body )

inline

Definition at line 434 of file world.h.

References seq().

seq_unsafe()

const Def * mim::World::seq_unsafe ( bool is_pack, const Def * body )

inline

Definition at line 437 of file world.h.

References seq(), and top_nat().

Referenced by arr_unsafe(), and pack_unsafe().

set() [1/2]

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

inline

Definition at line 95 of file world.h.

References name(), and sym().

set() [2/2]

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

inline

Definition at line 94 of file world.h.

References name().

Referenced by main().

set_loc()

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

inline

Definition at line 123 of file world.h.

Referenced by push().

sigma() [1/2]

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

inline

The unit type within Type 0.

Definition at line 397 of file world.h.

Referenced by cn(), cn(), fn(), fn(), fn(), pi(), pi(), pi(), prod(), prod(), sigma(), unit(), and World().

sigma() [2/2]

const Def * mim::World::sigma

(

Defs

ops

)

Definition at line 283 of file world.cpp.

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

Referenced by mim::cat_sigma(), ext(), extract(), mim::flatten(), mim::Sigma::immutabilize(), mim::is_unit(), mim::plug::mem::pass::CopyProp::rewrite(), mim::plug::affine::phase::LowerFor::rewrite_imm_App(), and tuple().

split()

const Def * mim::World::split	(	const Def *	type,
		const Def *	value )

Definition at line 607 of file world.cpp.

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

state()

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

inline

Definition at line 88 of file world.h.

Referenced by inherit(), and World().

sym() [1/3]

Sym mim::World::sym

(

const char *

s

)

Definition at line 89 of file world.cpp.

References driver().

sym() [2/3]

Sym mim::World::sym

(

const std::string &

s

)

Definition at line 91 of file world.cpp.

References driver().

sym() [3/3]

Sym mim::World::sym

(

std::string_view

s

)

Definition at line 90 of file world.cpp.

References driver().

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

top()

const Def * mim::World::top ( const Def * type )

inline

Definition at line 523 of file world.h.

References ext(), and type().

Referenced by lit_idx_unsafe().

top_nat()

const Def * mim::World::top_nat ( )

inline

Definition at line 526 of file world.h.

Referenced by seq_unsafe().

tuple() [1/4]

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

inline

the unit value of type []

Definition at line 445 of file world.h.

Referenced by app(), ext(), implicit_app(), insert(), prod(), prod(), raw_app(), select(), seq(), tuple(), tuple(), tuple(), unit(), and var().

tuple() [2/4]

const Def * mim::World::tuple	(	const Def *	type,
		Defs	ops )

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

Definition at line 308 of file world.cpp.

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

tuple() [3/4]

const Def * mim::World::tuple

(

Defs

ops

)

Definition at line 293 of file world.cpp.

References mim::Checker::assignable(), mim::error(), mim::Tuple::infer(), sigma(), tuple(), and mim::Def::zonk().

Referenced by mim::plug::autodiff::Eval::augment_tuple(), mim::cat_tuple(), mim::plug::matrix::counting_for(), mim::plug::autodiff::Eval::derive_(), extract(), mim::flatten(), mim::Rewriter::map(), mim::Rewriter::map(), mim::Rewriter::map(), mim::plug::mem::pass::SSA::rewrite(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), mim::plug::affine::phase::LowerFor::rewrite_imm_App(), and mim::tuple_of_dict().

tuple() [4/4]

const Def * mim::World::tuple

(

Sym

sym

)

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

Definition at line 345 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 265 of file world.h.

References lit_univ(), and type().

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

type() [2/2]

const Type * mim::World::type

(

const Def *

level

)

Definition at line 108 of file world.cpp.

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

Referenced by app(), axm(), axm(), axm(), axm(), bot(), ext(), extract(), global(), inj(), insert(), lit(), match(), merge(), mut_arr(), mut_arr(), mut_hole(), mut_pack(), mut_pi(), mut_rule(), mut_seq(), mut_sigma(), mut_sigma(), proxy(), raw_app(), raw_app(), raw_app(), rule(), seq(), split(), top(), tuple(), and umax().

type_bool()

const Def * mim::World::type_bool ( )

inline

Definition at line 558 of file world.h.

type_bot()

const Def * mim::World::type_bot ( )

inline

Definition at line 524 of file world.h.

Referenced by cn().

type_i1()

const Def * mim::World::type_i1 ( )

inline

Definition at line 559 of file world.h.

type_i16()

const Def * mim::World::type_i16 ( )

inline

Definition at line 563 of file world.h.

References type_int().

type_i2()

const Def * mim::World::type_i2 ( )

inline

Definition at line 560 of file world.h.

References type_int().

type_i32()

const Def * mim::World::type_i32 ( )

inline

Definition at line 564 of file world.h.

References type_int().

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

type_i4()

const Def * mim::World::type_i4 ( )

inline

Definition at line 561 of file world.h.

References type_int().

type_i64()

const Def * mim::World::type_i64 ( )

inline

Definition at line 565 of file world.h.

References type_int().

type_i8()

const Def * mim::World::type_i8 ( )

inline

Definition at line 562 of file world.h.

References type_int().

type_idx() [1/3]

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

inline

Definition at line 548 of file world.h.

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

type_idx() [2/3]

const Def * mim::World::type_idx ( const Def * size )

inline

Note

size = 0 means 2^64.

Definition at line 550 of file world.h.

References app(), and type_idx().

Referenced by type_idx().

type_idx() [3/3]

const Def * mim::World::type_idx ( nat_t size )

inline

Note

size = 0 means 2^64.

Definition at line 552 of file world.h.

References lit_nat(), and type_idx().

Referenced by type_idx().

type_infer_univ()

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

inline

Definition at line 263 of file world.h.

References mut_hole_univ(), and type().

Referenced by mut_hole_infer_entity(), and mut_hole_type().

type_int()

const Def * 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 556 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 547 of file world.h.

Referenced by lit_idx_unsafe(), lit_nat(), and World().

type_top()

const Def * mim::World::type_top ( )

inline

Definition at line 525 of file world.h.

uinc()

const Def * mim::World::uinc	(	const Def *	op,
		level_t	offset = 1 )

Definition at line 118 of file world.cpp.

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

umax()

template<int sort>

const Def * mim::World::umax

(

Defs

ops_

)

Definition at line 138 of file world.cpp.

References mim::error(), mim::flatten_umax(), mim::Lit::isa(), mim::UMax::Kind, lit_univ(), mim::Def::loc(), mim::UMax::Term, mim::UMax::Type, mim::Def::type(), type(), type(), umax(), mim::Def::unfold_type(), mim::UMax::Univ, and mim::Def::zonk().

Referenced by bound(), merge(), and umax().

uniq()

const Def * mim::World::uniq

(

const Def *

inhabitant

)

Definition at line 650 of file world.cpp.

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

unit()

const Def * mim::World::unit ( bool is_pack )

inline

Definition at line 429 of file world.h.

References sigma(), and tuple().

Referenced by seq().

univ()

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

inline

Definition at line 258 of file world.h.

Referenced by lit_univ(), and mut_hole_univ().

var()

const Def * mim::World::var

(

Def *

mut

)

Definition at line 180 of file world.cpp.

References mim::Idx::isa(), mim::Lit::isa(), lit_idx_1_0(), tuple(), var(), and mim::Def::var_type().

Referenced by app(), extract(), reduce(), mim::EtaExpPhase::rewrite_imm_Var(), mim::EtaRedPhase::rewrite_imm_Var(), mim::Def::var(), and var().

vars() [1/2]

auto & mim::World::vars ( )

inlinenodiscard

Definition at line 621 of file world.h.

Referenced by mim::Def::free_vars(), and mim::VarRewriter::rewrite_mut().

vars() [2/2]

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

inlinenodiscard

Definition at line 623 of file world.h.

verify()

World & mim::World::verify

(

)

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

Definition at line 721 of file world.cpp.

References annexes(), externals(), muts(), and World().

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

watchpoint()

void mim::World::watchpoint

(

u32

gid

)

Trigger breakpoint in your debugger when Def::setting a Def with this gid.

Definition at line 713 of file world.cpp.

Referenced by main().

watchpoints()

const auto & mim::World::watchpoints ( )

inline

Definition at line 177 of file world.h.

write() [1/2]

void mim::World::write

(

)

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

Definition at line 564 of file dump.cpp.

References name(), and write().

write() [2/2]

void mim::World::write

(

const char *

file

)

Write to a file named file.

Definition at line 559 of file dump.cpp.

References dump().

Referenced by write().

zonker()

Zonker & mim::World::zonker ( )

inline

Definition at line 91 of file world.h.

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

Friends And Related Symbol Documentation

swap

void swap ( World & w1, World & w2 )

friend

Definition at line 839 of file world.h.

References swap, and World().

Referenced by swap, and World().

---

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

• include/mim/world.h
• src/mim/dot.cpp
• src/mim/dump.cpp
• src/mim/world.cpp