MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
mim::Def Class Referenceabstract

Base class for all Defs. More...

#include <mim/def.h>

Inheritance diagram for mim::Def:
[legend]

Public Member Functions

Getters
Worldworld () const noexcept
 
constexpr flags_t flags () const noexcept
 
constexpr u32 gid () const noexcept
 Global id - unique number for this Def.
 
constexpr u32 tid () const noexcept
 Trie id - only used in Trie.
 
constexpr u32 mark () const noexcept
 Used internally by free_vars().
 
constexpr size_t hash () const noexcept
 
constexpr Node node () const noexcept
 
std::string_view node_name () const
 
Judgement

What kind of Judgement represents this Def?

u32 judge () const noexcept
 
bool is_form () const noexcept
 
bool is_intro () const noexcept
 
bool is_elim () const noexcept
 
bool is_meta () const noexcept
 
type
const Deftype () const noexcept
 Yields the "raw" type of this Def (maybe nullptr).
 
const Defunfold_type () const
 Yields the type of this Def and builds a new Type (UInc n) if necessary.
 
bool is_term () const
 
arity
const Defarity () const
 
std::optional< nat_tisa_lit_arity () const
 
nat_t as_lit_arity () const
 
ops
template<size_t N = std::dynamic_extent>
constexpr auto ops () const noexcept
 
const Defop (size_t i) const noexcept
 
constexpr size_t num_ops () const noexcept
 
Setting Ops (Mutables Only)

You can set and change the Def::ops of a mutable after construction.

However, you have to obey the following rules: If Def::is_set() is ...

MimIR assumes that a mutable is final, when its last operand is set. Then, Def::check() will be invoked.

Defset (size_t i, const Def *)
 Successively set from left to right.
 
Defset (Defs ops)
 Def::set ops all at once.
 
Defunset ()
 Unsets all Def::ops; works even, if not set at all or partially.
 
bool is_set () const
 Yields true if empty or the last op is set.
 
deps

All dependencies of a Def and includes:

Defs deps () const noexcept
 
const Defdep (size_t i) const noexcept
 
size_t num_deps () const noexcept
 
has_dep

Checks whether one Def::deps() contains specific elements defined in Dep.

This works up to the next mutable. For example, consider the Tuple tup: (?, lam (x: Nat) = y):

bool has_hole = tup->has_dep(Dep::Hole); // true
bool has_mut = tup->has_dep(Dep::Mut); // true
bool has_var = tup->has_dep(Dep::Var); // false - y is contained in another mutable
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
Definition def.h:378
@ Var
Definition def.h:100
@ Hole
Definition def.h:101
@ Mut
Definition def.h:99
bool has_dep () const
 
bool has_dep (Dep d) const
 
bool has_dep (unsigned u) const
 
proj

Splits this Def via Extracts or directly accessing the Def::ops in the case of Sigmas or Arrays.

std::array<const Def*, 2> ab = def->projs<2>();
std::array<u64, 2> xy = def->projs<2>([](auto def) { return Lit::as(def); });
auto [a, b] = def->projs<2>();
auto [x, y] = def->projs<2>([](auto def) { return Lit::as(def); });
Vector<const Def*> projs1 = def->projs(); // "projs1" has def->num_projs() many elements
Vector<const Def*> projs2 = def->projs(n);// "projs2" has n elements - asserts if incorrect
// same as above but applies Lit::as<nat_t>(def) to each element
Vector<const Lit*> lits1 = def->projs( [](auto def) { return Lit::as(def); });
Vector<const Lit*> lits2 = def->projs(n, [](auto def) { return Lit::as(def); });
static T as(const Def *def)
Definition def.h:724
Vector(I, I, A=A()) -> Vector< typename std::iterator_traits< I >::value_type, Default_Inlined_Size< typename std::iterator_traits< I >::value_type >, A >
nat_t num_projs () const
 Yields Def::as_lit_arity(), if it is in fact a Lit, or 1 otherwise.
 
nat_t num_tprojs () const
 As above but yields 1, if Flags::scalarize_threshold is exceeded.
 
const Defproj (nat_t a, nat_t i) const
 Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.
 
const Defproj (nat_t i) const
 As above but takes Def::num_projs as arity.
 
const Deftproj (nat_t i) const
 As above but takes Def::num_tprojs.
 
template<nat_t A = std::dynamic_extent, class F>
auto projs (F f) const
 Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (otherwise).
 
template<class F>
auto tprojs (F f) const
 
template<class F>
auto projs (nat_t a, F f) const
 
template<nat_t A = std::dynamic_extent>
auto projs () const
 
auto tprojs () const
 
auto projs (nat_t a) const
 
var

Retrieve Var for mutables.

See also
proj
nat_t num_vars () noexcept
 
nat_t num_tvars () noexcept
 
const Defvar (nat_t a, nat_t i) noexcept
 
const Defvar (nat_t i) noexcept
 
const Deftvar (nat_t i) noexcept
 
template<nat_t A = std::dynamic_extent, class F>
auto vars (F f) noexcept
 
template<class F>
auto tvars (F f) noexcept
 
template<nat_t A = std::dynamic_extent>
auto vars () noexcept
 
auto tvars () noexcept
 
template<class F>
auto vars (nat_t a, F f) noexcept
 
auto vars (nat_t a) noexcept
 
const Defvar ()
 Not necessarily a Var: E.g., if the return type is [], this will yield ().
 
