MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
mim::World Class Reference

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

#include <mim/world.h>

Classes

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

Public Member Functions

Construction & Destruction
Worldoperator= (World)=delete
 
 World (Driver *)
 
 World (Driver *, const State &)
 
 World (World &&other) noexcept
 
 ~World ()
 
World inherit ()
 Inherits the state into the new World.
 
std::unique_ptr< Worldinherit_ptr ()
 As above.
 
Getters/Setters
const Statestate () const
 
const Driverdriver () const
 
Driverdriver ()
 
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 ()
 
Flagsflags ()
 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 auto & watchpoints ()
 
const Defgid2def (u32 gid)
 Lookup Def by gid.
 
void breakpoint (u32 gid)
 Trigger breakpoint in your debugger when creating a Def with this gid.
 
void watchpoint (u32 gid)
 Trigger breakpoint in your debugger when Def::setting a Def with this gid.
 
Worldverify ()
 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 Defannex (Id id)
 Lookup annex by Axm::id.
 
template<annex_without_subs id>
const Defannex ()
 Get Axm from a plugin.
 
const Defregister_annex (flags_t f, const Def *)
 
const Defregister_annex (plugin_t p, tag_t t, sub_t s, const Def *def)
 
Externals
const auto & sym2external () const
 
Defexternal (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 Univuniv ()
 
const Defuinc (const Def *op, level_t offset=1)
 
template<int sort = UMax::Univ>
const Defumax (Defs)
 
const Typetype (const Def *level)
 
const Typetype_infer_univ ()
 
template<level_t level = 0>
const Typetype ()
 
const Defvar (const Def *type, Def *mut)
 
const Proxyproxy (const Def *type, Defs ops, u32 index, u32 tag)
 
Holemut_hole (const Def *type)
 
Holemut_hole_univ ()
 
Holemut_hole_type ()
 
Holemut_hole_infer_entity ()
 Either a value ?:?:Type ? or a type ?:Type ?:Type ?.
 
Axm
const Axmaxm (NormalizeFn n, u8 curry, u8 trip, const Def *type, plugin_t p, tag_t t, sub_t s)
 
const Axmaxm (const Def *type, plugin_t p, tag_t t, sub_t s)
 
const Axmaxm (NormalizeFn n, u8 curry, u8 trip, const Def *type)
 Builds a fresh Axm with descending Axm::sub.
 
const Axmaxm (const Def *type)
 See above.
 
Pi
const Pipi (const Def *dom, const Def *codom, bool implicit=false)
 
const Pipi (Defs dom, const Def *codom, bool implicit=false)
 
const Pipi (const Def *dom, Defs codom, bool implicit=false)
 
const Pipi (Defs dom, Defs codom, bool implicit=false)
 
Pimut_pi (const Def *type, bool implicit=false)
 
Cn

Pi with codom mim::Bottom

const Picn ()
 
const Picn (const Def *dom, bool implicit=false)
 
const Picn (Defs dom, bool implicit=false)
 
const Pifn (const Def *dom, const Def *codom, bool implicit=false)
 
const Pifn (Defs dom, const Def *codom, bool implicit=false)
 
const Pifn (const Def *dom, Defs codom, bool implicit=false)
 
const Pifn (Defs dom, Defs codom, bool implicit=false)
 
Lam
const Deffilter (Lam::Filter filter)
 
const Lamlam (const Pi *pi, Lam::Filter f, const Def *body)
 
Lammut_lam (const Pi *pi)
 
const Lamcon (const Def *dom, Lam::Filter f, const Def *body)
 
const Lamcon (Defs dom, Lam::Filter f, const Def *body)
 
const Lamlam (const Def *dom, const Def *codom, Lam::Filter f, const Def *body)
 
const Lamlam (Defs dom, const Def *codom, Lam::Filter f, const Def *body)
 
const Lamlam (const Def *dom, Defs codom, Lam::Filter f, const Def *body)
 
const Lamlam (Defs dom, Defs codom, Lam::Filter f, const Def *body)
 
const Lamfun (const Def *dom, const Def *codom, Lam::Filter f, const Def *body)
 
const Lamfun (Defs dom, const Def *codom, Lam::Filter f, const Def *body)
 
const Lamfun (const Def *dom, Defs codom, Lam::Filter f, const Def *body)
 
const Lamfun (Defs dom, Defs codom, Lam::Filter f, const Def *body)
 
Lammut_con (const Def *dom)
 
Lammut_con (Defs dom)
 
Lammut_lam (const Def *dom, const Def *codom)
 
Lammut_lam (Defs dom, const Def *codom)
 
Lammut_lam (const Def *dom, Defs codom)
 
Lammut_lam (Defs dom, Defs codom)
 
Lammut_fun (const Def *dom, const Def *codom)
 
Lammut_fun (Defs dom, const Def *codom)
 
Lammut_fun (const Def *dom, Defs codom)
 
Lammut_fun (Defs dom, Defs codom)
 
Rewrite Rules
const Reformreform (const Def *meta_type)
 
Rulemut_rule (const Reform *type)
 
const Rulerule (const Reform *type, const Def *lhs, const Def *rhs, const Def *guard)
 
const Rulerule (const Def *meta_type, const Def *lhs, const Def *rhs, const Def *guard)
 
App
template<bool Normalize = true>
const Defapp (const Def *callee, const Def *arg)
 
template<bool Normalize = true>
const Defapp (const Def *callee, Defs args)
 
const Defraw_app (const Axm *axm, u8 curry, u8 trip, const Def *type, const Def *callee, const Def *arg)
 
const Defraw_app (const Def *type, const Def *callee, const Def *arg)
 
const Defraw_app (const Def *type, const Def *callee, Defs args)
 
Sigma
Sigmamut_sigma (const Def *type, size_t size)
 
template<level_t level = 0>
Sigmamut_sigma (size_t size)
 A mutable Sigma of type level.
 
const Defsigma (Defs ops)
 
const Sigmasigma ()
 The unit type within Type 0.
 
Arr
const Defunit (bool term)
 
Seqmut_seq (bool term, const Def *type)
 
const Defseq (bool term, const Def *arity, const Def *body)
 
const Defseq (bool term, Defs shape, const Def *body)
 
const Defseq (bool term, u64 n, const Def *body)
 
const Defseq (bool term, View< u64 > shape, const Def *body)
 
const Defseq_unsafe (bool term, const Def *body)
 
template<level_t level = 0>
Arrmut_arr ()
 
Arrmut_arr (const Def *type)
 
Packmut_pack (const Def *type)
 
const Defarr (const Def *arity, const Def *body)
 
const Defpack (const Def *arity, const Def *body)
 
const Defarr (Defs shape, const Def *body)
 
const Defpack (Defs shape, const Def *body)
 
const Defarr (u64 n, const Def *body)
 
const Defpack (u64 n, const Def *body)
 
const Defarr (View< u64 > shape, const Def *body)
 
const Defpack (View< u64 > shape, const Def *body)
 
const Defarr_unsafe (const Def *body)
 
const Defpack_unsafe (const Def *body)
 
const Defprod (bool term, Defs ops)
 
const Defprod (bool term)
 
Tuple
const Deftuple (Defs ops)
 
const Deftuple (const Def *type, Defs ops)
 Ascribes type to this tuple - needed for dependently typed and mutable Sigmas.
 
const Tupletuple ()
 the unit value of type []
 
const Deftuple (Sym sym)
 Converts sym to a tuple of type '«n; I8»'.
 
Extract
See also
core::extract_unsafe
const Defextract (const Def *d, const Def *i)
 
const Defextract (const Def *d, u64 a, u64 i)
 
const Defextract (const Def *d, u64 i)
 
const Defselect (const Def *cond, const Def *t, const Def *f)
 Builds (f, t)#cond.
 
Insert
See also
core::insert_unsafe
const Definsert (const Def *d, const Def *i, const Def *val)
 
const Definsert (const Def *d, u64 a, u64 i, const Def *val)
 
const Definsert (const Def *d, u64 i, const Def *val)
 
Lit
const Litlit (const Def *type, u64 val)
 
const Litlit_univ (u64 level)
 
const Litlit_univ_0 ()
 
const Litlit_univ_1 ()
 
const Litlit_nat (nat_t a)
 
const Litlit_nat_0 ()
 
const Litlit_nat_1 ()
 
const Litlit_nat_max ()
 
const Litlit_idx_1_0 ()
 
const Litlit_i1 ()
 
const Litlit_i8 ()
 
const Litlit_i16 ()
 
const Litlit_i32 ()
 
const Litlit_i64 ()
 
const Litlit_idx (nat_t size, u64 val)
 Constructs a Lit of type Idx of size size.
 
const Litlit_idx_unsafe (u64 val)
 
template<class I>
const Litlit_idx (I val)
 
const Litlit_int (nat_t width, u64 val)
 Constructs a Lit of type Idx of size 2^width.
 
const Litlit_i1 (bool val)
 
const Litlit_i2 (u8 val)
 
const Litlit_i4 (u8 val)
 
const Litlit_i8 (u8 val)
 
const Litlit_i16 (u16 val)
 
const Litlit_i32 (u32 val)
 
const Litlit_i64 (u64 val)
 
const Litlit_idx_mod (nat_t mod, u64 val)
 Constructs a Lit of type Idx of size mod.
 
const Litlit_bool (bool val)
 
const Litlit_ff ()
 
const Litlit_tt ()
 
Lattice
template<bool Up>
const Defext (const Def *type)
 
const Defbot (const Def *type)
 
const Deftop (const Def *type)
 
const Deftype_bot ()
 
const Deftype_top ()
 
const Deftop_nat ()
 
template<bool Up>
const Defbound (Defs ops)
 
const Defjoin (Defs ops)
 
const Defmeet (Defs ops)
 
const Defmerge (const Def *type, Defs ops)
 
const Defmerge (Defs ops)
 Infers the type using a Meet.
 
const Definj (const Def *type, const Def *value)
 
const Defsplit (const Def *type, const Def *value)
 
const Defmatch (Defs)
 
const Defuniq (const Def *inhabitant)
 
Globals
Deprecated
Will be removed.
Globalglobal (const Def *type, bool is_mutable=true)
 
Types
const Nattype_nat ()
 
const Idxtype_idx ()
 
const Deftype_idx (const Def *size)
 
const Deftype_idx (nat_t size)
 
const Deftype_int (nat_t width)
 Constructs a type Idx of size 2^width.
 
const Deftype_bool ()
 
const Deftype_i1 ()
 
const Deftype_i2 ()
 
const Deftype_i4 ()
 
const Deftype_i8 ()
 
const Deftype_i16 ()
 
const Deftype_i32 ()
 
const Deftype_i64 ()
 
Cope with implicit Arguments
template<bool Normalize = true>
const Defimplicit_app (const Def *callee, const Def *arg)
 Places Holes as demanded by Pi::is_implicit() and then apps arg.
 
template<bool Normalize = true>
const Defimplicit_app (const Def *callee, Defs args)
 
template<bool Normalize = true>
const Defimplicit_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 Defimplicit_app (const Def *callee, E arg)
 
template<class Id, bool Normalize = true, class... Args>
const Defcall (Id id, Args &&... args)
 Complete curried call of annexes obeying implicits.
 
template<class Id, bool Normalize = true, class... Args>
const Defcall (Args &&... args)
 
Vars & Muts

Manges sets of Vars and Muts.

auto & vars ()
 
auto & muts ()
 
const auto & vars () const
 
const auto & muts () const
 
Defs reduce (const Var *var, const Def *arg)
 Yields the new body of [mut->var() -> arg]mut.
 
dump/log
Loglog ()
 
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
 

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


Class Documentation

◆ mim::World::Move.arena

struct mim::World::Move.arena

Definition at line 711 of file world.h.

Class Members
Arena defs
Arena substs

Constructor & Destructor Documentation

◆ World() [1/3]

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

◆ World() [2/3]

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

◆ World() [3/3]

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

Definition at line 73 of file world.h.

References swap, and World().

◆ ~World()

mim::World::~World ( )

Definition at line 62 of file world.cpp.

Member Function Documentation

◆ annex() [1/2]

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

Get Axm from a plugin.

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

Definition at line 191 of file world.h.

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

Referenced by annex(), and call().

◆ annex() [2/2]

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

Lookup annex by Axm::id.

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

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

◆ app() [1/2]

◆ app() [2/2]

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

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

References name(), and sym().

◆ arr() [1/4]

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

Definition at line 374 of file world.h.

References seq().

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

◆ arr() [2/4]

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

Definition at line 376 of file world.h.

References seq().

◆ arr() [3/4]

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

Definition at line 378 of file world.h.

References seq().

◆ arr() [4/4]

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

Definition at line 380 of file world.h.

References seq().

◆ arr_unsafe()

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

Definition at line 382 of file world.h.

References seq_unsafe().

◆ axm() [1/4]

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

See above.

Definition at line 258 of file world.h.

References axm(), and type().

Referenced by axm().

◆ axm() [2/4]

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

Definition at line 249 of file world.h.

References axm(), and type().

Referenced by axm().

◆ axm() [3/4]

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

Builds a fresh Axm with descending Axm::sub.

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

Definition at line 255 of file world.h.

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

◆ axm() [4/4]

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

Definition at line 246 of file world.h.

References type().

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

◆ bot()

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

◆ bound()

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

Definition at line 539 of file world.cpp.

References ext(), and umax().

Referenced by join(), and meet().

◆ breakpoint()

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

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

Definition at line 678 of file world.cpp.

Referenced by main().

◆ breakpoints()

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

Definition at line 161 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 543 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

◆ cn() [1/3]

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

Definition at line 276 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 277 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 278 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 295 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 296 of file world.h.

References cn(), and filter().

◆ copy_externals()

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

Definition at line 206 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 95 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 493 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 137 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
osOutput stream
annexesIf true, include all annexes - even if unused.
typesFollow type dependencies?

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

◆ driver() [2/2]

◆ dummy()

void mim::World::dummy ( )
inline

Definition at line 564 of file world.h.

◆ dump() [1/2]

void mim::World::dump ( )

Dump to std::cout.

Definition at line 491 of file dump.cpp.

References dump().

◆ dump() [2/2]

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

Dump to os.

Definition at line 469 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 529 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

◆ externals()

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

Definition at line 205 of file world.h.

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

◆ extract() [1/3]

◆ extract() [2/3]

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

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

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

Referenced by extract().

◆ filter()

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

Definition at line 288 of file world.h.

References filter(), and lit_bool().

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

◆ flags()

Flags & mim::World::flags ( )

Retrieve compile Flags.

Definition at line 72 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 176 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 279 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 281 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 280 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 282 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 140 of file world.h.

Referenced by mim::World::Freezer::Freezer(), and inherit().

◆ fun() [1/4]

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

Definition at line 301 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 303 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 302 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 304 of file world.h.

References filter(), and fn().

◆ get_loc()

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

Definition at line 116 of file world.h.

Referenced by push().

◆ gid2def()

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

Lookup Def by gid.

Definition at line 681 of file world.cpp.

◆ global()

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

Definition at line 492 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 189 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 526 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 534 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 530 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 79 of file world.h.

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

◆ inherit_ptr()

std::unique_ptr< World > mim::World::inherit_ptr ( )
inline

As above.

Definition at line 80 of file world.h.

References driver(), and state().

◆ inj()

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

Definition at line 580 of file world.cpp.

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

◆ insert() [1/3]

◆ insert() [2/3]

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

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

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

Referenced by insert().

◆ is_frozen()

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

Definition at line 137 of file world.h.

◆ join()

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

Definition at line 479 of file world.h.

References bound().

Referenced by extract(), and match().

◆ lam() [1/5]

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

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

References filter(), and pi().

◆ lit()

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

Definition at line 508 of file world.cpp.

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

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

◆ lit_bool()

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

Definition at line 463 of file world.h.

Referenced by filter().

◆ lit_ff()

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

Definition at line 464 of file world.h.

Referenced by app().

◆ lit_i1() [1/2]

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

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

References lit_int().

◆ lit_i16() [1/2]

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

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

References lit_int().

◆ lit_i2()

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

Definition at line 450 of file world.h.

References lit_int().

◆ lit_i32() [1/2]

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

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

References lit_int().

◆ lit_i4()

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

Definition at line 451 of file world.h.

References lit_int().

◆ lit_i64() [1/2]

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

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

References lit_int().

◆ lit_i8() [1/2]

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

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

References lit(), and type_idx().

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

◆ lit_idx_1_0()

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

Definition at line 429 of file world.h.

Referenced by var().

◆ lit_idx_mod()

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

Constructs a Lit of type Idx of size mod.

The value val will be adjusted modulo mod.

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

Definition at line 461 of file world.h.

References lit_idx().

◆ lit_idx_unsafe()

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

Definition at line 439 of file world.h.

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

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

◆ lit_int()

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

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

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

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

◆ lit_nat_0()

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

Definition at line 426 of file world.h.

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

◆ lit_nat_1()

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

Definition at line 427 of file world.h.

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

◆ lit_nat_max()

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

Definition at line 428 of file world.h.

◆ lit_tt()

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

Definition at line 465 of file world.h.

Referenced by app().

◆ lit_univ()

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

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

Referenced by World().

◆ lit_univ_1()

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

Definition at line 424 of file world.h.

Referenced by World().

◆ log()

Log & mim::World::log ( )

Definition at line 71 of file world.cpp.

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

Referenced by debug_dump().

◆ make_external()

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

◆ make_internal()

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

Definition at line 95 of file world.cpp.

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

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

◆ match()

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

◆ meet()

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

Definition at line 480 of file world.h.

References bound().

Referenced by merge().

◆ merge() [1/2]

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

Definition at line 562 of file world.cpp.

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

Referenced by merge().

◆ merge() [2/2]

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

Infers the type using a Meet.

Definition at line 575 of file world.cpp.

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

◆ mut_arr() [1/2]

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

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

References mut_seq(), and type().

◆ mut_con() [1/2]

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

Definition at line 305 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 306 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 311 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 313 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 312 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 314 of file world.h.

References fn(), and insert().

◆ mut_hole()

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

Definition at line 231 of file world.h.

References insert(), and type().

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

◆ mut_hole_infer_entity()

Hole * mim::World::mut_hole_infer_entity ( )
inline

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

Definition at line 236 of file world.h.

References mut_hole(), and type_infer_univ().

◆ mut_hole_type()

Hole * mim::World::mut_hole_type ( )
inline

Definition at line 233 of file world.h.

References mut_hole(), and type_infer_univ().

Referenced by mim::tuple_of_dict().

◆ mut_hole_univ()

Hole * mim::World::mut_hole_univ ( )
inline

Definition at line 232 of file world.h.

References mut_hole(), and univ().

Referenced by type_infer_univ().

◆ mut_lam() [1/5]

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

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

References insert(), and pi().

◆ mut_lam() [3/5]

◆ mut_lam() [4/5]

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

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

References insert(), and pi().

◆ mut_pack()

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

Definition at line 373 of file world.h.

References mut_seq(), 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 268 of file world.h.

References insert(), and type().

◆ mut_rule()

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

Definition at line 321 of file world.h.

References insert(), and type().

Referenced by rule().

◆ mut_seq()

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

Definition at line 360 of file world.h.

References insert(), and type().

Referenced by mut_arr(), and mut_pack().

◆ mut_sigma() [1/2]

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

Definition at line 345 of file world.h.

References insert(), and type().

Referenced by mut_sigma().

◆ mut_sigma() [2/2]

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

A mutable Sigma of type level.

Definition at line 348 of file world.h.

References mut_sigma(), and type().

◆ muts() [1/2]

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

Definition at line 551 of file world.h.

◆ muts() [2/2]

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

Definition at line 553 of file world.h.

◆ name()

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

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

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

◆ next_run()

u32 mim::World::next_run ( )
inline

Definition at line 97 of file world.h.

◆ operator=()

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

References World().

◆ pack() [1/4]

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

Definition at line 375 of file world.h.

References seq().

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

◆ pack() [2/4]

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

Definition at line 377 of file world.h.

References seq().

◆ pack() [3/4]

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

Definition at line 379 of file world.h.

References seq().

◆ pack() [4/4]

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

Definition at line 381 of file world.h.

References seq().

◆ pack_unsafe()

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

Definition at line 383 of file world.h.

References seq_unsafe().

◆ pi() [1/4]

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

◆ pi() [2/4]

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

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

References pi(), and sigma().

Referenced by pi().

◆ prod() [1/2]

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

Definition at line 386 of file world.h.

References sigma(), and tuple().

◆ prod() [2/2]

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

Definition at line 385 of file world.h.

References sigma(), and tuple().

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

◆ proxy()

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

Definition at line 229 of file world.h.

References type().

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

◆ push()

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

Definition at line 118 of file world.h.

References get_loc(), and set_loc().

◆ raw_app() [1/3]

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

Definition at line 274 of file world.cpp.

References axm(), and type().

Referenced by app(), and raw_app().

◆ raw_app() [2/3]

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

Definition at line 260 of file world.cpp.

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

◆ raw_app() [3/3]

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

Definition at line 340 of file world.h.

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

Referenced by raw_app().

◆ reduce()

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

Yields the new body of [mut->var() -> arg]mut.

The new body may have fewer elements as mut->num_ops() according to Def::reduction_offset. E.g. a Pi has a Pi::reduction_offset of 1, and only Pi::dom will be reduced - not Pi::codom.

Definition at line 656 of file world.cpp.

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

◆ reform()

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

Definition at line 320 of file world.h.

References mim::Reform::infer().

Referenced by rule().

◆ register_annex() [1/2]

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

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

References register_annex().

◆ rule() [1/2]

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

Definition at line 325 of file world.h.

References reform(), and rule().

◆ rule() [2/2]

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

Definition at line 322 of file world.h.

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

Referenced by mim::Rule::immutabilize(), and rule().

◆ select()

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

Builds (f, t)#cond.

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

Definition at line 408 of file world.h.

References extract(), and tuple().

◆ seq() [1/4]

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

◆ seq() [2/4]

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

Definition at line 503 of file world.cpp.

References seq().

◆ seq() [3/4]

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

Definition at line 363 of file world.h.

References lit_nat(), and seq().

Referenced by seq().

◆ seq() [4/4]

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

Definition at line 364 of file world.h.

References seq().

Referenced by seq().

◆ seq_unsafe()

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

Definition at line 365 of file world.h.

References seq(), and top_nat().

Referenced by arr_unsafe(), and pack_unsafe().

◆ set() [1/2]

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

Definition at line 92 of file world.h.

References name(), and sym().

◆ set() [2/2]

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

Definition at line 91 of file world.h.

References name().

Referenced by main().

◆ set_loc()

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

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

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

◆ sigma() [2/2]

◆ split()

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

Definition at line 588 of file world.cpp.

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

◆ state()

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

Definition at line 85 of file world.h.

Referenced by inherit(), inherit_ptr(), and World().

◆ sym() [1/3]

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

Definition at line 74 of file world.cpp.

References driver().

◆ sym() [2/3]

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

Definition at line 76 of file world.cpp.

References driver().

◆ sym() [3/3]

◆ sym2external()

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

Definition at line 203 of file world.h.

◆ top()

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

Definition at line 473 of file world.h.

References ext(), and type().

Referenced by lit_idx_unsafe().

◆ top_nat()

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

Definition at line 476 of file world.h.

Referenced by seq_unsafe().

◆ tuple() [1/4]

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

the unit value of type []

Definition at line 395 of file world.h.

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

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

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

◆ tuple() [3/4]

◆ tuple() [4/4]

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

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

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

References lit_univ(), and type().

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

◆ type() [2/2]

◆ type_bool()

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

Definition at line 508 of file world.h.

◆ type_bot()

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

Definition at line 474 of file world.h.

Referenced by cn().

◆ type_i1()

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

Definition at line 509 of file world.h.

◆ type_i16()

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

Definition at line 513 of file world.h.

References type_int().

◆ type_i2()

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

Definition at line 510 of file world.h.

References type_int().

◆ type_i32()

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

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

References type_int().

◆ type_i64()

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

Definition at line 515 of file world.h.

References type_int().

◆ type_i8()

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

Definition at line 512 of file world.h.

References type_int().

◆ type_idx() [1/3]

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

◆ type_idx() [2/3]

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

Definition at line 500 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 502 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 218 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 506 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 497 of file world.h.

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

◆ type_top()

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

Definition at line 475 of file world.h.

◆ uinc()

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

◆ umax()

◆ uniq()

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

Definition at line 631 of file world.cpp.

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

◆ unit()

const Def * mim::World::unit ( bool term)
inline

Definition at line 358 of file world.h.

References sigma(), and tuple().

Referenced by seq().

◆ univ()

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

Definition at line 213 of file world.h.

Referenced by lit_univ(), and mut_hole_univ().

◆ var()

◆ vars() [1/2]

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

◆ vars() [2/2]

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

Definition at line 552 of file world.h.

◆ verify()

World & mim::World::verify ( )

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

Definition at line 687 of file world.cpp.

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

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

◆ watchpoint()

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

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

Definition at line 679 of file world.cpp.

Referenced by main().

◆ watchpoints()

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

Definition at line 162 of file world.h.

◆ write() [1/2]

void mim::World::write ( )

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

Definition at line 502 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 497 of file dump.cpp.

References dump().

Referenced by write().

Friends And Related Symbol Documentation

◆ swap

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

Definition at line 761 of file world.h.

References swap, and World().

Referenced by swap, and World().


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