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

#include <thorin/world.h>

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

struct	State

Public Member Functions

template<class Id , class... Args>

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

template<class Id , class... Args>

const Def * call (Args &&... args)

template<class T , class... Args>

const Def * call_ (Ref callee, T arg, Args &&... args)

template<class T >

const Def * call_ (Ref callee, T arg)

C'tor and D'tor

World & operator= (World)=delete

World (Driver *)

Inherits the state into the new World.

World (Driver *, const State &)

World (World &&other) noexcept

World inherit ()

~World ()

Getters/Setters

const State & state () const

const Driver & driver () const

Driver & driver ()

Sym name () const

void set (Sym name)

void set (std::string_view name)

u32 curr_gid () const

Manage global identifier - a unique number for each Def.

u32 next_gid ()

Flags & flags ()

Retrive compile Flags.

Loc & emit_loc ()

Sym

Sym sym (std::string_view)

Sym sym (const char *)

Sym sym (const std::string &)

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

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

Freeze

In frozen state the World does not create any nodes.

bool is_frozen () const

bool freeze (bool on=true) const

Yields old frozen state.

Debugging Features

const auto & breakpoints ()

Ref gid2def (u32 gid)

Lookup Def by gid.

void breakpoint (u32 gid)

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

World & verify ()

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

Manage Nodes

const auto & annexes () const

const auto & externals () const

void make_external (Def *def)

void make_internal (Def *def)

Def * external (Sym name)

Lookup by name.

template<class Id >

const Def * annex (Id id)

Lookup annex by Axiom::id.

template<annex_without_subs id>

const Def * annex ()

Get Axiom from a plugin.

const Def * register_annex (flags_t f, const Def *)

Univ, Type, Var, Proxy, Infer

const Univ * univ ()

Ref uinc (Ref op, level_t offset=1)

template<Sort = Sort::Univ>

Ref umax (Defs)

const Type * type (Ref level)

const Type * type_infer_univ ()

template<level_t level = 0>

const Type * type ()

Ref var (Ref type, Def *mut)

const Proxy * proxy (Ref type, Defs ops, u32 index, u32 tag)

Infer * mut_infer (Ref type)

Infer * mut_infer_univ ()

Infer * mut_infer_type ()

Infer * mut_infer_entity ()

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

Axiom

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

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

const Axiom * axiom (NormalizeFn n, u8 curry, u8 trip, Ref type)

Builds a fresh Axiom with descending Axiom::sub.

const Axiom * axiom (Ref type)

See above.

Pi

const Pi * pi (Ref dom, Ref codom, bool implicit=false)

const Pi * pi (Defs dom, Ref codom, bool implicit=false)

const Pi * pi (Ref dom, Defs codom, bool implicit=false)

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

Pi * mut_pi (Ref type, bool implicit=false)

Cn

Pi with codom thorin::Bottom

const Pi * cn ()

const Pi * cn (Ref dom)

const Pi * cn (Defs dom)

const Pi * fn (Ref dom, Ref codom)

const Pi * fn (Defs dom, Ref codom)

const Pi * fn (Ref dom, Defs codom)

const Pi * fn (Defs dom, Defs codom)

Lam

Ref filter (Lam::Filter filter)

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

Lam * mut_lam (const Pi *pi)

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

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

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

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

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

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

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

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

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

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

Lam * mut_con (Ref dom)

Lam * mut_con (Defs dom)

Lam * mut_lam (Ref dom, Ref codom)

Lam * mut_lam (Defs dom, Ref codom)

Lam * mut_lam (Ref dom, Defs codom)

Lam * mut_lam (Defs dom, Defs codom)

Lam * mut_fun (Ref dom, Ref codom)

Lam * mut_fun (Defs dom, Ref codom)

Lam * mut_fun (Ref dom, Defs codom)

Lam * mut_fun (Defs dom, Defs codom)

Lam * exit ()

Used as a dummy exit node within Scope.

App

Ref app (Ref callee, Ref arg)

Ref app (Ref callee, Defs args)

template<bool Normalize = false>

Ref raw_app (Ref type, Ref callee, Ref arg)

template<bool Normalize = false>

Ref raw_app (Ref type, Ref callee, Defs args)

Sigma

Sigma * mut_sigma (Ref type, size_t size)

template<level_t level = 0>

Sigma * mut_sigma (size_t size)

A *mut*able Sigma of type level.

Ref sigma (Defs ops)

const Sigma * sigma ()

The unit type within Type 0.

Arr

Arr * mut_arr (Ref type)

template<level_t level = 0>

Arr * mut_arr ()

Ref arr (Ref shape, Ref body)

Ref arr (Defs shape, Ref body)

Ref arr (u64 n, Ref body)

Ref arr (View< u64 > shape, Ref body)

Ref arr_unsafe (Ref body)

Tuple

Ref tuple (Defs ops)

Ref tuple (Ref type, Defs ops)

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

const Tuple * tuple ()

the unit value of type []

Ref tuple (Sym sym)

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

Pack

Pack * mut_pack (Ref type)

Ref pack (Ref arity, Ref body)

Ref pack (Defs shape, Ref body)