const Varhas_var ()
 Only returns not nullptr, if Var of this mutable has ever been created.
 
const Varhas_var () const
 As above if this is a mutable.
 
Free Vars and Muts
Muts local_muts () const
 Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }.
 
Vars local_vars () const
 Vars reachable by following immutable deps().
 
Vars free_vars () const
 Compute a global solution by transitively following mutables as well.
 
Vars free_vars ()
 
Muts users ()
 Set of mutables where this mutable is locally referenced.
 
bool is_open () const
 Has free_vars()?
 
bool is_closed () const
 Has no free_vars()?
 
external
bool is_external () const
 
void make_external ()
 
void make_internal ()
 
void transfer_external (Def *to)
 
Casts
template<class T = Def>
const T * isa_imm () const
 
template<class T = Def>
const T * as_imm () const
 
template<class T = Def, class R>
const T * isa_imm (R(T::*f)() const) const
 
template<class T = Def, bool invert = false>
T * isa_mut () const
 If this is mutable, it will cast constness away and perform a dynamic_cast to T.
 
template<class T = Def, bool invert = false>
T * as_mut () const
 Asserts that this is a mutable, casts constness away and performs a static_cast to T.
 
Dbg Getters
Dbg dbg () const
 
Loc loc () const
 
Sym sym () const
 
std::string unique_name () const
 name + "_" + Def::gid
 
Dbg Setters

Every subclass S of Def has the same setters that return S*/const S* via the mixin Setters.

template<bool Ow = false>
const Defset (Loc l) const
 
template<bool Ow = false>
Defset (Loc l)
 
template<bool Ow = false>
const Defset (Sym s) const
 
template<bool Ow = false>
Defset (Sym s)
 
template<bool Ow = false>
const Defset (std::string s) const
 
template<bool Ow = false>
Defset (std::string s)
 
template<bool Ow = false>
const Defset (Loc l, Sym s) const
 
template<bool Ow = false>
Defset (Loc l, Sym s)
 
template<bool Ow = false>
const Defset (Loc l, std::string s) const
 
template<bool Ow = false>
Defset (Loc l, std::string s)
 
template<bool Ow = false>
const Defset (Dbg d) const
 
template<bool Ow = false>
Defset (Dbg d)
 
debug_prefix/suffix

Prepends/Appends a prefix/suffix to Def::name - but only in Debug build.

const Defdebug_prefix (std::string) const
 
const Defdebug_suffix (std::string) const
 
Rebuild
Defstub (World &w, const Def *type)
 
Defstub (const Def *type)
 
const Defrebuild (World &w, const Def *type, Defs ops) const
 Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
 
const Defrebuild (const Def *type, Defs ops) const
 
virtual const Defimmutabilize ()
 Tries to make an immutable from a mutable.
 
bool is_immutabilizable ()
 
const Defrefine (size_t i, const Def *new_op) const
 
template<size_t N = std::dynamic_extent>
constexpr auto reduce (const Def *arg) const
 
virtual constexpr size_t reduction_offset () const noexcept
 First Def::op that needs to be dealt with during reduction; e.g.
 
Type Checking
virtual const Defcheck (size_t i, const Def *def)
 Checks whether the ith operand can be set to def.
 
virtual const Defcheck ()
 After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
 
const Defzonk () const
 If Holes have been filled, reconstruct the program without them.
 
dump
void dump () const
 
void dump (int max) const
 
void write (int max) const
 
void write (int max, const char *file) const
 
std::ostream & stream (std::ostream &, int max) const
 
dot

Dumps DOT to os while obeying maximum recursion depth of max.

If types is true, Def::type() dependencies will be followed as well.

void dot (std::ostream &os, uint32_t max=0xFFFFFF, bool types=false) const
 
void dot (const char *file=nullptr, uint32_t max=0xFFFFFF, bool types=false) const
 Same as above but write to file or std::cout if file is nullptr.
 
void dot (const std::string &file, uint32_t max=0xFFFFFF, bool types=false) const
 

Protected Member Functions

C'tors and D'tors
 Def (World *, Node, const Def *type, Defs ops, flags_t flags)
 Constructor for an immutable Def.
 
 Def (Node, const Def *type, Defs ops, flags_t flags)
 As above but World retrieved from type.
 
 Def (Node, const Def *type, size_t num_ops, flags_t flags)
 Constructor for a mutable Def.
 
virtual ~Def ()=default
 
Wrappers for World::sym

These are here to have Def::setters inline without including mim/world.h.

Sym sym (const char *) const
 
Sym sym (std::string_view) const
 
Sym sym (std::string) const
 

Protected Attributes

Dbg dbg_
 
union { 
 
NormalizeFn normalizer_
 Axm only: Axms use this member to store their normalizer.
 
const Axmaxm_
 App only: Curried Apps of Axms use this member to propagate the Axm.
 
const Varvar_
 Mutable only: Var of a mutable.
 
Worldworld_
 
};  
 
flags_t flags_
 
u8 curry_ = 0
 
u8 trip_ = 0
 

Private Member Functions

virtual Defstub_ (World &, const Def *)
 
virtual const Defrebuild_ (World &w, const Def *type, Defs ops) const =0
 

Friends

template<class D, size_t N>
class Sets
 
class World
 
void swap (World &, World &) noexcept
 
std::ostream & operator<< (std::ostream &os, const Def *def)
 This will stream def as an operand.
 

Detailed Description

Base class for all Defs.

These are the most important subclasses:

