#include <mim/axiom.h>

Inheritance diagram for mim::Axiom:

Classes
struct	Match
	Type of Match::def_. More...

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 mim::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

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

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 = -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 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, 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

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

Axiom *	set (Loc l)

const Axiom *	set (Sym s) const

Axiom *	set (Sym s)

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

Axiom *	set (std::string s)

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

Axiom *	set (Loc l, Sym s)

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

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

const Axiom *	set (Dbg d) const

Axiom *	set (Dbg d)

Static Public Attributes
static constexpr auto	Node = Node::Axiom

Private Member Functions
Ref	rebuild_ (World &, Ref, Defs) const override

Friends
class	World

Normalization
For a curried App of an Axiom, you only want to trigger normalization at specific spots. For this reason, MimIR 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 mim::match / mim::force / mim::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 mim::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 mim::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

◆ mim::Axiom::Match

struct mim::Axiom::Match

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

Type of Match::def_.

Definition at line 59 of file axiom.h.

Class Members
typedef App	type App

Member Function Documentation

◆ base()

flags_t mim::Axiom::base ( ) const

inline

Definition at line 55 of file axiom.h.

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

◆ curry()

u8 mim::Axiom::curry ( ) const

inline

Definition at line 37 of file axiom.h.

References mim::Def::curry_.

◆ get()

std::tuple< const Axiom *, u8, u8 > mim::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 mim::match(), mim::match(), and mim::World::raw_app().

◆ infer_curry_and_trip()

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

static

Definition at line 14 of file axiom.cpp.

Referenced by mim::ast::AxiomDecl::emit().

◆ normalizer()

NormalizeFn mim::Axiom::normalizer ( ) const

inline

Definition at line 36 of file axiom.h.

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

◆ plugin()

plugin_t mim::Axiom::plugin ( ) const

inline

Definition at line 52 of file axiom.h.

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

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

◆ rebuild_()

Ref mim::Axiom::rebuild_	(	World &	w,
		Ref	t,
		Defs	) const

overrideprivatevirtual

Implements mim::Def.

Definition at line 115 of file def.cpp.

References mim::Check::alpha().

◆ sub()

sub_t mim::Axiom::sub ( ) const

inline

Definition at line 54 of file axiom.h.

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

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

◆ tag()

tag_t mim::Axiom::tag ( ) const

inline

Definition at line 53 of file axiom.h.

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

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

◆ trip()

u8 mim::Axiom::trip ( ) const

inline

Definition at line 38 of file axiom.h.

References mim::Def::trip_.

Friends And Related Symbol Documentation

◆ World

friend class World

friend

Definition at line 68 of file axiom.h.

Member Data Documentation

◆ Node

auto mim::Axiom::Node = Node::Axiom

staticconstexpr

Definition at line 63 of file axiom.h.

◆ Trip_End

u8 mim::Axiom::Trip_End = u8(-1)

staticconstexpr

Definition at line 45 of file axiom.h.

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

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

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

Classes

Public Member Functions

Static Public Attributes

Private Member Functions

Friends

Normalization

Additional Inherited Members

Detailed Description

Class Documentation

◆ mim::Axiom::Match

Member Function Documentation

◆ base()

◆ curry()

◆ get()

◆ infer_curry_and_trip()

◆ normalizer()

◆ plugin()

◆ rebuild_()

◆ sub()

◆ tag()

◆ trip()

Friends And Related Symbol Documentation

◆ World

Member Data Documentation

◆ Node

◆ Trip_End