charon_lib/pretty/
formatter.rs

1use std::borrow::Cow;
2use std::fmt::Display;
3
4use index_vec::Idx;
5
6use crate::ast::*;
7use crate::common::TAB_INCR;
8use crate::gast;
9use crate::ids::Vector;
10use crate::llbc_ast;
11use crate::pretty::{fmt_with_ctx, FmtWithCtx};
12use crate::ullbc_ast;
13use crate::ullbc_ast as ast;
14
15/// [`Formatter`](Formatter) is a trait for converting objects to string.
16///
17/// We need it because pretty-printing data structures often requires some
18/// context. For instance, because values use value ids to point to other values,
19/// we need a context to give us the mapping from value ids to values when pretty
20/// printing. As the `EvalContext` data structure handles such a mapping, we
21/// implement the `Formatter<ValueId>` trait for it.
22///
23/// Our way of implementing pretty-printing for data-structures while factorizing
24/// the code is as follows:
25/// - for every data structure which requires formatting, we implement a
26///   function `fn fmt_with_ctx(&self, ctx: T) -> String`, with proper trait
27///   constraints on the context type T. We implement this kind of functions
28///   for values, types, places, operands, rvalues, statements, etc, and
29///   the formatting trait constraints often require the context to implement
30///   `Formatter` for a various set of indices (type variable index, variable
31///   index, type definition index, etc.).
32/// - later on, whenever we have a suitable context type (like `EvalContext`),
33///   we implement the `Formatter` trait for all the index types we need, and
34///   then can easily implement it for all the above data-structures (values,
35///   types, places, etc.) by calling the appropriate `fmt_with_ctx` functions.
36/// The advantage of using auxiliary `fmt_with_ctx` functions is that we can
37/// easily reuse those functions to implement pretty-printing with different
38/// contexts, without duplicating the "non-trivial" code.
39pub trait Formatter<T> {
40    fn format_object(&self, x: T) -> String;
41}
42
43/// Provided some id, print the declaration (not simply its name).
44pub trait DeclFormatter<Id> {
45    fn format_decl(&self, x: Id) -> String;
46}
47
48impl<C, T> Formatter<T> for &C
49where
50    C: Formatter<T>,
51{
52    fn format_object(&self, x: T) -> String {
53        (*self).format_object(x)
54    }
55}
56
57pub trait IntoFormatter {
58    type C: AstFormatter;
59
60    fn into_fmt(self) -> Self::C;
61}
62
63impl<C: AstFormatter> IntoFormatter for C {
64    type C = Self;
65
66    fn into_fmt(self) -> Self::C {
67        self
68    }
69}
70
71/// We use this trait with the formatter to update the context,
72/// for instance when we enter a declaration that we need to print.
73pub trait SetGenerics<'a> {
74    type C: 'a + AstFormatter;
75
76    fn set_generics(&'a self, generics: &'a GenericParams) -> Self::C;
77}
78
79impl<'a, 'b> SetGenerics<'a> for FmtCtx<'b> {
80    type C = FmtCtx<'a>;
81
82    fn set_generics(&'a self, generics: &'a GenericParams) -> Self::C {
83        FmtCtx {
84            translated: self.translated.as_deref(),
85            generics: BindingStack::new(Cow::Borrowed(generics)),
86            locals: self.locals.as_deref(),
87        }
88    }
89}
90
91/// We use this trait with the formatter to update the context,
92/// for instance when we enter a declaration that we need to print.
93pub trait SetLocals<'a> {
94    type C: 'a + AstFormatter;
95
96    fn set_locals(&'a self, locals: &'a Locals) -> Self::C;
97}
98
99impl<'a, 'b> SetLocals<'a> for FmtCtx<'b> {
100    type C = FmtCtx<'a>;
101
102    fn set_locals(&'a self, locals: &'a Locals) -> Self::C {
103        FmtCtx {
104            translated: self.translated.as_deref(),
105            generics: self.generics.clone(),
106            locals: Some(locals),
107        }
108    }
109}
110
111/// We use this trait to update the context by pushing a group of bound regions.
112pub trait PushBinder<'a> {
113    type C: 'a + AstFormatter;
114
115    fn push_binder(&'a self, new_params: Cow<'a, GenericParams>) -> Self::C;
116
117    fn push_bound_regions(&'a self, regions: &'a Vector<RegionId, RegionVar>) -> Self::C {
118        self.push_binder(Cow::Owned(GenericParams {
119            regions: regions.clone(),
120            ..Default::default()
121        }))
122    }
123}
124
125impl<'a, 'b> PushBinder<'a> for FmtCtx<'b> {
126    type C = FmtCtx<'a>;
127
128    fn push_binder(&'a self, new_params: Cow<'a, GenericParams>) -> Self::C {
129        let mut generics = self.generics.clone();
130        generics.push(new_params);
131        FmtCtx {
132            translated: self.translated.as_deref(),
133            generics,
134            locals: self.locals.as_deref(),
135        }
136    }
137}
138
139pub trait AstFormatter = Formatter<TypeDeclId>
140    + Formatter<FunDeclId>
141    + Formatter<GlobalDeclId>
142    + Formatter<TraitDeclId>
143    + Formatter<TraitImplId>
144    + Formatter<AnyTransId>
145    + Formatter<RegionDbVar>
146    + Formatter<TypeDbVar>
147    + Formatter<ConstGenericDbVar>
148    + Formatter<ClauseDbVar>
149    + Formatter<LocalId>
150    + Formatter<(TypeDeclId, VariantId)>
151    + Formatter<(TypeDeclId, Option<VariantId>, FieldId)>
152    + for<'a> Formatter<&'a ImplElem>
153    + for<'a> Formatter<&'a RegionVar>
154    + for<'a> Formatter<&'a Vector<ullbc_ast::BlockId, ullbc_ast::BlockData>>
155    + for<'a> Formatter<&'a llbc_ast::Block>
156    + for<'a> SetGenerics<'a>
157    + for<'a> SetLocals<'a>
158    + for<'a> PushBinder<'a>;
159
160/// For formatting.
161///
162/// Note that we use the ULLBC definitions, even when formatting LLBC
163/// definitions. It doesn't really matter, as all we use is the *name*
164/// of the definitions.
165///
166/// Remark: we take shared borrows to the top-level declarations, but
167/// clone the generics, because we may dive into different contexts and may
168/// need to update those. We can think of a smarter way of doing this, but
169/// for now it is simple and efficient enough.
170#[derive(Default)]
171pub struct FmtCtx<'a> {
172    pub translated: Option<&'a TranslatedCrate>,
173    /// Generics form a stack, where each binder introduces a new level. For DeBruijn indices to
174    /// work, we keep the innermost parameters at the start of the vector.
175    pub generics: BindingStack<Cow<'a, GenericParams>>,
176    pub locals: Option<&'a Locals>,
177}
178
179impl<'a> FmtCtx<'a> {
180    pub fn new() -> Self {
181        FmtCtx::default()
182    }
183
184    pub fn format_decl_id(&self, id: AnyTransId) -> String {
185        match id {
186            AnyTransId::Type(id) => self.format_decl(id),
187            AnyTransId::Fun(id) => self.format_decl(id),
188            AnyTransId::Global(id) => self.format_decl(id),
189            AnyTransId::TraitDecl(id) => self.format_decl(id),
190            AnyTransId::TraitImpl(id) => self.format_decl(id),
191        }
192    }
193
194    pub fn get_item(&self, id: AnyTransId) -> Result<AnyTransItem<'_>, Option<&Name>> {
195        let Some(translated) = &self.translated else {
196            return Err(None);
197        };
198        translated
199            .get_item(id)
200            .ok_or_else(|| translated.item_name(id))
201    }
202
203    fn format_any_decl(&self, id: AnyTransId) -> String {
204        match self.get_item(id) {
205            Ok(d) => d.fmt_with_ctx(self),
206            Err(opt_name) => {
207                let opt_name = opt_name
208                    .map(|n| n.fmt_with_ctx(self))
209                    .map(|n| format!(" ({n})"))
210                    .unwrap_or_default();
211                format!("Missing decl: {id:?}{opt_name}")
212            }
213        }
214    }
215}
216
217impl<'a> Formatter<TypeDeclId> for FmtCtx<'a> {
218    fn format_object(&self, id: TypeDeclId) -> String {
219        self.format_object(AnyTransId::from(id))
220    }
221}
222
223impl<'a> Formatter<GlobalDeclId> for FmtCtx<'a> {
224    fn format_object(&self, id: GlobalDeclId) -> String {
225        self.format_object(AnyTransId::from(id))
226    }
227}
228
229impl<'a> Formatter<FunDeclId> for FmtCtx<'a> {
230    fn format_object(&self, id: ast::FunDeclId) -> String {
231        self.format_object(AnyTransId::from(id))
232    }
233}
234
235impl<'a> Formatter<TraitDeclId> for FmtCtx<'a> {
236    fn format_object(&self, id: ast::TraitDeclId) -> String {
237        self.format_object(AnyTransId::from(id))
238    }
239}
240
241impl<'a> Formatter<TraitImplId> for FmtCtx<'a> {
242    fn format_object(&self, id: ast::TraitImplId) -> String {
243        self.format_object(AnyTransId::from(id))
244    }
245}
246
247impl<'a> Formatter<AnyTransId> for FmtCtx<'a> {
248    fn format_object(&self, id: AnyTransId) -> String {
249        match self
250            .translated
251            .and_then(|translated| translated.item_name(id))
252        {
253            None => id.to_string(),
254            Some(name) => name.fmt_with_ctx(self),
255        }
256    }
257}
258
259impl<'a> FmtCtx<'a> {
260    fn format_bound_var<Id: Idx + Display, T>(
261        &self,
262        var: DeBruijnVar<Id>,
263        var_prefix: &str,
264        f: impl Fn(&T) -> Option<String>,
265    ) -> String
266    where
267        GenericParams: HasVectorOf<Id, Output = T>,
268    {
269        if self.generics.is_empty() {
270            return format!("{var_prefix}{var}");
271        }
272        match self.generics.get_var::<_, GenericParams>(var) {
273            None => format!("missing({var_prefix}{var})"),
274            Some(v) => match f(v) {
275                Some(name) => name,
276                None => {
277                    let (dbid, varid) = self.generics.as_bound_var(var);
278                    if dbid == self.generics.depth() {
279                        format!("{var_prefix}{varid}")
280                    } else {
281                        format!("{var_prefix}{var}")
282                    }
283                }
284            },
285        }
286    }
287}
288
289impl<'a> Formatter<RegionDbVar> for FmtCtx<'a> {
290    fn format_object(&self, var: RegionDbVar) -> String {
291        self.format_bound_var(var, "'_", |v| v.name.as_ref().map(|name| name.to_string()))
292    }
293}
294
295impl<'a> Formatter<&RegionVar> for FmtCtx<'a> {
296    fn format_object(&self, var: &RegionVar) -> String {
297        match &var.name {
298            Some(name) => name.to_string(),
299            None => format!("'_{}", var.index),
300        }
301    }
302}
303
304impl<'a> Formatter<TypeDbVar> for FmtCtx<'a> {
305    fn format_object(&self, var: TypeDbVar) -> String {
306        self.format_bound_var(var, "@Type", |v| Some(v.to_string()))
307    }
308}
309
310impl<'a> Formatter<ConstGenericDbVar> for FmtCtx<'a> {
311    fn format_object(&self, var: ConstGenericDbVar) -> String {
312        self.format_bound_var(var, "@ConstGeneric", |v| Some(v.fmt_with_ctx(self)))
313    }
314}
315
316impl<'a> Formatter<ClauseDbVar> for FmtCtx<'a> {
317    fn format_object(&self, var: ClauseDbVar) -> String {
318        self.format_bound_var(var, "@TraitClause", |_| None)
319    }
320}
321
322impl<'a> Formatter<&ImplElem> for FmtCtx<'a> {
323    fn format_object(&self, elem: &ImplElem) -> String {
324        let inner = match elem {
325            ImplElem::Ty(bound_ty) => {
326                // Just printing the generics (not the predicates)
327                let ctx = self.set_generics(&bound_ty.params);
328                bound_ty.skip_binder.fmt_with_ctx(&ctx)
329            }
330            ImplElem::Trait(impl_id) => {
331                match &self.translated {
332                    None => format!("impl#{impl_id}"),
333                    Some(translated) => match translated.trait_impls.get(*impl_id) {
334                        None => format!("impl#{impl_id}"),
335                        Some(timpl) => {
336                            // We need to put the first type parameter aside: it is
337                            // the type for which we implement the trait.
338                            // This is not very clean because it's hard to move the
339                            // first element out of a vector...
340                            let ctx = &self.set_generics(&timpl.generics);
341                            let TraitDeclRef { trait_id, generics } = &timpl.impl_trait;
342                            let (ty, generics) = generics.pop_first_type_arg();
343                            let tr = TraitDeclRef {
344                                trait_id: *trait_id,
345                                generics,
346                            };
347                            format!("impl {} for {}", tr.fmt_with_ctx(ctx), ty.fmt_with_ctx(ctx))
348                        }
349                    },
350                }
351            }
352        };
353
354        format!("{{{inner}}}")
355    }
356}
357
358/// For enum values: `List::Cons`
359impl<'a> Formatter<(TypeDeclId, VariantId)> for FmtCtx<'a> {
360    fn format_object(&self, id: (TypeDeclId, VariantId)) -> String {
361        let (def_id, variant_id) = id;
362        match &self.translated {
363            None => format!(
364                "{}::{}",
365                def_id.to_pretty_string(),
366                variant_id.to_pretty_string()
367            ),
368            Some(translated) => {
369                // The definition may not be available yet, especially if we print-debug
370                // while translating the crate
371                match translated.type_decls.get(def_id) {
372                    None => format!(
373                        "{}::{}",
374                        def_id.to_pretty_string(),
375                        variant_id.to_pretty_string()
376                    ),
377                    Some(def) if def.kind.is_enum() => {
378                        let variants = def.kind.as_enum().unwrap();
379                        let mut name = def.item_meta.name.fmt_with_ctx(self);
380                        let variant_name = &variants.get(variant_id).unwrap().name;
381                        name.push_str("::");
382                        name.push_str(variant_name);
383                        name
384                    }
385                    _ => format!("__unknown_variant"),
386                }
387            }
388        }
389    }
390}
391
392/// For struct/enum values: retrieve a field name
393impl<'a> Formatter<(TypeDeclId, Option<VariantId>, FieldId)> for FmtCtx<'a> {
394    fn format_object(&self, id: (TypeDeclId, Option<VariantId>, FieldId)) -> String {
395        let (def_id, opt_variant_id, field_id) = id;
396        match &self.translated {
397            None => match opt_variant_id {
398                None => format!(
399                    "{}::{}",
400                    def_id.to_pretty_string(),
401                    field_id.to_pretty_string()
402                ),
403                Some(variant_id) => format!(
404                    "{}::{}::{}",
405                    def_id.to_pretty_string(),
406                    variant_id.to_pretty_string(),
407                    field_id.to_pretty_string()
408                ),
409            },
410            Some(translated) =>
411            // The definition may not be available yet, especially if we
412            // print-debug while translating the crate
413            {
414                match translated.type_decls.get(def_id) {
415                    None => match opt_variant_id {
416                        None => format!(
417                            "{}::{}",
418                            def_id.to_pretty_string(),
419                            field_id.to_pretty_string()
420                        ),
421                        Some(variant_id) => format!(
422                            "{}::{}::{}",
423                            def_id.to_pretty_string(),
424                            variant_id.to_pretty_string(),
425                            field_id.to_pretty_string()
426                        ),
427                    },
428                    Some(gen_def) => match (&gen_def.kind, opt_variant_id) {
429                        (TypeDeclKind::Enum(variants), Some(variant_id)) => {
430                            let field = variants
431                                .get(variant_id)
432                                .unwrap()
433                                .fields
434                                .get(field_id)
435                                .unwrap();
436                            match &field.name {
437                                Some(name) => name.clone(),
438                                None => field_id.to_string(),
439                            }
440                        }
441                        (TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields), None) => {
442                            let field = fields.get(field_id).unwrap();
443                            match &field.name {
444                                Some(name) => name.clone(),
445                                None => field_id.to_string(),
446                            }
447                        }
448                        _ => format!("__unknown_field"),
449                    },
450                }
451            }
452        }
453    }
454}
455
456impl<'a> Formatter<LocalId> for FmtCtx<'a> {
457    fn format_object(&self, id: LocalId) -> String {
458        match &self.locals {
459            None => id.to_pretty_string(),
460            Some(locals) => match locals.locals.get(id) {
461                None => id.to_pretty_string(),
462                Some(v) => v.to_string(),
463            },
464        }
465    }
466}
467
468impl<'a> Formatter<&llbc_ast::Block> for FmtCtx<'a> {
469    fn format_object(&self, x: &llbc_ast::Block) -> String {
470        x.fmt_with_ctx(self)
471    }
472}
473
474impl<'a> Formatter<&Vector<ullbc_ast::BlockId, ullbc_ast::BlockData>> for FmtCtx<'a> {
475    fn format_object(&self, x: &Vector<ullbc_ast::BlockId, ullbc_ast::BlockData>) -> String {
476        fmt_with_ctx::fmt_body_blocks_with_ctx(x, TAB_INCR, self)
477    }
478}
479
480impl<'a> Formatter<&Ty> for FmtCtx<'a> {
481    fn format_object(&self, x: &Ty) -> String {
482        x.fmt_with_ctx(self)
483    }
484}
485
486impl<'a> Formatter<&TypeDecl> for FmtCtx<'a> {
487    fn format_object(&self, def: &TypeDecl) -> String {
488        def.fmt_with_ctx(self)
489    }
490}
491
492impl<'a> Formatter<&ullbc_ast::ExprBody> for FmtCtx<'a> {
493    fn format_object(&self, body: &ullbc_ast::ExprBody) -> String {
494        body.fmt_with_ctx(self)
495    }
496}
497
498impl<'a> Formatter<&llbc_ast::ExprBody> for FmtCtx<'a> {
499    fn format_object(&self, body: &llbc_ast::ExprBody) -> String {
500        body.fmt_with_ctx(self)
501    }
502}
503
504impl<'a> Formatter<&gast::FunDecl> for FmtCtx<'a> {
505    fn format_object(&self, def: &llbc_ast::FunDecl) -> String {
506        def.fmt_with_ctx(self)
507    }
508}
509
510impl<'a> Formatter<&gast::GlobalDecl> for FmtCtx<'a> {
511    fn format_object(&self, def: &llbc_ast::GlobalDecl) -> String {
512        def.fmt_with_ctx(self)
513    }
514}
515
516impl<'a> Formatter<&FunSig> for FmtCtx<'a> {
517    fn format_object(&self, x: &FunSig) -> String {
518        x.fmt_with_ctx(self)
519    }
520}
521
522impl<'a> Formatter<&gast::TraitDecl> for FmtCtx<'a> {
523    fn format_object(&self, def: &gast::TraitDecl) -> String {
524        def.fmt_with_ctx(self)
525    }
526}
527
528impl<'a> Formatter<&gast::TraitImpl> for FmtCtx<'a> {
529    fn format_object(&self, def: &gast::TraitImpl) -> String {
530        def.fmt_with_ctx(self)
531    }
532}
533
534impl<'a> DeclFormatter<TypeDeclId> for FmtCtx<'a> {
535    fn format_decl(&self, id: TypeDeclId) -> String {
536        self.format_any_decl(id.into())
537    }
538}
539
540impl<'a> DeclFormatter<GlobalDeclId> for FmtCtx<'a> {
541    fn format_decl(&self, id: GlobalDeclId) -> String {
542        self.format_any_decl(id.into())
543    }
544}
545
546impl<'a> DeclFormatter<FunDeclId> for FmtCtx<'a> {
547    fn format_decl(&self, id: FunDeclId) -> String {
548        self.format_any_decl(id.into())
549    }
550}
551
552impl<'a> DeclFormatter<TraitDeclId> for FmtCtx<'a> {
553    fn format_decl(&self, id: TraitDeclId) -> String {
554        self.format_any_decl(id.into())
555    }
556}
557
558impl<'a> DeclFormatter<TraitImplId> for FmtCtx<'a> {
559    fn format_decl(&self, id: TraitImplId) -> String {
560        self.format_any_decl(id.into())
561    }
562}
charon_lib/pretty/formatter.rs

charon_lib/pretty/
formatter.rs