Type Formation Term Introduction Term Elimination
Pi Lam App
Sigma / Arr Tuple / Pack Extract
Insert Insert
Uniq Wrap Unwrap
Join Inj Match
Meet Merge Split
Nat Lit
Idx Lit

In addition there is:

  • Var: A variable. Currently the following Defs may be binders:
  • Axm: To introduce new entities.
  • Proxy: Used for intermediate values during optimizations.
  • Hole: A metavariable filled in by the type inference (always mutable as holes are filled in later).
  • Type, Univ, UMax, UInc: To keep track of type levels.

The data layout (see World::alloc and Def::deps) looks like this:

Def| type | op(0) ... op(num_ops-1) |
|-----------ops-----------|
|--------------------------------| if type() != nullptr && is_set()
|-------------------------| if type() == nullptr && is_set()
|------| if type() != nullptr && !is_set()
|| if type() == nullptr && !is_set()
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:262
Defs deps() const noexcept
Definition def.cpp:399
constexpr auto ops() const noexcept
Definition def.h:261
const Def * op(size_t i) const noexcept
Definition def.h:264
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:242
constexpr size_t num_ops() const noexcept
Definition def.h:265
Attention
This means that any subclass of Def must not introduce additional members.
See also
Immutables vs. Mutables

Definition at line 198 of file def.h.

Constructor & Destructor Documentation

◆ Def() [1/3]

mim::Def::Def ( World * world,
Node node,
const Def * type,
Defs ops,
flags_t flags )
protected

Constructor for an immutable Def.

Definition at line 23 of file def.cpp.

References flags(), flags_, mim::hash_begin(), mim::Mut, node(), ops(), type(), mim::Univ, var(), World, and world().

◆ Def() [2/3]

mim::Def::Def ( Node n,
const Def * type,
Defs ops,
flags_t flags )
protected

As above but World retrieved from type.

Definition at line 81 of file def.cpp.

References flags(), ops(), and type().

◆ Def() [3/3]

mim::Def::Def ( Node node,
const Def * type,
size_t num_ops,
flags_t flags )
protected

Constructor for a mutable Def.

Definition at line 84 of file def.cpp.

References flags(), flags_, gid(), mim::hash(), mim::Mut, mim::World::next_gid(), node(), mim::None, num_ops(), type(), and world().

◆ ~Def()

virtual mim::Def::~Def ( )
protectedvirtualdefault

References World.

Member Function Documentation

◆ arity()

const Def * mim::Def::arity ( ) const

◆ as_imm()

template<class T = Def>
const T * mim::Def::as_imm ( ) const
inline

Definition at line 420 of file def.h.

References as_mut().

◆ as_lit_arity()

nat_t mim::Def::as_lit_arity ( ) const
inline

◆ as_mut()

template<class T = Def, bool invert = false>
T * mim::Def::as_mut ( ) const
inline

Asserts that this is a mutable, casts constness away and performs a static_cast to T.

Definition at line 433 of file def.h.

Referenced by as_imm(), mim::plug::clos::clos_type(), mim::plug::autodiff::AutoDiffEval::derive_(), mim::ast::TuplePtrn::emit_body(), mim::Var::mut(), mim::Var::rebuild_(), and mim::Cleanup::start().

◆ check() [1/2]

virtual const Def * mim::Def::check ( )
inlinevirtual

After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.

The method returns a possibly updated version of its type (e.g. where Holes have been resolved). If different from Def::type, it will update its Def::type to a Def::zonked version of that.

Reimplemented in mim::Arr, mim::Pi, and mim::Sigma.

Definition at line 521 of file def.h.

References type().

Referenced by set().

◆ check() [2/2]

virtual const Def * mim::Def::check ( size_t i,
const Def * def )
inlinevirtual

Checks whether the ith operand can be set to def.

The method returns a possibly updated version of def (e.g. where Holes have been resolved). This is the actual def that will be set as the ith operand.

Reimplemented in mim::Arr, mim::Lam, mim::Pi, and mim::Sigma.

Definition at line 516 of file def.h.

◆ dbg()

◆ debug_prefix()

const Def * mim::Def::debug_prefix ( std::string prefix) const

Definition at line 427 of file def.cpp.

References dbg_, sym(), and world().

◆ debug_suffix()

const Def * mim::Def::debug_suffix ( std::string suffix) const

Definition at line 428 of file def.cpp.

References dbg_, sym(), and world().

◆ dep()

const Def * mim::Def::dep ( size_t i) const
inlinenoexcept

Definition at line 294 of file def.h.

References dep(), and deps().

Referenced by dep().

◆ deps()

◆ dot() [1/3]

void mim::Def::dot ( const char * file = nullptr,
uint32_t max = 0xFFFFFF,
bool types = false ) const

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

Definition at line 129 of file dot.cpp.

References dot().

◆ dot() [2/3]

void mim::Def::dot ( const std::string & file,
uint32_t max = 0xFFFFFF,
bool types = false ) const
inline

Definition at line 545 of file def.h.

References dot().

◆ dot() [3/3]

void mim::Def::dot ( std::ostream & os,
uint32_t max = 0xFFFFFF,
bool types = false ) const

Definition at line 127 of file dot.cpp.

Referenced by dot(), and dot().

◆ dump() [1/2]

void mim::Def::dump ( ) const

Definition at line 447 of file dump.cpp.

◆ dump() [2/2]

void mim::Def::dump ( int max) const

