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

virtual const Def *	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 to right. `true`, Def::unset() the operands first and then start over: `mut->unset()->set({a, b, c});` MimIR assumes that a mutable is final, when its last operand is set. Then, Def::check() will be invoked.
bool	is_set () const
	Yields `true` if empty or the last op is set.

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

Def *	set (Defs ops)
	Set `ops` all at once (no Def::unset necessary beforehand).

Def *	unset ()
	Unsets all Def::ops; works even, if not set at all or only partially set.

Def *	set_type (const Def *)
	Update type.

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:433 mim::Dep::Var @ Var Definition def.h:126 mim::Dep::Hole @ Hole Definition def.h:127 mim::Dep::Mut @ Mut Definition def.h:125
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:828 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::arity(), if it is 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.

const Def *	var_type ()
	If `this` is a binder, compute the type of its Variable.

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 noexcept

void	make_external ()

void	make_internal ()

void	transfer_external (Def *to)

Casts
See also Downcast for Built-ins
bool	is_mutable () const noexcept

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

template<class T = Def>
const T *	as_imm () 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

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 Def *	check (size_t i, const Def *def)
	Checks whether the `i`th operand can be set to `def`.

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

const Def *	zonk () const
	If Holes have been filled, reconstruct the program without them.

const Def *	zonk_mut () const
	If *mutable, zonks all ops and tries to immutabilize it; otherwise just zonk.

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

Static Public Member Functions
static DefVec	zonk (Defs defs)
	zonks all `defs` and retuns a new DefVec.

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 Axm *	axm_
	App only: Curried Apps of Axms use this member to propagate the Axm.

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

class	Zonker

void	swap (World &, World &) noexcept

std::ostream &	operator<< (std::ostream &os, const Def *def)
	This will stream `def` as an operand.

Syntactic Comparison
enum class	Cmp { L , G , E , U }

static Cmp	cmp (const Def a, const Def b)

static bool	less (const Def a, const Def b)

static bool	greater (const Def a, const Def b)

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
Reform	Rule
Nat	Lit
Idx	Lit

In addition there is:

Var: A variable. Currently the following Defs may be binders:
- Pi, Lam, Sigma, Arr, Pack
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-----------|
                 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 251 of file def.h.

Member Enumeration Documentation

◆ Cmp

enum class mim::Def::Cmp

strong

Enumerator
L	Less.
G	Greater.
E	Equal.
U	Unknown.

Definition at line 608 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 24 of file def.cpp.

References flags(), flags_, mim::hash_begin(), 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 78 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 81 of file def.cpp.

References flags(), flags_, gid(), mim::hash(), 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

virtual

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

Definition at line 553 of file def.cpp.

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

Referenced by mim::Pack::arity(), mim::Sigma::arity(), mim::World::extract(), mim::flatten(), mim::plug::regex::normalize_conj(), mim::plug::regex::normalize_disj(), num_projs(), num_tprojs(), mim::Rewriter::rewrite_imm_Seq(), mim::Rewriter::rewrite_mut_Seq(), mim::Seq::set(), mim::tuple2str(), mim::unflatten(), and var_type().

◆ as_imm()

template<class T = Def>

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

inline

Definition at line 480 of file def.h.

References as_mut().

◆ 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 494 of file def.h.

Referenced by as_imm(), mim::plug::clos::clos_type(), mim::plug::autodiff::Eval::derive_(), mim::ast::TuplePtrn::emit_body(), mim::Var::mut(), mim::Var::rebuild_(), mim::PrefixCleanup::rewrite_external(), mim::RWPhase::rewrite_external(), and mim::Rewriter::rewrite_mut_Seq().

◆ 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, mim::Reform, mim::Rule, and mim::Sigma.

Definition at line 583 of file def.h.

References type().

Referenced by set(), and 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, mim::Rule, and mim::Sigma.

Definition at line 578 of file def.h.

◆ cmp()

Def::Cmp mim::Def::cmp	(	const Def *	a,
		const Def *	b )

staticnodiscard

Definition at line 507 of file def.cpp.

References cmp(), mim::Sets< D, N >::Set::contains(), E, flags(), free_vars(), G, is_set(), isa_imm(), isa_mut(), L, mim::Var::mut(), node(), num_ops(), op(), type(), and U.

