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

charon_lib/pretty/
formatter.rs