Definition at line 448 of file dump.cpp.

References stream().

◆ flags()

◆ free_vars() [1/2]

Vars mim::Def::free_vars ( )

Definition at line 291 of file def.cpp.

References free_vars(), is_set(), and world().

◆ free_vars() [2/2]

Vars mim::Def::free_vars ( ) const

Compute a global solution by transitively following mutables as well.

Definition at line 279 of file def.cpp.

References isa_mut(), local_muts(), local_vars(), vars(), mim::World::vars(), and world().

Referenced by mim::Nest::contains(), free_vars(), mim::plug::clos::ClosConvPrep::from_outer_scope(), is_closed(), is_open(), mim::VarRewriter::rewrite_imm(), and mim::VarRewriter::rewrite_mut().

◆ gid()

◆ has_dep() [1/3]

bool mim::Def::has_dep ( ) const
inline

Definition at line 308 of file def.h.

Referenced by mim::VarRewriter::rewrite_imm().

◆ has_dep() [2/3]

bool mim::Def::has_dep ( Dep d) const
inline

Definition at line 309 of file def.h.

References has_dep().

Referenced by has_dep().

◆ has_dep() [3/3]

bool mim::Def::has_dep ( unsigned u) const
inline

Definition at line 310 of file def.h.

◆ has_var() [1/2]

const Var * mim::Def::has_var ( )
inline

Only returns not nullptr, if Var of this mutable has ever been created.

Definition at line 378 of file def.h.

References has_var().

Referenced by has_var(), has_var(), is_immutabilizable(), and mim::VarRewriter::rewrite_mut().

◆ has_var() [2/2]

const Var * mim::Def::has_var ( ) const
inline

As above if this is a mutable.

Definition at line 380 of file def.h.

References has_var(), and isa_mut().

◆ hash()

size_t mim::Def::hash ( ) const
inlineconstexprnoexcept

Definition at line 220 of file def.h.

◆ immutabilize()

virtual const Def * mim::Def::immutabilize ( )
inlinevirtual

Tries to make an immutable from a mutable.

This usually works if the mutable isn't recursive and its var isn't used.

Reimplemented in mim::Arr, mim::Pack, mim::Pi, and mim::Sigma.

Definition at line 495 of file def.h.

◆ is_closed()

◆ is_elim()

bool mim::Def::is_elim ( ) const
inlinenoexcept

Definition at line 232 of file def.h.

References mim::Elim, and judge().

◆ is_external()

bool mim::Def::is_external ( ) const
inline

◆ is_form()

bool mim::Def::is_form ( ) const
inlinenoexcept

Definition at line 230 of file def.h.

References mim::Form, is_form(), and judge().

Referenced by is_form().

◆ is_immutabilizable()

bool mim::Def::is_immutabilizable ( )

◆ is_intro()

bool mim::Def::is_intro ( ) const
inlinenoexcept

Definition at line 231 of file def.h.

References mim::Intro, and judge().

Referenced by mim::flatten().

◆ is_meta()

bool mim::Def::is_meta ( ) const
inlinenoexcept

Definition at line 233 of file def.h.

References judge(), and mim::Meta.

◆ is_open()

bool mim::Def::is_open ( ) const

Has free_vars()?

Definition at line 358 of file def.cpp.

References mim::Sets< D, N >::Set::empty(), free_vars(), and local_vars().

◆ is_set()

bool mim::Def::is_set ( ) const

Yields true if empty or the last op is set.

Definition at line 262 of file def.cpp.

References num_ops(), op(), and ops().

Referenced by mim::EtaExp::analyze(), deps(), free_vars(), mim::isa_workable(), mim::EtaExp::rewrite(), mim::EtaRed::rewrite(), mim::Rewriter::rewrite_mut(), and mim::Hole::tuplefy().

◆ is_term()

bool mim::Def::is_term ( ) const

Definition at line 415 of file def.cpp.

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

◆ isa_imm() [1/2]

template<class T = Def>
const T * mim::Def::isa_imm ( ) const
inline

Definition at line 419 of file def.h.

References isa_mut().

Referenced by mim::World::app(), mim::commute_(), mim::merge_sigma(), mim::merge_tuple(), and rebuild().

◆ isa_imm() [2/2]

template<class T = Def, class R>
const T * mim::Def::isa_imm ( R(T::* )() const) const
inline

Definition at line 421 of file def.h.

References isa_mut().

◆ isa_lit_arity()

std::optional< nat_t > mim::Def::isa_lit_arity ( ) const

Definition at line 456 of file def.cpp.

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

Referenced by as_lit_arity(), mim::flatten(), num_projs(), and num_tprojs().

◆ isa_mut()

◆ judge()

u32 mim::Def::judge ( ) const
noexcept

Definition at line 405 of file def.cpp.

References mim::CODE, MIM_NODE, and node().

Referenced by is_elim(), is_form(), is_intro(), and is_meta().

◆ loc()

◆ local_muts()

Muts mim::Def::local_muts ( ) const

Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }.

Definition at line 274 of file def.cpp.

References isa_mut().

Referenced by free_vars(), is_closed(), mim::post_order(), mim::VarRewriter::rewrite_imm(), and mim::ClosedMutPhase< M >::start().

◆ local_vars()

Vars mim::Def::local_vars ( ) const

Vars reachable by following immutable deps().

Note
var->local_vars() is by definition the set { var }.

Definition at line 289 of file def.cpp.

