MimIR
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  CurrLoc
 World::get_loc together with its interned DbgKey, so pushing/popping a Loc never re-interns it. More...
struct  State
class  Externals
class  Annexes

Public Types

using ScopedLoc = fe::Restore<CurrLoc>

Public Member Functions

Construction & Destruction
World & operator= (World)=delete
 World (Driver *, Sym name)
 World (Driver *, const State &)
 World (World &&other) noexcept
 ~World ()
std::unique_ptr< World > inherit ()
 Inherits the State into the new World.
Getters/Setters
const State & state () const
Driver & driver ()
const Driver & driver () const
fe::Error & error ()
const fe::Error & error () const
Zonker & zonker ()
Sym name () const
void set (Sym name)
void set (std::string_view name)
u32 curr_gid () const
 Manage global identifier - a unique number for each Def.
u32 next_gid ()
u32 curr_run () const
 Manage run - used to track fixed-point iterations to compute Def::free_vars.
u32 next_run ()
Flags & flags ()
 Retrieve compile Flags.
Loc
Loc get_loc () const
DbgKey dbg_key () const
 World::get_loc, already interned.
ScopedLoc push (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.

Dumping freezes: a dump that allocated gids would perturb the very program you are debugging. So whatever a frozen query cannot answer from what is already there comes back as nullptr.

bool is_frozen () const
auto freeze () const
 Freezes the World until the end of the scope and restores the previous frozen state afterwards:
Lenient

A lenient World builds ill-typed Apps and Tuples instead of reporting them.

An Analysis rewrites under partial substitutions, which may disagree with dependent types until its fixed point.

bool is_lenient () const
auto lenient () const
Debugging Features
const auto & breakpoints ()
const auto & watchpoints ()
const Def * gid2def (u32 gid)
 Lookup Def by gid.
void breakpoint (u32 gid)
 Trigger breakpoint in your debugger when creating a Def with this gid.
void watchpoint (u32 gid)
 Trigger breakpoint in your debugger when Def::setting a Def with this gid.
World & verify ()
 Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.
Externals & Annexes
const Externals & externals () const
Externals & externals ()
Annexes & annexes ()
const Annexes & annexes () const
const Def * annex (Sym sym)
 Lookup annex by Sym.
const Def * annex (flags_t flags)
 Lookup annex by flags.
const Def * annex (Enum auto id)
 Lookup annex by Axm::id.
template<annex_without_subs id>
const Def * annex ()
 Get Axm from a plugin.
const Def * import (const Def *def)
 Imports def of Driver::library into this World.
Level, Type, Var, Proxy, Hole
const Level * type_level ()
const Def * lsucc (const Def *op, level_t offset=1)
const Def * lmax (Defs levels)
const Def * level (Defs types)
 The lmax of the levels of all types, each of which must be a Type level.
const Type * type (const Def *level)
const Level * type_pending ()
 Placeholder type of a mutable whose sort Def::finalize infers from its ops.
const Type * type_infer_level ()
void postpone (const LMax *lmax, const Def *level)
 Postpones lmax = level as it does not determine the level Holes of lmax yet.
void solve_levels ()
 Defaults the level Holes of all postponed constraints that are still unknown to 0 and checks them.
template<level_t level = 0>
const Type * type ()
const Def * var (Def *mut)
const Def * inhabitant (const Def *type)
 The sole inhabitant of type, if it has exactly one, nullptr otherwise.
const Proxy * proxy (const Def *type, Defs ops, u32 tag, bool vars=false, bool muts=false)
Hole * mut_hole (const Def *type)
Hole * mut_hole_level ()
Hole * mut_hole_type ()
Axm
const Axm * axm (NormalizeFn n, u8 curry, u8 trip, const Def *type, plugin_t p, tag_t t, sub_t s)
const Axm * axm (const Def *type, plugin_t p, tag_t t, sub_t s)
const Axm * axm (NormalizeFn n, u8 curry, u8 trip, const Def *type)
 Builds a fresh Axm with descending Axm::sub.
const Axm * axm (const Def *type)
 See above.
Pi
const Pi * pi (const Def *dom, const Def *codom, bool implicit=false)
const Pi * pi (Defs dom, const Def *codom, bool implicit=false)
const Pi * pi (const Def *dom, Defs codom, bool implicit=false)
const Pi * pi (Defs dom, Defs codom, bool implicit=false)
Pi * mut_pi (const Def *type, bool implicit=false)
Cn

Pi with codom mim::Bottom

const Pi * cn ()
const Pi * cn (const Def *dom, bool implicit=false)
const Pi * cn (Defs dom, bool implicit=false)
const Pi * fn (const Def *dom, const Def *codom, bool implicit=false)
const Pi * fn (Defs dom, const Def *codom, bool implicit=false)
const Pi * fn (const Def *dom, Defs codom, bool implicit=false)
const Pi * fn (Defs dom, Defs codom, bool implicit=false)
Lam
const Def * filter (Lam::Filter filter)
const Lam * lam (const Pi *pi, Lam::Filter f, const Def *body)
Lam * mut_lam (const Pi *pi)
const Lam * con (const Def *dom, Lam::Filter f, const Def *body)
const Lam * con (Defs dom, Lam::Filter f, const Def *body)
const Lam * lam (const Def *dom, const Def *codom, Lam::Filter f, const Def *body)
const Lam * lam (Defs dom, const Def *codom, Lam::Filter f, const Def *body)
const Lam * lam (const Def *dom, Defs codom, Lam::Filter f, const Def *body)
const Lam * lam (Defs dom, Defs codom, Lam::Filter f, const Def *body)
const Lam * fun (const Def *dom, const Def *codom, Lam::Filter f, const Def *body)
const Lam * fun (Defs dom, const Def *codom, Lam::Filter f, const Def *body)
const Lam * fun (const Def *dom, Defs codom, Lam::Filter f, const Def *body)
const Lam * fun (Defs dom, Defs codom, Lam::Filter f, const Def *body)
Lam * mut_con (const Def *dom)
Lam * mut_con (Defs dom)
Lam * mut_lam (const Def *dom, const Def *codom)
Lam * mut_lam (Defs dom, const Def *codom)
Lam * mut_lam (const Def *dom, Defs codom)
Lam * mut_lam (Defs dom, Defs codom)
Lam * mut_fun (const Def *dom, const Def *codom)
Lam * mut_fun (Defs dom, const Def *codom)
Lam * mut_fun (const Def *dom, Defs codom)
Lam * mut_fun (Defs dom, Defs codom)
Rewrite Rules
const Reform * reform (const Def *dom)
Rule * mut_rule (const Reform *type)
const Rule * rule (const Reform *type, const Def *lhs, const Def *rhs, const Def *guard)
App
template<bool Normalize = true>
const Def * app (const Def *callee, const Def *arg)
template<bool Normalize = true>
const Def * app (const Def *callee, Defs args)
const Def * raw_app (const Axm *axm, u8 curry, u8 trip, const Def *type, const Def *callee, const Def *arg)
const Def * raw_app (const Def *type, const Def *callee, const Def *arg)
const Def * raw_app (const Def *type, const Def *callee, Defs args)
Sigma
Sigma * mut_sigma (const Def *type, size_t size)
template<level_t level = 0>
Sigma * mut_sigma (size_t size)
 A mutable Sigma of type level.
const Def * sigma (Defs ops)
const Sigma * sigma ()
 The unit type within Type 0.
Arr & Pack
template<level_t level = 0>
Arr * mut_arr ()
Arr * mut_arr (const Def *type)
Pack * mut_pack (const Def *type)
const Def * arr (Shape shape, const Def *body)
const Def * pack (Shape shape, const Def *body)
const Def * arr (Defs shape, const Def *body)
const Def * pack (Defs shape, const Def *body)
const Def * arr (fe::View< u64 > shape, const Def *body)
const Def * pack (fe::View< u64 > shape, const Def *body)
const Def * arr (u64 n, const Def *body)
const Def * pack (u64 n, const Def *body)
prod

Generic constructor for tuple or sigma.

const Def * prod (bool term, Defs ops)
const Def * prod (bool term)
 () or [].
Seq

These either build a Pack or an Arr depending on the first argument.

Oftentimes, the logic for Packs and Arrays can be quite similar; these methods help factoring such code.

Seq * mut_seq (bool is_pack, const Def *type)
const Def * seq (bool is_pack, Shape shape, const Def *body)
const Def * seq (bool is_pack, Defs shape, const Def *body)
const Def * seq (bool is_pack, u64 n, const Def *body)
const Def * seq (bool is_pack, fe::View< u64 > shape, const Def *body)
const Def * drop (const Seq *s, nat_t k)
 s without its leading k axes - its body once k covers all of them; nullptr if that isn't a type.
const Def * fuse (Seq *seq)
 «i: a; «j: b; T»» -> «v: (a, b); T» - the inverse of World::peel, for a nest that World::seq cannot fuse on construction because its body still binds an index.
const Def * peel (const Seq *seq, const Def *index)
 seq with the axes covered by index peeled off - the element itself once index covers all of them.
const Def * type_indices (Shape shape)
 The type of an index into shape: Idx n, a Sigma of those, or «i: r; Idx (s#i)» for a dynamic rank.
Tuple
const Def * tuple (Defs ops)
const Def * tuple (const Def *type, Defs ops)
 Ascribes type to this tuple - needed for dependently typed and mutable Sigmas.
const Tuple * tuple ()
 the unit value of type []
const Def * tuple (Sym sym)
 Converts sym to a tuple of type '«n; I8»'.
Extract
const Def * extract (const Def *d, const Def *i)
const Def * extract (const Def *d, u64 a, u64 i)
const Def * extract (const Def *d, u64 i)
const Def * select (const Def *cond, const Def *t, const Def *f)
 Builds (f, t)#cond.
Insert
const Def * insert (const Def *d, const Def *i, const Def *val)
const Def * insert (const Def *d, u64 a, u64 i, const Def *val)
const Def * insert (const Def *d, u64 i, const Def *val)
Lattice
template<bool Up>
const Def * ext (const Def *type)
const Def * bot (const Def *type)
const Def * top (const Def *type)
const Def * type_bot ()
const Def * type_top ()
Join & Variant
const Def * join (Defs ops)
Variant * mut_variant (const Def *type, size_t size)
const Def * variant (Defs ops)
const Def * inj (const Def *type, const Def *value)
const Def * inj (const Def *type, nat_t index, const Def *value)
 Injects value as case index of a Variant.
const Def * match (Defs)
Types
const Nat * type_nat ()
const Idx * type_idx ()
const Def * type_idx (const Def *size)
const Def * type_idx (nat_t size)
const Def * type_int (nat_t width)
 Constructs a type Idx of size 2^width.
const Def * type_bool ()
const Def * type_i1 ()
const Def * type_i8 ()
const Def * type_i16 ()
const Def * type_i32 ()
const Def * type_i64 ()
Nominal Newtypes
const Nom * nom (flags_t key, const Def *type)
 Make type Nominal under key.
const Def * name (const Def *nom, const Def *struc)
 Name a structural to make it nominal.
const Def * struc (const Def *nom)
 Get the structural part of a nominal.
implicit_app - Cope with implicit Arguments

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

const Def * implicit_holes (const Def *callee)
 Only places the Holes.
template<bool Normalize = true>
const Def * implicit_app (const Def *callee, const Def *arg)
template<bool Normalize = true>
const Def * implicit_app (const Def *callee, Defs args)
template<bool Normalize = true>
const Def * implicit_app (const Def *callee, nat_t arg)
template<bool Normalize = true>
requires std::is_same_v<std::underlying_type_t<decltype(arg)>, nat_t>
const Def * implicit_app (const Def *callee, Enum auto arg)
call

Complete curried call of callee obeying implicits.

template<bool Normalize = true, class... Args>
const Def * call (const Def *callee, auto &&arg, Args &&... args)
template<bool Normalize = true>
const Def * call (const Def *callee, auto &&arg)
 Base case.
template<Enum Id, bool Normalize = true, class... Args>
const Def * call (Id id, Args &&... args)
 Annex overload with enum instance as first argument.
template<class Id, bool Normalize = true, class... Args>
requires std::is_enum_v<Id>
const Def * call (Args &&... args)
 Annex overload with enum tempalte argument Id for annexes w/o subtag.
template<bool Normalize = true, class... Args>
const Def * call (flags_t id, Args &&... args)
 Annex overload with flags_t as first argument.
Singletons
const Def * single (const Def *)
 Singleton type formation.
const Def * wrap (const Def *)
 Singleton term introduction.
const Def * unwrap (const Def *)
 Singleton term elimination.
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.
const Def * reduce (const Var *var, const Def *arg, size_t i)
 As above but reduces only the i th op.
const Def * component (const Def *type, Defs parts, size_t n, size_t i)
 The type of component i of the n-ary type, given its leading components parts.
for_each

Visits all closed mutables in this World.

void for_each (bool elide_empty, std::function< void(Def *)>, bool schedule=false)
template<class M>
void for_each (bool elide_empty, std::invocable< M * > auto f, bool schedule=false)
dump/log
const fe::Log & log () const
 Log via log().e("...", args) etc.; owned by the Driver.
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 fe::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, DotConfig cfg={}) const
 Dumps DOT to os, configured via cfg (see DotConfig).
void dot (const char *file=nullptr, DotConfig cfg={}) const
 Same as above but write to file or std::cout if file is nullptr.

Friends

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

Lit

static constexpr nat_t Num_Lit_Nats = 64
 Def::arity of a Sigma is lit_nat(num_ops()) and Def::num_projs reads it straight back out, so a plain World::lit would hash-cons a Lit just to launder an integer.
const Lit * lit (const Def *type, u64 val)
const Lit * lit_level (u64 level)
const Lit * lit_level_0 ()
const Lit * lit_level_1 ()
const Lit * lit_nat (nat_t a)
const Lit * lit_nat_0 ()
const Lit * lit_nat_1 ()
const Lit * lit_nat_max ()
const Lit * lit_idx_1_0 ()
const Lit * lit_i1 ()
const Lit * lit_i8 ()
const Lit * lit_i16 ()
const Lit * lit_i32 ()
const Lit * lit_i64 ()
const Lit * lit_idx (nat_t size, u64 val)
 Constructs a Lit of type Idx of size size.
const Lit * lit_idx (std::integral auto 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_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 ()

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


Class Documentation

◆ mim::World::CurrLoc

struct mim::World::CurrLoc

World::get_loc together with its interned DbgKey, so pushing/popping a Loc never re-interns it.

Definition at line 46 of file world.h.

Class Members
DbgKey key = {}
Loc loc = {}

Member Typedef Documentation

◆ ScopedLoc

using mim::World::ScopedLoc = fe::Restore<CurrLoc>

Definition at line 129 of file world.h.

Constructor & Destructor Documentation

◆ World() [1/3]

mim::World::World ( Driver * driver,
Sym name )
explicit

Definition at line 208 of file world.cpp.

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

Referenced by operator=(), swap, verify(), World(), and World().

◆ World() [2/3]

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

◆ World() [3/3]

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

Definition at line 89 of file world.h.

References swap, and World().

◆ ~World()

mim::World::~World ( )
default

Member Function Documentation

◆ annex() [1/4]

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

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

◆ annex() [2/4]

const Def * mim::World::annex ( Enum auto id)
inline

Lookup annex by Axm::id.

Definition at line 303 of file world.h.

References annex().

Referenced by annex().

◆ annex() [3/4]

const Def * mim::World::annex ( flags_t flags)
inline

Lookup annex by flags.

An annex this World does not have yet is imported from Driver::library.

Definition at line 297 of file world.h.

References annexes(), and flags().

◆ annex() [4/4]

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

Lookup annex by Sym.

Definition at line 160 of file world.cpp.

References annex(), annexes(), driver(), flags(), and sym().

Referenced by annex(), annex(), mim::plug::autodiff::phase::Eval::augment_(), call(), call(), call(), and mim::plug::gpu::phase::run_stage().

◆ annexes() [1/2]

Annexes & mim::World::annexes ( )
inline

◆ annexes() [2/2]

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

Definition at line 290 of file world.h.

◆ app() [1/2]

◆ app() [2/2]

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

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

References name(), and sym().

◆ arr() [1/4]

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

Definition at line 485 of file world.h.

References seq().

◆ arr() [2/4]

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

Definition at line 487 of file world.h.

References seq().

◆ arr() [3/4]

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

Definition at line 483 of file world.h.

References seq().

Referenced by component(), ext(), insert(), seq(), and sigma().

◆ arr() [4/4]

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

Definition at line 489 of file world.h.

References seq().

◆ axm() [1/4]

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

See above.

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

References type().

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

◆ bot()

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

Definition at line 604 of file world.h.

References ext(), and type().

Referenced by join(), and variant().

◆ breakpoint()

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

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

Definition at line 1253 of file world.cpp.

Referenced by main().

◆ breakpoints()

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

Definition at line 174 of file world.h.

◆ call() [1/5]

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

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

Definition at line 693 of file world.h.

References annex(), and call().

◆ call() [2/5]

template<bool Normalize = true>
const Def * mim::World::call ( const Def * callee,
auto && arg )
inline

Base case.

Definition at line 681 of file world.h.

References implicit_app().

◆ call() [3/5]

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

◆ call() [4/5]

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

Annex overload with flags_t as first argument.

Definition at line 699 of file world.h.

References annex(), and call().

◆ call() [5/5]

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

Annex overload with enum instance as first argument.

Definition at line 687 of file world.h.

References annex(), and call().

◆ cn() [1/3]

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

Definition at line 398 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 399 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 400 of file world.h.

References cn(), and sigma().

Referenced by cn().

◆ component()

const Def * mim::World::component ( const Def * type,
Defs parts,
size_t n,
size_t i )

The type of component i of the n-ary type, given its leading components parts.

Definition at line 585 of file world.cpp.

References arr(), mim::Def::proj(), reduce(), tuple(), type(), and var().

◆ con() [1/2]

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

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

References cn(), and filter().

◆ curr_gid()

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

Manage global identifier - a unique number for each Def.

Definition at line 118 of file world.h.

Referenced by dump(), and mim::RWPhase::start().

◆ curr_run()

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

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

Definition at line 122 of file world.h.

◆ dbg_key()

DbgKey mim::World::dbg_key ( ) const
inline

World::get_loc, already interned.

Definition at line 133 of file world.h.

◆ debug_dump()

void mim::World::debug_dump ( )

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

Definition at line 1550 of file dump.cpp.

References debug_dump(), dump(), level(), and log().

Referenced by debug_dump().

◆ dot() [1/2]

void mim::World::dot ( const char * file = nullptr,
DotConfig cfg = {} ) const

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

Definition at line 265 of file dot.cpp.

◆ dot() [2/2]

void mim::World::dot ( std::ostream & os,
DotConfig cfg = {} ) const

Dumps DOT to os, configured via cfg (see DotConfig).

Definition at line 267 of file dot.cpp.

References dot(), externals(), mim::DotConfig::max, and muts().

Referenced by dot(), and dump().

◆ driver() [1/2]

◆ driver() [2/2]

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

Definition at line 108 of file world.h.

◆ drop()

const Def * mim::World::drop ( const Seq * s,
nat_t k )

s without its leading k axes - its body once k covers all of them; nullptr if that isn't a type.

Definition at line 637 of file world.cpp.

References is_frozen(), and seq().

Referenced by mim::Seq::elem(), and peel().

◆ dump() [1/2]

void mim::World::dump ( )

Dump to std::cout.

Definition at line 1548 of file dump.cpp.

References dump().

◆ dump() [2/2]

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

◆ error() [1/2]

fe::Error & mim::World::error ( )

Definition at line 222 of file world.cpp.

References driver().

Referenced by solve_levels().

◆ error() [2/2]

const fe::Error & mim::World::error ( ) const

Definition at line 223 of file world.cpp.

References driver().

◆ ext()

template<bool Up>
const Def * mim::World::ext ( const Def * type)

Definition at line 939 of file world.cpp.

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

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

◆ externals() [1/2]

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

Definition at line 287 of file world.h.

◆ externals() [2/2]

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

◆ extract() [1/3]

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

◆ extract() [2/3]

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

Definition at line 537 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 538 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 410 of file world.h.

References filter(), and lit_bool().

Referenced by mim::Lam::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 225 of file world.cpp.

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

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

◆ fn() [1/4]

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

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

References fn(), and sigma().

Referenced by fn().

◆ for_each() [1/2]

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

Definition at line 1220 of file world.cpp.

References externals(), muts(), and mim::post_order().

Referenced by for_each().

◆ for_each() [2/2]

template<class M>
void mim::World::for_each ( bool elide_empty,
std::invocable< M * > auto f,
bool schedule = false )
inline

Definition at line 739 of file world.h.

References for_each().

◆ freeze()

auto mim::World::freeze ( ) const
inlinenodiscard

Freezes the World until the end of the scope and restores the previous frozen state afterwards:

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

Definition at line 160 of file world.h.

Referenced by dump(), and mim::Def::operator<<.

◆ fun() [1/4]

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

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

References filter(), and fn().

◆ fuse()

const Def * mim::World::fuse ( Seq * seq)

«i: a; «j: b; T»» -> «v: (a, b); T» - the inverse of World::peel, for a nest that World::seq cannot fuse on construction because its body still binds an index.

Yields a Def::zonk_mut seq if the nest is ragged, i.e. if the inner extents depend on the outer index.

Definition at line 660 of file world.cpp.

References mim::Seq::body(), mim::Def::has_free_var(), mim::Def::has_var(), mim::Def::node(), seq(), mim::Seq::shape(), var(), mim::Def::zonk(), and mim::Def::zonk_mut().

◆ get_loc()

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

Definition at line 132 of file world.h.

Referenced by postpone().

◆ gid2def()

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

Lookup Def by gid.

Definition at line 1256 of file world.cpp.

◆ implicit_app() [1/4]

template<bool Normalize>
const Def * mim::World::implicit_app ( const Def * callee,
const Def * arg )

Definition at line 411 of file world.cpp.

References app(), and implicit_holes().

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

◆ implicit_app() [2/4]

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

Definition at line 656 of file world.h.

References implicit_app(), and tuple().

◆ implicit_app() [3/4]

template<bool Normalize = true>
requires std::is_same_v<std::underlying_type_t<decltype(arg)>, nat_t>
const Def * mim::World::implicit_app ( const Def * callee,
Enum auto arg )
inline

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

References implicit_app(), and lit_nat().

◆ implicit_holes()

const Def * mim::World::implicit_holes ( const Def * callee)

Only places the Holes.

Definition at line 401 of file world.cpp.

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

Referenced by implicit_app().

◆ import()

const Def * mim::World::import ( const Def * def)
inline

Imports def of Driver::library into this World.

Definition at line 314 of file world.h.

Referenced by mim::Driver::move_to_library().

◆ inhabitant()

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

The sole inhabitant of type, if it has exactly one, nullptr otherwise.

Definition at line 342 of file world.h.

References mim::App, app(), mim::Arr, mim::Lit::isa(), lit_idx_1_0(), mim::Sigma, mim::Single, type(), and mim::Variant.

Referenced by mim::eta_callee(), insert(), mim::Analysis::is_singleton(), raw_app(), and var().

◆ inherit()

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

Inherits the State into the new World.

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

Definition at line 97 of file world.h.

References driver(), and state().

Referenced by mim::Driver::move_to_library().

◆ inj() [1/2]

◆ inj() [2/2]

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

◆ 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 547 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 548 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 151 of file world.h.

Referenced by app(), drop(), insert(), and peel().

◆ is_lenient()

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

Definition at line 167 of file world.h.

Referenced by app().

◆ join()

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

Definition at line 948 of file world.cpp.

References bot(), join(), level(), mim::Def::ops(), push(), top(), and type().

Referenced by inj(), join(), 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 419 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 421 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 414 of file world.h.

References filter(), and pi().

Referenced by app(), and dump().

◆ lam() [4/5]

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

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

References filter(), and pi().

◆ lenient()

auto mim::World::lenient ( ) const
inlinenodiscard

Definition at line 168 of file world.h.

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

◆ level()

const Def * mim::World::level ( Defs types)

The lmax of the levels of all types, each of which must be a Type level.

Definition at line 349 of file world.cpp.

References mim::Lit::isa(), level(), mim::level_of(), lit_level(), lmax(), and type().

Referenced by debug_dump(), join(), level(), lit_level(), lmax(), postpone(), type(), and type().

◆ lit()

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

Definition at line 919 of file world.cpp.

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

Referenced by lit_idx(), lit_level(), lit_nat(), and World().

◆ lit_bool()

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

Definition at line 595 of file world.h.

Referenced by filter().

◆ lit_ff()

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

Definition at line 596 of file world.h.

Referenced by app().

◆ lit_i1() [1/2]

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

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

References lit_int().

◆ lit_i16() [1/2]

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

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

References lit_int().

◆ lit_i32() [1/2]

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

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

References lit_int().

◆ lit_i64() [1/2]

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

Definition at line 573 of file world.h.

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

◆ lit_i64() [2/2]

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

Definition at line 587 of file world.h.

References lit_int().

◆ lit_i8() [1/2]

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

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

References lit_int().

◆ lit_idx() [1/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 576 of file world.h.

References lit(), and type_idx().

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

◆ lit_idx() [2/2]

const Lit * mim::World::lit_idx ( std::integral auto val)
inline

Definition at line 578 of file world.h.

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

Referenced by lit_idx().

◆ lit_idx_1_0()

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

Definition at line 567 of file world.h.

Referenced by inhabitant().

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

References lit_idx().

◆ lit_int()

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

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

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

Definition at line 582 of file world.h.

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

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

◆ lit_level()

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

Definition at line 554 of file world.h.

References level(), lit(), lit_level_0(), lit_level_1(), and type_level().

Referenced by level(), lmax(), lsucc(), and type().

◆ lit_level_0()

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

Definition at line 557 of file world.h.

Referenced by lit_level(), type(), and World().

◆ lit_level_1()

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

Definition at line 558 of file world.h.

Referenced by lit_level(), type(), and World().

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

◆ lit_nat_1()

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

Definition at line 565 of file world.h.

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

◆ lit_nat_max()

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

Definition at line 566 of file world.h.

◆ lit_tt()

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

Definition at line 597 of file world.h.

Referenced by app().

◆ lmax()

const Def * mim::World::lmax ( Defs levels)

◆ log()

const fe::Log & mim::World::log ( ) const

◆ lsucc()

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

Definition at line 247 of file world.cpp.

References mim::Lit::isa(), lit_level(), lmax(), lsucc(), and mim::type_of().

Referenced by lsucc().

◆ match()

◆ mut_arr() [1/2]

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

Definition at line 478 of file world.h.

References mut_arr(), and type().

Referenced by mut_arr(), and type_indices().

◆ mut_arr() [2/2]

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

Definition at line 481 of file world.h.

References mut_seq(), and type().

◆ mut_con() [1/2]

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

◆ mut_con() [2/2]

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

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

References fn(), and insert().

◆ mut_fun() [2/4]

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

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

References fn(), and insert().

◆ mut_hole()

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

Definition at line 361 of file world.h.

References insert(), and type().

Referenced by implicit_holes(), mut_hole_level(), mut_hole_type(), and mim::tuple_of_dict().

◆ mut_hole_level()

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

Definition at line 362 of file world.h.

References mut_hole(), and type_level().

Referenced by type_infer_level().

◆ mut_hole_type()

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

Definition at line 363 of file world.h.

References mut_hole(), and type_infer_level().

Referenced by mim::tuple_of_dict().

◆ mut_lam() [1/5]

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

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

References insert(), and pi().

◆ mut_pack()

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

Definition at line 482 of file world.h.

References mut_seq(), and type().

◆ mut_pi()

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

Definition at line 390 of file world.h.

References insert(), and type().

◆ mut_rule()

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

Definition at line 443 of file world.h.

References insert(), and type().

◆ mut_seq()

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

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

References insert(), and type().

Referenced by mut_sigma(), and mim::SingleErasure::rewrite_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 467 of file world.h.

References mut_sigma(), and type().

◆ mut_variant()

Variant * mim::World::mut_variant ( const Def * type,
size_t size )
inline

Definition at line 613 of file world.h.

References insert(), and type().

◆ muts() [1/2]

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

Definition at line 715 of file world.h.

Referenced by mim::Def::collect_locals(), dot(), dump(), for_each(), proxy(), and verify().

◆ muts() [2/2]

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

Definition at line 717 of file world.h.

◆ name() [1/2]

◆ name() [2/2]

const Def * mim::World::name ( const Def * nom,
const Def * struc )

Name a structural to make it nominal.

Definition at line 1140 of file world.cpp.

References mim::Def::blame(), mim::Check::coerce(), nom(), mim::Nom::op(), mim::type_of(), and mim::Def::zonk().

◆ next_gid()

u32 mim::World::next_gid ( )
inline

Definition at line 119 of file world.h.

◆ next_run()

u32 mim::World::next_run ( )
inline

Definition at line 123 of file world.h.

◆ nom()

const Nom * mim::World::nom ( flags_t key,
const Def * type )

Make type Nominal under key.

Definition at line 1134 of file world.cpp.

References type().

Referenced by dump(), inj(), name(), and struc().

◆ operator=()

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

References name(), and World().

◆ pack() [1/4]

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

Definition at line 486 of file world.h.

References seq().

◆ pack() [2/4]

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

Definition at line 488 of file world.h.

References seq().

◆ pack() [3/4]

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

Definition at line 484 of file world.h.

References seq().

Referenced by ext().

◆ pack() [4/4]

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

Definition at line 490 of file world.h.

References seq().

◆ peel()

const Def * mim::World::peel ( const Seq * seq,
const Def * index )

seq with the axes covered by index peeled off - the element itself once index covers all of them.

Definition at line 646 of file world.cpp.

References mim::Seq::body(), drop(), mim::Def::has_var(), is_frozen(), mim::Seq::reduce(), seq(), mim::Shape::Shape(), mim::Seq::shape(), and mim::Def::unfold_type().

Referenced by insert().

◆ pi() [1/4]

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

Definition at line 386 of file world.h.

References mim::Pi::infer().

Referenced by app(), cn(), implicit_holes(), lam(), lam(), lam(), lam(), lam(), match(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), mut_lam(), and World().

◆ pi() [2/4]

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

Definition at line 388 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 387 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 389 of file world.h.

References pi(), and sigma().

Referenced by pi().

◆ postpone()

void mim::World::postpone ( const LMax * lmax,
const Def * level )
inline

Postpones lmax = level as it does not determine the level Holes of lmax yet.

Definition at line 328 of file world.h.

References get_loc(), level(), and lmax().

◆ prod() [1/2]

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

() or [].

Definition at line 498 of file world.h.

References sigma(), and tuple().

◆ prod() [2/2]

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

◆ proxy()

const Proxy * mim::World::proxy ( const Def * type,
Defs ops,
u32 tag,
bool vars = false,
bool muts = false )
inline
See also
Proxy::tracks_vars, Proxy::tracks_muts

Definition at line 357 of file world.h.

References muts(), type(), and vars().

◆ push()

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

Definition at line 1285 of file world.cpp.

References driver().

Referenced by join(), lmax(), and solve_levels().

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

References axm(), inhabitant(), 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 492 of file world.cpp.

References axm(), mim::Axm::next(), raw_app(), 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 459 of file world.h.

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

Referenced by raw_app().

◆ reduce() [1/2]

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

References mim::Var::binder(), mim::Def::reduction_offset(), var(), and mim::VarRewriter::VarRewriter().

Referenced by app(), and component().

◆ reduce() [2/2]

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

As above but reduces only the i th op.

A dependent Sigma is projected while it is still being built - its later ops do not exist yet - so reducing all of them is not an option there.

Definition at line 1201 of file world.cpp.

References mim::Var::binder(), mim::Def::reduction_offset(), var(), and mim::VarRewriter::VarRewriter().

◆ reform()

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

Definition at line 442 of file world.h.

References mim::Reform::infer().

◆ rule()

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

Definition at line 444 of file world.h.

References type().

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

References extract(), and tuple().

◆ seq() [1/4]

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

Definition at line 914 of file world.cpp.

References seq(), and tuple().

◆ seq() [2/4]

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

Definition at line 509 of file world.h.

References lit_nat(), and seq().

◆ seq() [3/4]

◆ seq() [4/4]

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

Definition at line 508 of file world.h.

References lit_nat(), and seq().

Referenced by seq().

◆ set() [1/2]

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

Definition at line 115 of file world.h.

References name(), and sym().

◆ set() [2/2]

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

Definition at line 114 of file world.h.

References name().

Referenced by mim::plug::gpu::phase::SplitOffKernels::rewrite_mut_Lam().

◆ sigma() [1/2]

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

The unit type within Type 0.

Definition at line 471 of file world.h.

◆ sigma() [2/2]

◆ single()

const Def * mim::World::single ( const Def * op)

Singleton type formation.

Definition at line 1114 of file world.cpp.

Referenced by inj(), unwrap(), and wrap().

◆ solve_levels()

void mim::World::solve_levels ( )

Defaults the level Holes of all postponed constraints that are still unknown to 0 and checks them.

Definition at line 313 of file world.cpp.

References mim::Check::alpha(), mim::default_level(), error(), mim::eval0(), and push().

◆ state()

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

Definition at line 106 of file world.h.

Referenced by inherit(), and World().

◆ struc()

const Def * mim::World::struc ( const Def * nom)

Get the structural part of a nominal.

Definition at line 1150 of file world.cpp.

References mim::Def::blame(), mim::Def::isa_type(), name(), nom(), mim::Nom::op(), mim::type_of(), and mim::Def::zonk().

◆ sym() [1/3]

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

Definition at line 227 of file world.cpp.

References driver().

◆ sym() [2/3]

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

Definition at line 229 of file world.cpp.

References driver().

◆ sym() [3/3]

◆ top()

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

Definition at line 605 of file world.h.

References ext(), and type().

Referenced by join().

◆ tuple() [1/4]

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

the unit value of type []

Definition at line 530 of file world.h.

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

References tuple(), and type().

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

References level(), lit_level(), and type().

◆ type() [2/2]

◆ type_bool()

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

Definition at line 633 of file world.h.

◆ type_bot()

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

Definition at line 606 of file world.h.

Referenced by cn().

◆ type_i1()

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

Definition at line 634 of file world.h.

◆ type_i16()

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

Definition at line 636 of file world.h.

References type_int().

◆ type_i32()

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

Definition at line 637 of file world.h.

References type_int().

◆ type_i64()

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

Definition at line 638 of file world.h.

References type_int().

Referenced by mim::plug::affine::phase::LowerIndex::rewrite().

◆ type_i8()

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

Definition at line 635 of file world.h.

References type_int().

◆ type_idx() [1/3]

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

Definition at line 623 of file world.h.

Referenced by lit_idx(), type_indices(), type_int(), and World().

◆ type_idx() [2/3]

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

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

References lit_nat(), and type_idx().

Referenced by type_idx().

◆ type_indices()

const Def * mim::World::type_indices ( Shape shape)

The type of an index into shape: Idx n, a Sigma of those, or «i: r; Idx (s#i)» for a dynamic rank.

Definition at line 678 of file world.cpp.

References extract(), mut_arr(), mim::Arr::set_body(), mim::Arr::set_shape(), sigma(), type(), type_idx(), and mim::Def::zonk_mut().

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

◆ type_infer_level()

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

Definition at line 326 of file world.h.

References mut_hole_level(), and type().

Referenced by 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 631 of file world.h.

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

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

◆ type_level()

const Level * mim::World::type_level ( )
inline

Definition at line 319 of file world.h.

Referenced by lit_level(), mut_hole_level(), type_pending(), and World().

◆ type_nat()

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

Definition at line 622 of file world.h.

Referenced by lit_nat(), and World().

◆ type_pending()

const Level * mim::World::type_pending ( )
inline

Placeholder type of a mutable whose sort Def::finalize infers from its ops.

Definition at line 325 of file world.h.

References type_level().

◆ type_top()

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

Definition at line 607 of file world.h.

◆ unwrap()

const Def * mim::World::unwrap ( const Def * op)

Singleton term elimination.

Note
There is no explicite Unwrap node.

Definition at line 1128 of file world.cpp.

References mim::Def::op(), single(), and mim::type_of().

◆ var()

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

◆ variant()

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

Definition at line 1023 of file world.cpp.

References bot(), mim::Variant::infer(), and mim::Def::zonk().

Referenced by inj(), and match().

◆ vars() [1/2]

◆ vars() [2/2]

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

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

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

Referenced by 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 1254 of file world.cpp.

Referenced by main().

◆ watchpoints()

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

Definition at line 175 of file world.h.

◆ wrap()

const Def * mim::World::wrap ( const Def * op)

Singleton term introduction.

Definition at line 1123 of file world.cpp.

References single().

◆ write() [1/2]

void mim::World::write ( )

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

Definition at line 1559 of file dump.cpp.

References mim::file_stem(), and write().

◆ write() [2/2]

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

Write to a file named file.

Definition at line 1554 of file dump.cpp.

References dump(), and write().

Referenced by write(), and write().

◆ zonker()

Zonker & mim::World::zonker ( )
inline

Definition at line 111 of file world.h.

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

◆ swap

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

Definition at line 993 of file world.h.

References swap, and World().

Referenced by swap, and World().

Member Data Documentation

◆ Num_Lit_Nats

nat_t mim::World::Num_Lit_Nats = 64
staticconstexpr

Def::arity of a Sigma is lit_nat(num_ops()) and Def::num_projs reads it straight back out, so a plain World::lit would hash-cons a Lit just to launder an integer.

Worth ~4% of an -Og Debug compile.

Definition at line 561 of file world.h.

Referenced by lit_nat(), and World().


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