#include <mim/def.h>

Inheritance diagram for mim::Type:

Public Member Functions
ops
const Def *	level () const

Public Member Functions inherited from mim::Def
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

u32	judge () const noexcept

bool	is_form () const noexcept

bool	is_intro () const noexcept

bool	is_elim () const noexcept

bool	is_meta () const noexcept

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

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

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.

Defs	deps () const noexcept

const Def *	dep (size_t i) const noexcept

size_t	num_deps () const noexcept

bool	has_dep () const

bool	has_dep (Dep d) const

bool	has_dep (unsigned u) const

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

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.

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

bool	is_external () const noexcept

void	make_external ()

void	make_internal ()

void	transfer_external (Def *to)

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	dbg () const

Loc	loc () const

Sym	sym () const

std::string	unique_name () const
	name + "_" + Def::gid

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)

const Def *	debug_prefix (std::string) const

const Def *	debug_suffix (std::string) const

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.

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.

bool	needs_zonk () const
	Yields `true`, if Def::local_muts() contain a Hole that is set.

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.

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

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

Public Member Functions inherited from mim::Setters< Type >
const Type *	set (Loc l) const

Type *	set (Loc l)

const Type *	set (Sym s) const

Type *	set (Sym s)

const Type *	set (std::string s) const

Type *	set (std::string s)

const Type *	set (Loc l, Sym s) const

Type *	set (Loc l, Sym s)

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

Type *	set (Loc l, std::string s)

const Type *	set (Dbg d) const

Type *	set (Dbg d)

Static Public Attributes
static constexpr auto	Node = mim::Node::Type

static constexpr size_t	Num_Ops = 1

Private Member Functions
const Def *	rebuild_ (World &, const Def *, Defs) const final

Friends
class	World

Additional Inherited Members
enum class	Cmp { L , G , E , U }

Static Public Member Functions inherited from mim::Def
static DefVec	zonk (Defs defs)
	zonks all `defs` and retuns a new DefVec.

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)

Protected Member Functions inherited from mim::Def
	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

Sym	sym (const char *) const

Sym	sym (std::string_view) const

Sym	sym (std::string) const

Protected Attributes inherited from mim::Def
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

Detailed Description

Definition at line 778 of file def.h.

Member Function Documentation

◆ level()

const Def * mim::Type::level ( ) const

inline

Definition at line 788 of file def.h.

References mim::Def::op().

◆ rebuild_()

const Def * mim::Type::rebuild_	(	World &	w,
		const Def *	,
		Defs	o ) const

finalprivatevirtual

Implements mim::Def.

Definition at line 129 of file def.cpp.

References World.

Friends And Related Symbol Documentation

◆ World

friend class World

friend

Definition at line 797 of file def.h.

References World.

Referenced by rebuild_(), and World.

Member Data Documentation

◆ Node

auto mim::Type::Node = mim::Node::Type

staticconstexpr

Definition at line 791 of file def.h.

◆ Num_Ops

size_t mim::Type::Num_Ops = 1

staticconstexpr

Definition at line 792 of file def.h.

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

include/mim/def.h
src/mim/def.cpp

Public Member Functions

Static Public Attributes

Private Member Functions

Friends

Additional Inherited Members