Ref pack (u64 n, Ref body)

Ref pack (View< u64 > shape, Ref body)

Extract

See also: core::extract_unsafe

Ref extract (Ref d, Ref i)

Ref extract (Ref d, u64 a, u64 i)

Ref extract (Ref d, u64 i)

Ref select (Ref cond, Ref t, Ref f)

Builds (f, t)#cond.

Insert

See also: core::insert_unsafe

Ref insert (Ref d, Ref i, Ref val)

Ref insert (Ref d, u64 a, u64 i, Ref val)

Ref insert (Ref d, u64 i, Ref val)

Lit

const Lit * lit (Ref type, u64 val)

const Lit * lit_univ (u64 level)

const Lit * lit_univ_0 ()

const Lit * lit_univ_1 ()

const Lit * lit_nat (nat_t a)

const Lit * lit_nat_0 ()

const Lit * lit_nat_1 ()

const Lit * lit_nat_max ()

const Lit * lit_0_1 ()

const Lit * lit_i1 ()

const Lit * lit_i8 ()

const Lit * lit_i16 ()

const Lit * lit_i32 ()

const Lit * lit_i64 ()

const Lit * lit_idx (nat_t size, u64 val)

Constructs a Lit of type Idx of size size.

template<class I >

const Lit * lit_idx (I val)

const Lit * lit_int (nat_t width, u64 val)

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

const Lit * lit_i1 (bool val)

const Lit * lit_i2 (u8 val)

const Lit * lit_i4 (u8 val)

const Lit * lit_i8 (u8 val)

const Lit * lit_i16 (u16 val)

const Lit * lit_i32 (u32 val)

const Lit * lit_i64 (u64 val)

const Lit * lit_idx_mod (nat_t mod, u64 val)

Constructs a Lit of type Idx of size mod.

const Lit * lit_bool (bool val)

const Lit * lit_ff ()

const Lit * lit_tt ()

Lattice

template<bool Up>

Ref ext (Ref type)

Ref bot (Ref type)

Ref top (Ref type)

Ref Bot ()

Ref top_nat ()

template<bool Up>

TBound< Up > * mut_bound (Ref type, size_t size)

template<bool Up, level_t l = 0>

TBound< Up > * mut_bound (size_t size)

A *mut*able Bound of Type level.

template<bool Up>

Ref bound (Defs ops)

Join * mut_join (Ref type, size_t size)

Meet * mut_meet (Ref type, size_t size)

template<level_t l = 0>

Join * mut_join (size_t size)

template<level_t l = 0>

Meet * mut_meet (size_t size)

Ref join (Defs ops)

Ref meet (Defs ops)

Ref ac (Ref type, Defs ops)

Ref ac (Defs ops)

Infers the type using an immutable Meet.

Ref vel (Ref type, Ref value)

Ref pick (Ref type, Ref value)

Ref test (Ref value, Ref probe, Ref match, Ref clash)

Ref singleton (Ref inner_type)

Globals

Deprecated:: { will be removed }

Global * global (Ref type, bool is_mutable=true)

Types

const Nat * type_nat ()

const Idx * type_idx ()

Ref type_idx (Ref size)

Ref type_idx (nat_t size)

Ref type_int (nat_t width)

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

Ref type_bool ()

Ref type_i1 ()

Ref type_i2 ()

Ref type_i4 ()

Ref type_i8 ()

Ref type_i16 ()

Ref type_i32 ()

Ref type_i64 ()

Cope with implicit Arguments

Ref iapp (Ref callee, Ref arg)

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

Ref iapp (Ref callee, Defs args)

Ref iapp (Ref callee, nat_t arg)

template<class E >
requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>

Ref iapp (Ref callee, E arg)

Vars & Muts

Manges sets of Vars and Muts.

Vars vars (const Var *var)

Muts muts (Def *mut)

Vars merge (Vars a, Vars b)

Muts merge (Muts a, Muts b)

Vars insert (Vars vars, const Var *var)

Muts insert (Muts muts, Def *mut)

Vars erase (Vars vars, const Var *var)

Muts erase (Muts muts, Def *mut)

bool has_intersection (Vars v1, Vars v2)

bool has_intersection (Muts m1, Muts m2)

Helpers

Ref iinfer (Ref def)

dump/log

Log & log ()

void dummy ()

void dump (std::ostream &os)

Dump to os.

void dump ()

Dump to std::cout.

void debug_dump ()

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

void write (const char *file)

Write to a file named file.

void write ()

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

dot

Dumps DOT to os.

Parameters

annex	If `true`, include all annexes - even if unused.
types	Follow type dependencies?

void dot (std::ostream &os, bool annexes=false, bool types=false) const

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

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

Detailed Description

The World represents the whole program and manages creation of Thorin 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 35 of file world.h.

Constructor & Destructor Documentation

◆ World() [1/3]

thorin::World::World ( Driver * driver )

explicit

Inherits the state into the new World.

Definition at line 62 of file world.cpp.

◆ World() [2/3]

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

Definition at line 38 of file world.cpp.

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

◆ World() [3/3]

thorin::World::World ( World && other )

