mim::Rule Class Reference

A rewrite rule. More...

#include <mim/rule.h>

Inheritance diagram for mim::Rule:

Public Member Functions
lhs & rhs
See also proj
const Reform *	type () const
const Def *	lhs () const
const Def *	rhs () const
const Def *	guard () const
Setters
See also Setting Ops
Rule *	set (const Def *lhs, const Def *rhs)
Rule *	set (const Def *lhs, const Def *rhs, const Def *guard)
Rule *	set_lhs (const Def *lhs)
Rule *	set_rhs (const Def *rhs)
Rule *	set_guard (const Def *guard)
Rule *	unset ()
Type checking
const Def *	check (size_t, const Def *) override
	Checks whether the ith operand can be set to def.
const Def *	check () override
	After all Def::ops have been Def::set, this method will be invoked to check the type of this mutable.
Rebuild
Rule *	stub (const Def *type)
const Rule *	immutabilize () override
	Tries to make an immutable from a mutable.
const Def *	reduce (const Def *arg) const
constexpr size_t	reduction_offset () const noexcept override
	First Def::op that needs to be dealt with during reduction; e.g.
Apply
bool	its_a_match (const Def *expr, Def2Def &) const
const Def *	replace (const Def *expr, Def2Def &) 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	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, 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< Rule >
const Rule *	set (Loc l) const

Static Public Member Functions
static bool	is_in_rule (const Def *)
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)

Static Public Attributes
static constexpr auto	Node = mim::Node::Rule
static constexpr size_t	Num_Ops = 3

Private Member Functions
const Def *	rebuild_ (World &, const Def *, Defs) const override
Rule *	stub_ (World &, const Def *) override

Friends
class	World

Additional Inherited Members
enum class	Cmp {   L ,   G ,   E ,   U }
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 rewrite rule.

Definition at line 38 of file rule.h.

Member Function Documentation

check() [1/2]

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

overridevirtual

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

References mim::Checker::alpha(), mim::Checker::assignable(), mim::error(), guard(), lhs(), mim::Def::loc(), rhs(), mim::Def::type(), type(), and mim::Def::world().

check() [2/2]

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

overridevirtual

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

guard()

const Def * mim::Rule::guard ( ) const

inline

Definition at line 52 of file rule.h.

References mim::Def::op().

Referenced by check(), replace(), set(), and set_guard().

immutabilize()

const Rule * mim::Rule::immutabilize ( )

overridevirtual

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

is_in_rule()

bool mim::Rule::is_in_rule ( const Def * expr )

static

Definition at line 38 of file rule.cpp.

References mim::Def::free_vars(), and mim::Def::var().

Referenced by its_a_match().

its_a_match()

bool mim::Rule::its_a_match	(	const Def *	expr,
		Def2Def &	v2v ) const

Definition at line 49 of file rule.cpp.

References is_in_rule(), and lhs().

lhs()

const Def * mim::Rule::lhs ( ) const

inline

Definition at line 50 of file rule.h.

References mim::Def::op().

Referenced by check(), its_a_match(), set(), set(), and set_lhs().

rebuild_()

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

overrideprivatevirtual

Implements mim::Def.

Definition at line 125 of file def.cpp.

References World.

reduce()

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

inline

Definition at line 80 of file rule.h.

References mim::Def::reduce().

reduction_offset()

size_t mim::Rule::reduction_offset ( ) const

inlineconstexproverridevirtualnoexcept

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 81 of file rule.h.

replace()

const Def * mim::Rule::replace	(	const Def *	expr,
		Def2Def &	v2v ) const

Definition at line 116 of file rule.cpp.

References guard(), rhs(), mim::tuple_of_dict(), mim::Def::var(), and mim::Def::world().

rhs()

const Def * mim::Rule::rhs ( ) const

inline

Definition at line 51 of file rule.h.

References mim::Def::op().

Referenced by check(), replace(), set(), set(), and set_rhs().

set() [1/2]

Rule * mim::Rule::set ( const Def * lhs, const Def * rhs )

inline

Definition at line 62 of file rule.h.

References lhs(), rhs(), set(), set_lhs(), and set_rhs().

Referenced by mim::World::rule(), set(), and stub().

set() [2/2]

Rule * mim::Rule::set ( const Def * lhs, const Def * rhs, const Def * guard )

inline

Definition at line 63 of file rule.h.

References guard(), lhs(), rhs(), set_guard(), set_lhs(), and set_rhs().

set_guard()

Rule * mim::Rule::set_guard ( const Def * guard )

inline

Definition at line 66 of file rule.h.

References guard(), and mim::Def::set().

Referenced by set().

set_lhs()

Rule * mim::Rule::set_lhs ( const Def * lhs )

inline

Definition at line 64 of file rule.h.

References lhs(), and mim::Def::set().

Referenced by set(), and set().

set_rhs()

Rule * mim::Rule::set_rhs ( const Def * rhs )

inline

Definition at line 65 of file rule.h.

References rhs(), and mim::Def::set().

Referenced by set(), and set().

stub()

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

inline

Definition at line 78 of file rule.h.

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

stub_()

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

overrideprivatevirtual

Reimplemented from mim::Def.

Definition at line 156 of file def.cpp.

References World.

Referenced by stub().

type()

const Reform * mim::Rule::type ( ) const

inline

Definition at line 49 of file rule.h.

References mim::Def::type().

Referenced by check(), and stub().

unset()

Rule * mim::Rule::unset ( )

inline

Definition at line 67 of file rule.h.

References mim::Def::unset().

Friends And Related Symbol Documentation

World

friend class World

friend

Definition at line 99 of file rule.h.

References World.

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

Member Data Documentation

Node

auto mim::Rule::Node = mim::Node::Rule

staticconstexpr

Definition at line 92 of file rule.h.

Num_Ops

size_t mim::Rule::Num_Ops = 3

staticconstexpr

Definition at line 93 of file rule.h.

---

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

• include/mim/rule.h
• src/mim/check.cpp
• src/mim/def.cpp
• src/mim/rule.cpp