Struct chalk_solve::display::state::InternalWriterState
source · pub(super) struct InternalWriterState<'a, I: Interner> {
persistent_state: WriterState<I, dyn RustIrDatabase<I> + 'a, &'a dyn RustIrDatabase<I>>,
indent_level: usize,
debrujin_indices_deep: u32,
remapping: Rc<BTreeMap<InvertedBoundVar, InvertedBoundVar>>,
self_mapping: Option<InvertedBoundVar>,
}
Expand description
Writer state for a single write call, persistent only as long as necessary to write a single item.
Stores things necessary for .
Fields§
§persistent_state: WriterState<I, dyn RustIrDatabase<I> + 'a, &'a dyn RustIrDatabase<I>>
§indent_level: usize
§debrujin_indices_deep: u32
§remapping: Rc<BTreeMap<InvertedBoundVar, InvertedBoundVar>>
§self_mapping: Option<InvertedBoundVar>
Implementations§
source§impl<'a, I: Interner> InternalWriterState<'a, I>
impl<'a, I: Interner> InternalWriterState<'a, I>
pub fn new<DB, P>(persistent_state: &'a WriterState<I, DB, P>) -> Selfwhere
DB: RustIrDatabase<I>,
P: Borrow<DB>,
pub(super) fn db(&self) -> &dyn RustIrDatabase<I>
pub(super) fn add_indent(&self) -> Self
pub(super) fn indent(&self) -> impl Display
pub(super) fn alias_for_adt_id_name( &self, id: I::InternedAdtId, name: String, ) -> impl Display
pub(super) fn alias_for_id_name( &self, id: I::DefId, name: String, ) -> impl Display
sourcepub(super) fn add_debrujin_index(&self, self_binding: Option<usize>) -> Self
pub(super) fn add_debrujin_index(&self, self_binding: Option<usize>) -> Self
Adds a level of debrujin index, and possibly a “Self” parameter.
This should be called whenever recursing into the value within a
Binders
.
If self_binding
is Some
, then it will introduce a new variable named
Self
with the within-debrujin index given within and the innermost
debrujian index after increasing debrujin index.
sourcepub(super) fn add_parameter_mapping(
&self,
lowered_vars: impl Iterator<Item = InvertedBoundVar>,
original_vars: impl Iterator<Item = InvertedBoundVar>,
) -> Self
pub(super) fn add_parameter_mapping( &self, lowered_vars: impl Iterator<Item = InvertedBoundVar>, original_vars: impl Iterator<Item = InvertedBoundVar>, ) -> Self
Adds parameter remapping.
Each of the parameters in lowered_vars
will be mapped to its
corresponding variable in original_vars
when printed through the
InternalWriterState
returned from this method.
lowered_vars
and original_vars
must have the same length.
sourcepub(super) fn invert_debrujin_idx(
&self,
debrujin_idx: u32,
index: usize,
) -> InvertedBoundVar
pub(super) fn invert_debrujin_idx( &self, debrujin_idx: u32, index: usize, ) -> InvertedBoundVar
Inverts the debrujin index so as to create a canonical name we can anywhere for each bound variable.
See InvertedBoundVar
.
pub(super) fn apply_mappings(&self, b: InvertedBoundVar) -> impl Display
pub(super) fn indices_for_bound_var(&self, b: &BoundVar) -> InvertedBoundVar
pub(super) fn indices_for_introduced_bound_var( &self, idx: usize, ) -> InvertedBoundVar
pub(super) fn display_bound_var(&self, b: &BoundVar) -> impl Display
pub(super) fn name_for_introduced_bound_var(&self, idx: usize) -> impl Display
pub(super) fn binder_var_indices<'b>( &'b self, binders: &'b VariableKinds<I>, ) -> impl Iterator<Item = InvertedBoundVar> + 'b
pub(super) fn binder_var_display<'b>( &'b self, binders: &'b VariableKinds<I>, ) -> impl Iterator<Item = String> + 'b
Trait Implementations§
Auto Trait Implementations§
impl<'a, I> Freeze for InternalWriterState<'a, I>
impl<'a, I> !RefUnwindSafe for InternalWriterState<'a, I>
impl<'a, I> !Send for InternalWriterState<'a, I>
impl<'a, I> !Sync for InternalWriterState<'a, I>
impl<'a, I> !Unpin for InternalWriterState<'a, I>
impl<'a, I> !UnwindSafe for InternalWriterState<'a, I>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
source§impl<T> Cast for T
impl<T> Cast for T
source§fn cast<U>(self, interner: <U as HasInterner>::Interner) -> Uwhere
Self: CastTo<U>,
U: HasInterner,
fn cast<U>(self, interner: <U as HasInterner>::Interner) -> Uwhere
Self: CastTo<U>,
U: HasInterner,
U
using CastTo
.source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
source§default unsafe fn clone_to_uninit(&self, dst: *mut T)
default unsafe fn clone_to_uninit(&self, dst: *mut T)
clone_to_uninit
)