inlinenoexcept

Definition at line 71 of file world.h.

References swap.

◆ ~World()

thorin::World::~World ( )

Definition at line 65 of file world.cpp.

Member Function Documentation

◆ ac() [1/2]

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

Infers the type using an immutable Meet.

Definition at line 492 of file world.cpp.

References ac().

◆ ac() [2/2]

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

Definition at line 482 of file world.cpp.

References meet(), and type().

Referenced by ac().

◆ annex() [1/2]

template<annex_without_subs id>

const Def * thorin::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 176 of file world.h.

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

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

◆ annex() [2/2]

template<class Id >

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

inline

Lookup annex by Axiom::id.

Definition at line 167 of file world.h.

References thorin::Annex::demangle(), thorin::error(), and flags().

Referenced by thorin::plug::autodiff::AutoDiffEval::augment_pack(), and thorin::plug::matrix::LowerMatrixMediumLevel::rewrite_().

◆ annexes()

const auto & thorin::World::annexes ( ) const

inline

Definition at line 149 of file world.h.

Referenced by dot(), dot(), thorin::RWPhase::start(), thorin::Cleanup::start(), and verify().

◆ app() [1/2]

Ref thorin::World::app	(	Ref	callee,
		Defs	args
	)

inline

Definition at line 292 of file world.h.

References app(), and tuple().

Referenced by app().

◆ app() [2/2]

Ref thorin::World::app	(	Ref	callee,
		Ref	arg
	)

Definition at line 183 of file world.cpp.

References thorin::Check::assignable(), thorin::Lam::body(), DLOG, thorin::Pi::dom(), thorin::Infer::eliminate(), thorin::error(), thorin::Lam::filter(), thorin::Def::is_set(), thorin::Def::isa_imm(), thorin::Def::isa_mut(), lam(), lit_ff(), lit_tt(), pi(), thorin::Def::reduce(), thorin::Rewriter::rewrite(), type(), thorin::Def::type(), and thorin::Def::var().

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

◆ append_suffix()

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

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

Definition at line 517 of file world.cpp.

References name(), and sym().

◆ arr() [1/4]

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

Definition at line 425 of file world.cpp.

References arr().

◆ arr() [2/4]

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

Definition at line 378 of file world.cpp.

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

Referenced by arr(), arr(), arr(), arr_unsafe(), thorin::plug::autodiff::AutoDiffEval::augment_pack(), ext(), extract(), pack(), and sigma().

◆ arr() [3/4]

Ref thorin::World::arr	(	u64	n,
		Ref	body
	)

inline

Definition at line 314 of file world.h.

References arr(), and lit_nat().

Referenced by arr().

◆ arr() [4/4]

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

inline

Definition at line 315 of file world.h.

References arr().

◆ arr_unsafe()

Ref thorin::World::arr_unsafe ( Ref body )

inline

Definition at line 318 of file world.h.

References arr(), and top_nat().

◆ axiom() [1/4]

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

inline

Builds a fresh Axiom with descending Axiom::sub.

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

Definition at line 225 of file world.h.

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

◆ axiom() [2/4]

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

inline

Definition at line 216 of file world.h.

References type().

Referenced by axiom(), and raw_app().

◆ axiom() [3/4]

const Axiom * thorin::World::axiom ( Ref type )

inline

See above.

Definition at line 228 of file world.h.

References axiom(), and type().

Referenced by axiom().

◆ axiom() [4/4]

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

inline

Definition at line 219 of file world.h.

References axiom(), and type().

Referenced by axiom().

◆ Bot()

Ref thorin::World::Bot ( )

inline

Definition at line 416 of file world.h.

Referenced by cn(), and World().

◆ bot()

Ref thorin::World::bot ( Ref type )

inline

Definition at line 414 of file world.h.

References type().

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

◆ bound()

template<bool Up>

Ref thorin::World::bound ( Defs ops )

Definition at line 458 of file world.cpp.

◆ breakpoint()

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

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

Definition at line 543 of file world.cpp.

References thorin::World::State::breakpoints.

Referenced by main().

◆ breakpoints()

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

inline

Definition at line 136 of file world.h.

References thorin::World::State::breakpoints.

◆ call() [1/2]

template<class Id , class... Args>

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

inline

Definition at line 498 of file world.h.

References call_().

◆ call() [2/2]

template<class Id , class... Args>

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

inline

Definition at line 497 of file world.h.

References annex(), and call_().

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

◆ call_() [1/2]

template<class T >

const Def * thorin::World::call_	(	Ref	callee,
		T	arg
	)

inline

Definition at line 500 of file world.h.

References iapp().

◆ call_() [2/2]

template<class T , class... Args>

const Def * thorin::World::call_	(	Ref	callee,
		T	arg,
		Args &&...	args
	)

inline

Definition at line 499 of file world.h.

References call_(), and iapp().

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

◆ cn() [1/3]

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

inline

Definition at line 246 of file world.h.

References cn(), and sigma().

Referenced by thorin::TailRecElim::analyze(), cn(), con(), con(), fn(), mut_con(), mut_con(), thorin::LamSpec::rewrite(), and World().

