Trait SubstWith 

pub trait SubstWith<'db, Term> {
    type Output;

    // Required methods
    fn identity(&self) -> Self::Output;
    fn subst_with<'subst>(
        &'subst self,
        db: &'db dyn Db,
        bound_vars: &mut Vec<SymVariable<'db>>,
        subst_fns: &mut SubstitutionFns<'_, 'db, Term>,
    ) -> Self::Output;
}

Core substitution operation: produce a version of this type with variables replaced with instances of Term.

Most types implement this for only a single Term, but not all (see the macro identity_subst).

Required Associated Types

type Output

The type of the resulting term; typically Self but not always.

Required Methods

fn identity(&self) -> Self::Output

Reproduce self with no edits.

fn subst_with<'subst>( &'subst self, db: &'db dyn Db, bound_vars: &mut Vec<SymVariable<'db>>, subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

Replace self applying the changes from subst_fns.

Parameters

• db, the database
• start_binder, the index of the binder we started from. This always begins as SymBinderIndex::INNERMOST but gets incremented as we traverse binders.
• subst_fns, a struct containing callbacks for substitution

Implementations on Foreign Types

impl<'db, O, E, Term> SubstWith<'db, Term> for Result<O, E>

where O: SubstWith<'db, Term>, E: SubstWith<'db, Term>,

type Output = Result<<O as SubstWith<'db, Term>>::Output, <E as SubstWith<'db, Term>>::Output>

fn identity(&self) -> Self::Output

fn subst_with<'subst>( &'subst self, db: &'db dyn Db, bound_vars: &mut Vec<SymVariable<'db>>, subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

impl<'db, T, Term> SubstWith<'db, Term> for &T

where T: SubstWith<'db, Term>,

type Output = <T as SubstWith<'db, Term>>::Output

fn subst_with<'subst>( &'subst self, db: &'db dyn Db, bound_vars: &mut Vec<SymVariable<'db>>, subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

fn identity(&self) -> Self::Output

impl<'db, T: Subst<'db>> SubstWith<'db, <T as Subst<'db>>::GenericTerm> for Vec<T>

type Output = Vec<<T as SubstWith<'db, <T as Subst<'db>>::GenericTerm>>::Output>

fn identity(&self) -> Self::Output

fn subst_with<'subst>( &'subst self, db: &'db dyn Db, bound_vars: &mut Vec<SymVariable<'db>>, subst_fns: &mut SubstitutionFns<'_, 'db, T::GenericTerm>, ) -> Self::Output

impl<'db, Term> SubstWith<'db, Term> for PermissionOp

type Output = PermissionOp

fn identity(&self) -> Self::Output

fn subst_with<'subst>( &self, _db: &'db dyn Db, _bound_vars: &mut Vec<SymVariable<'db>>, _subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

impl<'db, Term> SubstWith<'db, Term> for Never

type Output = Never

fn identity(&self) -> Self::Output

fn subst_with<'subst>( &'subst self, _db: &'db dyn Db, _bound_vars: &mut Vec<SymVariable<'db>>, _subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

impl<'db, Term> SubstWith<'db, Term> for ()

type Output = ()

fn identity(&self) -> Self::Output

fn subst_with<'subst>( &self, _db: &'db dyn Db, _bound_vars: &mut Vec<SymVariable<'db>>, _subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

impl<'db, Term> SubstWith<'db, Term> for Reported

type Output = Reported

fn identity(&self) -> Self::Output

fn subst_with<'subst>( &self, _db: &'db dyn Db, _bound_vars: &mut Vec<SymVariable<'db>>, _subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

impl<'db, Term> SubstWith<'db, Term> for Span<'db>

type Output = Span<'db>

fn identity(&self) -> Self::Output

fn subst_with<'subst>( &self, _db: &'db dyn Db, _bound_vars: &mut Vec<SymVariable<'db>>, _subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

impl<'db, Term, T> SubstWith<'db, Term> for Option<T>

where T: SubstWith<'db, Term>,

type Output = Option<<T as SubstWith<'db, Term>>::Output>

fn identity(&self) -> Self::Output

fn subst_with<'subst>( &'subst self, db: &'db dyn Db, bound_vars: &mut Vec<SymVariable<'db>>, subst_fns: &mut SubstitutionFns<'_, 'db, Term>, ) -> Self::Output

Implementors

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymExprKind<'db>

type Output = SymExprKind<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymPlaceExprKind<'db>

type Output = SymPlaceExprKind<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymGenericTerm<'db>

type Output = SymGenericTerm<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymExpr<'db>

type Output = SymExpr<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymMatchArm<'db>

type Output = SymMatchArm<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymPlaceExpr<'db>

type Output = SymPlaceExpr<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymFunctionSignature<'db>

type Output = SymFunctionSignature<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymInputOutput<'db>

type Output = SymInputOutput<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymWhereClause<'db>

type Output = SymWhereClause<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymPerm<'db>

type Output = SymPerm<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymPlace<'db>

type Output = SymPlace<'db>

impl<'db> SubstWith<'db, SymGenericTerm<'db>> for SymTy<'db>

type Output = SymTy<'db>

impl<'db, T, Term> SubstWith<'db, Term> for NeverBinder<T>

type Output = NeverBinder<T>

impl<'db, T: BoundTerm<'db>> SubstWith<'db, <T as Subst<'db>>::GenericTerm> for Binder<'db, T>

type Output = Binder<'db, T>

impl<'db, Term> SubstWith<'db, Term> for SymBinaryOp

type Output = SymBinaryOp

impl<'db, Term> SubstWith<'db, Term> for SymLiteral

type Output = SymLiteral

impl<'db, Term> SubstWith<'db, Term> for SymWhereClauseKind

type Output = SymWhereClauseKind

impl<'db, Term> SubstWith<'db, Term> for SymGenericKind

type Output = SymGenericKind

impl<'db, Term> SubstWith<'db, Term> for SymTyName<'db>

type Output = SymTyName<'db>

impl<'db, Term> SubstWith<'db, Term> for SymField<'db>

type Output = SymField<'db>

impl<'db, Term> SubstWith<'db, Term> for SymByteLiteral<'db>

type Output = SymByteLiteral<'db>

impl<'db, Term> SubstWith<'db, Term> for SymFunction<'db>

type Output = SymFunction<'db>