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 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 Vector<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: HasVectorOf<Id, Output = T>;
55
56    fn format_enum_variant_name(
57        &self,
58        f: &mut fmt::Formatter<'_>,
59        type_id: TypeDeclId,
60        variant_id: VariantId,
61    ) -> fmt::Result {
62        let variant = if let Some(translated) = self.get_crate()
63            && let Some(def) = translated.type_decls.get(type_id)
64            && let Some(variants) = def.kind.as_enum()
65        {
66            &variants.get(variant_id).unwrap().name
67        } else {
68            &variant_id.to_pretty_string()
69        };
70        write!(f, "{variant}")
71    }
72    fn format_enum_variant(
73        &self,
74        f: &mut fmt::Formatter<'_>,
75        type_id: TypeDeclId,
76        variant_id: VariantId,
77    ) -> fmt::Result {
78        write!(f, "{}::", type_id.with_ctx(self))?;
79        self.format_enum_variant_name(f, type_id, variant_id)?;
80        Ok(())
81    }
82
83    fn format_field_name(
84        &self,
85        f: &mut fmt::Formatter<'_>,
86        type_id: TypeDeclId,
87        opt_variant_id: Option<VariantId>,
88        field_id: FieldId,
89    ) -> fmt::Result {
90        let field_name = if let Some(translated) = self.get_crate()
91            && let Some(def) = translated.type_decls.get(type_id)
92        {
93            match (&def.kind, opt_variant_id) {
94                (TypeDeclKind::Enum(variants), Some(variant_id)) => {
95                    variants[variant_id].fields[field_id].name.as_ref()
96                }
97                (TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields), None) => {
98                    fields[field_id].name.as_ref()
99                }
100                _ => None,
101            }
102        } else {
103            None
104        };
105        if let Some(field_name) = field_name {
106            write!(f, "{field_name}")
107        } else {
108            write!(f, "{field_id}")
109        }
110    }
111}
112
113/// Context for formatting.
114#[derive(Default)]
115pub struct FmtCtx<'a> {
116    pub translated: Option<&'a TranslatedCrate>,
117    /// Generics form a stack, where each binder introduces a new level. For DeBruijn indices to
118    /// work, we keep the innermost parameters at the start of the vector.
119    pub generics: BindingStack<Cow<'a, GenericParams>>,
120    pub locals: Option<&'a Locals>,
121    pub indent_level: usize,
122}
123
124impl<'c> AstFormatter for FmtCtx<'c> {
125    type Reborrow<'a>
126        = FmtCtx<'a>
127    where
128        Self: 'a;
129
130    fn get_crate(&self) -> Option<&TranslatedCrate> {
131        self.translated
132    }
133
134    fn no_generics<'a>(&'a self) -> Self::Reborrow<'a> {
135        FmtCtx {
136            generics: BindingStack::empty(),
137            ..self.reborrow()
138        }
139    }
140    fn set_generics<'a>(&'a self, generics: &'a GenericParams) -> Self::Reborrow<'a> {
141        FmtCtx {
142            generics: BindingStack::new(Cow::Borrowed(generics)),
143            ..self.reborrow()
144        }
145    }
146    fn set_locals<'a>(&'a self, locals: &'a Locals) -> Self::Reborrow<'a> {
147        FmtCtx {
148            locals: Some(locals),
149            ..self.reborrow()
150        }
151    }
152    fn push_binder<'a>(&'a self, new_params: Cow<'a, GenericParams>) -> Self::Reborrow<'a> {
153        let mut ret = self.reborrow();
154        ret.generics.push(new_params);
155        ret
156    }
157    fn binder_depth(&self) -> usize {
158        self.generics.len()
159    }
160
161    fn increase_indent<'a>(&'a self) -> Self::Reborrow<'a> {
162        FmtCtx {
163            indent_level: self.indent_level + 1,
164            ..self.reborrow()
165        }
166    }
167    fn indent(&self) -> String {
168        TAB_INCR.repeat(self.indent_level)
169    }
170
171    fn format_local_id(&self, f: &mut fmt::Formatter<'_>, id: LocalId) -> fmt::Result {
172        if let Some(locals) = &self.locals
173            && let Some(v) = locals.locals.get(id)
174        {
175            write!(f, "{v}")
176        } else {
177            write!(f, "{}", id.to_pretty_string())
178        }
179    }
180
181    fn format_bound_var<Id: Idx + Display, T>(
182        &self,
183        f: &mut fmt::Formatter<'_>,
184        var: DeBruijnVar<Id>,
185        var_prefix: &str,
186        fmt_var: impl Fn(&T) -> Option<String>,
187    ) -> fmt::Result
188    where
189        GenericParams: HasVectorOf<Id, Output = T>,
190    {
191        if self.generics.is_empty() {
192            return write!(f, "{var_prefix}{var}");
193        }
194        match self.generics.get_var::<_, GenericParams>(var) {
195            None => write!(f, "missing({var_prefix}{var})"),
196            Some(v) => match fmt_var(v) {
197                Some(name) => write!(f, "{name}"),
198                None => {
199                    write!(f, "{var_prefix}")?;
200                    let (dbid, varid) = self.generics.as_bound_var(var);
201                    let depth = self.generics.depth().index - dbid.index;
202                    if depth == 0 {
203                        write!(f, "{varid}")
204                    } else {
205                        write!(f, "{varid}_{depth}")
206                    }
207                }
208            },
209        }
210    }
211}
212
213impl<'a> FmtCtx<'a> {
214    pub fn new() -> Self {
215        FmtCtx::default()
216    }
217
218    pub fn get_item(&self, id: ItemId) -> Result<ItemRef<'_>, Option<&Name>> {
219        let Some(translated) = &self.translated else {
220            return Err(None);
221        };
222        translated
223            .get_item(id)
224            .ok_or_else(|| translated.item_short_name(id))
225    }
226
227    /// Print the whole definition.
228    pub fn format_decl_id(&self, id: impl Into<ItemId>) -> String {
229        let id = id.into();
230        match self.get_item(id) {
231            Ok(d) => d.to_string_with_ctx(self),
232            Err(opt_name) => {
233                let opt_name = opt_name
234                    .map(|n| format!(" ({})", n.with_ctx(self)))
235                    .unwrap_or_default();
236                format!("Missing decl: {id:?}{opt_name}")
237            }
238        }
239    }
240
241    fn reborrow<'b>(&'b self) -> FmtCtx<'b> {
242        FmtCtx {
243            translated: self.translated.as_deref(),
244            generics: self.generics.clone(),
245            locals: self.locals.as_deref(),
246            indent_level: self.indent_level,
247        }
248    }
249}
charon_lib/pretty/formatter.rs

charon_lib/pretty/
formatter.rs