◆ cn() [2/3]

const Pi * thorin::World::cn ( Defs dom )

inline

Definition at line 248 of file world.h.

References cn(), and sigma().

Referenced by cn().

◆ cn() [3/3]

const Pi * thorin::World::cn ( Ref dom )

inline

Definition at line 247 of file world.h.

References Bot(), and pi().

◆ con() [1/2]

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

inline

Definition at line 266 of file world.h.

References cn(), and filter().

◆ con() [2/2]

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

inline

Definition at line 265 of file world.h.

References cn(), and filter().

◆ curr_gid()

u32 thorin::World::curr_gid ( ) const

inline

Manage global identifier - a unique number for each Def.

Definition at line 91 of file world.h.

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

Referenced by dump().

◆ debug_dump()

void thorin::World::debug_dump ( )

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

Definition at line 458 of file dump.cpp.

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

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

◆ dot() [1/2]

void thorin::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 135 of file dot.cpp.

References annexes(), and dot().

◆ dot() [2/2]

void thorin::World::dot	(	std::ostream &	os,
		bool	annexes = `false`,
		bool	types = `false`
	)		const

Definition at line 144 of file dot.cpp.

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

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

◆ driver() [1/2]

Driver & thorin::World::driver ( )

inline

Definition at line 84 of file world.h.

◆ driver() [2/2]

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

inline

Definition at line 83 of file world.h.

Referenced by thorin::Parser::driver(), dump(), flags(), inherit(), log(), thorin::optimize(), register_annex(), sym(), sym(), and sym().

◆ dummy()

void thorin::World::dummy ( )

inline

Definition at line 512 of file world.h.

◆ dump() [1/2]

void thorin::World::dump ( )

Dump to std::cout.

Definition at line 456 of file dump.cpp.

References dump().

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

◆ dump() [2/2]

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

Dump to os.

Definition at line 436 of file dump.cpp.

References assertf, curr_gid(), driver(), externals(), flags(), thorin::Driver::imports(), thorin::Driver::is_loaded(), name(), and thorin::print().

Referenced by main().

◆ emit_loc()

Loc & thorin::World::emit_loc ( )

inline

Definition at line 97 of file world.h.

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

◆ erase() [1/2]

Muts thorin::World::erase	(	Muts	muts,
		Def *	mut
	)

inline

Definition at line 491 of file world.h.

References muts().

◆ erase() [2/2]

Vars thorin::World::erase	(	Vars	vars,
		const Var *	var
	)

inline

Definition at line 490 of file world.h.

References var(), and vars().

◆ exit()

Lam * thorin::World::exit ( )

inline

Used as a dummy exit node within Scope.

Definition at line 286 of file world.h.

◆ ext()

template<bool Up>

Ref thorin::World::ext ( Ref type )

Definition at line 451 of file world.cpp.

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

◆ external()

Def * thorin::World::external ( Sym name )

inline

Lookup by name.

Definition at line 164 of file world.h.

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

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

◆ externals()

const auto & thorin::World::externals ( ) const

inline

Definition at line 150 of file world.h.

Referenced by dot(), dump(), thorin::optimize(), thorin::PassMan::run(), thorin::RWPhase::start(), thorin::Cleanup::start(), thorin::ScopePhase::start(), thorin::ClosedMutPhase< M >::start(), and verify().

◆ extract() [1/3]

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

◆ extract() [2/3]

Ref thorin::World::extract	(	Ref	d,
		u64	a,
		u64	i
	)

inline

Definition at line 345 of file world.h.

References extract(), and lit_idx().

Referenced by extract().

◆ extract() [3/3]

Ref thorin::World::extract	(	Ref	d,
		u64	i
	)

inline

Definition at line 346 of file world.h.

References extract().

Referenced by extract().

◆ filter()

Ref thorin::World::filter ( Lam::Filter filter )

inline

Definition at line 258 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 & thorin::World::flags ( )

Retrive compile Flags.

Definition at line 74 of file world.cpp.

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

Referenced by annex(), dump(), thorin::plug::compile::handle_optimization_part(), insert(), and thorin::Def::num_tprojs().

◆ fn() [1/4]

const Pi * thorin::World::fn	(	Defs	dom,
		Defs	codom
	)

inline

Definition at line 252 of file world.h.

References fn(), and sigma().

Referenced by fn().

◆ fn() [2/4]

const Pi * thorin::World::fn	(	Defs	dom,
		Ref	codom
	)

inline

Definition at line 250 of file world.h.

References fn(), and sigma().

Referenced by fn().

◆ fn() [3/4]

const Pi * thorin::World::fn	(	Ref	dom,
		Defs	codom
	)

inline

Definition at line 251 of file world.h.

References fn(), and sigma().

Referenced by fn().

◆ fn() [4/4]

const Pi * thorin::World::fn	(	Ref	dom,
		Ref	codom
	)

inline

Definition at line 249 of file world.h.

References cn().

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

◆ freeze()

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

inline

Yields old frozen state.

Definition at line 115 of file world.h.

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

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

◆ fun() [1/4]

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

inline