Referenced by cmp().

◆ dbg()

Dbg mim::Def::dbg ( ) const

inline

Definition at line 505 of file def.h.

References dbg_.

Referenced by rebuild(), mim::Axm::rebuild_(), mim::Inj::rebuild_(), mim::TBound< Up >::rebuild_(), mim::TExt< Up >::rebuild_(), mim::Rewriter::rewrite(), mim::Arr::stub(), stub(), mim::Global::stub(), mim::Hole::stub(), mim::Lam::stub(), mim::Pack::stub(), mim::Pi::stub(), mim::Rule::stub(), and mim::Sigma::stub().

◆ debug_prefix()

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

Definition at line 499 of file def.cpp.

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

◆ debug_suffix()

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

Definition at line 500 of file def.cpp.

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

◆ dep()

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

inlinenoexcept

Definition at line 343 of file def.h.

References dep(), and deps().

Referenced by dep().

◆ deps()

Defs mim::Def::deps ( ) const

noexcept

Definition at line 470 of file def.cpp.

References is_set(), and ops().

Referenced by dep(), mim::Scheduler::early(), mim::World::for_each(), mim::plug::clos::free_defs(), is_immutabilizable(), num_deps(), mim::post_order(), mim::PassMan::run(), and zonk_mut().

◆ 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 128 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 625 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 126 of file dot.cpp.

Referenced by dot(), and dot().

◆ dump() [1/2]

void mim::Def::dump ( ) const

Definition at line 452 of file dump.cpp.

◆ dump() [2/2]

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

Definition at line 453 of file dump.cpp.

References stream().

◆ flags()

flags_t mim::Def::flags ( ) const

inlineconstexprnoexcept

Definition at line 269 of file def.h.

References flags(), and flags_.

Referenced by mim::Axm::base(), cmp(), Def(), Def(), Def(), flags(), mim::Axm::IsA< Id, D >::id(), mim::Pi::is_implicit(), mim::Global::is_mutable(), mim::UInc::offset(), mim::Proxy::pass(), mim::Axm::plugin(), mim::Axm::sub(), mim::Axm::tag(), and mim::Proxy::tag().

◆ free_vars() [1/2]

Vars mim::Def::free_vars ( )

Definition at line 350 of file def.cpp.

References free_vars(), 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 337 of file def.cpp.

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

Referenced by cmp(), mim::Nest::contains(), free_vars(), mim::plug::clos::ClosConvPrep::from_outer_scope(), is_closed(), mim::Rule::is_in_rule(), and is_open().

◆ gid()

u32 mim::Def::gid ( ) const

inlineconstexprnoexcept

Global id - unique number for this Def.

Definition at line 270 of file def.h.

Referenced by mim::plug::regex::compare_re(), Def(), mim::ll::Emitter::emit_bb(), mim::World::match(), mim::plug::refly::normalize_gid(), mim::UseHash::operator()(), set(), set(), and unique_name().

◆ greater()

bool mim::Def::greater	(	const Def *	a,
		const Def *	b )

staticnodiscard

Definition at line 550 of file def.cpp.

Referenced by mim::plug::core::normalize_bit2(), mim::plug::core::normalize_nat(), and mim::plug::core::normalize_ncmp().

◆ has_dep() [1/3]

bool mim::Def::has_dep ( ) const

inline

Definition at line 357 of file def.h.

Referenced by mim::needs_zonk().

◆ has_dep() [2/3]

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

inline

Definition at line 358 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 359 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 433 of file def.h.

References has_var().

Referenced by mim::Lam::eta_reduce(), has_var(), has_var(), is_immutabilizable(), and mim::Rewriter::rewrite_mut_Seq().

◆ has_var() [2/2]

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

inline

As above if this is a mutable.

Definition at line 435 of file def.h.

References has_var(), and isa_mut().

◆ hash()

size_t mim::Def::hash ( ) const

inlineconstexprnoexcept

Definition at line 273 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, mim::Rule, and mim::Sigma.

Definition at line 556 of file def.h.

Referenced by mim::Rewriter::rewrite_stub().

◆ is_closed()

bool mim::Def::is_closed ( ) const

Has no free_vars()?

Definition at line 418 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::vec::normalize_diff(), and mim::plug::core::normalize_pe().

◆ is_elim()

