Base class for all Defs. More...

#include <mim/def.h>

Inheritance diagram for mim::Def:

Public Member Functions
Getters
World &	world () 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 Def *	type () const noexcept
	Yields the "raw" type of this Def (maybe `nullptr`).

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

bool	is_term () const

arity
const Def *	arity () const

std::optional< nat_t >	isa_lit_arity () const

nat_t	as_lit_arity () const

ops
template<size_t N = std::dynamic_extent>
constexpr auto	ops () const noexcept

const Def *	op (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 ... ... `false`, set the operands from left (`i == 0`) to right (`i == num_ops() - 1`). ... `true`, reset the operands from left to right as in 1a. In addition, you can invoke Def::unset() at any time to start over with 1a: mut->unset()->set({a, b, c}); // This will always work, but should be your last resort. MimIR assumes that a mutable is final, when its last operand is set. Then, Def::check() will be invoked.
Def *	set (size_t i, const Def *)
	Successively set from left to right.

Def *	reset (size_t i, const Def *def)
	Successively reset from left to right.

Def *	set (Defs ops)
	Def::set `ops` all at once.

Def *	reset (Defs ops)
	Def::reset `ops` all at once.

Def *	unset ()
	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: Def::type() (if not `nullptr`) and the other Def::ops() (only included, if Def::is_set()) in this order.
Defs	deps () const noexcept

const Def *	dep (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; mim::Def::has_var const Var * has_var() Only returns not nullptr, if Var of this mutable has ever been created. Definition def.h:383 mim::Dep::Var @ Var Definition def.h:100 mim::Dep::Hole @ Hole Definition def.h:101 mim::Dep::Mut @ 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); }); mim::Lit::as static T as(const Def def) Definition def.h:735 mim::Vector 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 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.

const Def *	proj (nat_t i) const
	As above but takes Def::num_projs as arity.