Referenced by free_vars(), is_closed(), is_open(), and mim::VarRewriter::rewrite_imm().

◆ make_external()

void mim::Def::make_external ( )

Definition at line 476 of file def.cpp.

References mim::World::make_external(), and world().

Referenced by transfer_external().

◆ make_internal()

void mim::Def::make_internal ( )

◆ mark()

u32 mim::Def::mark ( ) const
inlineconstexprnoexcept

Used internally by free_vars().

Definition at line 219 of file def.h.

◆ node()

Node mim::Def::node ( ) const
inlineconstexprnoexcept

◆ node_name()

std::string_view mim::Def::node_name ( ) const

◆ num_deps()

size_t mim::Def::num_deps ( ) const
inlinenoexcept

Definition at line 295 of file def.h.

References deps().

◆ num_ops()

◆ num_projs()

nat_t mim::Def::num_projs ( ) const
inline

Yields Def::as_lit_arity(), if it is in fact a Lit, or 1 otherwise.

Definition at line 330 of file def.h.

References isa_lit_arity().

Referenced by mim::plug::clos::clos_insert_env(), mim::plug::clos::clos_remove_env(), mim::plug::mem::mem_def(), proj(), projs(), and mim::plug::mem::replace_mem().

◆ num_tprojs()

nat_t mim::Def::num_tprojs ( ) const

As above but yields 1, if Flags::scalarize_threshold is exceeded.

Definition at line 481 of file def.cpp.

References mim::World::flags(), isa_lit_arity(), mim::Flags::scalarize_threshold, and world().

Referenced by tproj(), and tprojs().

◆ num_tvars()

nat_t mim::Def::num_tvars ( )
inlinenoexcept

Definition at line 374 of file def.h.

References var().

◆ num_vars()

nat_t mim::Def::num_vars ( )
inlinenoexcept

Definition at line 374 of file def.h.

Referenced by mim::ll::Emitter::emit_epilogue(), and mim::Lam::ret_var().

◆ op()

◆ ops()

◆ proj() [1/2]

const Def * mim::Def::proj ( nat_t a,
nat_t i ) const

Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.

Definition at line 486 of file def.cpp.

References isa_mut(), op(), type(), World, and world().

Referenced by mim::plug::clos::clos_remove_env(), mim::ll::Emitter::emit_bb(), mim::flatten(), projs(), projs(), mim::plug::clos::ClosConvPrep::rewrite_arg(), tproj(), mim::tuple2str(), and mim::Hole::tuplefy().

◆ proj() [2/2]

const Def * mim::Def::proj ( nat_t i) const
inline

As above but takes Def::num_projs as arity.

Definition at line 335 of file def.h.

References num_projs(), and proj().

Referenced by proj().

◆ projs() [1/4]

template<nat_t A = std::dynamic_extent>
auto mim::Def::projs ( ) const
inline

Definition at line 358 of file def.h.

References projs().

Referenced by projs(), projs(), projs(), and tprojs().

◆ projs() [2/4]

template<nat_t A = std::dynamic_extent, class F>
auto mim::Def::projs ( F f) const
inline

Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (otherwise).

Applies f to each element.

Definition at line 340 of file def.h.

References as_lit_arity(), num_projs(), proj(), and projs().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_tuple(), mim::ll::Emitter::emit_bb(), mim::plug::clos::Clos2SJLJ::enter(), mim::plug::regex::flatten_in_arg(), mim::plug::mem::mem_def(), mim_get_plugin(), mim::plug::core::normalize_abs(), mim::plug::autodiff::normalize_add(), mim::plug::math::normalize_arith(), mim::plug::core::normalize_bit2(), mim::plug::refly::normalize_check(), mim::plug::math::normalize_cmp(), mim::plug::compile::normalize_combine_pass_list(), mim::plug::tuple::normalize_concat(), mim::plug::ord::normalize_contains(), mim::plug::tuple::normalize_contains(), mim::plug::refly::normalize_dbg(), mim::plug::vec::normalize_diff(), mim::plug::core::normalize_div(), mim::plug::refly::normalize_equiv(), mim::plug::core::normalize_extrema(), mim::plug::math::normalize_extrema(), mim::plug::vec::normalize_fold(), mim::plug::ord::normalize_get(), mim::plug::core::normalize_icmp(), mim::plug::mem::normalize_lea(), mim::plug::mem::normalize_load(), mim::plug::core::normalize_nat(), mim::plug::core::normalize_ncmp(), mim::plug::math::normalize_pow(), mim::plug::regex::normalize_range(), mim::plug::matrix::normalize_read(), mim::plug::refly::normalize_refine(), mim::plug::matrix::normalize_shape(), mim::plug::core::normalize_shr(), mim::plug::mem::normalize_store(), mim::plug::autodiff::normalize_sum(), mim::plug::core::normalize_wrap(), mim::plug::tuple::normalize_zip(), mim::plug::matrix::LowerMatrixLowLevel::rewrite_imm(), mim::plug::mem::strip_mem(), and mim::unflatten().

◆ projs() [3/4]

auto mim::Def::projs ( nat_t a) const
inline

Definition at line 364 of file def.h.

References projs().

◆ projs() [4/4]

template<class F>
auto mim::Def::projs ( nat_t a,
F f ) const
inline

Definition at line 354 of file def.h.

References proj(), and mim::Vector().

◆ rebuild() [1/2]

const Def * mim::Def::rebuild ( const Def * type,
Defs ops ) const
inline

