Struct move_model::ty::Substitution

pub struct Substitution { /* private fields */ }

A type substitution.

Implementations

impl Substitution

pub fn new() -> Self

Creates a new substitution.

pub fn bind(&mut self, var: u16, ty: Type)

Binds the type variables.

pub fn specialize(&self, t: &Type) -> Type

Specializes the type, substituting all variables bound in this substitution.

pub fn get_substitution(&self, var: u16, shallow: bool) -> Option<Type>

Return either a shallow or deep substitution of the type variable.

If deep substitution is requested, follow down the substitution chain until either

• Some(ty) when the final type is not a type variable or
• None when the final type variable does not have a substitution

pub fn unify(
    &mut self,
    variance: Variance,
    t1: &Type,
    t2: &Type
) -> Result<Type, TypeUnificationError>

Unify two types, returning the unified type.

This currently implements the following notion of type compatibility:

• 1. References are dropped (i.e. &T and T are compatible)
• 2. All integer types are compatible if co-variance is allowed.
• 3. With the joint effect of 1) and 2), if (P, Q) is compatible under co-variance, (&P, Q), (P, &Q), and (&P, &Q) are all compatible under co-variance.
• 4. If in two tuples (P1, P2, …, Pn) and (Q1, Q2, …, Qn), all (Pi, Qi) pairs are compatible under co-variance, then the two tuples are compatible under co-variance.

The substitution will be refined by variable assignments as needed to perform unification. If unification fails, the substitution will be in some intermediate state; to implement transactional unification, the substitution must be cloned before calling this.

Trait Implementations

impl Clone for Substitution

fn clone(&self) -> Substitution

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Substitution

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

Formats the value using the given formatter.

impl Default for Substitution

fn default() -> Self

Returns the “default value” for a type.