const Def *	tproj (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 Def *	var (nat_t a, nat_t i) noexcept

const Def *	var (nat_t i) noexcept

const Def *	tvar (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 Def *	var ()
	Not necessarily a Var: E.g., if the return type is `[]`, this will yield `()`.

const Var *	has_var ()
	Only returns not `nullptr`, if Var of this mutable has ever been created.

const Var *	has_var () const
	As above if `this` is a mutable.

Free Vars and Muts
local_muts() / local_vars() are cached and hash-consed. free_vars() are computed on demand and cached in mutables. They will be transitively invalidated by following users(), if a mutable is mutated.
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
See also Upcast for Built-ins
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 `const`ness 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 `const`ness 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 Def *	set (Loc l) const

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

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

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

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

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

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

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

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

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

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

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

debug_prefix/suffix
Prepends/Appends a prefix/suffix to Def::name - but only in `Debug` build.
const Def *	debug_prefix (std::string) const

const Def *	debug_suffix (std::string) const

Rebuild
Def *	stub (World &w, const Def *type)

Def *	stub (const Def *type)

const Def *	rebuild (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 Def *	rebuild (const Def *type, Defs ops) const

virtual const Def *	immutabilize ()
	Tries to make an immutable from a mutable.

bool	is_immutabilizable ()

const Def *	refine (size_t i, const Def *new_op) const

DefVec	reduce (const Def *arg) const
	Rewrites Def::ops by substituting `this` mutable's Var with `arg`.

DefVec	reduce (const Def *arg)

const Def *	reduce (size_t i, const Def *arg) const
	As above but only rewrites `this->op(i)`.

Type Checking
virtual const Def *	check (size_t, const Def *def)

virtual const Def *	check ()

const Def *	zonk () const

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_
	Axiom only: Axioms use this member to store their normalizer.

const Axiom *	axiom_
	App only: Curried Apps of Axioms use this member to propagate the Axiom.

const Var *	var_
	Mutable only: Var of a mutable.

World *	world_

};

flags_t	flags_

u8	curry_ = 0

u8	trip_ = 0

Private Member Functions
virtual Def *	stub_ (World &, const Def *)

virtual const Def *	rebuild_ (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	Vel	Test
Meet	Ac	Pick
Nat	Lit
Idx	Lit

In addition there is:

Var: A variable. Currently the following Defs may be binders:
- Pi, Lam, Sigma, Arr, Pack
Axiom: To introduce new entities.
Proxy: Used for intermediate values during optimizations.
Hole: Hole in the presentation filled by type inference (always mutable as the 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-----------|
                 deps
   |--------------------------------| if type() != nullptr &&  is_set()
          |-------------------------| if type() == nullptr &&  is_set()
   |------|                           if type() != nullptr && !is_set()
   ||                                 if type() == nullptr && !is_set()

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(), op(), ops(), type(), mim::Univ, mim::Var, 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

Definition at line 491 of file def.cpp.

References mim::World::lit_nat(), mim::World::lit_nat_1(), type(), and world().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_pack(), mim::tuple2str(), and mim::unflatten().

◆ as_imm()

template<class T = Def>

const T * mim::Def::as_imm ( ) const

inline

Definition at line 425 of file def.h.

References as_mut().

◆ as_lit_arity()

nat_t mim::Def::as_lit_arity ( ) const

inline

Definition at line 252 of file def.h.

References isa_lit_arity().

Referenced by mim::World::extract(), mim::plug::regex::normalize_conj(), mim::plug::regex::normalize_disj(), and projs().

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

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

Definition at line 515 of file def.h.

References type().

Referenced by set().

◆ check() [2/2]

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

inlinevirtual

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

Definition at line 514 of file def.h.

◆ dbg()

Dbg mim::Def::dbg ( ) const

inline

Definition at line 449 of file def.h.

References dbg_.

Referenced by rebuild(), mim::Axiom::rebuild_(), mim::TBound< Up >::rebuild_(), mim::TExt< Up >::rebuild_(), mim::Vel::rebuild_(), mim::Arr::stub(), stub(), mim::Global::stub(), mim::Hole::stub(), mim::Lam::stub(), mim::Pack::stub(), mim::Pi::stub(), mim::Sigma::stub(), mim::TBound< false >::stub(), and mim::TExt< false >::stub().

◆ debug_prefix()

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

Definition at line 469 of file def.cpp.

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

◆ debug_suffix()

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

Definition at line 470 of file def.cpp.

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

◆ dep()

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

inlinenoexcept

Definition at line 299 of file def.h.

References dep(), and deps().

Referenced by dep().

◆ deps()

Defs mim::Def::deps ( ) const

noexcept

Definition at line 441 of file def.cpp.

References is_set(), and type().

Referenced by dep(), mim::Scheduler::early(), mim::plug::clos::free_defs(), is_immutabilizable(), num_deps(), mim::post_order(), mim::PassMan::run(), and mim::ClosedMutPhase< M >::start().

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

flags_t mim::Def::flags ( ) const

inlineconstexprnoexcept

Definition at line 216 of file def.h.

References flags(), and flags_.

Referenced by mim::Axiom::base(), Def(), Def(), Def(), flags(), mim::Pi::is_implicit(), mim::Global::is_mutable(), mim::UInc::offset(), mim::optimize(), mim::Proxy::pass(), mim::Axiom::plugin(), mim::Axiom::sub(), mim::Axiom::tag(), and mim::Proxy::tag().

◆ free_vars() [1/2]

Vars mim::Def::free_vars ( )

Definition at line 333 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 321 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()

u32 mim::Def::gid ( ) const

inlineconstexprnoexcept

Global id - unique number for this Def.

Definition at line 217 of file def.h.

Referenced by mim::commute(), Def(), mim::PipelineBuilder::def2pass(), mim::plug::refly::normalize_gid(), mim::UseHash::operator()(), mim::register_pass_with_arg(), and unique_name().

◆ has_dep() [1/3]

bool mim::Def::has_dep ( ) const

inline

Definition at line 313 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 314 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 315 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 383 of file def.h.

References has_var().

Referenced by has_var(), has_var(), is_immutabilizable(), reduce(), reduce(), 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 385 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 500 of file def.h.

◆ is_closed()

bool mim::Def::is_closed ( ) const

Has no free_vars()?

Definition at line 392 of file def.cpp.

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

Referenced by mim::Scheduler::early(), mim::plug::clos::free_defs(), mim::Scheduler::late(), mim::World::make_external(), mim::plug::core::normalize_pe(), and mim::Rewriter::rewrite_imm().

◆ 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

Definition at line 414 of file def.h.

Referenced by is_closed(), mim::isa_workable(), mim::World::make_external(), and mim::World::make_internal().

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

Definition at line 181 of file def.cpp.

References deps(), has_var(), and op().

Referenced by mim::Arr::immutabilize(), mim::Pack::immutabilize(), mim::Pi::immutabilize(), and mim::Sigma::immutabilize().

◆ 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 400 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 304 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 457 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 424 of file def.h.

References isa_mut().

Referenced by mim::World::app(), mim::merge_sigma(), mim::merge_tuple(), mim::plug::core::normalize_trait(), and rebuild().

◆ isa_imm() [2/2]

template<class T = Def, class R>

const T * mim::Def::isa_imm ( R(T::* f )() const ) const

inline

Definition at line 426 of file def.h.

References isa_mut().

◆ isa_lit_arity()

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

Definition at line 498 of file def.cpp.

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

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

◆ isa_mut()

template<class T = Def, bool invert = false>

T * mim::Def::isa_mut ( ) const

inline

If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.

Definition at line 430 of file def.h.

Referenced by mim::BetaRed::analyze(), mim::EtaExp::analyze(), mim::EtaRed::analyze(), mim::plug::mem::SSAConstr::analyze(), mim::World::app(), mim::plug::autodiff::AutoDiffEval::augment_(), mim::Scheduler::early(), mim::Bound::find(), mim::Hole::find(), free_vars(), has_var(), mim::plug::clos::isa_clos_type(), isa_imm(), isa_imm(), mim::Scheduler::late(), local_muts(), proj(), reduce(), reduce(), mim::EtaExp::rewrite(), mim::EtaRed::rewrite(), mim::plug::affine::LowerFor::rewrite(), mim::plug::mem::SSAConstr::rewrite(), mim::Rewriter::rewrite(), mim::Scalarize::rewrite(), mim::plug::clos::ClosConvPrep::rewrite_arg(), mim::Scheduler::Scheduler(), and mim::Hole::tuplefy().

◆ judge()

u32 mim::Def::judge ( ) const

noexcept

Definition at line 447 of file def.cpp.

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

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

◆ loc()

Loc mim::Def::loc ( ) const

inline

Definition at line 450 of file def.h.

References dbg_.

Referenced by mim::World::app(), mim::Arr::check(), mim::Lam::check(), mim::Pi::check(), mim::World::extract(), mim::World::insert(), mim::World::type(), and mim::World::uinc().

◆ 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 316 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 331 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 518 of file def.cpp.

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

Referenced by transfer_external().

◆ make_internal()

void mim::Def::make_internal ( )

Definition at line 519 of file def.cpp.

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

Referenced by mim::plug::compile::InternalCleanup::enter(), mim::optimize(), and transfer_external().

◆ 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

Definition at line 221 of file def.h.

Referenced by mim::Bound::Bound(), mim::Bound::Bound(), Def(), Def(), mim::Ext::Ext(), mim::Pi::isa_cn(), judge(), and node_name().

◆ node_name()

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

Definition at line 431 of file def.cpp.

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

Referenced by mim::plug::autodiff::AutoDiffEval::augment_(), mim::plug::autodiff::autodiff_type_fun(), and mim::plug::autodiff::zero_def().

◆ num_deps()

size_t mim::Def::num_deps ( ) const

inlinenoexcept

Definition at line 300 of file def.h.

References deps().

◆ num_ops()

size_t mim::Def::num_ops ( ) const

inlineconstexprnoexcept

◆ 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 335 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 523 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 379 of file def.h.

References var().

◆ num_vars()

nat_t mim::Def::num_vars ( )

inlinenoexcept

Definition at line 379 of file def.h.

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

◆ op()

const Def * mim::Def::op ( size_t i ) const

inlinenoexcept

Definition at line 264 of file def.h.

References ops().

Referenced by mim::EtaExp::analyze(), mim::plug::mem::SSAConstr::analyze(), mim::App::arg(), mim::Arr::body(), mim::Lam::body(), mim::Pack::body(), mim::App::callee(), mim::Test::clash(), mim::plug::clos::clos_type_to_pi(), mim::Pi::codom(), Def(), mim::Pi::dom(), mim::World::extract(), mim::Lam::filter(), mim::Hole::find(), mim::Bound::get(), mim::Extract::index(), mim::Insert::index(), mim::Uniq::inhabitant(), mim::Global::init(), is_immutabilizable(), is_set(), mim::plug::clos::isa_clos_type(), mim::Type::level(), mim::Test::match(), mim::Var::mut(), mim::plug::mem::normalize_load(), mim::Hole::op(), mim::UInc::op(), mim::Test::probe(), proj(), reduce(), reduce(), mim::EtaExp::rewrite(), mim::EtaRed::rewrite(), mim::plug::mem::SSAConstr::rewrite(), mim::Rewriter::rewrite_imm(), mim::Rewriter::rewrite_mut(), set(), mim::Arr::shape(), mim::TBound< false >::stub_(), mim::Extract::tuple(), mim::Insert::tuple(), unset(), mim::Insert::value(), mim::Pick::value(), mim::Test::value(), and mim::Vel::value().

◆ ops()

template<size_t N = std::dynamic_extent>

auto mim::Def::ops ( ) const

inlineconstexprnoexcept

◆ 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 528 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(), 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 340 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 363 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 345 of file def.h.

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

◆ projs() [3/4]

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

inline

Definition at line 369 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 359 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 496 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 492 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_()

virtual const Def * mim::Def::rebuild_	(	World &	w,
		const Def *	type,
		Defs	ops ) const

privatepure virtual

Implemented in mim::Ac, mim::App, mim::Arr, mim::Axiom, mim::Extract, mim::Global, mim::Hole, mim::Idx, mim::Insert, mim::Lam, mim::Lit, mim::Nat, mim::Pack, mim::Pi, mim::Pick, mim::Proxy, mim::Sigma, mim::TBound< Up >, mim::TBound< false >, mim::TBound< false >, mim::TBound< true >, mim::TBound< true >, mim::Test, mim::TExt< Up >, mim::TExt< false >, mim::TExt< false >, mim::TExt< true >, mim::TExt< true >, mim::Tuple, mim::Type, mim::UInc, mim::UMax, mim::Uniq, mim::Univ, mim::Var, and mim::Vel.

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

Referenced by rebuild().

◆ reduce() [1/3]

DefVec mim::Def::reduce ( const Def * arg )

Definition at line 232 of file def.cpp.

References has_var(), num_ops(), op(), ops(), var(), and world().

◆ reduce() [2/3]

DefVec mim::Def::reduce ( const Def * arg ) const

Rewrites Def::ops by substituting this mutable's Var with arg.

Definition at line 227 of file def.cpp.

References isa_mut(), and ops().

Referenced by mim::plug::compile::handle_optimization_part(), mim::Arr::reduce(), mim::Pack::reduce(), and mim::Pi::reduce().

◆ reduce() [3/3]

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

As above but only rewrites this->op(i).

Definition at line 246 of file def.cpp.

References has_var(), isa_mut(), and op().

◆ refine()

const Def * mim::Def::refine	(	size_t	i,
		const Def *	new_op ) const

Definition at line 251 of file def.cpp.

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

Referenced by mim::plug::clos::clos_sub_env(), mim::EtaRed::rewrite(), mim::plug::mem::SSAConstr::rewrite(), mim::plug::clos::ClosConvPrep::rewrite_arg(), and mim::plug::clos::ClosConvPrep::rewrite_callee().

◆ reset() [1/2]

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

Def::reset ops all at once.

Definition at line 263 of file def.cpp.

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

◆ reset() [2/2]

Def * mim::Def::reset	(	size_t	i,
		const Def *	def )

inline

Successively reset from left to right.

Definition at line 286 of file def.h.

References set(), and unset().

Referenced by mim::plug::clos::Clos2SJLJ::enter(), mim::RetWrap::enter(), mim::Hole::find(), reset(), and mim::Hole::reset().

◆ set() [1/14]

template<bool Ow = false>

Def * mim::Def::set ( Dbg d )

inline

Definition at line 470 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 469 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 262 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 460 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 459 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 468 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 467 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 466 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 465 of file def.h.

References set().

Referenced by set().

◆ set() [10/14]

Def * mim::Def::set	(	size_t	i,
		const Def *	def )

Successively set from left to right.

Definition at line 266 of file def.cpp.

References check(), num_ops(), op(), and type().

Referenced by mim::plug::autodiff::AutoDiffEval::augment_extract(), mim::plug::autodiff::AutoDiffEval::augment_tuple(), mim::plug::autodiff::AutoDiffEval::derive_(), mim::ast::AliasPtrn::emit_value(), rebuild(), reset(), mim::LamSpec::rewrite(), mim::plug::affine::LowerFor::rewrite(), mim::plug::mem::SSAConstr::rewrite(), mim::plug::clos::ClosConvPrep::rewrite_arg(), mim::plug::clos::ClosConvPrep::rewrite_callee(), set(), mim::Global::set(), mim::Hole::set(), mim::Lam::set(), mim::Pack::set(), mim::Sigma::set(), mim::Sigma::set(), mim::Arr::set_body(), mim::Lam::set_body(), mim::Pi::set_codom(), mim::Pi::set_dom(), mim::Pi::set_dom(), mim::Lam::set_filter(), mim::Arr::set_shape(), mim::Arr::stub(), and stub().

◆ set() [11/14]

template<bool Ow = false>

Def * mim::Def::set ( std::string s )

inline

Definition at line 464 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 463 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 462 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 461 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 489 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 488 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, mim::Sigma, mim::TBound< Up >, mim::TBound< false >, mim::TBound< false >, mim::TBound< true >, mim::TBound< true >, mim::TExt< Up >, mim::TExt< false >, mim::TExt< false >, mim::TExt< true >, and mim::TExt< true >.

Definition at line 550 of file def.h.

References World.

Referenced by stub().

◆ sym() [1/4]

Sym mim::Def::sym ( ) const

inline

Definition at line 451 of file def.h.

References dbg_.

Referenced by mim::plug::autodiff::AutoDiffEval::augment_lam(), debug_prefix(), debug_suffix(), mim::plug::compile::InternalCleanup::enter(), mim::World::make_external(), mim::World::make_internal(), mim_get_plugin(), set(), set(), set(), set(), and unique_name().

◆ sym() [2/4]

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

protected

Definition at line 409 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 411 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 410 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 341 of file def.h.

References num_tprojs(), and proj().

◆ tprojs() [1/2]

auto mim::Def::tprojs ( ) const

inline

Definition at line 366 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 357 of file def.h.

References num_tprojs(), and projs().

◆ transfer_external()

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

inline

Definition at line 417 of file def.h.

References make_external(), and make_internal().

◆ tvar()

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

inlinenoexcept

Definition at line 379 of file def.h.

◆ tvars() [1/2]

auto mim::Def::tvars ( )

inlinenoexcept

Definition at line 379 of file def.h.

◆ tvars() [2/2]

template<class F>

auto mim::Def::tvars ( F f )

inlinenoexcept

Definition at line 379 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::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::Axiom::infer_curry_and_trip(), mim::World::insert(), is_term(), mim::is_unit(), mim::plug::clos::ClosLit::isa_clos_lit, isa_lit_arity(), 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::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::Axiom::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::TBound< false >::stub(), mim::TExt< false >::stub(), mim::World::test(), 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 420 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 521 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 282 of file def.cpp.

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

Referenced by reset(), mim::Arr::unset(), 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 407 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 475 of file def.cpp.

References world().

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

◆ var() [2/3]

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

inlinenoexcept

Definition at line 379 of file def.h.

Referenced by mim::plug::autodiff::AutoDiffEval::augment_app(), mim::plug::autodiff::AutoDiffEval::augment_lam(), Def(), mim::plug::autodiff::AutoDiffEval::derive_(), mim::ast::TuplePtrn::emit_body(), mim::plug::clos::ClosLit::env_var(), mim::plug::clos::ClosConvPrep::eta_wrap(), mim::plug::clos::isa_clos_type(), mim::plug::mem::mem_var(), num_tvars(), reduce(), mim::plug::matrix::LowerMatrixMediumLevel::rewrite_(), and mim::Hole::tuplefy().

◆ var() [3/3]

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

inlinenoexcept

Definition at line 379 of file def.h.

◆ vars() [1/4]

template<nat_t A = std::dynamic_extent>

auto mim::Def::vars ( )

inlinenoexcept

Definition at line 379 of file def.h.

◆ vars() [2/4]

template<nat_t A = std::dynamic_extent, class F>

auto mim::Def::vars ( F f )

inlinenoexcept

Definition at line 379 of file def.h.

Referenced by mim::plug::clos::Clos2SJLJ::enter(), mim::RetWrap::enter(), free_vars(), mim::ll::Emitter::prepare(), and mim::plug::affine::LowerFor::rewrite().

◆ vars() [3/4]

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

inlinenoexcept

Definition at line 379 of file def.h.

◆ vars() [4/4]

template<class F>

auto mim::Def::vars	(	nat_t	a,
		F	f )

inlinenoexcept

Definition at line 379 of file def.h.

◆ world()

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

noexcept

Definition at line 413 of file def.cpp.

References type(), and World.

◆ 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

Definition at line 35 of file check.cpp.

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

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

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 590 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 591 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 570 of file def.h.

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

◆ dbg_

Dbg mim::Def::dbg_

mutableprotected

Definition at line 562 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 569 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 571 of file def.h.

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

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

include/mim/def.h
src/mim/check.cpp
src/mim/def.cpp
src/mim/dot.cpp
src/mim/dump.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Def() [1/3]

◆ Def() [2/3]

◆ Def() [3/3]

◆ ~Def()

Member Function Documentation

◆ arity()

◆ as_imm()

◆ as_lit_arity()

◆ as_mut()

◆ check() [1/2]

◆ check() [2/2]

◆ dbg()

◆ debug_prefix()

◆ debug_suffix()

◆ dep()

◆ deps()

◆ dot() [1/3]

◆ dot() [2/3]

◆ dot() [3/3]

◆ dump() [1/2]

◆ dump() [2/2]

◆ flags()

◆ free_vars() [1/2]

◆ free_vars() [2/2]

◆ gid()

◆ has_dep() [1/3]

◆ has_dep() [2/3]

◆ has_dep() [3/3]

◆ has_var() [1/2]

◆ has_var() [2/2]

◆ hash()

◆ immutabilize()

◆ is_closed()

◆ is_elim()

◆ is_external()

◆ is_form()

◆ is_immutabilizable()

◆ is_intro()

◆ is_meta()

◆ is_open()

◆ is_set()

◆ is_term()

◆ isa_imm() [1/2]

◆ isa_imm() [2/2]

◆ isa_lit_arity()

◆ isa_mut()

◆ judge()

◆ loc()

◆ local_muts()

◆ local_vars()

◆ make_external()

◆ make_internal()

◆ mark()

◆ node()

◆ node_name()

◆ num_deps()

◆ num_ops()

◆ num_projs()

◆ num_tprojs()

◆ num_tvars()

◆ num_vars()

◆ op()

◆ ops()

◆ proj() [1/2]

◆ proj() [2/2]

◆ projs() [1/4]

◆ projs() [2/4]

◆ projs() [3/4]

◆ projs() [4/4]

◆ rebuild() [1/2]

◆ rebuild() [2/2]

◆ rebuild_()

◆ reduce() [1/3]