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) -> UnordSet<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) -> UnordSet<BoundVar>
fn redundant_bvars(&self) -> UnordSet<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".