bool mim::Def::is_elim ( ) const

inlinenoexcept

Definition at line 285 of file def.h.

References mim::Elim, and judge().

◆ is_external()

bool mim::Def::is_external ( ) const

inlinenoexcept

Definition at line 467 of file def.h.

Referenced by is_closed(), mim::isa_workable(), mim::World::make_external(), mim::World::make_internal(), mim::EtaExpPhase::rewrite_external(), mim::EtaRedPhase::rewrite_external(), mim::PrefixCleanup::rewrite_external(), and mim::RWPhase::rewrite_external().

◆ is_form()

bool mim::Def::is_form ( ) const

inlinenoexcept

Definition at line 283 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 174 of file def.cpp.

References deps(), has_var(), is_set(), 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 284 of file def.h.

References mim::Intro, and judge().

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

◆ is_meta()

bool mim::Def::is_meta ( ) const

inlinenoexcept

Definition at line 286 of file def.h.

References judge(), and mim::Meta.

◆ is_mutable()

bool mim::Def::is_mutable ( ) const

inlinenoexcept

Definition at line 476 of file def.h.

◆ is_open()

bool mim::Def::is_open ( ) const

Has free_vars()?

Definition at line 426 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 295 of file def.cpp.

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

Referenced by mim::EtaExp::analyze(), cmp(), deps(), is_immutabilizable(), mim::Hole::isa_set(), mim::isa_workable(), mim::EtaExp::rewrite(), mim::EtaRed::rewrite(), mim::BetaRedPhase::rewrite_imm_App(), mim::BranchNormalizePhase::rewrite_mut_Lam(), mim::Rewriter::rewrite_mut_Seq(), mim::Rewriter::rewrite_stub(), mim::Hole::tuplefy(), and zonk_mut().

◆ is_term()

bool mim::Def::is_term ( ) const

Definition at line 487 of file def.cpp.

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

Referenced by mim::Rewriter::rewrite_mut_Seq().

◆ isa_imm()

template<class T = Def>

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

inline

Definition at line 479 of file def.h.

References isa_mut().

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

◆ isa_mut()

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

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

inline

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

Definition at line 485 of file def.h.

Referenced by mim::BetaRed::analyze(), mim::EtaExp::analyze(), mim::EtaRed::analyze(), mim::plug::mem::pass::SSA::analyze(), mim::World::app(), mim::Sigma::arity(), mim::plug::autodiff::Eval::augment_(), cmp(), mim::Scheduler::early(), mim::Bound::find(), mim::Hole::find(), free_vars(), has_var(), mim::plug::clos::isa_clos_type(), isa_imm(), mim::Hole::isa_unset(), mim::Scheduler::late(), local_muts(), proj(), mim::EtaExp::rewrite(), mim::EtaRed::rewrite(), mim::plug::mem::pass::SSA::rewrite(), mim::Rewriter::rewrite(), mim::Scalarize::rewrite(), mim::plug::clos::ClosConvPrep::rewrite_arg(), mim::BetaRedPhase::rewrite_imm_App(), mim::plug::affine::phase::LowerFor::rewrite_imm_App(), mim::Scheduler::Scheduler(), mim::Hole::tuplefy(), and zonk_mut().

◆ judge()

u32 mim::Def::judge ( ) const

noexcept

Definition at line 477 of file def.cpp.

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

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

◆ less()

bool mim::Def::less	(	const Def *	a,
		const Def *	b )

staticnodiscard

Definition at line 549 of file def.cpp.

◆ loc()

Loc mim::Def::loc ( ) const

inline

Definition at line 506 of file def.h.

References dbg_.

Referenced by mim::World::app(), mim::Arr::check(), mim::Lam::check(), mim::Pi::check(), mim::Reform::check(), mim::Rule::check(), mim::World::extract(), mim::World::insert(), mim::plug::refly::normalize_equiv(), mim::World::seq(), mim::World::type(), mim::World::uinc(), and mim::World::umax().

◆ 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 332 of file def.cpp.

References isa_mut().

Referenced by mim::World::for_each(), free_vars(), is_closed(), mim::needs_zonk(), and mim::post_order().

◆ 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 348 of file def.cpp.

Referenced by free_vars(), is_closed(), and is_open().

◆ make_external()

void mim::Def::make_external ( )