Definition at line 491 of file def.h.

References ops(), rebuild(), type(), and world().

Referenced by rebuild().

◆ rebuild() [2/2]

const Def * mim::Def::rebuild ( World & w,
const Def * type,
Defs ops ) const
inline

Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.

Definition at line 487 of file def.h.

References dbg(), isa_imm(), ops(), rebuild_(), set(), type(), and World.

Referenced by refine(), mim::EtaExp::rewrite(), and mim::Rewriter::rewrite_imm().

◆ rebuild_()

◆ reduce()

template<size_t N = std::dynamic_extent>
auto mim::Def::reduce ( const Def * arg) const
inlineconstexpr

◆ reduction_offset()

virtual constexpr size_t mim::Def::reduction_offset ( ) const
inlineconstexprvirtualnoexcept

First Def::op that needs to be dealt with during reduction; e.g.

for a Pi we don't reduce the Pi::dom.

See also
World::reduce

Reimplemented in mim::Arr, mim::Bound, mim::Lam, mim::Pack, mim::Pi, and mim::Sigma.

Definition at line 507 of file def.h.

◆ refine()

◆ set() [1/14]

template<bool Ow = false>
Def * mim::Def::set ( Dbg d)
inline

Definition at line 465 of file def.h.

References set().

Referenced by set().

◆ set() [2/14]

template<bool Ow = false>
const Def * mim::Def::set ( Dbg d) const
inline

Definition at line 464 of file def.h.

References set().

Referenced by set().

◆ set() [3/14]

Def * mim::Def::set ( Defs ops)

Def::set ops all at once.

Definition at line 235 of file def.cpp.

References num_ops(), ops(), and set().

◆ set() [4/14]

template<bool Ow = false>
Def * mim::Def::set ( Loc l)
inline

Definition at line 455 of file def.h.

References dbg_.

◆ set() [5/14]

template<bool Ow = false>
const Def * mim::Def::set ( Loc l) const
inline

Definition at line 454 of file def.h.

References dbg_.

◆ set() [6/14]

template<bool Ow = false>
Def * mim::Def::set ( Loc l,
std::string s )
inline

Definition at line 463 of file def.h.

References set(), and sym().

Referenced by set().

◆ set() [7/14]

template<bool Ow = false>
const Def * mim::Def::set ( Loc l,
std::string s ) const
inline

Definition at line 462 of file def.h.

References set(), and sym().

Referenced by set().

◆ set() [8/14]

template<bool Ow = false>
Def * mim::Def::set ( Loc l,
Sym s )
inline

Definition at line 461 of file def.h.

References set().

Referenced by set().

◆ set() [9/14]

template<bool Ow = false>
const Def * mim::Def::set ( Loc l,
Sym s ) const
inline

Definition at line 460 of file def.h.

References set().

Referenced by set().

◆ set() [10/14]

◆ set() [11/14]

template<bool Ow = false>
Def * mim::Def::set ( std::string s)
inline

Definition at line 459 of file def.h.

References set(), and sym().

Referenced by set().

◆ set() [12/14]

template<bool Ow = false>
const Def * mim::Def::set ( std::string s) const
inline

Definition at line 458 of file def.h.

References set(), and sym().

Referenced by set().

◆ set() [13/14]

template<bool Ow = false>
Def * mim::Def::set ( Sym s)
inline

Definition at line 457 of file def.h.

References dbg_.

◆ set() [14/14]

template<bool Ow = false>
const Def * mim::Def::set ( Sym s) const
inline

Definition at line 456 of file def.h.

References dbg_.

◆ stream()

std::ostream & mim::Def::stream ( std::ostream & os,
int max ) const

Definition at line 428 of file dump.cpp.

References world().

Referenced by dump(), and write().

◆ stub() [1/2]

Def * mim::Def::stub ( const Def * type)
inline

Definition at line 484 of file def.h.

References stub(), type(), and world().

Referenced by stub().

◆ stub() [2/2]

Def * mim::Def::stub ( World & w,
const Def * type )
inline

Definition at line 483 of file def.h.

References dbg(), set(), stub_(), type(), and World.

Referenced by mim::LamSpec::rewrite(), and mim::Rewriter::rewrite_mut().

◆ stub_()

virtual Def * mim::Def::stub_ ( World & ,
const Def *  )
inlineprivatevirtual

Reimplemented in mim::Arr, mim::Global, mim::Hole, mim::Lam, mim::Pack, mim::Pi, and mim::Sigma.

Definition at line 561 of file def.h.

References World.

Referenced by stub().

◆ sym() [1/4]

◆ sym() [2/4]

Sym mim::Def::sym ( const char * s) const
protected

Definition at line 367 of file def.cpp.

References mim::World::sym(), and world().

◆ sym() [3/4]

Sym mim::Def::sym ( std::string s) const
protected

Definition at line 369 of file def.cpp.

References mim::World::sym(), and world().

◆ sym() [4/4]

Sym mim::Def::sym ( std::string_view s) const
protected

Definition at line 368 of file def.cpp.

References mim::World::sym(), and world().

◆ tid()

u32 mim::Def::tid ( ) const
inlineconstexprnoexcept

Trie id - only used in Trie.

Definition at line 218 of file def.h.

◆ tproj()

const Def * mim::Def::tproj ( nat_t i) const
inline

As above but takes Def::num_tprojs.

Definition at line 336 of file def.h.

References num_tprojs(), and proj().

