A (possibly paramterized) Array. More...

#include <mim/tuple.h>

Inheritance diagram for mim::Arr:

Public Member Functions
ops
const Def *	arity () const final
Setters
See also Setting Ops
Arr *	set_arity (const Def *arity)
Arr *	set_body (const Def *body)
Arr *	set (const Def arity, const Def body)
Arr *	unset ()
Rebuild
Arr *	stub (const Def *type)
const Def *	immutabilize () final
	Tries to make an immutable from a mutable.
const Def *	reduce (const Def *arg) const final
constexpr size_t	reduction_offset () const noexcept final
	First Def::op that needs to be dealt with during reduction; e.g.
Type Checking
const Def *	check (size_t, const Def *) final
	Checks whether the ith operand can be set to def.
const Def *	check () final
	After all Def::ops have been Def::set, this method will be invoked to check the type of this mutable.
Public Member Functions inherited from mim::Seq
const Def *	body () const
Seq *	set (const Def arity, const Def body)
	Common setter for Packs and Arrays.
Seq *	unset ()
Seq *	stub (World &w, const Def *type)
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
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 Def *	var_type ()
	If this is a binder, compute the type of its Variable.
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.
template<class D = Def>
std::pair< D , const Var >	isa_binder () const
	Is this a mutable that introduces a Var?
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()?
Def *	outermost_binder () const
	Transitively walks up free_vars() till the outermoust binder has been found.
bool	is_external () const noexcept
void	externalize ()
void	internalize ()
void	transfer_external (Def *to)
bool	is_annex () const noexcept
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 constness away and perform a dynamic_cast to `T`.
template<class T = Def, bool invert = false>
T *	as_mut () const
	Asserts that this is a mutable, casts constness away and performs a static_cast to `T`.
Dbg	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
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
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, zonk()s 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, int max=std::numeric_limits< int >::max(), bool types=false) const
void	dot (const char *file=nullptr, int max=std::numeric_limits< int >::max(), bool types=false) const
	Same as above but write to `file` or std::cout if `file` is nullptr.
void	dot (const std::string &file, int max=std::numeric_limits< int >::max(), bool types=false) const
Public Member Functions inherited from mim::Setters< Seq >
const Seq *	set (Loc l) const
Public Member Functions inherited from mim::Setters< Arr >
const Arr *	set (Loc l) const

Static Public Attributes
static constexpr auto	Node = mim::Node::Arr
static constexpr size_t	Num_Ops = 2

Private Member Functions
const Def *	rebuild_ (World &, const Def *, Defs) const final
Arr *	stub_ (World &, const Def *) 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 returns 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::Seq
	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.
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

A (possibly paramterized) Array.

Arrays are usually homogenous but they can be inhomogenous as well: «i: N; T#i»

See also: Sigma, Tuple, Pack

Definition at line 117 of file tuple.h.

Member Function Documentation

◆ arity()

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

inlinefinalvirtual

Reimplemented from mim::Def.

Definition at line 127 of file tuple.h.

References mim::Seq::Def(), and mim::Def::op().

Referenced by immutabilize(), set(), and set_arity().

◆ check() [1/2]

const Def * mim::Arr::check ( )

finalvirtual

After all Def::ops have been 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 from mim::Def.

Definition at line 277 of file check.cpp.

References mim::Checker::alpha(), mim::Seq::body(), mim::Seq::Def(), mim::error(), mim::Def::loc(), mim::Def::type(), and mim::Def::unfold_type().

◆ check() [2/2]

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

finalvirtual

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 from mim::Def.

Definition at line 275 of file check.cpp.

References mim::Seq::Def().

◆ immutabilize()

const Def * mim::Arr::immutabilize ( )

finalvirtual

Tries to make an immutable from a mutable.

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

Reimplemented from mim::Def.

Definition at line 203 of file def.cpp.

References arity(), mim::Seq::body(), mim::Seq::Def(), mim::Def::is_immutabilizable(), mim::Lit::isa(), reduce(), and mim::Def::world().

◆ rebuild_()

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

finalprivatevirtual

Implements mim::Def.

Definition at line 115 of file def.cpp.

References mim::Seq::Def(), and World.

◆ reduce()

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

inlinefinalvirtual

Implements mim::Seq.

Definition at line 144 of file tuple.h.

References mim::Seq::Def(), reduce(), and mim::Def::reduce().

Referenced by immutabilize(), and reduce().

◆ reduction_offset()

size_t mim::Arr::reduction_offset ( ) const

inlineconstexprfinalvirtualnoexcept

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 from mim::Def.

Definition at line 145 of file tuple.h.

◆ set()

Arr * mim::Arr::set	(	const Def *	arity,
		const Def *	body )

inline

Definition at line 136 of file tuple.h.

References arity(), mim::Seq::body(), mim::Seq::Def(), and set_arity().

◆ set_arity()

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

inline

Definition at line 134 of file tuple.h.

References arity(), mim::Seq::Def(), and mim::Def::set().

Referenced by set().

◆ set_body()

Arr * mim::Arr::set_body ( const Def * body )

inline

Definition at line 135 of file tuple.h.

References mim::Seq::body(), mim::Seq::Def(), and mim::Def::set().

◆ stub()

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

inline

Definition at line 142 of file tuple.h.

References mim::Def::dbg(), mim::Seq::Def(), stub_(), mim::Def::type(), and mim::Def::world().

◆ stub_()

Arr * mim::Arr::stub_	(	World &	w,
		const Def *	t )

finalprivatevirtual

Reimplemented from mim::Def.

Definition at line 150 of file def.cpp.

References mim::Seq::Def(), and World.

Referenced by stub().

◆ unset()

Arr * mim::Arr::unset ( )

inline

Definition at line 137 of file tuple.h.

References mim::Def::unset().

◆ World

friend class World

friend

Definition at line 161 of file tuple.h.

References World.

Referenced by rebuild_(), stub_(), and World.

Member Data Documentation

◆ Node

auto mim::Arr::Node = mim::Node::Arr

staticconstexpr

Definition at line 154 of file tuple.h.

◆ Num_Ops

size_t mim::Arr::Num_Ops = 2

staticconstexpr

Definition at line 155 of file tuple.h.

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

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

Public Member Functions

Static Public Attributes

Private Member Functions

Friends

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ arity()

◆ check() [1/2]

◆ check() [2/2]

◆ immutabilize()

◆ rebuild_()

◆ reduce()

◆ reduction_offset()

◆ set()

◆ set_arity()

◆ set_body()

◆ stub()

◆ stub_()

◆ unset()

Friends And Related Symbol Documentation

◆ World

Member Data Documentation

◆ Node

◆ Num_Ops