Struct Subst

pub struct Subst<T> { /* private fields */ }

Map from variables (usize) to T that can be efficiently restored to earlier states.

Implementations

impl<T> Subst<T>

pub fn get_dom_len(&self) -> usize

Return the number of assigned variables.

pub fn get_dom_max(&self) -> usize

Return the maximally assignable index.

pub fn set_dom_max(&mut self, dom_max: usize)

Permit the assignment of variables at least up to (excluding) the given index.

pub fn set_dom_len(&mut self, new_len: usize)

Omit the most recent variable bindings to keep only the given number of bindings.

pub fn insert(&mut self, v: usize, tm: T)

Assign a given variable to the given term.

Panic if the index exceeds the maximum domain.

pub fn get(&self, v: usize) -> Option<&T>

Obtain a variable binding.

Panic if the index exceeds the maximum domain.

impl<T: Copy> Subst<T>

pub fn fix(&self, x: T, f: impl Fn(T) -> Option<usize>) -> T

Repeatedly apply substitution to a value.

The function terminates as soon as either the given function returns no index or the substitution is not defined at the index.

Trait Implementations

impl<T> Default for Subst<T>

fn default() -> Self

Returns the “default value” for a type.

impl<T: Display> Display for Subst<T>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.