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 `i`th operand can be set to `def`.

const Def *	check () override
	After all Def::ops have ben 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	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

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

Rule *	set (Loc l)

const Rule *	set (Sym s) const

Rule *	set (Sym s)

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

Rule *	set (std::string s)

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

Rule *	set (Loc l, Sym s)

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

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

const Rule *	set (Dbg d) const

Rule *	set (Dbg d)

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

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 ben 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(), immutabilize(), 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 193 of file def.cpp.

References guard(), lhs(), rhs(), mim::World::rule(), type(), and mim::Def::world().

◆ 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(), immutabilize(), 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 123 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(), immutabilize(), 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 154 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(), immutabilize(), 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

Public Member Functions

Static Public Member Functions

Static Public Attributes

Private Member Functions

Friends

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ check() [1/2]

◆ check() [2/2]

◆ guard()

◆ immutabilize()

◆ is_in_rule()

◆ its_a_match()

◆ lhs()

◆ rebuild_()

◆ reduce()

◆ reduction_offset()

◆ replace()

◆ rhs()

◆ set() [1/2]

◆ set() [2/2]

◆ set_guard()

◆ set_lhs()

◆ set_rhs()

◆ stub()

◆ stub_()

◆ type()

◆ unset()

Friends And Related Symbol Documentation

◆ World

Member Data Documentation

◆ Node

◆ Num_Ops