dedekind::sets::Term< K > Struct Template Reference

A term built at run time, the grammar with its shape a value; defined after the binding below. More...

Collaboration diagram for dedekind::sets::Term< K >:

Classes
struct	SubstOne
	The one-slot substitution as a slot map. More...

Public Types
enum class	Kind { Proj , Const , Bin , Cond }

Public Member Functions
constexpr Term	subst (unsigned variable, const Term &with) const
	The term with the variable variable replaced by with: the substitution a structural arrow's image is (π ↦ π - 1 for the successor's).
template<typename F>
constexpr Term	map_slots (const F &f) const
	Every slot replaced at once by the term f gives it: a simultaneous substitution, so a renaming (a product's shift, a permutation) never captures.

Static Public Member Functions
static constexpr Term	proj (unsigned slot)
	π (slot 0), π_1, π_2.
static constexpr Term	constant (K k)
	A constant.
static constexpr Term	cond (Pred< K > q, Term a, Term b)
	McCarthy's conditional: a where q holds, else b; its body is instantiated where it is used, after Pred is complete.
static constexpr Term	bin (Arith op, Term x, Term y)
	x op y.

Public Attributes
Kind	kind {Kind::Const}
unsigned	slot {}
K	value {}
Arith	op {}
std::shared_ptr< const Term >	a
std::shared_ptr< const Term >	b
std::shared_ptr< const Pred< K > >	p

Detailed Description

template<typename K>
struct dedekind::sets::Term< K >

A term built at run time, the grammar with its shape a value; defined after the binding below.

A term built at run time: the grammar of IsTerm with its shape a value and its constants of type K, which meets the carrier through carrier_cast when the term is bound; McCarthy's conditional cond(p, a, b) chooses a branch by a predicate. Its legs are shared, so a term is cheap to copy and to combine. A division by the constant 0 is refused when the term is built, as for the typed grammar.

Template Parameters

K	the constants' type.

Member Function Documentation

bin()

template<typename K>

constexpr Term dedekind::sets::Term< K >::bin ( Arith op, Term< K > x, Term< K > y )

inlinestaticconstexpr

x op y.

Exceptions

std::domain_error

on a division by the constant 0.

cond()

template<typename K>

constexpr Term dedekind::sets::Term< K >::cond ( Pred< K > q, Term< K > a, Term< K > b )

inlinestaticconstexpr

McCarthy's conditional: a where q holds, else b; its body is instantiated where it is used, after Pred is complete.

Parameters

q	the predicate.
a,b	the branches.

map_slots()

template<typename K>

template<typename F>

Term dedekind::sets::Term< K >::map_slots ( const F & f ) const

inlineconstexpr

Every slot replaced at once by the term f gives it: a simultaneous substitution, so a renaming (a product's shift, a permutation) never captures.

Parameters

f	a slot to its replacement.

subst()

template<typename K>

Term dedekind::sets::Term< K >::subst ( unsigned variable, const Term< K > & with ) const

inlineconstexpr

The term with the variable variable replaced by with: the substitution a structural arrow's image is (π ↦ π - 1 for the successor's).

Parameters

variable	the slot.
with	its replacement.

Returns

the substituted term.

---

The documentation for this struct was generated from the following file:

• src/main/modules/dedekind/sets/terms.cppm