thorin::Axiom Class Reference

#include <thorin/axiom.h>

Inheritance diagram for thorin::Axiom:

Classes
struct	Match
	Type of Match::def_. More...
struct	Match< plug::regex::any >

Public Member Functions
Annex Name
See also annex_name "Annex Name"
plugin_t	plugin () const
tag_t	tag () const
sub_t	sub () const
flags_t	base () const
Public Member Functions inherited from thorin::Def
World &	world () const
flags_t	flags () const
u32	gid () const
hash_t	hash () const
node_t	node () const
std::string_view	node_name () const
const Def *	type () const
	Yields the raw type of this Def, i.e. 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
	Yields true if this:T and T:(.Type 0).
Ref	arity () const
std::optional< nat_t >	isa_lit_arity () const
nat_t	as_lit_arity () const
template<size_t N = std::dynamic_extent>
auto	ops () const
const Def *	op (size_t i) const
size_t	num_ops () const
Def *	set (size_t i, const Def *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.
Def *	set_type (const Def *)
void	unset_type ()
void	update ()
	Resolves Infers of this Def's type.
bool	is_set () const
	Yields true if empty or the last op is set.
Defs	extended_ops () const
const Def *	extended_op (size_t i) const
size_t	num_extended_ops () const
Defs	partial_ops () const
const Def *	partial_op (size_t i) const
size_t	num_partial_ops () const
const Uses &	uses () const
size_t	num_uses () const
unsigned	dep () const
bool	has_dep (Dep d) const
bool	has_dep (unsigned u) const
bool	dep_const () const
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::scalerize_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 = -1_n, class F >
auto	projs (F f) const
	Splits this Def via Def::projections into an Array (if A == -1_n) 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 = -1_n>
auto	projs () const
auto	tprojs () const
auto	projs (nat_t a) const
nat_t	num_vars ()
nat_t	num_tvars ()
Ref	var (nat_t a, nat_t i)
Ref	var (nat_t i)
Ref	tvar (nat_t i)
template<nat_t A = std::dynamic_extent, class F >
auto	vars (F f)
template<class F >
auto	tvars (F f)
template<nat_t A = std::dynamic_extent>
auto	vars ()
auto	tvars ()
template<class F >
auto	vars (nat_t a, F f)
auto	vars (nat_t a)
Ref	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.
Muts	local_muts () const
Vars	local_vars () const
Vars	free_vars () const
Vars	free_vars ()
bool	is_open () const
	Has free_vars()?
bool	is_closed () const
	Has no free_vars()?
Muts	fv_consumers ()
bool	is_external () const
void	make_external ()
void	make_internal ()
void	transfer_external (Def *to)
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 *mut*able, 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, Ref type)
Def *	stub (Ref type)
Ref	rebuild (World &w, Ref type, Defs ops) const
	Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
Ref	rebuild (Ref type, Defs ops) const
virtual const Def *	immutabilize ()
	Tries to make an immutable from a mutable.
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)
virtual void	check ()
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

Normalization
For a curried App of an Axiom, you only want to trigger normalization at specific spots. For this reason, Thorin maintains a Def::curry_ counter that each App decrements. The Axiom::normalizer() will be triggered when Axiom::curry() becomes 0. These are also the spots that you can thorin::match/thorinforce/Match. After that, the counter will be set to Axiom::trip(). E.g., let's say an Axiom has this type: A -> B -> C -> D -> E ^ | | | +---------+ Using an initial value as 5 for Axiom::curry and 3 as Axiom::trip has the effect that here x a b c1 d1 e1 c2 d2 e2 c3 d3 e3 the Axiom::normalizer will be triggered after App'ing e1, e2, and e3.
static constexpr u8	Trip_End = u8(-1)
NormalizeFn	normalizer () const
u8	curry () const
u8	trip () const
static std::tuple< const Axiom *, u8, u8 >	get (const Def *def)
	Yields currying counter of def.
static std::pair< u8, u8 >	infer_curry_and_trip (const Def *type)

Additional Inherited Members
Protected Member Functions inherited from thorin::Def
	Def (World *, node_t, const Def *type, Defs ops, flags_t flags)
	Constructor for an immutable Def.
	Def (node_t n, const Def *type, Defs ops, flags_t flags)
	As above but World retrieved from type.
	Def (node_t, 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 thorin::Def
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_
u8	trip_

Detailed Description

Definition at line 9 of file axiom.h.

---

Class Documentation

thorin::Axiom::Match

struct thorin::Axiom::Match

template<class T>
struct thorin::Axiom::Match< T >

Type of Match::def_.

Definition at line 57 of file axiom.h.

Class Members
typedef App	type

thorin::Axiom::Match< plug::regex::any >

struct thorin::Axiom::Match< plug::regex::any >

Definition at line 6 of file regex.h.

Class Members
typedef Axiom	type

Member Function Documentation

base()

flags_t thorin::Axiom::base ( ) const

inline

Definition at line 53 of file axiom.h.

References thorin::Def::flags(), and thorin::Annex::flags2base().

curry()

u8 thorin::Axiom::curry ( ) const

inline

Definition at line 35 of file axiom.h.

References thorin::Def::curry_.

get()

std::tuple< const Axiom *, u8, u8 > thorin::Axiom::get ( const Def *  def )

static

Yields currying counter of def.

Returns

{nullptr, 0, 0} if no Axiom is present.

Definition at line 38 of file axiom.cpp.

Referenced by thorin::match(), thorin::match(), and thorin::World::raw_app().

infer_curry_and_trip()

std::pair< u8, u8 > thorin::Axiom::infer_curry_and_trip ( const Def *  type )

static

Definition at line 14 of file axiom.cpp.

normalizer()

NormalizeFn thorin::Axiom::normalizer ( ) const

inline

Definition at line 34 of file axiom.h.

Referenced by thorin::World::raw_app().

plugin()

plugin_t thorin::Axiom::plugin ( ) const

inline

Definition at line 50 of file axiom.h.

References thorin::Def::flags(), and thorin::Annex::flags2plugin().

Referenced by thorin::Match< Id, D >::plugin().

sub()

sub_t thorin::Axiom::sub ( ) const

inline

Definition at line 52 of file axiom.h.

References thorin::Def::flags(), and thorin::Annex::flags2sub().

Referenced by thorin::Match< Id, D >::base(), and thorin::Match< Id, D >::sub().

tag()

tag_t thorin::Axiom::tag ( ) const

inline

Definition at line 51 of file axiom.h.

References thorin::Def::flags(), and thorin::Annex::flags2tag().

Referenced by thorin::Match< Id, D >::tag().

trip()

u8 thorin::Axiom::trip ( ) const

inline

Definition at line 36 of file axiom.h.

References thorin::Def::trip_.

Member Data Documentation

Trip_End

constexpr u8 thorin::Axiom::Trip_End = u8(-1)

staticconstexpr

Definition at line 43 of file axiom.h.

Referenced by thorin::World::raw_app().

---

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

• include/thorin/axiom.h
• src/thorin/axiom.cpp