◆ tprojs() [1/2]

auto mim::Def::tprojs ( ) const
inline

Definition at line 361 of file def.h.

References tprojs().

Referenced by tprojs().

◆ tprojs() [2/2]

template<class F>
auto mim::Def::tprojs ( F f) const
inline

Definition at line 352 of file def.h.

References num_tprojs(), and projs().

◆ transfer_external()

void mim::Def::transfer_external ( Def * to)
inline

Definition at line 412 of file def.h.

References make_external(), and make_internal().

◆ tvar()

const Def * mim::Def::tvar ( nat_t i)
inlinenoexcept

Definition at line 374 of file def.h.

◆ tvars() [1/2]

auto mim::Def::tvars ( )
inlinenoexcept

Definition at line 374 of file def.h.

◆ tvars() [2/2]

template<class F>
auto mim::Def::tvars ( F f)
inlinenoexcept

Definition at line 374 of file def.h.

◆ type()

const Def * mim::Def::type ( ) const
inlinenoexcept

Yields the "raw" type of this Def (maybe nullptr).

See also
Def::unfold_type.

Definition at line 242 of file def.h.

Referenced by mim::World::app(), arity(), mim::plug::autodiff::AutoDiffEval::augment_(), mim::plug::autodiff::AutoDiffEval::augment_app(), mim::plug::autodiff::AutoDiffEval::augment_extract(), mim::plug::autodiff::AutoDiffEval::augment_lam(), mim::plug::autodiff::AutoDiffEval::augment_pack(), mim::plug::autodiff::AutoDiffEval::augment_tuple(), mim::Bound::Bound(), mim::App::callee_type(), mim::Arr::check(), check(), mim::Lam::check(), mim::Pi::check(), mim::Sigma::check(), mim::plug::clos::clos_pack(), mim::plug::matrix::counting_for(), Def(), Def(), Def(), deps(), mim::plug::autodiff::AutoDiffEval::derive_(), mim::ll::Emitter::emit_bb(), mim::plug::clos::ClosLit::env_type(), mim::plug::clos::ClosConvPrep::eta_wrap(), mim::Ext::Ext(), mim::World::extract(), mim::Bound::find(), mim::flatten(), mim::plug::clos::ClosLit::fnc_type(), mim::Bound::get(), mim::plug::compile::handle_optimization_part(), mim::World::implicit_app(), mim::Axm::infer_curry_and_trip(), mim::World::insert(), is_term(), mim::is_unit(), mim::plug::clos::ClosLit::isa_clos_lit, isa_lit_arity(), mim::World::match(), mim::plug::mem::mem_def(), mim::merge_tuple(), mim::plug::core::normalize_bitcast(), mim::plug::core::normalize_conv(), mim::plug::math::normalize_conv(), mim::plug::core::normalize_shr(), mim::plug::refly::normalize_type(), mim::plug::core::op(), mim::plug::direct::op_cps2ds_dep(), mim::plug::mem::op_lea(), mim::plug::mem::op_lea_unsafe(), mim::optimize(), mim::World::pack(), mim::Pi::Pi(), mim::Pi::Pi(), proj(), rebuild(), rebuild(), mim::Axm::rebuild_(), rebuild_(), mim::TBound< false >::rebuild_(), refine(), mim::plug::mem::replace_mem(), mim::EtaExp::rewrite(), mim::plug::matrix::LowerMatrixHighLevelMapRed::rewrite_(), mim::plug::clos::ClosConvPrep::rewrite_callee(), mim::plug::matrix::LowerMatrixLowLevel::rewrite_imm(), mim::Rewriter::rewrite_imm(), mim::Rewriter::rewrite_mut(), mim::Scheduler::Scheduler(), set(), mim::Pack::shape(), mim::plug::mem::strip_mem(), mim::Arr::stub(), stub(), stub(), mim::Hole::stub(), mim::Pack::stub(), mim::Pi::stub(), mim::Sigma::stub(), mim::Hole::tuplefy(), mim::Global::type(), mim::Lam::type(), mim::World::type(), mim::World::uinc(), mim::World::uniq(), and world().

◆ unfold_type()

const Def * mim::Def::unfold_type ( ) const

Yields the type of this Def and builds a new Type (UInc n) if necessary.

Definition at line 378 of file def.cpp.

References world().

Referenced by mim::World::arr(), mim::Arr::check(), and mim::World::uniq().

◆ unique_name()

std::string mim::Def::unique_name ( ) const

name + "_" + Def::gid

Definition at line 479 of file def.cpp.

References gid(), and sym().

Referenced by mim::Nest::Node::name(), and mim::ll::Emitter::prepare().

◆ unset()

Def * mim::Def::unset ( )

Unsets all Def::ops; works even, if not set at all or partially.

Definition at line 253 of file def.cpp.

References num_ops().

Referenced by mim::Arr::unset(), mim::Hole::unset(), mim::Lam::unset(), mim::Pack::unset(), mim::Pi::unset(), and mim::Sigma::unset().

◆ users()

Muts mim::Def::users ( )
inline

Set of mutables where this mutable is locally referenced.

Definition at line 402 of file def.h.

◆ var() [1/3]

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

Not necessarily a Var: E.g., if the return type is [], this will yield ().

Definition at line 433 of file def.cpp.

References world().

Referenced by mim::Lam::ret_var().

◆ var() [2/3]

◆ var() [3/3]