Definition at line 570 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 571 of file def.cpp.

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

Referenced by mim::optimize(), and transfer_external().

◆ mark()

u32 mim::Def::mark ( ) const

inlineconstexprnoexcept

Used internally by free_vars().

Definition at line 272 of file def.h.

◆ node()

Node mim::Def::node ( ) const

inlineconstexprnoexcept

Definition at line 274 of file def.h.

Referenced by mim::Bound::Bound(), cmp(), Def(), Def(), mim::Ext::Ext(), mim::Pi::isa_cn(), judge(), node_name(), mim::Rewriter::rewrite_imm(), mim::Rewriter::rewrite_mut(), and mim::Seq::set().

◆ node_name()

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

Definition at line 460 of file def.cpp.

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

Referenced by mim::plug::autodiff::Eval::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 344 of file def.h.

References deps().

◆ num_ops()

size_t mim::Def::num_ops ( ) const

inlineconstexprnoexcept

Definition at line 309 of file def.h.

Referenced by mim::EtaExp::analyze(), mim::plug::mem::pass::SSA::analyze(), mim::Sigma::arity(), cmp(), mim::plug::core::convert(), Def(), is_set(), mim::plug::mem::normalize_load(), refine(), mim::EtaExp::rewrite(), mim::EtaRed::rewrite(), mim::plug::mem::pass::SSA::rewrite(), mim::Rewriter::rewrite_stub(), set(), set(), mim::Sigma::stub_(), and unset().

◆ num_projs()

nat_t mim::Def::num_projs ( ) const

Yields Def::arity(), if it is a Lit, or 1 otherwise.

Definition at line 581 of file def.cpp.

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

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 583 of file def.cpp.

References arity(), mim::World::flags(), mim::Lit::isa(), mim::Flags::scalarize_threshold, and world().

Referenced by tproj(), and tprojs().

◆ num_tvars()

nat_t mim::Def::num_tvars ( )

inlinenoexcept

Definition at line 429 of file def.h.

References var().

◆ num_vars()

nat_t mim::Def::num_vars ( )

inlinenoexcept

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

References ops().

Referenced by mim::EtaExp::analyze(), mim::plug::mem::pass::SSA::analyze(), mim::App::arg(), mim::Arr::arity(), mim::Sigma::arity(), mim::Lam::body(), mim::App::callee(), mim::plug::clos::clos_type_to_pi(), cmp(), mim::Pi::codom(), mim::Pi::dom(), mim::Lam::filter(), mim::Hole::find(), mim::Bound::get(), mim::Rule::guard(), mim::Extract::index(), mim::Insert::index(), mim::Global::init(), is_immutabilizable(), is_set(), mim::plug::clos::isa_clos_type(), mim::Hole::isa_set(), mim::Type::level(), mim::Rule::lhs(), mim::Reform::meta_type(), mim::Var::mut(), mim::plug::mem::normalize_load(), mim::Hole::op(), mim::UInc::op(), mim::Uniq::op(), proj(), refine(), mim::EtaExp::rewrite(), mim::EtaRed::rewrite(), mim::plug::mem::pass::SSA::rewrite(), mim::Rewriter::rewrite_stub(), mim::Rule::rhs(), mim::Match::scrutinee(), set(), mim::Extract::tuple(), mim::Insert::tuple(), mim::Inj::value(), mim::Insert::value(), mim::Split::value(), and zonk_mut().

◆ ops()

template<size_t N = std::dynamic_extent>

auto mim::Def::ops ( ) const

inlineconstexprnoexcept

Definition at line 305 of file def.h.

References ops().

Referenced by mim::BetaRed::analyze(), mim::Match::arms(), mim::Seq::body(), mim::Bound::Bound(), mim::Sigma::check(), mim::plug::core::convert(), Def(), Def(), deps(), mim::World::extract(), mim::Bound::find(), mim::Sigma::immutabilize(), mim::Sigma::infer(), mim::Tuple::infer(), is_set(), op(), ops(), rebuild(), rebuild(), rebuild_(), mim::EtaExp::rewrite(), set(), mim::Lam::set(), mim::Reform::set(), mim::Sigma::set(), and mim::plug::mem::strip_mem_ty().

◆ 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 588 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 384 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 413 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 390 of file def.h.

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

