Trait oxidd_core::util::Substitution

pub trait Substitution {
    type Var;
    type Replacement;

    // Required methods
    fn id(&self) -> u32;
    fn pairs(
        &self,
    ) -> impl ExactSizeIterator<Item = (Self::Var, Self::Replacement)>;

    // Provided method
    fn map<V, R, F>(&self, f: F) -> MapSubst<'_, Self, F>
       where F: Fn((Self::Var, Self::Replacement)) -> (V, R) { ... }
}

Substitution mapping variables to replacement functions

The intent behind substitution structs is to optimize the case where the same substitution is applied multiple times. We would like to re-use apply cache entries across these operations, and therefore, we need a compact identifier for the substitution (provided by Self::id() here).

To create a substitution, you’ll probably want to use Subst::new().

Required Associated Types

type Var

Variable type

type Replacement

Replacement type

Required Methods

fn id(&self) -> u32

Get the ID of this substitution

This unique identifier may safely be used as part of a cache key, i.e., two different substitutions to be used with one manager must not have the same ID. (That two equal substitutions have the same ID would be ideal but is not required for correctness.)

fn pairs(&self) -> impl ExactSizeIterator<Item = (Self::Var, Self::Replacement)>

Iterate over pairs of variable and replacement

Provided Methods

fn map<V, R, F>(&self, f: F) -> MapSubst<'_, Self, F>

where F: Fn((Self::Var, Self::Replacement)) -> (V, R),

Map the substitution, e.g., to use different variable and replacement types

f should be injective with respect to variables (the first component), i.e., two different variables should not be mapped to one. This is required to preserve that the substitution is a mapping from variables to replacement functions.

Object Safety

This trait is not object safe.

Implementations on Foreign Types

impl<T: Substitution> Substitution for &T

type Var = <T as Substitution>::Var

type Replacement = <T as Substitution>::Replacement

fn id(&self) -> u32

fn pairs(&self) -> impl ExactSizeIterator<Item = (Self::Var, Self::Replacement)>

Implementors

impl<'a, F> Substitution for Subst<'a, F>

type Var = &'a F

type Replacement = &'a F

impl<V, R, S: Substitution + ?Sized, F: Fn((S::Var, S::Replacement)) -> (V, R)> Substitution for MapSubst<'_, S, F>

type Var = V

type Replacement = R