Definition at line 274 of file world.h.

References filter(), and fn().

◆ fun() [2/4]

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

inline

Definition at line 272 of file world.h.

References filter(), and fn().

◆ fun() [3/4]

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

inline

Definition at line 273 of file world.h.

References filter(), and fn().

◆ fun() [4/4]

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

inline

Definition at line 271 of file world.h.

References filter(), and fn().

◆ gid2def()

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

Lookup Def by gid.

Definition at line 545 of file world.cpp.

◆ global()

Global * thorin::World::global	(	Ref	type,
		bool	is_mutable = `true`
	)

inline

Definition at line 440 of file world.h.

References type().

◆ has_intersection() [1/2]

bool thorin::World::has_intersection	(	Muts	m1,
		Muts	m2
	)

inline

Definition at line 493 of file world.h.

◆ has_intersection() [2/2]

bool thorin::World::has_intersection	(	Vars	v1,
		Vars	v2
	)

inline

Definition at line 492 of file world.h.

◆ iapp() [1/4]

Ref thorin::World::iapp	(	Ref	callee,
		Defs	args
	)

inline

Definition at line 473 of file world.h.

References iapp(), and tuple().

Referenced by iapp().

◆ iapp() [2/4]

template<class E >
requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>

Ref thorin::World::iapp	(	Ref	callee,
		E	arg
	)

inline

Definition at line 476 of file world.h.

References iapp(), and lit_nat().

◆ iapp() [3/4]

Ref thorin::World::iapp	(	Ref	callee,
		nat_t	arg
	)

inline

Definition at line 474 of file world.h.

References iapp(), and lit_nat().

Referenced by iapp().

◆ iapp() [4/4]

Ref thorin::World::iapp	(	Ref	callee,
		Ref	arg
	)

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

Definition at line 162 of file world.cpp.

References app(), thorin::Check::assignable(), thorin::decurry(), thorin::Pi::dom(), thorin::Pi::is_implicit(), mut_infer(), pi(), thorin::Ref::refer(), and thorin::Def::type().

Referenced by call_(), call_(), and iapp().

◆ iinfer()

Ref thorin::World::iinfer ( Ref def )

inline

Definition at line 506 of file world.h.

References thorin::Idx::size(), and thorin::Def::type().

◆ inherit()

World thorin::World::inherit ( )

inline

Definition at line 75 of file world.h.

References driver(), and state().

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

◆ insert() [1/5]

Muts thorin::World::insert	(	Muts	muts,
		Def *	mut
	)

inline

Definition at line 489 of file world.h.

References muts().

◆ insert() [2/5]

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

Definition at line 340 of file world.cpp.

References thorin::Check::alpha(), thorin::Def::arity(), thorin::Check::assignable(), thorin::error(), flags(), insert(), thorin::Lit::isa(), thorin::Def::isa_lit_arity(), pack(), thorin::Def::proj(), thorin::Flags::scalerize_threshold, thorin::Idx::size(), tuple(), type(), and thorin::Def::type().

Referenced by thorin::plug::autodiff::AutoDiffEval::augment_extract(), extract(), insert(), and thorin::VarRewriter::rewrite_mut().

◆ insert() [3/5]

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

inline

Definition at line 357 of file world.h.

References insert(), and lit_idx().

Referenced by insert().

◆ insert() [4/5]

Ref thorin::World::insert	(	Ref	d,
		u64	i,
		Ref	val
	)

inline

Definition at line 358 of file world.h.

References insert().

Referenced by insert().

◆ insert() [5/5]

Vars thorin::World::insert	(	Vars	vars,
		const Var *	var
	)

inline

Definition at line 488 of file world.h.

References var(), and vars().

◆ is_frozen()

bool thorin::World::is_frozen ( ) const

inline

Definition at line 112 of file world.h.

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

◆ join()

Ref thorin::World::join ( Defs ops )

inline

Definition at line 426 of file world.h.

Referenced by test().

◆ lam() [1/5]

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

inline

Definition at line 262 of file world.h.

References filter(), and pi().

Referenced by app().

◆ lam() [2/5]

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

inline

Definition at line 270 of file world.h.

References filter(), and pi().

◆ lam() [3/5]

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

inline

Definition at line 268 of file world.h.

References filter(), and pi().

◆ lam() [4/5]

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

inline

Definition at line 269 of file world.h.

References filter(), and pi().

◆ lam() [5/5]

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

inline

Definition at line 267 of file world.h.

References filter(), and pi().

◆ lit()

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

inline

Definition at line 377 of file world.h.

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

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

◆ lit_i64() [2/2]

const Lit * thorin::World::lit_i64 ( u64 val )

inline

Definition at line 396 of file world.h.

References lit_int().

◆ lit_i8() [1/2]

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

inline

Definition at line 374 of file world.h.

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

Referenced by tuple().

◆ lit_i8() [2/2]

const Lit * thorin::World::lit_i8 ( u8 val )

inline

Definition at line 393 of file world.h.

References lit_int().

◆ lit_idx() [1/2]

template<class I >

const Lit * thorin::World::lit_idx ( I val )

inline

Definition at line 382 of file world.h.

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