Referenced by mim::plug::autodiff::Eval::augment_tuple(), mim::ll::Emitter::emit_bb(), mim::plug::clos::Clos2SJLJ::enter(), mim::plug::regex::flatten_in_arg(), mim::plug::mem::mem_def(), mim::plug::core::normalize_abs(), mim::plug::autodiff::normalize_add(), mim::plug::math::normalize_arith(), mim::plug::core::normalize_bit2(), mim::plug::tuple::normalize_cat(), mim::plug::vec::normalize_cat(), mim::plug::refly::normalize_check(), mim::plug::math::normalize_cmp(), 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::ord::normalize_insert(), 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_App(), mim::plug::mem::strip_mem(), and mim::unflatten().

◆ projs() [3/4]

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

inline

Definition at line 419 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 408 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 552 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 548 of file def.h.

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

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

◆ rebuild_()

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

privatepure virtual

Implemented in mim::App, mim::Arr, mim::Axm, mim::Extract, mim::Global, mim::Hole, mim::Idx, mim::Inj, mim::Insert, mim::Lam, mim::Lit, mim::Match, mim::Merge, mim::Nat, mim::Pack, mim::Pi, mim::Proxy, mim::Reform, mim::Rule, mim::Sigma, mim::Split, 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 >, mim::TExt< true >, mim::Tuple, mim::Type, mim::UInc, mim::UMax, mim::Uniq, mim::Univ, and mim::Var.

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

Referenced by rebuild().

◆ reduce()

template<size_t N = std::dynamic_extent>

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

inlineconstexpr

See also: World::reduce

Definition at line 563 of file def.h.

Referenced by mim::Arr::reduce(), mim::Lam::reduce(), mim::Pack::reduce(), mim::Pi::reduce(), and mim::Rule::reduce().

◆ 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, mim::Rule, and mim::Sigma.

Definition at line 569 of file def.h.

◆ refine()

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

Definition at line 229 of file def.cpp.

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

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

◆ set() [1/14]

template<bool Ow = false>

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

inline

Definition at line 526 of file def.h.

References set().

◆ set() [2/14]

template<bool Ow = false>

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

inline

Definition at line 525 of file def.h.

References set().

◆ set() [3/14]

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

Set ops all at once (no Def::unset necessary beforehand).

Definition at line 240 of file def.cpp.

References check(), gid(), num_ops(), ops(), type(), world(), and zonk().

◆ set() [4/14]

template<bool Ow = false>

Def * mim::Def::set ( Loc l )

inline

Definition at line 516 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 515 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 524 of file def.h.

References set(), and sym().

◆ set() [7/14]

template<bool Ow = false>

const Def * mim::Def::set	(	Loc	l,
		std::string	s ) const

inline

Definition at line 523 of file def.h.

References set(), and sym().

◆ set() [8/14]

template<bool Ow = false>

Def * mim::Def::set	(	Loc	l,
		Sym	s )

inline

Definition at line 522 of file def.h.

References set().

◆ set() [9/14]

template<bool Ow = false>

const Def * mim::Def::set	(	Loc	l,
		Sym	s ) const

inline

Definition at line 521 of file def.h.

References set().

◆ set() [10/14]

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

Successively set from left to right.

Definition at line 263 of file def.cpp.

References check(), gid(), num_ops(), op(), type(), world(), and zonk().

Referenced by mim::Lam::app(), mim::plug::autodiff::Eval::augment_extract(), mim::plug::autodiff::Eval::derive_(), mim::ast::MatchExpr::Arm::emit(), mim::ast::AliasPtrn::emit_value(), rebuild(), mim::LamSpec::rewrite(), mim::plug::mem::pass::SSA::rewrite(), mim::VarRewriter::rewrite(), mim::plug::clos::ClosConvPrep::rewrite_arg(), mim::plug::clos::ClosConvPrep::rewrite_callee(), mim::Rewriter::rewrite_stub(), set(), set(), set(), set(), set(), set(), set(), set(), mim::Global::set(), mim::Hole::set(), mim::Lam::set(), mim::Lam::set(), mim::Pack::set(), mim::Pi::set(), mim::Reform::set(), mim::Reform::set(), mim::Seq::set(), mim::Sigma::set(), mim::Sigma::set(), mim::Arr::set_arity(), 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::Rule::set_guard(), mim::Rule::set_lhs(), mim::Rule::set_rhs(), and stub().

