Struct flux_middle::rty::Binder

pub struct Binder<T> {
    vars: List<BoundVariableKind>,
    value: T,
}

Fields

vars: List<BoundVariableKind>

value: T

Implementations

impl<T> Binder<T>

pub fn bind_with_vars(value: T, vars: BoundVariableKinds) -> Binder<T>

pub fn dummy(value: T) -> Binder<T>

pub fn bind_with_sorts(value: T, sorts: &[Sort]) -> Binder<T>

pub fn bind_with_sort(value: T, sort: Sort) -> Binder<T>

pub fn vars(&self) -> &List<BoundVariableKind>

pub fn as_ref(&self) -> Binder<&T>

pub fn skip_binder(self) -> T

pub fn skip_binder_ref(&self) -> &T

pub fn rebind<U>(&self, value: U) -> Binder<U>

pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Binder<U>

pub fn try_map<U, E>( self, f: impl FnOnce(T) -> Result<U, E>, ) -> Result<Binder<U>, E>

pub fn sort(&self) -> Sort

impl<T> Binder<T>

where T: TypeFoldable,

pub fn replace_bound_vars( &self, replace_region: impl FnMut(BoundRegion) -> Region, replace_expr: impl FnMut(&Sort, InferMode) -> Expr, ) -> T

pub fn replace_bound_refts(&self, exprs: &[Expr]) -> T

pub fn replace_bound_reft(&self, expr: &Expr) -> T

pub fn replace_bound_refts_with( &self, f: impl FnMut(&Sort, InferMode, BoundReftKind) -> Expr, ) -> T

impl Binder<TraitPredicate>

fn def_id(&self) -> DefId

fn self_ty(&self) -> Binder<SubsetTyCtor>

impl Binder<TraitRef>

pub fn def_id(&self) -> DefId

impl Binder<ExistentialTraitRef>

pub fn def_id(&self) -> DefId

impl Binder<ProjectionPredicate>

fn projection_def_id(&self) -> DefId

pub fn self_ty(&self) -> Binder<SubsetTyCtor>

impl Binder<Ty>

pub fn to_ty(&self) -> Ty

impl Binder<SubsetTy>

pub fn as_bty_skipping_binder(&self) -> &BaseTy

pub fn to_ty(&self) -> Ty

pub fn to_ty_ctor(&self) -> TyCtor

Trait Implementations

impl<T: Clone> Clone for Binder<T>

fn clone(&self) -> Binder<T>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<T: Pretty> Debug for Binder<T>

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

Formats the value using the given formatter.

impl<T, __D: TyDecoder> Decodable<__D> for Binder<T>

where T: Decodable<__D>,

fn decode(__decoder: &mut __D) -> Self

impl<T, __E: TyEncoder> Encodable<__E> for Binder<T>

where T: Encodable<__E>,

fn encode(&self, __encoder: &mut __E)

impl From<Binder<ClauseKind>> for Clause

fn from(kind: Binder<ClauseKind>) -> Self

Converts to this type from the input type.

impl<T: Hash> Hash for Binder<T>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<T: PartialEq> PartialEq for Binder<T>

fn eq(&self, other: &Binder<T>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Pretty for Binder<FnOutput>

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

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_>

impl<T> Pretty for Binder<T>

where T: Pretty,

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

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_>

impl SliceInternable for Binder<ExistentialPredicate>

fn storage() -> &'static InternStorage<[Self]>

impl<'tcx, V> ToRustc<'tcx> for Binder<V>

where V: ToRustc<'tcx, T: TypeVisitable<TyCtxt<'tcx>>>,

type T = Binder<TyCtxt<'tcx>, <V as ToRustc<'tcx>>::T>

fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T

impl<T> TypeFoldable for Binder<T>

where T: TypeFoldable,

fn try_fold_with<F: FallibleTypeFolder>( &self, folder: &mut F, ) -> Result<Self, F::Error>

fn fold_with<F: TypeFolder>(&self, folder: &mut F) -> Self

fn normalize_projections<'tcx>( &self, genv: GlobalEnv<'_, 'tcx>, infcx: &InferCtxt<'tcx>, callsite_def_id: DefId, ) -> QueryResult<Self>

fn normalize(&self, defns: &SpecFuncDefns) -> Self

Normalize expressions by applying beta reductions for tuples and lambda abstractions.

fn replace_holes( &self, f: impl FnMut(&[BoundVariableKinds], HoleKind) -> Expr, ) -> Self

Replaces all holes with the result of calling a closure. The closure takes a list with all the layers of bound variables at the point the hole was found. Each layer corresponds to the list of bound variables at that level. The list is ordered from outermost to innermost binder, i.e., the last element is the binder closest to the hole.

fn with_holes(&self) -> Self

Remove all refinements and turn each underlying BaseTy into a TyKind::Exists with a TyKind::Constr and a hole. For example, Vec<{v. i32[v] | v > 0}>[n] becomes {n. Vec<{v. i32[v] | *}>[n] | *}.

fn replace_evars(&self, evars: &EVarSol) -> Self

fn shift_in_escaping(&self, amount: u32) -> Self

fn shift_out_escaping(&self, amount: u32) -> Self

fn erase_regions(&self) -> Self

impl<T> TypeSuperFoldable for Binder<T>

where T: TypeFoldable,

fn try_super_fold_with<F: FallibleTypeFolder>( &self, folder: &mut F, ) -> Result<Self, F::Error>

fn super_fold_with<F: TypeFolder>(&self, folder: &mut F) -> Self

impl<T> TypeSuperVisitable for Binder<T>

where T: TypeVisitable,

fn super_visit_with<V: TypeVisitor>( &self, visitor: &mut V, ) -> ControlFlow<V::BreakTy>

impl<T> TypeVisitable for Binder<T>

where T: TypeVisitable,

fn visit_with<V: TypeVisitor>(&self, visitor: &mut V) -> ControlFlow<V::BreakTy>

fn has_escaping_bvars(&self) -> bool

fn has_escaping_bvars_at_or_above(&self, binder: DebruijnIndex) -> bool

Returns true if self has any late-bound vars that are either bound by binder or bound by some binder outside of binder. If binder is ty::INNERMOST, this indicates whether there are any late-bound vars that appear free.

fn fvars(&self) -> FxHashSet<Name>

Returns the set of all free variables. For example, Vec<i32[n]>{v : v > m} returns {n, m}.

impl<T: Eq> Eq for Binder<T>

impl<T> StructuralPartialEq for Binder<T>