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
Construction & Destruction
World &	operator= (World)=delete

	World (Driver *)

	World (Driver *, const State &)

	World (World &&other) noexcept

World	inherit ()
	Inherits the `state` into the new World.

	~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 ()

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	freeze (bool on=true) const
	Yields old frozen state.

Debugging Features
const auto &	breakpoints ()

const Def *	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`.

Annexes
const auto &	flags2annex () const

auto	annexes () const

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)

Externals
const auto &	sym2external () const

Def *	external (Sym name)
	Lookup by `name`.

auto	externals () const

Vector< Def * >	copy_externals () const

void	make_external (Def *)

void	make_internal (Def *)

Univ, Type, Var, Proxy, Hole
const Univ *	univ ()

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

template<Sort = Sort::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 (const Def type, 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 ?`.

Axiom
const Axiom *	axiom (NormalizeFn n, u8 curry, u8 trip, const Def *type, plugin_t p, tag_t t, sub_t s)

const Axiom *	axiom (const Def *type, plugin_t p, tag_t t, sub_t s)

const Axiom *	axiom (NormalizeFn n, u8 curry, u8 trip, const Def *type)
	Builds a fresh Axiom with descending Axiom::sub.

const Axiom *	axiom (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)

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 Axiom axiom, 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
Arr *	mut_arr (const Def *type)

template<level_t level = 0>
Arr *	mut_arr ()

const Def *	arr (const Def shape, const Def body)

const Def *	arr (Defs shape, const Def *body)

const Def *	arr (u64 n, const Def *body)

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