◆ set() [11/14]

template<bool Ow = false>

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

inline

Definition at line 520 of file def.h.

References set(), and sym().

◆ set() [12/14]

template<bool Ow = false>

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

inline

Definition at line 519 of file def.h.

References set(), and sym().

◆ set() [13/14]

template<bool Ow = false>

Def * mim::Def::set ( Sym s )

inline

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

References dbg_.

◆ set_type()

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

Update type.

Warning: Only make type-preserving updates such as removing Holes. Do this even before updating all other ops()!.

Definition at line 280 of file def.cpp.

References type().

◆ stream()

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

Definition at line 432 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 545 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 544 of file def.h.

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

Referenced by mim::LamSpec::rewrite(), and mim::Seq::stub().

◆ 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::Rule, and mim::Sigma.

Definition at line 641 of file def.h.

References World.

Referenced by stub().

◆ sym() [1/4]

Sym mim::Def::sym ( ) const

inline

Definition at line 507 of file def.h.

References dbg_.

Referenced by mim::plug::autodiff::Eval::augment_lam(), debug_prefix(), debug_suffix(), mim::World::make_external(), mim::World::make_internal(), mim::PrefixCleanup::rewrite_external(), set(), set(), set(), set(), transfer_external(), and unique_name().

◆ sym() [2/4]

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

protected

Definition at line 435 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 437 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 436 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 271 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 385 of file def.h.

References num_tprojs(), and proj().

◆ tprojs() [1/2]

auto mim::Def::tprojs ( ) const

inline

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

References num_tprojs(), and projs().

◆ transfer_external()

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

Definition at line 573 of file def.cpp.

References make_external(), make_internal(), and sym().

◆ tvar()

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

inlinenoexcept

Definition at line 429 of file def.h.

◆ tvars() [1/2]

auto mim::Def::tvars ( )

inlinenoexcept

Definition at line 429 of file def.h.

◆ tvars() [2/2]

template<class F>

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

inlinenoexcept

Definition at line 429 of file def.h.

◆ type()

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

noexcept

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

See also: Def::unfold_type.

Definition at line 447 of file def.cpp.

References var().

Referenced by mim::World::app(), arity(), mim::Pack::arity(), mim::Checker::assignable(), mim::plug::autodiff::Eval::augment_(), mim::plug::autodiff::Eval::augment_app(), mim::plug::autodiff::Eval::augment_extract(), mim::plug::autodiff::Eval::augment_lam(), mim::plug::autodiff::Eval::augment_pack(), mim::plug::autodiff::Eval::augment_tuple(), mim::Bound::Bound(), mim::App::callee_type(), mim::Arr::check(), check(), mim::Lam::check(), mim::Pi::check(), mim::Reform::check(), mim::Rule::check(), mim::Sigma::check(), mim::plug::clos::clos_pack(), cmp(), mim::plug::matrix::counting_for(), Def(), Def(), Def(), mim::plug::autodiff::Eval::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::World::implicit_app(), mim::Axm::infer_curry_and_trip(), mim::World::insert(), is_term(), mim::is_unit(), mim::plug::clos::ClosLit::isa_clos_lit, 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::Pi::Pi(), mim::Pi::Pi(), proj(), rebuild(), rebuild(), mim::Axm::rebuild_(), rebuild_(), refine(), mim::Reform::Reform(), 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_App(), mim::Rewriter::rewrite_mut_Seq(), mim::Scheduler::Scheduler(), mim::World::seq(), set(), set(), set_type(), mim::plug::mem::strip_mem(), mim::Arr::stub(), stub(), stub(), mim::Hole::stub(), mim::Pack::stub(), mim::Pi::stub(), mim::Seq::stub(), mim::Sigma::stub(), mim::Hole::tuplefy(), mim::Global::type(), mim::Lam::type(), mim::Rule::type(), mim::World::type(), mim::World::uinc(), mim::World::umax(), unfold_type(), 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 452 of file def.cpp.

References type(), and world().

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

◆ unique_name()

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

name + "_" + Def::gid

Definition at line 579 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 only partially set.

Definition at line 286 of file def.cpp.

References num_ops().

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

◆ users()

Muts mim::Def::users ( )

