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::IndexVec;
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 no_generics<'a>(&'a self) -> Self::Reborrow<'a>;
27    fn set_generics<'a>(&'a self, generics: &'a GenericParams) -> Self::Reborrow<'a>;
28    fn set_locals<'a>(&'a self, locals: &'a Locals) -> Self::Reborrow<'a>;
29    fn push_binder<'a>(&'a self, new_params: Cow<'a, GenericParams>) -> Self::Reborrow<'a>;
30    fn push_bound_regions<'a>(
31        &'a self,
32        regions: &'a IndexVec<RegionId, RegionParam>,
33    ) -> Self::Reborrow<'a> {
34        self.push_binder(Cow::Owned(GenericParams {
35            regions: regions.clone(),
36            ..Default::default()
37        }))
38    }
39    /// Return the depth of binders we're under.
40    fn binder_depth(&self) -> usize;
41
42    fn increase_indent<'a>(&'a self) -> Self::Reborrow<'a>;
43    fn indent(&self) -> String;
44
45    fn format_local_id(&self, f: &mut fmt::Formatter<'_>, id: LocalId) -> fmt::Result;
46    fn format_bound_var<Id: Idx + Display, T>(
47        &self,
48        f: &mut fmt::Formatter<'_>,
49        var: DeBruijnVar<Id>,
50        var_prefix: &str,
51        fmt_var: impl Fn(&T) -> Option<String>,
52    ) -> fmt::Result
53    where
54        GenericParams: HasIdxVecOf<Id, Output = T>;
55
56    fn format_method_name(
57        &self,
58        f: &mut fmt::Formatter<'_>,
59        trait_id: TraitDeclId,
60        method_id: TraitMethodId,
61    ) -> fmt::Result {
62        if let Some(translated) = self.get_crate()
63            && let Some(names) = translated.assoc_item_names.get(trait_id)
64            && let Some(name) = names.methods.get(method_id).copied()
65        {
66            write!(f, "{name}")
67        } else {
68            write!(f, "{}", &method_id.to_pretty_string())
69        }
70    }
71    fn format_assoc_type_name(
72        &self,
73        f: &mut fmt::Formatter<'_>,
74        trait_id: TraitDeclId,
75        type_id: AssocTypeId,
76    ) -> fmt::Result {
77        if let Some(translated) = self.get_crate()
78            && let Some(names) = translated.assoc_item_names.get(trait_id)
79            && let Some(name) = names.types.get(type_id).copied()
80        {
81            write!(f, "{name}")
82        } else {
83            write!(f, "{}", &type_id.to_pretty_string())
84        }
85    }
86    fn format_assoc_const_name(
87        &self,
88        f: &mut fmt::Formatter<'_>,
89        trait_id: TraitDeclId,
90        const_id: AssocConstId,
91    ) -> fmt::Result {
92        if let Some(translated) = self.get_crate()
93            && let Some(names) = translated.assoc_item_names.get(trait_id)
94            && let Some(name) = names.consts.get(const_id).copied()
95        {
96            write!(f, "{name}")
97        } else {
98            write!(f, "{}", &const_id.to_pretty_string())
99        }
100    }
101    fn format_enum_variant_name(
102        &self,
103        f: &mut fmt::Formatter<'_>,
104        type_id: TypeDeclId,
105        variant_id: VariantId,
106    ) -> fmt::Result {
107        let variant = if let Some(translated) = self.get_crate()
108            && let Some(def) = translated.type_decls.get(type_id)
109            && let Some(variants) = def.kind.as_enum()
110        {
111            &variants.get(variant_id).unwrap().name
112        } else {
113            &variant_id.to_pretty_string()
114        };
115        write!(f, "{variant}")
116    }
117    fn format_enum_variant(
118        &self,
119        f: &mut fmt::Formatter<'_>,
120        type_id: TypeDeclId,
121        variant_id: VariantId,
122    ) -> fmt::Result {
123        write!(f, "{}::", type_id.with_ctx(self))?;
124        self.format_enum_variant_name(f, type_id, variant_id)?;
125        Ok(())
126    }
127
128    fn format_field_name(
129        &self,
130        f: &mut fmt::Formatter<'_>,
131        type_id: TypeDeclId,
132        opt_variant_id: Option<VariantId>,
133        field_id: FieldId,
134    ) -> fmt::Result {
135        let field_name = if let Some(translated) = self.get_crate()
136            && let Some(def) = translated.type_decls.get(type_id)
137        {
138            match (&def.kind, opt_variant_id) {
139                (TypeDeclKind::Enum(variants), Some(variant_id)) => {
140                    variants[variant_id].fields[field_id].name.as_ref()
141                }
142                (TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields), None) => {
143                    fields[field_id].name.as_ref()
144                }
145                _ => None,
146            }
147        } else {
148            None
149        };
150        if let Some(field_name) = field_name {
151            write!(f, "{field_name}")
152        } else {
153            write!(f, "{field_id}")
154        }
155    }
156}
157
158/// Context for formatting.
159#[derive(Default)]
160pub struct FmtCtx<'a> {
161    pub translated: Option<&'a TranslatedCrate>,
162    /// Generics form a stack, where each binder introduces a new level. For DeBruijn indices to
163    /// work, we keep the innermost parameters at the start of the vector.
164    pub generics: BindingStack<Cow<'a, GenericParams>>,
165    pub locals: Option<&'a Locals>,
166    pub indent_level: usize,
167}
168
169impl<'c> AstFormatter for FmtCtx<'c> {
170    type Reborrow<'a>
171        = FmtCtx<'a>
172    where
173        Self: 'a;
174
175    fn get_crate(&self) -> Option<&TranslatedCrate> {
176        self.translated
177    }
178
179    fn no_generics<'a>(&'a self) -> Self::Reborrow<'a> {
180        FmtCtx {
181            generics: BindingStack::empty(),
182            ..self.reborrow()
183        }
184    }
185    fn set_generics<'a>(&'a self, generics: &'a GenericParams) -> Self::Reborrow<'a> {
186        FmtCtx {
187            generics: BindingStack::new(Cow::Borrowed(generics)),
188            ..self.reborrow()
189        }
190    }
191    fn set_locals<'a>(&'a self, locals: &'a Locals) -> Self::Reborrow<'a> {
192        FmtCtx {
193            locals: Some(locals),
194            ..self.reborrow()
195        }
196    }
197    fn push_binder<'a>(&'a self, new_params: Cow<'a, GenericParams>) -> Self::Reborrow<'a> {
198        let mut ret = self.reborrow();
199        ret.generics.push(new_params);
200        ret
201    }
202    fn binder_depth(&self) -> usize {
203        self.generics.len()
204    }
205
206    fn increase_indent<'a>(&'a self) -> Self::Reborrow<'a> {
207        FmtCtx {
208            indent_level: self.indent_level + 1,
209            ..self.reborrow()
210        }
211    }
212    fn indent(&self) -> String {
213        TAB_INCR.repeat(self.indent_level)
214    }
215
216    fn format_local_id(&self, f: &mut fmt::Formatter<'_>, id: LocalId) -> fmt::Result {
217        if let Some(locals) = &self.locals
218            && let Some(v) = locals.locals.get(id)
219        {
220            write!(f, "{v}")
221        } else {
222            write!(f, "_{id}")
223        }
224    }
225
226    fn format_bound_var<Id: Idx + Display, T>(
227        &self,
228        f: &mut fmt::Formatter<'_>,
229        var: DeBruijnVar<Id>,
230        var_prefix: &str,
231        fmt_var: impl Fn(&T) -> Option<String>,
232    ) -> fmt::Result
233    where
234        GenericParams: HasIdxVecOf<Id, Output = T>,
235    {
236        if self.generics.is_empty() {
237            return write!(f, "{var_prefix}{var}");
238        }
239        match self.generics.get_var::<_, GenericParams>(var) {
240            None => write!(f, "missing({var_prefix}{var})"),
241            Some(v) => match fmt_var(v) {
242                Some(name) => write!(f, "{name}"),
243                None => {
244                    write!(f, "{var_prefix}")?;
245                    let (dbid, varid) = self.generics.as_bound_var(var);
246                    let depth = self.generics.depth().index - dbid.index;
247                    if depth == 0 {
248                        write!(f, "{varid}")
249                    } else {
250                        write!(f, "{varid}_{depth}")
251                    }
252                }
253            },
254        }
255    }
256}
257
258impl<'a> FmtCtx<'a> {
259    pub fn new() -> Self {
260        FmtCtx::default()
261    }
262
263    pub fn get_item(&self, id: ItemId) -> Result<ItemRef<'_>, Option<&Name>> {
264        let Some(translated) = &self.translated else {
265            return Err(None);
266        };
267        translated
268            .get_item(id)
269            .ok_or_else(|| translated.item_short_name(id))
270    }
271
272    /// Print the whole definition.
273    pub fn format_decl_id(&self, id: impl Into<ItemId>) -> String {
274        let id = id.into();
275        match self.get_item(id) {
276            Ok(d) => d.to_string_with_ctx(self),
277            Err(opt_name) => {
278                let opt_name = opt_name
279                    .map(|n| format!(" ({})", n.with_ctx(self)))
280                    .unwrap_or_default();
281                format!("Missing decl: {id:?}{opt_name}")
282            }
283        }
284    }
285
286    fn reborrow<'b>(&'b self) -> FmtCtx<'b> {
287        FmtCtx {
288            translated: self.translated,
289            generics: self.generics.clone(),
290            locals: self.locals,
291            indent_level: self.indent_level,
292        }
293    }
294}
charon_lib/pretty/formatter.rs

charon_lib/pretty/
formatter.rs