◆ lit_idx() [2/2]

const Lit * thorin::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 380 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 * thorin::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 402 of file world.h.

References lit_idx().

◆ lit_int()

const Lit * thorin::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 389 of file world.h.

References thorin::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 * thorin::World::lit_nat ( nat_t a )

inline

Definition at line 367 of file world.h.

References lit(), and type_nat().

Referenced by thorin::Def::arity(), arr(), iapp(), iapp(), lit_i1(), lit_i16(), lit_i32(), lit_i64(), lit_i8(), thorin::plug::refly::normalize_gid(), thorin::plug::core::normalize_trait(), pack(), type_idx(), type_int(), and World().

◆ lit_nat_0()

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

inline

Definition at line 368 of file world.h.

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

◆ lit_nat_1()

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

inline

Definition at line 369 of file world.h.

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

◆ lit_nat_max()

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

inline

Definition at line 370 of file world.h.

◆ lit_tt()

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

inline

Definition at line 406 of file world.h.

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

◆ lit_univ()

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

inline

Definition at line 364 of file world.h.

References lit(), and univ().

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

◆ lit_univ_0()

const Lit * thorin::World::lit_univ_0 ( )

inline

Definition at line 365 of file world.h.

Referenced by World().

◆ lit_univ_1()

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

inline

Definition at line 366 of file world.h.

Referenced by World().

◆ log()

Log & thorin::World::log ( )

Definition at line 73 of file world.cpp.

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

Referenced by debug_dump().

◆ make_external()

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

inline

Definition at line 151 of file world.h.

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

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

◆ make_internal()

void thorin::World::make_internal ( Def * def )

inline

Definition at line 157 of file world.h.

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

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

◆ meet()

Ref thorin::World::meet ( Defs ops )

inline

Definition at line 427 of file world.h.

Referenced by ac().

◆ merge() [1/2]

Muts thorin::World::merge	(	Muts	a,
		Muts	b
	)

inline

Definition at line 487 of file world.h.

◆ merge() [2/2]

Vars thorin::World::merge	(	Vars	a,
		Vars	b
	)

inline

Definition at line 486 of file world.h.

Referenced by thorin::Def::Def(), and thorin::Def::free_vars().

◆ mut_arr() [1/2]

template<level_t level = 0>

Arr * thorin::World::mut_arr ( )

inline

Definition at line 311 of file world.h.

References mut_arr().

Referenced by mut_arr().

◆ mut_arr() [2/2]

Arr * thorin::World::mut_arr ( Ref type )

inline

Definition at line 310 of file world.h.

References type().

◆ mut_bound() [1/2]

template<bool Up>

TBound< Up > * thorin::World::mut_bound	(	Ref	type,
		size_t	size
	)

inline

Definition at line 418 of file world.h.

References type().

◆ mut_bound() [2/2]

template<bool Up, level_t l = 0>

TBound< Up > * thorin::World::mut_bound ( size_t size )

inline

A *mut*able Bound of Type level.

Definition at line 420 of file world.h.

◆ mut_con() [1/2]

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

inline

Definition at line 276 of file world.h.

References cn().

◆ mut_con() [2/2]

Lam * thorin::World::mut_con ( Ref dom )

inline

Definition at line 275 of file world.h.

References cn().

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

◆ mut_fun() [1/4]

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

inline

Definition at line 284 of file world.h.

References fn().

◆ mut_fun() [2/4]

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

inline

Definition at line 282 of file world.h.

References fn().

◆ mut_fun() [3/4]

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

inline

Definition at line 283 of file world.h.

References fn().

◆ mut_fun() [4/4]

Lam * thorin::World::mut_fun	(	Ref	dom,
		Ref	codom
	)

inline

Definition at line 281 of file world.h.

References fn().

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

◆ mut_infer()

Infer * thorin::World::mut_infer ( Ref type )

inline

Definition at line 201 of file world.h.

References type().

Referenced by iapp(), mut_infer_entity(), mut_infer_type(), and mut_infer_univ().

◆ mut_infer_entity()

Infer * thorin::World::mut_infer_entity ( )

inline

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

Definition at line 206 of file world.h.

References mut_infer(), and type_infer_univ().

◆ mut_infer_type()

Infer * thorin::World::mut_infer_type ( )

inline

Definition at line 203 of file world.h.

References mut_infer(), and type_infer_univ().

Referenced by thorin::IdPtrn::type().

◆ mut_infer_univ()

Infer * thorin::World::mut_infer_univ ( )

inline

Definition at line 202 of file world.h.

References mut_infer(), and univ().

Referenced by type_infer_univ().

◆ mut_join() [1/2]

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

inline

Definition at line 422 of file world.h.

References type().

◆ mut_join() [2/2]

template<level_t l = 0>

Join * thorin::World::mut_join ( size_t size )

inline

Definition at line 424 of file world.h.

References mut_join().

Referenced by mut_join().

◆ mut_lam() [1/5]

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

inline

Definition at line 263 of file world.h.

References pi().

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

◆ mut_lam() [2/5]

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

inline

Definition at line 280 of file world.h.

References pi().