inline

Set of mutables where this mutable is locally referenced.

Definition at line 460 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 307 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

◆ var() [3/3]

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

inlinenoexcept

Definition at line 429 of file def.h.

◆ var_type()

const Def * mim::Def::var_type ( )

If this is a binder, compute the type of its Variable.

Definition at line 314 of file def.cpp.

References arity(), and world().

Referenced by mim::Var::type(), and mim::World::var().

◆ vars() [1/4]

template<nat_t A = std::dynamic_extent>

auto mim::Def::vars ( )

inlinenoexcept

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

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

◆ vars() [3/4]

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

inlinenoexcept

Definition at line 429 of file def.h.

◆ vars() [4/4]

template<class F>

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

inlinenoexcept

Definition at line 429 of file def.h.

◆ world()

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

noexcept

Definition at line 439 of file def.cpp.

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

Referenced by mim::Checker::alpha(), mim::Lam::app(), mim::Lam::app(), mim::plug::clos::apply_closure(), arity(), mim::Pack::arity(), mim::Sigma::arity(), mim::plug::autodiff::autodiff_type_fun(), mim::plug::autodiff::autodiff_type_fun_pi(), mim::Lam::branch(), mim::Lam::check(), mim::Rule::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(), mim::Stage::create(), 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::Rule::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(), mim::plug::core::normalize_idx_unsafe(), mim::plug::compile::normalize_is_loaded(), 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::Lam::reduce(), mim::Rule::replace(), set(), set(), mim::Lam::set(), mim::Pi::set_dom(), mim::Lam::set_filter(), 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::Rule::stub(), mim::Sigma::stub(), sym(), sym(), sym(), mim::tuple2str(), mim::Hole::tuplefy(), unfold_type(), var(), var_type(), mim::plug::autodiff::zero_def(), mim::plug::autodiff::zero_pullback(), zonk(), and zonk_mut().

◆ write() [1/2]

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

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

References stream().

◆ zonk() [1/2]

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 71 of file check.cpp.

References mim::needs_zonk(), world(), and Zonker.

Referenced by mim::World::app(), mim::World::extract(), mim::World::inj(), mim::World::insert(), mim::World::match(), mim::World::merge(), mim::World::merge(), mim::World::raw_app(), mim::World::seq(), set(), set(), mim::World::sigma(), mim::World::split(), mim::World::tuple(), mim::World::tuple(), mim::World::type(), mim::World::uinc(), mim::World::umax(), mim::World::uniq(), and zonk_mut().

◆ zonk() [2/2]

DefVec mim::Def::zonk ( Defs defs )

static

zonks all defs and retuns a new DefVec.

Definition at line 102 of file check.cpp.

◆ zonk_mut()

const Def * mim::Def::zonk_mut ( ) const

If *mutable, zonks all ops and tries to immutabilize it; otherwise just zonk.

Definition at line 76 of file check.cpp.

References deps(), is_set(), isa_mut(), mim::needs_zonk(), op(), world(), zonk(), and Zonker.

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 423 of file dump.cpp.

References world().

◆ Sets

template<class D, size_t N>

friend class Sets

friend

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

References World.

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

◆ Zonker

friend class Zonker

friend

Definition at line 688 of file def.h.

References Zonker.

Referenced by zonk(), zonk_mut(), and Zonker.

Member Data Documentation

◆ [union]

union { ... } mim::Def

◆ curry_

u8 mim::Def::curry_ = 0

protected

Definition at line 664 of file def.h.

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

◆ dbg_

Dbg mim::Def::dbg_

mutableprotected

Definition at line 656 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 663 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 665 of file def.h.

Referenced by mim::App::trip(), and mim::Axm::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

Static Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Friends

Syntactic Comparison

Detailed Description

Member Enumeration Documentation

◆ Cmp

Constructor & Destructor Documentation

◆ Def() [1/3]

◆ Def() [2/3]

◆ Def() [3/3]

◆ ~Def()

Member Function Documentation

◆ arity()

◆ as_imm()

◆ as_mut()

◆ check() [1/2]

◆ check() [2/2]

◆ cmp()

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

◆ greater()

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

◆ is_open()

◆ is_set()

◆ is_term()

◆ isa_imm()

◆ isa_mut()

◆ judge()

◆ less()

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