Struct Hoister

pub struct Hoister<D> {
    delegate: D,
    in_boxes: bool,
    in_downcast: bool,
    in_mut_refs: bool,
    in_shr_refs: bool,
    in_strg_refs: bool,
    in_tuples: bool,
    existentials: bool,
}

The Hoister struct is responsible for hoisting existentials and predicates out of a type. It can be configured to stop hoisting at specific type constructors.

The struct is generic on a delegate D because we use it to do local hoisting, keeping variables bound with a Binder, and for freeing variables into the refinement context.

Fields

delegate: D

in_boxes: bool

in_downcast: bool

in_mut_refs: bool

in_shr_refs: bool

in_strg_refs: bool

in_tuples: bool

existentials: bool

Implementations

impl<D> Hoister<D>

pub fn with_delegate(delegate: D) -> Self

pub fn hoist_inside_shr_refs(self, shr_refs: bool) -> Self

pub fn hoist_inside_mut_refs(self, mut_refs: bool) -> Self

pub fn hoist_inside_strg_refs(self, strg_refs: bool) -> Self

pub fn hoist_inside_tuples(self, tuples: bool) -> Self

pub fn hoist_inside_boxes(self, boxes: bool) -> Self

pub fn hoist_inside_downcast(self, downcast: bool) -> Self

pub fn hoist_existentials(self, exists: bool) -> Self

pub fn transparent(self) -> Self

pub fn shallow(self) -> Self

impl<D: HoisterDelegate> Hoister<D>

pub fn hoist(&mut self, ty: &Ty) -> Ty

Trait Implementations

impl<D: HoisterDelegate> TypeFolder for Hoister<D>

fn fold_ty(&mut self, ty: &Ty) -> Ty

fn fold_bty(&mut self, bty: &BaseTy) -> BaseTy

fn fold_binder<T: TypeFoldable>(&mut self, t: &Binder<T>) -> Binder<T>

fn fold_sort(&mut self, sort: &Sort) -> Sort

fn fold_subset_ty(&mut self, constr: &SubsetTy) -> SubsetTy

fn fold_region(&mut self, re: &Region) -> Region

fn fold_const(&mut self, c: &Const) -> Const

fn fold_expr(&mut self, expr: &Expr) -> Expr