◆ mut_lam() [3/5]

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

inline

Definition at line 278 of file world.h.

References pi().

◆ mut_lam() [4/5]

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

inline

Definition at line 279 of file world.h.

References pi().

◆ mut_lam() [5/5]

Lam * thorin::World::mut_lam	(	Ref	dom,
		Ref	codom
	)

inline

Definition at line 277 of file world.h.

References pi().

◆ mut_meet() [1/2]

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

inline

Definition at line 423 of file world.h.

References type().

◆ mut_meet() [2/2]

template<level_t l = 0>

Meet * thorin::World::mut_meet ( size_t size )

inline

Definition at line 425 of file world.h.

References mut_meet().

Referenced by mut_meet().

◆ mut_pack()

Pack * thorin::World::mut_pack ( Ref type )

inline

Definition at line 332 of file world.h.

References type().

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

◆ mut_pi()

Pi * thorin::World::mut_pi	(	Ref	type,
		bool	implicit = `false`
	)

inline

Definition at line 238 of file world.h.

References type().

◆ mut_sigma() [1/2]

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

inline

Definition at line 301 of file world.h.

References type().

Referenced by extract(), and thorin::TuplePtrn::type().

◆ mut_sigma() [2/2]

template<level_t level = 0>

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

inline

A *mut*able Sigma of type level.

Definition at line 303 of file world.h.

References mut_sigma().

Referenced by mut_sigma().

World & thorin::World::operator= ( World )

delete

◆ pack() [1/4]

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

Definition at line 430 of file world.cpp.

References pack().

◆ pack() [2/4]

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

Definition at line 405 of file world.cpp.

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

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

◆ pack() [3/4]

Ref thorin::World::pack	(	u64	n,
		Ref	body
	)

inline

Definition at line 335 of file world.h.

References lit_nat(), and pack().

Referenced by pack().

◆ pack() [4/4]

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

inline

Definition at line 336 of file world.h.

References pack().

◆ pi() [1/4]

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

inline

Definition at line 237 of file world.h.

References pi(), and sigma().

Referenced by pi().

◆ pi() [2/4]

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

inline

Definition at line 235 of file world.h.

References pi(), and sigma().

Referenced by pi().

◆ pi() [3/4]

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

inline

Definition at line 236 of file world.h.

References pi(), and sigma().

Referenced by pi().

◆ pi() [4/4]

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

inline

Definition at line 234 of file world.h.

References thorin::Pi::infer().

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

◆ pick()

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

Definition at line 499 of file world.cpp.

References type().

◆ proxy()

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

inline

Definition at line 197 of file world.h.

References type().

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

◆ raw_app() [1/2]

template<bool Normalize = false>

Ref thorin::World::raw_app	(	Ref	type,
		Ref	callee,
		Defs	args
	)

inline

Definition at line 294 of file world.h.

References tuple(), and type().

◆ raw_app() [2/2]

template<bool Normalize>

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

Definition at line 205 of file world.cpp.

References axiom(), thorin::Axiom::get(), thorin::Axiom::normalizer(), thorin::Axiom::Trip_End, and type().

Referenced by thorin::plug::autodiff::normalize_ad(), thorin::plug::matrix::normalize_insert(), thorin::plug::matrix::normalize_map_reduce(), thorin::plug::regex::normalize_not(), thorin::plug::matrix::normalize_prod(), thorin::plug::mem::normalize_remem(), thorin::plug::matrix::normalize_transpose(), and thorin::plug::autodiff::normalize_zero().

◆ register_annex()

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

Definition at line 80 of file world.cpp.

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

◆ select()

Ref thorin::World::select	(	Ref	cond,
		Ref	t,
		Ref	f
	)

inline

Builds (f, t)#cond.

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

Definition at line 350 of file world.h.

References extract(), and tuple().

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

Definition at line 218 of file world.cpp.

References arr(), thorin::Check::is_uniform(), and sigma().

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

◆ singleton()

Ref thorin::World::singleton ( Ref inner_type )

Definition at line 515 of file world.cpp.

◆ state()

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

inline

Definition at line 81 of file world.h.

Referenced by inherit().

◆ sym() [1/3]

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

Definition at line 76 of file world.cpp.

References driver().

◆ sym() [2/3]

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

Definition at line 78 of file world.cpp.

References driver().

◆ sym() [3/3]

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

Definition at line 77 of file world.cpp.

References driver().

Referenced by append_suffix(), thorin::plug::autodiff::AutoDiffEval::augment_(), thorin::Def::debug_prefix(), thorin::Def::debug_suffix(), thorin::Annex::demangle(), main(), thorin::optimize(), thorin::plug::matrix::LowerMatrixMediumLevel::rewrite_(), set(), thorin::Annex::split(), thorin::Def::sym(), thorin::Def::sym(), thorin::Def::sym(), tuple(), and World().

◆ test()

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

Definition at line 501 of file world.cpp.

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

◆ top()

Ref thorin::World::top ( Ref type )

inline

Definition at line 415 of file world.h.

References type().

◆ top_nat()

Ref thorin::World::top_nat ( )

inline