const Def * mim::Def::var ( nat_t i)
inlinenoexcept

Definition at line 374 of file def.h.

◆ vars() [1/4]

template<nat_t A = std::dynamic_extent>
auto mim::Def::vars ( )
inlinenoexcept

Definition at line 374 of file def.h.

◆ vars() [2/4]

template<nat_t A = std::dynamic_extent, class F>
auto mim::Def::vars ( F f)
inlinenoexcept

◆ vars() [3/4]

auto mim::Def::vars ( nat_t a)
inlinenoexcept

Definition at line 374 of file def.h.

◆ vars() [4/4]

template<class F>
auto mim::Def::vars ( nat_t a,
F f )
inlinenoexcept

Definition at line 374 of file def.h.

◆ world()

World & mim::Def::world ( ) const
noexcept

Definition at line 371 of file def.cpp.

References type(), and World.

Referenced by mim::Checker::alpha(), mim::Lam::app(), mim::Lam::app(), mim::plug::clos::apply_closure(), arity(), mim::plug::autodiff::autodiff_type_fun(), mim::plug::autodiff::autodiff_type_fun_pi(), mim::Lam::branch(), mim::Lam::check(), mim::Sigma::check(), mim::plug::clos::clos_apply(), mim::plug::clos::clos_insert_env(), mim::plug::clos::clos_pack(), mim::plug::clos::clos_remove_env(), mim::plug::clos::clos_type(), mim::plug::clos::clos_type_to_pi(), mim::plug::core::convert(), mim::plug::matrix::counting_for(), debug_prefix(), debug_suffix(), Def(), Def(), mim::flatten(), free_vars(), free_vars(), mim::plug::autodiff::id_pullback(), mim::Arr::immutabilize(), mim::Pack::immutabilize(), mim::Pi::immutabilize(), mim::Sigma::immutabilize(), mim::Tuple::infer(), mim::is_unit(), mim::plug::clos::isa_clos_type(), make_external(), make_internal(), mim::merge_sigma(), mim::merge_tuple(), mim::plug::mem::mut_con(), mim::plug::core::normalize_bitcast(), mim::plug::ord::normalize_contains(), mim::plug::core::normalize_conv(), mim::plug::math::normalize_conv(), mim::plug::core::normalize_div(), mim::plug::refly::normalize_gid(), num_tprojs(), mim::plug::core::op(), mim::plug::direct::op_cps2ds_dep(), mim::plug::mem::op_lea(), mim::plug::mem::op_lea_unsafe(), mim::plug::mem::op_lea_unsafe(), mim::plug::autodiff::op_sum(), operator<<, proj(), mim::plug::autodiff::pullback_type(), rebuild(), mim::Axm::rebuild_(), mim::Pi::set_dom(), mim::Lam::set_filter(), mim::Pack::shape(), stream(), mim::plug::mem::strip_mem(), mim::plug::mem::strip_mem_ty(), mim::Arr::stub(), stub(), mim::Global::stub(), mim::Hole::stub(), mim::Lam::stub(), mim::Pack::stub(), mim::Pi::stub(), mim::Sigma::stub(), sym(), sym(), sym(), mim::tuple2str(), mim::Hole::tuplefy(), unfold_type(), var(), mim::plug::autodiff::zero_def(), mim::plug::autodiff::zero_pullback(), and zonk().

◆ write() [1/2]

void mim::Def::write ( int max) const

Definition at line 455 of file dump.cpp.

References write().

Referenced by write().

◆ write() [2/2]

void mim::Def::write ( int max,
const char * file ) const

Definition at line 450 of file dump.cpp.

References stream().

◆ zonk()

const Def * mim::Def::zonk ( ) const

If Holes have been filled, reconstruct the program without them.

Only gues up to but excluding other mutables.

See also
https://stackoverflow.com/questions/31889048/what-does-the-ghc-source-mean-by-zonk

Definition at line 35 of file check.cpp.

References mim::Hole::find(), and world().

Referenced by mim::World::app(), and set().

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream & os,
const Def * def )
friend

This will stream def as an operand.

This is usually id(def) unless it can be displayed Inline.

Definition at line 419 of file dump.cpp.

References world().

◆ Sets

template<class D, size_t N>
friend class Sets
friend

Definition at line 600 of file def.h.

References Sets.

Referenced by Sets.

◆ swap

void swap ( World & ,
World &  )
friend

References World.

◆ World

friend class World
friend

Definition at line 601 of file def.h.

References World.

Referenced by Def(), proj(), rebuild(), rebuild_(), stub(), stub_(), swap, World, world(), and ~Def().

Member Data Documentation

◆ [union]

union { ... } mim::Def

◆ curry_

u8 mim::Def::curry_ = 0
protected

Definition at line 580 of file def.h.

Referenced by mim::App::curry(), and mim::Axm::curry().

◆ dbg_

Dbg mim::Def::dbg_
mutableprotected

Definition at line 572 of file def.h.

Referenced by dbg(), debug_prefix(), debug_suffix(), loc(), set(), set(), set(), set(), and sym().

◆ flags_

flags_t mim::Def::flags_
protected

Definition at line 579 of file def.h.

Referenced by Def(), Def(), flags(), mim::Lit::get(), mim::Pi::make_explicit(), and mim::Pi::make_implicit().

◆ trip_

u8 mim::Def::trip_ = 0
protected

Definition at line 581 of file def.h.

Referenced by mim::App::trip(), and mim::Axm::trip().


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