const Def *	arr_unsafe (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»'.

Pack
Pack *	mut_pack (const Def *type)

const Def *	pack (const Def arity, const Def body)

const Def *	pack (Defs shape, const Def *body)

const Def *	pack (u64 n, const Def *body)

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

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_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>
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>
TBound< Up > *	mut_bound (const Def *type, size_t size)

template<bool Up, level_t l = 0>
TBound< Up > *	mut_bound (size_t size)
	A mutable Bound of Type `level`.

template<bool Up>
const Def *	bound (Defs ops)

Join *	mut_join (const Def *type, size_t size)

Meet *	mut_meet (const Def *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)

const Def *	join (Defs ops)

const Def *	meet (Defs ops)

const Def *	ac (const Def *type, Defs ops)

const Def *	ac (Defs ops)
	Infers the type using an immutable Meet.

const Def *	vel (const Def type, const Def value)

const Def *	pick (const Def type, const Def value)

const Def *	test (const Def value, const Def probe, const Def match, const Def clash)

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 ()

Cope with implicit Arguments
template<bool Normalize = true>
const Def *	implicit_app (const Def callee, const Def arg)
	Places Holes as demanded by Pi::is_implicit() and then apps `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)

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

DefVec	Def::reduce (const Def *)

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

Definition at line 59 of file world.cpp.

References driver(), and World().

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

◆ World() [2/3]

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

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

References swap, and World().

◆ ~World()

mim::World::~World ( )

Definition at line 62 of file world.cpp.

Member Function Documentation

◆ ac() [1/2]

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

Definition at line 511 of file world.cpp.

References meet(), and type().

Referenced by ac().

◆ ac() [2/2]

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

Infers the type using an immutable Meet.

Definition at line 521 of file world.cpp.

References ac(), and umax().

◆ 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 180 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 Axiom::id.

Definition at line 171 of file world.h.

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

Referenced by call(), dot(), and mim::plug::matrix::LowerMatrixMediumLevel::rewrite_().

◆ annexes()

auto mim::World::annexes ( ) const

inline

Definition at line 168 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 )

◆ app() [2/2]

template<bool Normalize = true>

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

inline

Definition at line 308 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 546 of file world.cpp.

References name(), and sym().

◆ arr() [1/4]

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

Definition at line 407 of file world.cpp.

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

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

◆ arr() [2/4]

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

Definition at line 454 of file world.cpp.

References arr().

◆ arr() [3/4]

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

inline

Definition at line 331 of file world.h.

References arr(), and lit_nat().

Referenced by arr().

◆ arr() [4/4]

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

inline

Definition at line 332 of file world.h.

References arr().

◆ arr_unsafe()

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

inline

Definition at line 335 of file world.h.

References arr(), and top_nat().

◆ axiom() [1/4]

const Axiom * mim::World::axiom ( const Def * type )

inline

See above.

Definition at line 245 of file world.h.

References axiom(), and type().

Referenced by axiom().

◆ axiom() [2/4]

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

inline

Definition at line 236 of file world.h.

References axiom(), and type().

Referenced by axiom().

◆ axiom() [3/4]

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

inline

Builds a fresh Axiom with descending Axiom::sub.

This is useful during testing to come up with some entity 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 242 of file world.h.

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

◆ axiom() [4/4]

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

inline

Definition at line 233 of file world.h.

References type().

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

◆ bot()

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

inline

Definition at line 431 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>

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

Definition at line 487 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 572 of file world.cpp.

Referenced by main().

◆ breakpoints()

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

inline

Definition at line 154 of file world.h.

◆ call() [1/2]

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

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

inline

Definition at line 507 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 506 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 263 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 264 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 265 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 282 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 283 of file world.h.

References cn(), and filter().

◆ copy_externals()

Vector< Def * > mim::World::copy_externals ( ) const

inline

Definition at line 193 of file world.h.

References externals().

Referenced by mim::optimize().

◆ curr_gid()

u32 mim::World::curr_gid ( ) const

inline

Manage global identifier - a unique number for each Def.

Definition at line 88 of file world.h.

Referenced by dump().

◆ debug_dump()

void mim::World::debug_dump ( )

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

Definition at line 486 of file dump.cpp.

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

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 138 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 147 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 81 of file world.h.

◆ driver() [2/2]

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

inline

Definition at line 80 of file world.h.

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

◆ dummy()

void mim::World::dummy ( )

inline

Definition at line 523 of file world.h.

◆ dump() [1/2]

void mim::World::dump ( )

Dump to std::cout.

Definition at line 484 of file dump.cpp.

References dump().

◆ dump() [2/2]

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

Dump to os.

Definition at line 464 of file dump.cpp.

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

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

◆ ext()

template<bool Up>

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

Definition at line 480 of file world.cpp.

References arr(), ext(), 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 191 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()

auto mim::World::externals ( ) const

inline

Definition at line 192 of file world.h.

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

◆ extract() [1/3]

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

Definition at line 301 of file world.cpp.

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

Referenced by arr(), mim::plug::autodiff::AutoDiffEval::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 362 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 363 of file world.h.

References extract().

Referenced by extract().

◆ filter()

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

inline

Definition at line 275 of file world.h.

References filter(), and lit_bool().

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

◆ flags()

Flags & mim::World::flags ( )

Retrieve compile Flags.

Definition at line 71 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 167 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 266 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 268 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 267 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 269 of file world.h.

References fn(), and sigma().

Referenced by fn().

◆ freeze()

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

inline

Yields old frozen state.

Definition at line 133 of file world.h.

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

◆ fun() [1/4]

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

inline

Definition at line 288 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 290 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 289 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 291 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.

Referenced by push().

◆ gid2def()

const Def * mim::World::gid2def ( u32 gid )

Lookup Def by gid.

Definition at line 574 of file world.cpp.

◆ global()

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

inline

Definition at line 458 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 )

Places Holes as demanded by Pi::is_implicit() and then apps arg.

Definition at line 176 of file world.cpp.

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

Referenced by 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 491 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 498 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 494 of file world.h.

References implicit_app(), and lit_nat().

◆ inherit()

World mim::World::inherit ( )

inline

Inherits the state into the new World.

Definition at line 72 of file world.h.

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

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

◆ insert() [1/3]

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

Definition at line 363 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(), 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_hole(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mut_pack(), mut_pi(), 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 374 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 375 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.

◆ join()

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

inline

Definition at line 444 of file world.h.

References bound().

Referenced by test().

◆ lam() [1/5]

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

inline

Definition at line 284 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 286 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 279 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 285 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 287 of file world.h.

References filter(), and pi().

◆ lit()

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

Definition at line 464 of file world.cpp.

References mim::error(), mim::Idx::isa(), mim::Lit::isa(), 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 388 of file world.h.

Referenced by var().

◆ lit_bool()

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

inline

Definition at line 421 of file world.h.

Referenced by filter().

◆ lit_ff()

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

inline

Definition at line 422 of file world.h.

Referenced by app().

◆ lit_i1() [1/2]

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

inline

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

References lit_int().

◆ lit_i16() [1/2]

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

inline

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

References lit_int().

◆ lit_i2()

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

inline

Definition at line 408 of file world.h.

References lit_int().

◆ lit_i32() [1/2]

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

inline

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

References lit_int().

◆ lit_i4()

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

inline

Definition at line 409 of file world.h.

References lit_int().

◆ lit_i64() [1/2]

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

inline

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

References lit_int().

◆ lit_i8() [1/2]

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

inline

Definition at line 391 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 410 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 399 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 397 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 419 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 406 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 384 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 385 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 386 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 387 of file world.h.

◆ lit_tt()

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

inline

Definition at line 423 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 381 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 382 of file world.h.

Referenced by World().

◆ lit_univ_1()

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

inline

Definition at line 383 of file world.h.

Referenced by World().

◆ log()

Log & mim::World::log ( )

Definition at line 70 of file world.cpp.

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

Referenced by debug_dump().

◆ make_external()

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

Definition at line 87 of file world.cpp.

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 )

Definition at line 94 of file world.cpp.

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

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

◆ meet()

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

inline

Definition at line 445 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 328 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 327 of file world.h.

References insert(), and type().

◆ mut_bound() [1/2]

template<bool Up>

TBound< Up > * mim::World::mut_bound	(	const Def *	type,
		size_t	size )

inline

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

References mut_bound(), and type().

◆ mut_con() [1/2]

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

inline

Definition at line 292 of file world.h.

References cn(), and insert().

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

◆ mut_con() [2/2]

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

inline

Definition at line 293 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 298 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 300 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 299 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 301 of file world.h.

References fn(), and insert().

◆ mut_hole()

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

inline

Definition at line 218 of file world.h.

References insert(), and type().

Referenced by implicit_app(), mut_hole_infer_entity(), mut_hole_type(), and mut_hole_univ().

◆ mut_hole_infer_entity()

Hole * mim::World::mut_hole_infer_entity ( )

inline

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

Definition at line 223 of file world.h.

References mut_hole(), and type_infer_univ().

◆ mut_hole_type()

Hole * mim::World::mut_hole_type ( )

inline

Definition at line 220 of file world.h.

References mut_hole(), and type_infer_univ().

◆ mut_hole_univ()

Hole * mim::World::mut_hole_univ ( )

inline

Definition at line 219 of file world.h.

References mut_hole(), and univ().

Referenced by type_infer_univ().

◆ mut_join() [1/2]

Join * mim::World::mut_join	(	const Def *	type,
		size_t	size )

inline

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

References mut_join(), and type().

Referenced by mut_join().

◆ mut_lam() [1/5]

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

inline

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

References insert(), and pi().

◆ mut_lam() [3/5]

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

inline

Definition at line 280 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_(), and mim::RetWrap::enter().

◆ mut_lam() [4/5]

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

inline

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

References insert(), and pi().

◆ mut_meet() [1/2]

Meet * mim::World::mut_meet	(	const Def *	type,
		size_t	size )

inline

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

References mut_meet(), and type().

Referenced by mut_meet().

◆ mut_pack()

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

inline

Definition at line 349 of file world.h.

References insert(), and type().

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

◆ mut_pi()

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

inline

Definition at line 255 of file world.h.

References insert(), and type().

◆ mut_sigma() [1/2]

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

inline

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

References mut_sigma(), and type().

Referenced by mut_sigma().

◆ muts() [1/2]

auto & mim::World::muts ( )

inlinenodiscard

Definition at line 515 of file world.h.

◆ muts() [2/2]

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

inlinenodiscard

Definition at line 517 of file world.h.

◆ name()

Sym mim::World::name ( ) const

inline

Definition at line 83 of file world.h.

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

◆ next_gid()

u32 mim::World::next_gid ( )

inline

Definition at line 89 of file world.h.

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

◆ next_run()

u32 mim::World::next_run ( )

inline

Definition at line 90 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 )

Definition at line 434 of file world.cpp.

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

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

◆ pack() [2/4]

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

Definition at line 459 of file world.cpp.

References pack().

◆ pack() [3/4]

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

inline

Definition at line 352 of file world.h.

References lit_nat(), and pack().

Referenced by pack().

◆ pack() [4/4]

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

inline

Definition at line 353 of file world.h.

References pack().

◆ pi() [1/4]

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

inline

Definition at line 251 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().

◆ pi() [2/4]

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

inline

Definition at line 253 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 252 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 254 of file world.h.

References pi(), and sigma().

Referenced by pi().

◆ pick()

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

Definition at line 528 of file world.cpp.

References type().

◆ proxy()

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

inline

Definition at line 214 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]

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

Definition at line 234 of file world.cpp.

References axiom(), 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 224 of file world.cpp.

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

◆ raw_app() [3/3]

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

inline

Definition at line 313 of file world.h.

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

Referenced by raw_app().

◆ register_annex() [1/2]

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

Definition at line 77 of file world.cpp.

References mim::assert_emplace(), mim::Annex::demangle(), DLOG, 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 183 of file world.h.

References register_annex().

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

References extract(), and tuple().

◆ set() [1/2]

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

inline

Definition at line 85 of file world.h.

References name(), and sym().

◆ set() [2/2]

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

inline

Definition at line 84 of file world.h.

References name().

Referenced by main().

◆ set_loc()

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

inline

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

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

◆ sigma() [2/2]

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

Definition at line 238 of file world.cpp.

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

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

◆ state()

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

inline

Definition at line 78 of file world.h.

Referenced by inherit(), and World().

◆ sym() [1/3]

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

Definition at line 73 of file world.cpp.

References driver().

◆ sym() [2/3]

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

Definition at line 75 of file world.cpp.

References driver().

◆ sym() [3/3]

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

Definition at line 74 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(), and tuple().

◆ sym2external()

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

inline

Definition at line 190 of file world.h.

◆ test()

const Def * mim::World::test	(	const Def *	value,
		const Def *	probe,
		const Def *	match,
		const Def *	clash )

Definition at line 530 of file world.cpp.

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

◆ top()

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

inline

Definition at line 432 of file world.h.

References ext(), and type().

◆ top_nat()

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

inline

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

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

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

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

◆ tuple() [3/4]

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

◆ tuple() [4/4]

const Def * mim::World::tuple ( Sym sym )

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

Definition at line 295 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 205 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 105 of file world.cpp.

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

Referenced by ac(), app(), mim::plug::autodiff::AutoDiffEval::augment_app(), axiom(), axiom(), axiom(), axiom(), bot(), ext(), extract(), global(), insert(), lit(), mut_arr(), mut_arr(), mut_bound(), mut_bound(), mut_hole(), 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(), mim::plug::affine::LowerFor::rewrite(), top(), tuple(), umax(), var(), and vel().

◆ type_bool()

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

inline

Definition at line 475 of file world.h.

◆ type_bot()

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

inline

Definition at line 433 of file world.h.

Referenced by cn().

◆ type_i1()

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

inline

Definition at line 476 of file world.h.

◆ type_i16()

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

inline

Definition at line 480 of file world.h.

References type_int().

◆ type_i2()

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

inline

Definition at line 477 of file world.h.

References type_int().

◆ type_i32()

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

inline

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

References type_int().

◆ type_i64()

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

inline

Definition at line 482 of file world.h.

References type_int().

◆ type_i8()

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

inline

Definition at line 479 of file world.h.

References type_int().

◆ type_idx() [1/3]

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

inline

Definition at line 465 of file world.h.

Referenced by lit_idx(), 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 467 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 469 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 204 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 473 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 464 of file world.h.

Referenced by lit_nat(), and World().

◆ type_top()

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

inline

Definition at line 434 of file world.h.

◆ uinc()

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

Definition at line 112 of file world.cpp.

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

◆ umax()

template<Sort sort>

const Def * mim::World::umax ( Defs ops_ )

Definition at line 121 of file world.cpp.

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

Referenced by ac(), and bound().

◆ uniq()

const Def * mim::World::uniq ( const Def * inhabitant )

Definition at line 544 of file world.cpp.

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

◆ univ()

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

inline

Definition at line 200 of file world.h.

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

◆ var()

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

Definition at line 167 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::autodiff::AutoDiffEval::derive_(), mim::plug::affine::LowerFor::rewrite(), and var().

◆ vars() [1/2]

auto & mim::World::vars ( )

inlinenodiscard

Definition at line 514 of file world.h.

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

◆ vars() [2/2]

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

inlinenodiscard

Definition at line 516 of file world.h.

◆ vel()

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

Definition at line 523 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 580 of file world.cpp.

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

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 495 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 490 of file dump.cpp.

References dump().

Referenced by write().

Friends And Related Symbol Documentation

◆ Def::reduce

DefVec Def::reduce ( const Def * )

friend

◆ swap

void swap	(	World &	w1,
		World &	w2 )

friend

Definition at line 683 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

Classes

Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ World() [1/3]

◆ World() [2/3]

◆ World() [3/3]

◆ ~World()

Member Function Documentation

◆ ac() [1/2]

◆ ac() [2/2]

◆ annex() [1/2]

◆ annex() [2/2]

◆ annexes()

◆ app() [1/2]

◆ app() [2/2]

◆ append_suffix()

◆ arr() [1/4]

◆ arr() [2/4]

◆ arr() [3/4]

◆ arr() [4/4]

◆ arr_unsafe()

◆ axiom() [1/4]

◆ axiom() [2/4]

◆ axiom() [3/4]

◆ axiom() [4/4]

◆ bot()

◆ bound()

◆ breakpoint()

◆ breakpoints()

◆ call() [1/2]

◆ call() [2/2]

◆ cn() [1/3]

◆ cn() [2/3]

◆ cn() [3/3]

◆ con() [1/2]

◆ con() [2/2]

◆ copy_externals()

◆ curr_gid()

◆ debug_dump()

◆ dot() [1/2]

◆ dot() [2/2]

◆ driver() [1/2]

◆ driver() [2/2]

◆ dummy()

◆ dump() [1/2]

◆ dump() [2/2]

◆ ext()

◆ external()

◆ externals()

◆ extract() [1/3]

◆ extract() [2/3]

◆ extract() [3/3]

◆ filter()

◆ flags()

◆ flags2annex()

◆ fn() [1/4]

◆ fn() [2/4]

◆ fn() [3/4]

◆ fn() [4/4]

◆ freeze()

◆ fun() [1/4]

◆ fun() [2/4]

◆ fun() [3/4]

◆ fun() [4/4]

◆ get_loc()

◆ gid2def()

◆ global()

◆ implicit_app() [1/4]

◆ implicit_app() [2/4]

◆ implicit_app() [3/4]

◆ implicit_app() [4/4]

◆ inherit()

◆ insert() [1/3]

◆ insert() [2/3]

◆ insert() [3/3]

◆ is_frozen()

◆ join()

◆ lam() [1/5]