Definition at line 417 of file world.h.

Referenced by arr_unsafe().

◆ tuple() [1/4]

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

inline

the unit value of type []

Definition at line 326 of file world.h.

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

◆ tuple() [2/4]

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

Definition at line 226 of file world.cpp.

References thorin::Check::assignable(), thorin::error(), sigma(), and tuple().

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

◆ tuple() [3/4]

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

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

Definition at line 237 of file world.cpp.

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

◆ tuple() [4/4]

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

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

Definition at line 272 of file world.cpp.

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

◆ type() [1/2]

template<level_t level = 0>

const Type * thorin::World::type ( )

inline

Definition at line 188 of file world.h.

References lit_univ(), and type().

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

◆ type() [2/2]

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

Definition at line 92 of file world.cpp.

References thorin::error(), and thorin::Def::type().

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

◆ type_bool()

Ref thorin::World::type_bool ( )

inline

Definition at line 457 of file world.h.

Ref thorin::World::type_i32 ( )

inline

Definition at line 463 of file world.h.

References type_int().

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

◆ type_i4()

Ref thorin::World::type_i4 ( )

inline

Definition at line 460 of file world.h.

References type_int().

◆ type_i64()

Ref thorin::World::type_i64 ( )

inline

Definition at line 464 of file world.h.

References type_int().

◆ type_i8()

Ref thorin::World::type_i8 ( )

inline

Definition at line 461 of file world.h.

References type_int().

◆ type_idx() [1/3]

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

inline

Definition at line 447 of file world.h.

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

◆ type_idx() [2/3]

Ref thorin::World::type_idx ( nat_t size )

inline

Note: size = 0 means 2^64.

Definition at line 451 of file world.h.

References lit_nat(), and type_idx().

Referenced by type_idx().

◆ type_idx() [3/3]

Ref thorin::World::type_idx ( Ref size )

inline

Note: size = 0 means 2^64.

Definition at line 449 of file world.h.

References app(), and type_idx().

Referenced by type_idx().

◆ type_infer_univ()

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

inline

Definition at line 187 of file world.h.

References mut_infer_univ(), and type().

Referenced by mut_infer_entity(), and mut_infer_type().

◆ type_int()

Ref thorin::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 455 of file world.h.

References thorin::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 * thorin::World::type_nat ( )

inline

Definition at line 446 of file world.h.

Referenced by lit_nat(), and World().

◆ uinc()

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

Definition at line 99 of file world.cpp.

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

◆ umax()

template<Sort sort>

Ref thorin::World::umax ( Defs ops_ )

Definition at line 107 of file world.cpp.

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

Referenced by thorin::TuplePtrn::type().

◆ univ()

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

inline

Definition at line 183 of file world.h.

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

◆ var()

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

Definition at line 153 of file world.cpp.

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

Referenced by thorin::plug::autodiff::AutoDiffEval::augment_extract(), thorin::plug::autodiff::AutoDiffEval::augment_tuple(), erase(), insert(), thorin::plug::affine::LowerFor::rewrite(), var(), and vars().

◆ vars()

Vars thorin::World::vars ( const Var * var )

inline

Definition at line 484 of file world.h.

References var().

Referenced by thorin::Def::Def(), erase(), insert(), thorin::plug::matrix::LowerMatrixMediumLevel::rewrite_(), and thorin::VarRewriter::VarRewriter().

◆ vel()

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

Definition at line 494 of file world.cpp.

References type().

◆ verify()

World & thorin::World::verify ( )

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

Definition at line 551 of file world.cpp.

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

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

◆ write() [1/2]

void thorin::World::write ( )

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

Definition at line 467 of file dump.cpp.

References name(), and write().

Referenced by write().

◆ write() [2/2]

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

Write to a file named file.

Definition at line 462 of file dump.cpp.

References dump().

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

include/thorin/world.h
src/thorin/dot.cpp
src/thorin/dump.cpp
src/thorin/world.cpp

Classes

Public Member Functions

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

◆ bot()

◆ bound()

◆ breakpoint()

◆ breakpoints()

◆ call() [1/2]

◆ call() [2/2]

◆ call_() [1/2]

◆ call_() [2/2]

◆ cn() [1/3]

◆ cn() [2/3]

◆ cn() [3/3]

◆ con() [1/2]

◆ con() [2/2]

◆ curr_gid()

◆ debug_dump()

◆ dot() [1/2]

◆ dot() [2/2]

◆ driver() [1/2]

◆ driver() [2/2]

◆ dummy()

◆ dump() [1/2]

◆ dump() [2/2]

◆ emit_loc()

◆ erase() [1/2]

◆ erase() [2/2]

◆ exit()

◆ ext()

◆ external()

◆ externals()

◆ extract() [1/3]

◆ extract() [2/3]

◆ extract() [3/3]

◆ filter()

◆ flags()

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

◆ gid2def()

◆ global()

◆ has_intersection() [1/2]

◆ has_intersection() [2/2]

◆ iapp() [1/4]

◆ iapp() [2/4]

◆ iapp() [3/4]

◆ iapp() [4/4]

◆ iinfer()

◆ inherit()