Trait Substitution

pub trait Substitution<'a>
where
    Self: Shiftable<'a>,
{
    type Error: From<<<Self as Shiftable<'a>>::Inner as Substitution<'a>>::Error>;

    // Required methods
    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Self::Error>;
    fn subst_evar(
        &self,
        o: u32,
        i: u32,
    ) -> Result<Option<Defined<'a>>, Self::Error>;
    fn subst_uvar(
        &self,
        o: u32,
        i: u32,
    ) -> Result<Option<Defined<'a>>, Self::Error>;

    // Provided methods
    fn record_fields(
        &self,
        rfs: &[RecordField<'a>],
    ) -> Result<Vec<RecordField<'a>>, Self::Error> { ... }
    fn variant_cases(
        &self,
        vcs: &[VariantCase<'a>],
    ) -> Result<Vec<VariantCase<'a>>, Self::Error> { ... }
    fn value_option(
        &self,
        vt: &Option<Value<'a>>,
    ) -> Result<Option<Value<'a>>, Self::Error> { ... }
    fn value(&self, vt: &Value<'a>) -> Result<Value<'a>, Self::Error> { ... }
    fn param(&self, pt: &Param<'a>) -> Result<Param<'a>, Self::Error> { ... }
    fn params(
        &self,
        pts: &Vec<Param<'a>>,
    ) -> Result<Vec<Param<'a>>, Self::Error> { ... }
    fn result(&self, rt: &Result<'a>) -> Result<Result<'a>, Self::Error> { ... }
    fn func(&self, ft: &Func<'a>) -> Result<Func<'a>, Self::Error> { ... }
    fn var(&self, tv: &Tyvar) -> Result<Option<Defined<'a>>, Self::Error> { ... }
    fn handleable(&self, h: &Handleable) -> Result<Defined<'a>, Self::Error> { ... }
    fn handleable_(&self, h: &Handleable) -> Result<Handleable, Self::Error> { ... }
    fn defined(&self, dt: &Defined<'a>) -> Result<Defined<'a>, Self::Error> { ... }
    fn type_bound(
        &self,
        tb: &TypeBound<'a>,
    ) -> Result<TypeBound<'a>, Self::Error> { ... }
    fn bounded_tyvar(
        &self,
        btv: &BoundedTyvar<'a>,
    ) -> Result<BoundedTyvar<'a>, Self::Error> { ... }
    fn extern_desc(
        &self,
        ed: &ExternDesc<'a>,
    ) -> Result<ExternDesc<'a>, Self::Error> { ... }
    fn extern_decl(
        &self,
        ed: &ExternDecl<'a>,
    ) -> Result<ExternDecl<'a>, Self::Error> { ... }
    fn instance(&self, it: &Instance<'a>) -> Result<Instance<'a>, Self::Error> { ... }
    fn qualified_instance(
        &self,
        qit: &QualifiedInstance<'a>,
    ) -> Result<QualifiedInstance<'a>, Self::Error> { ... }
    fn component(
        &self,
        ct: &Component<'a>,
    ) -> Result<Component<'a>, Self::Error> { ... }
}

A substitution

This trait can be implemented by specific structures that have specific substitution behavior, which only need to define how the act on bound/existential/universal variables. The implemented methods on the trait will then allow applying that substitution in a capture-avoiding manner to any relevant term.

The Shiftable bound is required because the implementation of substitution for components and instances needs to be able to shift the substitution in order to make substitution capture-avoiding.

Required Associated Types

type Error: From<<<Self as Shiftable<'a>>::Inner as Substitution<'a>>::Error>

Some, but not all, substitutions are fallible (i.e. may reveal latent misbehaviour in the type they are being applied to), so any given Substitution can provide its own Substitution::Error type.

An infallible substitution can use Void to reflect the fact that error is impossible, and callers can use Unvoidable::not_void to eliminate the impossible case of the result neatly.

Required Methods

fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Self::Error>

Any substitution should define whether a given bound variable should be substituted, and if so with what.

fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error>

Any substitution should define whether a given existential variable should be substituted, and if so with what.

fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error>

Any substitution should define whether a given universal variable should be substituted, and if so with what.

Provided Methods

fn record_fields( &self, rfs: &[RecordField<'a>], ) -> Result<Vec<RecordField<'a>>, Self::Error>

fn variant_cases( &self, vcs: &[VariantCase<'a>], ) -> Result<Vec<VariantCase<'a>>, Self::Error>

fn value_option( &self, vt: &Option<Value<'a>>, ) -> Result<Option<Value<'a>>, Self::Error>

fn value(&self, vt: &Value<'a>) -> Result<Value<'a>, Self::Error>

fn param(&self, pt: &Param<'a>) -> Result<Param<'a>, Self::Error>

fn params(&self, pts: &Vec<Param<'a>>) -> Result<Vec<Param<'a>>, Self::Error>

fn result(&self, rt: &Result<'a>) -> Result<Result<'a>, Self::Error>

fn func(&self, ft: &Func<'a>) -> Result<Func<'a>, Self::Error>

fn var(&self, tv: &Tyvar) -> Result<Option<Defined<'a>>, Self::Error>

fn handleable(&self, h: &Handleable) -> Result<Defined<'a>, Self::Error>

fn handleable_(&self, h: &Handleable) -> Result<Handleable, Self::Error>

fn defined(&self, dt: &Defined<'a>) -> Result<Defined<'a>, Self::Error>

fn type_bound(&self, tb: &TypeBound<'a>) -> Result<TypeBound<'a>, Self::Error>

fn bounded_tyvar( &self, btv: &BoundedTyvar<'a>, ) -> Result<BoundedTyvar<'a>, Self::Error>

fn extern_desc( &self, ed: &ExternDesc<'a>, ) -> Result<ExternDesc<'a>, Self::Error>

fn extern_decl( &self, ed: &ExternDecl<'a>, ) -> Result<ExternDecl<'a>, Self::Error>

fn instance(&self, it: &Instance<'a>) -> Result<Instance<'a>, Self::Error>

fn qualified_instance( &self, qit: &QualifiedInstance<'a>, ) -> Result<QualifiedInstance<'a>, Self::Error>

fn component(&self, ct: &Component<'a>) -> Result<Component<'a>, Self::Error>

Implementors

impl<'a> Substitution<'a> for Closing

type Error = ClosingError

impl<'a> Substitution<'a> for Opening

type Error = Void

impl<'a, 'b, A: ?Sized + Substitution<'a>> Substitution<'a> for Shifted<'b, A>

type Error = <A as Substitution<'a>>::Error

impl<'c, 'p, 'a> Substitution<'a> for Innerize<'c, 'p, 'a>

type Error = InnerizeError