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

charon_lib/pretty/
formatter.rs
