charon_lib/pretty/
formatter.rs

1use std::borrow::Cow;
2use std::fmt;
3use std::fmt::Display;
4
5use index_vec::Idx;
6
7use crate::ast::*;
8use crate::common::TAB_INCR;
9use crate::ids::Vector;
10use crate::pretty::FmtWithCtx;
11
12pub trait IntoFormatter {
13    type C: AstFormatter;
14    fn into_fmt(self) -> Self::C;
15}
16
17/// An [`AstFormatter`] contains the context required to pretty-print the ast. An ast type can then
18/// be pretty-printed using the [`FmtWithCtx`] trait.
19pub trait AstFormatter: Sized {
20    type Reborrow<'a>: AstFormatter + 'a
21    where
22        Self: 'a;
23
24    fn get_crate(&self) -> Option<&TranslatedCrate>;
25
26    fn set_generics<'a>(&'a self, generics: &'a GenericParams) -> Self::Reborrow<'a>;
27    fn set_locals<'a>(&'a self, locals: &'a Locals) -> Self::Reborrow<'a>;
28    fn push_binder<'a>(&'a self, new_params: Cow<'a, GenericParams>) -> Self::Reborrow<'a>;
29    fn push_bound_regions<'a>(
30        &'a self,
31        regions: &'a Vector<RegionId, RegionParam>,
32    ) -> Self::Reborrow<'a> {
33        self.push_binder(Cow::Owned(GenericParams {
34            regions: regions.clone(),
35            ..Default::default()
36        }))
37    }
38    /// Return the depth of binders we're under.
39    fn binder_depth(&self) -> usize;
40
41    fn increase_indent<'a>(&'a self) -> Self::Reborrow<'a>;
42    fn indent(&self) -> String;
43
44    fn format_local_id(&self, f: &mut fmt::Formatter<'_>, id: LocalId) -> fmt::Result;
45    fn format_bound_var<Id: Idx + Display, T>(
46        &self,
47        f: &mut fmt::Formatter<'_>,
48        var: DeBruijnVar<Id>,
49        var_prefix: &str,
50        fmt_var: impl Fn(&T) -> Option<String>,
51    ) -> fmt::Result
52    where
53        GenericParams: HasVectorOf<Id, Output = T>;
54
55    fn format_enum_variant(
56        &self,
57        f: &mut fmt::Formatter<'_>,
58        type_id: TypeDeclId,
59        variant_id: VariantId,
60    ) -> fmt::Result {
61        let variant = if let Some(translated) = self.get_crate()
62            && let Some(def) = translated.type_decls.get(type_id)
63            && let Some(variants) = def.kind.as_enum()
64        {
65            &variants.get(variant_id).unwrap().name
66        } else {
67            &variant_id.to_pretty_string()
68        };
69        write!(f, "{}::{variant}", type_id.with_ctx(self))
70    }
71
72    fn format_field_name(
73        &self,
74        f: &mut fmt::Formatter<'_>,
75        type_id: TypeDeclId,
76        opt_variant_id: Option<VariantId>,
77        field_id: FieldId,
78    ) -> fmt::Result {
79        let field_name = if let Some(translated) = self.get_crate()
80            && let Some(def) = translated.type_decls.get(type_id)
81        {
82            match (&def.kind, opt_variant_id) {
83                (TypeDeclKind::Enum(variants), Some(variant_id)) => {
84                    variants[variant_id].fields[field_id].name.as_ref()
85                }
86                (TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields), None) => {
87                    fields[field_id].name.as_ref()
88                }
89                _ => None,
90            }
91        } else {
92            None
93        };
94        if let Some(field_name) = field_name {
95            write!(f, "{field_name}")
96        } else {
97            write!(f, "{field_id}")
98        }
99    }
100}
101
102/// Context for formatting.
103#[derive(Default)]
104pub struct FmtCtx<'a> {
105    pub translated: Option<&'a TranslatedCrate>,
106    /// Generics form a stack, where each binder introduces a new level. For DeBruijn indices to
107    /// work, we keep the innermost parameters at the start of the vector.
108    pub generics: BindingStack<Cow<'a, GenericParams>>,
109    pub locals: Option<&'a Locals>,
110    pub indent_level: usize,
111}
112
113impl<'c> AstFormatter for FmtCtx<'c> {
114    type Reborrow<'a>
115        = FmtCtx<'a>
116    where
117        Self: 'a;
118
119    fn get_crate(&self) -> Option<&TranslatedCrate> {
120        self.translated
121    }
122
123    fn set_generics<'a>(&'a self, generics: &'a GenericParams) -> Self::Reborrow<'a> {
124        FmtCtx {
125            generics: BindingStack::new(Cow::Borrowed(generics)),
126            ..self.reborrow()
127        }
128    }
129    fn set_locals<'a>(&'a self, locals: &'a Locals) -> Self::Reborrow<'a> {
130        FmtCtx {
131            locals: Some(locals),
132            ..self.reborrow()
133        }
134    }
135    fn push_binder<'a>(&'a self, new_params: Cow<'a, GenericParams>) -> Self::Reborrow<'a> {
136        let mut ret = self.reborrow();
137        ret.generics.push(new_params);
138        ret
139    }
140    fn binder_depth(&self) -> usize {
141        self.generics.len()
142    }
143
144    fn increase_indent<'a>(&'a self) -> Self::Reborrow<'a> {
145        FmtCtx {
146            indent_level: self.indent_level + 1,
147            ..self.reborrow()
148        }
149    }
150    fn indent(&self) -> String {
151        TAB_INCR.repeat(self.indent_level)
152    }
153
154    fn format_local_id(&self, f: &mut fmt::Formatter<'_>, id: LocalId) -> fmt::Result {
155        if let Some(locals) = &self.locals
156            && let Some(v) = locals.locals.get(id)
157        {
158            write!(f, "{v}")
159        } else {
160            write!(f, "{}", id.to_pretty_string())
161        }
162    }
163
164    fn format_bound_var<Id: Idx + Display, T>(
165        &self,
166        f: &mut fmt::Formatter<'_>,
167        var: DeBruijnVar<Id>,
168        var_prefix: &str,
169        fmt_var: impl Fn(&T) -> Option<String>,
170    ) -> fmt::Result
171    where
172        GenericParams: HasVectorOf<Id, Output = T>,
173    {
174        if self.generics.is_empty() {
175            return write!(f, "{var_prefix}{var}");
176        }
177        match self.generics.get_var::<_, GenericParams>(var) {
178            None => write!(f, "missing({var_prefix}{var})"),
179            Some(v) => match fmt_var(v) {
180                Some(name) => write!(f, "{name}"),
181                None => {
182                    write!(f, "{var_prefix}")?;
183                    let (dbid, varid) = self.generics.as_bound_var(var);
184                    let depth = self.generics.depth().index - dbid.index;
185                    if depth == 0 {
186                        write!(f, "{varid}")
187                    } else {
188                        write!(f, "{varid}_{depth}")
189                    }
190                }
191            },
192        }
193    }
194}
195
196impl<'a> FmtCtx<'a> {
197    pub fn new() -> Self {
198        FmtCtx::default()
199    }
200
201    pub fn get_item(&self, id: ItemId) -> Result<ItemRef<'_>, Option<&Name>> {
202        let Some(translated) = &self.translated else {
203            return Err(None);
204        };
205        translated
206            .get_item(id)
207            .ok_or_else(|| translated.item_short_name(id))
208    }
209
210    /// Print the whole definition.
211    pub fn format_decl_id(&self, id: impl Into<ItemId>) -> String {
212        let id = id.into();
213        match self.get_item(id) {
214            Ok(d) => d.to_string_with_ctx(self),
215            Err(opt_name) => {
216                let opt_name = opt_name
217                    .map(|n| format!(" ({})", n.with_ctx(self)))
218                    .unwrap_or_default();
219                format!("Missing decl: {id:?}{opt_name}")
220            }
221        }
222    }
223
224    fn reborrow<'b>(&'b self) -> FmtCtx<'b> {
225        FmtCtx {
226            translated: self.translated.as_deref(),
227            generics: self.generics.clone(),
228            locals: self.locals.as_deref(),
229            indent_level: self.indent_level,
230        }
231    }
232}
charon_lib/pretty/formatter.rs

charon_lib/pretty/
formatter.rs
