Enum Opaqueness 

pub enum Opaqueness<T> {
    Opaque,
    Transparent(T),
}

Option-like enum to explicitly mark that we don’t have information about an ADT because it was annotated with #[flux::opaque]. Note that only structs can be marked as opaque.

Variants

Opaque

Transparent(T)

Implementations

impl<T> Opaqueness<T>

pub fn map<S>(self, f: impl FnOnce(T) -> S) -> Opaqueness<S>

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

pub fn as_deref(&self) -> Opaqueness<&T::Target>

where T: Deref,

pub fn ok_or_else<E>(self, err: impl FnOnce() -> E) -> Result<T, E>

pub fn expect(self, msg: &str) -> T

pub fn ok_or_query_err(self, struct_id: DefId) -> Result<T, QueryErr>

impl<T, E> Opaqueness<Result<T, E>>

pub fn transpose(self) -> Result<Opaqueness<T>, E>

Trait Implementations

impl<T: Clone> Clone for Opaqueness<T>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T: Debug> Debug for Opaqueness<T>

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

Formats the value using the given formatter.

impl<'tcx, T, __D: TyDecoder<'tcx>> Decodable<__D> for Opaqueness<T>

where T: Decodable<__D>,

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

impl<'tcx, T, __E: TyEncoder<'tcx>> Encodable<__E> for Opaqueness<T>

where T: Encodable<__E>,

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

impl<T> TypeFoldable for Opaqueness<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(&self, genv: GlobalEnv<'_, '_>) -> 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, f: &mut impl FnMut(EVid) -> Option<Expr>, ) -> Result<Self, EVid>

fn shift_horizontally(&self, amount: usize) -> Self

Shift the BoundVar of all the the variables at index INNERMOST “horizontally” to the right by the specified amount.

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

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

fn erase_regions(&self) -> Self

impl<T> TypeVisitable for Opaqueness<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}.

fn early_params(&self) -> FxHashSet<EarlyReftParam>

fn redundant_bvars(&self) -> FxHashSet<BoundVar>

Gives the indices of the provided bvars which: