pub trait TypeVisitable: Sized {
// Required method
fn visit_with<V: TypeVisitor>(
&self,
visitor: &mut V,
) -> ControlFlow<V::BreakTy>;
// Provided methods
fn has_escaping_bvars(&self) -> bool { ... }
fn has_escaping_bvars_at_or_above(&self, binder: DebruijnIndex) -> bool { ... }
fn fvars(&self) -> FxHashSet<Name> { ... }
fn early_params(&self) -> FxHashSet<EarlyReftParam> { ... }
fn redundant_bvars(&self) -> FxHashSet<BoundVar> { ... }
}Required Methods§
fn visit_with<V: TypeVisitor>(&self, visitor: &mut V) -> ControlFlow<V::BreakTy>
Provided Methods§
fn has_escaping_bvars(&self) -> bool
Sourcefn has_escaping_bvars_at_or_above(&self, binder: DebruijnIndex) -> 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.
Sourcefn fvars(&self) -> FxHashSet<Name>
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>
Sourcefn redundant_bvars(&self) -> FxHashSet<BoundVar>
fn redundant_bvars(&self) -> FxHashSet<BoundVar>
Gives the indices of the provided bvars which:
- Only occur a single time.
- In their occurrence, are either
a. The direct argument in an index (e.g.
exists b0. usize[b0]) b. The direct argument of a constructor in an index (e.g.exists b0. Vec<usize>[{len: b0}])
This is to be used for “re-sugaring” existentials into surface syntax that doesn’t use existentials.
For 2b., we do need to be careful to ensure that if a constructor has multiple arguments, they all are redundant bvars, e.g. as in
exists b0, b1. RMat<f32>[{rows: b0, cols: b1}]which may be rewritten as RMat<f32>,
versus the (unlikely) edge case
exists b0. RMat<f32>[{rows: b0, cols: b0}]for which the existential is now necessary.
NOTE: this only applies to refinement bvars.
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.