charon_lib/pretty/
fmt_with_ctx.rs

1//! Utilities for pretty-printing (u)llbc.
2use crate::{
3    common::TAB_INCR,
4    formatter::*,
5    gast,
6    ids::Vector,
7    llbc_ast::{self as llbc, *},
8    reorder_decls::*,
9    ullbc_ast::{self as ullbc, *},
10};
11use itertools::Itertools;
12use std::{
13    borrow::Cow,
14    fmt::{self, Debug, Display, Write},
15};
16
17/// Format the AST type as a string.
18pub trait FmtWithCtx<C> {
19    fn fmt_with_ctx(&self, ctx: &C) -> String {
20        // By default use no tab.
21        self.fmt_with_ctx_and_indent("", ctx)
22    }
23
24    fn fmt_with_ctx_and_indent(&self, _tab: &str, _ctx: &C) -> String {
25        panic!("This type does not know how to be formatted with indent")
26    }
27
28    /// Returns a struct that implements `Display`. This allows the following:
29    /// ```text
30    ///     println!("{}", self.with_ctx(ctx));
31    /// ```
32    fn with_ctx<'a>(&'a self, ctx: &'a C) -> impl std::fmt::Display + 'a {
33        pub struct WithCtx<'a, C, T: ?Sized> {
34            val: &'a T,
35            ctx: &'a C,
36        }
37
38        impl<'a, C, T: ?Sized> std::fmt::Display for WithCtx<'a, C, T>
39        where
40            T: FmtWithCtx<C>,
41        {
42            fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
43                let s = self.val.fmt_with_ctx(self.ctx);
44                f.write_str(&s)
45            }
46        }
47
48        WithCtx { val: self, ctx }
49    }
50}
51
52impl<C: AstFormatter> FmtWithCtx<C> for AbortKind {
53    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
54        match self {
55            AbortKind::Panic(name) => {
56                let name = if let Some(name) = name {
57                    format!("({})", name.fmt_with_ctx(ctx))
58                } else {
59                    format!("")
60                };
61                format!("{tab}panic{name}")
62            }
63            AbortKind::UndefinedBehavior => format!("{tab}undefined_behavior"),
64        }
65    }
66}
67
68impl<C: AstFormatter> FmtWithCtx<C> for AnyTransItem<'_> {
69    fn fmt_with_ctx(&self, ctx: &C) -> String {
70        match self {
71            AnyTransItem::Type(d) => d.fmt_with_ctx(ctx),
72            AnyTransItem::Fun(d) => d.fmt_with_ctx(ctx),
73            AnyTransItem::Global(d) => d.fmt_with_ctx(ctx),
74            AnyTransItem::TraitDecl(d) => d.fmt_with_ctx(ctx),
75            AnyTransItem::TraitImpl(d) => d.fmt_with_ctx(ctx),
76        }
77    }
78}
79
80impl<C: AstFormatter> FmtWithCtx<C> for Assert {
81    fn fmt_with_ctx(&self, ctx: &C) -> String {
82        format!(
83            "assert({} == {})",
84            self.cond.fmt_with_ctx(ctx),
85            self.expected,
86        )
87    }
88}
89
90impl<T> Binder<T> {
91    /// Format the parameters and contents of this binder and returns the resulting strings. Note:
92    /// this assumes the binder fully replaces the existing generics.
93    fn fmt_split<'a, C>(&'a self, ctx: &'a C) -> (String, String)
94    where
95        C: AstFormatter,
96        T: FmtWithCtx<<C as PushBinder<'a>>::C>,
97    {
98        let ctx = &ctx.push_binder(Cow::Borrowed(&self.params));
99        (
100            self.params.fmt_with_ctx_single_line(ctx),
101            self.skip_binder.fmt_with_ctx(ctx),
102        )
103    }
104}
105
106impl<C: AstFormatter> FmtWithCtx<C> for llbc::Block {
107    fn fmt_with_ctx(&self, ctx: &C) -> String {
108        // By default use a tab.
109        self.fmt_with_ctx_and_indent(TAB_INCR, ctx)
110    }
111
112    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
113        self.statements
114            .iter()
115            .map(|st| st.fmt_with_ctx_and_indent(tab, ctx))
116            .map(|st| format!("{st}\n"))
117            .join("")
118    }
119}
120
121impl<C: AstFormatter> FmtWithCtx<C> for ullbc::BlockData {
122    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
123        let mut out: Vec<String> = Vec::new();
124
125        // Format the statements
126        for statement in &self.statements {
127            out.push(format!("{};\n", statement.fmt_with_ctx_and_indent(tab, ctx)).to_string());
128        }
129
130        // Format the terminator
131        out.push(format!(
132            "{};",
133            self.terminator.fmt_with_ctx_and_indent(tab, ctx)
134        ));
135
136        // Join the strings
137        out.join("")
138    }
139}
140
141impl<C: AstFormatter> FmtWithCtx<C> for gast::Body {
142    fn fmt_with_ctx(&self, ctx: &C) -> String {
143        match self {
144            Body::Unstructured(b) => b.fmt_with_ctx(ctx),
145            Body::Structured(b) => b.fmt_with_ctx(ctx),
146        }
147    }
148
149    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
150        match self {
151            Body::Unstructured(b) => b.fmt_with_ctx_and_indent(tab, ctx),
152            Body::Structured(b) => b.fmt_with_ctx_and_indent(tab, ctx),
153        }
154    }
155}
156
157impl<C: AstFormatter> FmtWithCtx<C> for CastKind {
158    fn fmt_with_ctx(&self, ctx: &C) -> String {
159        match self {
160            CastKind::Scalar(src, tgt) => format!("cast<{src}, {tgt}>"),
161            CastKind::FnPtr(src, tgt) | CastKind::RawPtr(src, tgt) => {
162                format!("cast<{}, {}>", src.fmt_with_ctx(ctx), tgt.fmt_with_ctx(ctx))
163            }
164            CastKind::Unsize(src, tgt) => {
165                format!(
166                    "unsize_cast<{}, {}>",
167                    src.fmt_with_ctx(ctx),
168                    tgt.fmt_with_ctx(ctx)
169                )
170            }
171            CastKind::Transmute(src, tgt) => {
172                format!(
173                    "transmute<{}, {}>",
174                    src.fmt_with_ctx(ctx),
175                    tgt.fmt_with_ctx(ctx)
176                )
177            }
178        }
179    }
180}
181
182impl<C: AstFormatter> FmtWithCtx<C> for ConstantExpr {
183    fn fmt_with_ctx(&self, ctx: &C) -> String {
184        self.value.fmt_with_ctx(ctx)
185    }
186}
187
188impl<C: AstFormatter> FmtWithCtx<C> for ConstGeneric {
189    fn fmt_with_ctx(&self, ctx: &C) -> String {
190        match self {
191            ConstGeneric::Var(id) => ctx.format_object(*id),
192            ConstGeneric::Value(v) => v.to_string(),
193            ConstGeneric::Global(id) => ctx.format_object(*id),
194        }
195    }
196}
197
198impl<C: AstFormatter> FmtWithCtx<C> for ConstGenericVar {
199    fn fmt_with_ctx(&self, ctx: &C) -> String {
200        let ty = self.ty.fmt_with_ctx(ctx);
201        format!("const {} : {}", self.name, ty)
202    }
203}
204
205impl<C: AstFormatter> FmtWithCtx<C> for DeclarationGroup {
206    fn fmt_with_ctx(&self, ctx: &C) -> String {
207        use DeclarationGroup::*;
208        match self {
209            Type(g) => format!("Type decls group: {}", g.fmt_with_ctx(ctx)),
210            Fun(g) => format!("Fun decls group: {}", g.fmt_with_ctx(ctx)),
211            Global(g) => format!("Global decls group: {}", g.fmt_with_ctx(ctx)),
212            TraitDecl(g) => format!("Trait decls group: {}", g.fmt_with_ctx(ctx)),
213            TraitImpl(g) => format!("Trait impls group: {}", g.fmt_with_ctx(ctx)),
214            Mixed(g) => format!("Mixed group: {}", g.fmt_with_ctx(ctx)),
215        }
216    }
217}
218
219impl<C: AstFormatter> FmtWithCtx<C> for ExistentialPredicate {
220    fn fmt_with_ctx(&self, _ctx: &C) -> String {
221        format!("exists(TODO)")
222    }
223}
224
225impl<C: AstFormatter> FmtWithCtx<C> for Field {
226    fn fmt_with_ctx(&self, ctx: &C) -> String {
227        match &self.name {
228            Some(name) => format!("{}: {}", name, self.ty.fmt_with_ctx(ctx)),
229            None => self.ty.fmt_with_ctx(ctx),
230        }
231    }
232}
233
234impl<C: AstFormatter> FmtWithCtx<C> for FnOperand {
235    fn fmt_with_ctx(&self, ctx: &C) -> String {
236        match self {
237            FnOperand::Regular(func) => func.fmt_with_ctx(ctx),
238            FnOperand::Move(p) => format!("(move {})", p.fmt_with_ctx(ctx)),
239        }
240    }
241}
242
243impl<C: AstFormatter> FmtWithCtx<C> for FnPtr {
244    fn fmt_with_ctx(&self, ctx: &C) -> String {
245        let generics = self.generics.fmt_with_ctx(ctx);
246        let f = match self.func.as_ref() {
247            FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id)) => {
248                format!("{}", ctx.format_object(*def_id),)
249            }
250            FunIdOrTraitMethodRef::Fun(FunId::Builtin(builtin)) => {
251                format!("@{}", builtin)
252            }
253            FunIdOrTraitMethodRef::Trait(trait_ref, method_id, _) => {
254                format!("{}::{}", trait_ref.fmt_with_ctx(ctx), &method_id.0)
255            }
256        };
257        format!("{}{}", f, generics)
258    }
259}
260
261impl<C: AstFormatter> FmtWithCtx<C> for FunSig {
262    fn fmt_with_ctx(&self, ctx: &C) -> String {
263        let ctx = &ctx.set_generics(&self.generics);
264
265        // Unsafe keyword
266        let unsafe_kw = if self.is_unsafe {
267            "unsafe ".to_string()
268        } else {
269            "".to_string()
270        };
271
272        // Generic parameters
273        let (params, clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "");
274
275        // Arguments
276        let mut args: Vec<String> = Vec::new();
277        for ty in &self.inputs {
278            args.push(ty.fmt_with_ctx(ctx).to_string());
279        }
280        let args = args.join(", ");
281
282        // Return type
283        let ret_ty = &self.output;
284        let ret_ty = if ret_ty.is_unit() {
285            "".to_string()
286        } else {
287            format!(" -> {}", ret_ty.fmt_with_ctx(ctx))
288        };
289
290        // Put everything together
291        format!("{unsafe_kw}fn{params}({args}){ret_ty}{clauses}",)
292    }
293}
294
295impl<Id: Copy, C: AstFormatter + Formatter<Id>> FmtWithCtx<C> for GDeclarationGroup<Id> {
296    fn fmt_with_ctx(&self, ctx: &C) -> String {
297        use GDeclarationGroup::*;
298        match self {
299            NonRec(id) => format!("Non rec: {}", ctx.format_object(*id)),
300            Rec(ids) => {
301                let ids = ids
302                    .iter()
303                    .map(|id| ctx.format_object(*id))
304                    .collect::<Vec<String>>()
305                    .join(", ");
306                format!("Rec: {}", ids)
307            }
308        }
309    }
310}
311
312impl GenericArgs {
313    pub(crate) fn fmt_with_ctx_no_brackets<C>(&self, ctx: &C) -> String
314    where
315        C: AstFormatter,
316    {
317        assert!(self.trait_refs.is_empty());
318        let mut params = Vec::new();
319        let GenericArgs {
320            regions,
321            types,
322            const_generics,
323            trait_refs: _,
324            target: _,
325        } = self;
326        for x in regions {
327            params.push(x.fmt_with_ctx(ctx));
328        }
329        for x in types {
330            params.push(x.fmt_with_ctx(ctx));
331        }
332        for x in const_generics {
333            params.push(x.fmt_with_ctx(ctx));
334        }
335        params.join(", ")
336    }
337
338    pub fn fmt_with_ctx_split_trait_refs<C>(&self, ctx: &C) -> String
339    where
340        C: AstFormatter,
341    {
342        let mut params = Vec::new();
343        let GenericArgs {
344            regions,
345            types,
346            const_generics,
347            trait_refs,
348            target: _,
349        } = self;
350        for x in regions {
351            params.push(x.fmt_with_ctx(ctx));
352        }
353        for x in types {
354            params.push(x.fmt_with_ctx(ctx));
355        }
356        for x in const_generics {
357            params.push(x.fmt_with_ctx(ctx));
358        }
359        let params = if params.is_empty() {
360            "".to_string()
361        } else {
362            format!("<{}>", params.join(", "))
363        };
364
365        let mut clauses = Vec::new();
366        for x in trait_refs {
367            clauses.push(x.fmt_with_ctx(ctx));
368        }
369        let clauses = if clauses.is_empty() {
370            "".to_string()
371        } else {
372            format!("[{}]", clauses.join(", "))
373        };
374        format!("{params}{clauses}")
375    }
376}
377
378impl<C: AstFormatter> FmtWithCtx<C> for GenericArgs {
379    fn fmt_with_ctx(&self, ctx: &C) -> String {
380        self.fmt_with_ctx_split_trait_refs(ctx)
381    }
382}
383
384impl GenericParams {
385    fn format_params<'a, C>(&'a self, ctx: &'a C) -> impl Iterator<Item = String> + use<'a, C>
386    where
387        C: AstFormatter,
388    {
389        let regions = self.regions.iter().map(|x| x.fmt_with_ctx(ctx));
390        let types = self.types.iter().map(|x| x.fmt_with_ctx(ctx));
391        let const_generics = self.const_generics.iter().map(|x| x.fmt_with_ctx(ctx));
392        regions.chain(types).chain(const_generics)
393    }
394
395    fn format_clauses<'a, C>(&'a self, ctx: &'a C) -> impl Iterator<Item = String> + use<'a, C>
396    where
397        C: AstFormatter,
398    {
399        let trait_clauses = self.trait_clauses.iter().map(|x| x.fmt_with_ctx(ctx));
400        let types_outlive = self.types_outlive.iter().map(|x| x.fmt_as_for(ctx));
401        let regions_outlive = self.regions_outlive.iter().map(|x| x.fmt_as_for(ctx));
402        let type_constraints = self
403            .trait_type_constraints
404            .iter()
405            .map(|x| x.fmt_as_for(ctx));
406        trait_clauses
407            .chain(types_outlive)
408            .chain(regions_outlive)
409            .chain(type_constraints)
410    }
411
412    pub fn fmt_with_ctx_with_trait_clauses<C>(&self, ctx: &C, tab: &str) -> (String, String)
413    where
414        C: AstFormatter,
415    {
416        let params = self.format_params(ctx).join(", ");
417        let params = if params.is_empty() {
418            String::new()
419        } else {
420            format!("<{}>", params)
421        };
422        let clauses = self
423            .format_clauses(ctx)
424            .map(|x| format!("\n{tab}{TAB_INCR}{x},"))
425            .join("");
426        let clauses = if clauses.is_empty() {
427            String::new()
428        } else {
429            format!("\n{tab}where{clauses}")
430        };
431        (params, clauses)
432    }
433
434    pub fn fmt_with_ctx_single_line<C>(&self, ctx: &C) -> String
435    where
436        C: AstFormatter,
437    {
438        let params = self
439            .format_params(ctx)
440            .chain(self.format_clauses(ctx))
441            .join(", ");
442        if params.is_empty() {
443            String::new()
444        } else {
445            format!("<{}>", params)
446        }
447    }
448}
449
450impl<T, C> FmtWithCtx<C> for GExprBody<T>
451where
452    C: for<'a> SetLocals<'a>,
453    for<'a> <C as SetLocals<'a>>::C: AstFormatter,
454    for<'a, 'b> <C as SetLocals<'a>>::C: AstFormatter + Formatter<&'b T>,
455{
456    fn fmt_with_ctx(&self, ctx: &C) -> String {
457        // By default use a tab.
458        self.fmt_with_ctx_and_indent(TAB_INCR, ctx)
459    }
460
461    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
462        // Update the context
463        let ctx = &ctx.set_locals(&self.locals);
464
465        // Format the local variables
466        let mut locals: Vec<String> = Vec::new();
467        for v in &self.locals.locals {
468            let index = v.index.index();
469            let comment = if index == 0 {
470                "// return".to_string()
471            } else if index <= self.locals.arg_count {
472                format!("// arg #{index}").to_string()
473            } else {
474                match &v.name {
475                    Some(_) => "// local".to_string(),
476                    None => "// anonymous local".to_string(),
477                }
478            };
479
480            let var_id = v.index.to_pretty_string();
481            let var_name = match &v.name {
482                Some(name) => format!("{name}{var_id}"),
483                None => var_id,
484            };
485
486            locals.push(
487                format!(
488                    "{tab}let {var_name}: {}; {comment}\n",
489                    v.ty.fmt_with_ctx(ctx),
490                )
491                .to_string(),
492            );
493        }
494
495        let mut locals = locals.join("");
496        locals.push('\n');
497
498        // Format the body blocks - TODO: we don't take the indentation
499        // into account, here
500        let body = ctx.format_object(&self.body);
501
502        // Put everything together
503        let mut out = locals;
504        out.push_str(&body);
505        out
506    }
507}
508
509impl<C> FmtWithCtx<C> for FunDecl
510where
511    C: AstFormatter,
512    // For the signature
513    C: for<'a> SetGenerics<'a>,
514    for<'a> <C as SetGenerics<'a>>::C: AstFormatter,
515    // For the body
516    for<'a, 'b> <C as SetGenerics<'a>>::C: SetLocals<'b>,
517    for<'a, 'b> <<C as SetGenerics<'a>>::C as SetLocals<'b>>::C: AstFormatter,
518{
519    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
520        let keyword = if self.signature.is_unsafe {
521            "unsafe fn"
522        } else {
523            "fn"
524        };
525        let intro = self.item_meta.fmt_item_intro(ctx, tab, keyword);
526
527        // Update the context
528        let ctx = &ctx.set_generics(&self.signature.generics);
529
530        // Generic parameters
531        let (params, preds) = self
532            .signature
533            .generics
534            .fmt_with_ctx_with_trait_clauses(ctx, tab);
535
536        // Arguments
537        let mut args: Vec<String> = Vec::new();
538        for i in 0..self.signature.inputs.len() {
539            // The input variables start at index 1
540            let id = LocalId::new(i + 1);
541            let arg_ty = &self.signature.inputs.get(i).unwrap();
542            args.push(
543                format!("{}: {}", id.to_pretty_string(), arg_ty.fmt_with_ctx(ctx)).to_string(),
544            );
545        }
546        let args = args.join(", ");
547
548        // Return type
549        let ret_ty = &self.signature.output;
550        let ret_ty = if ret_ty.is_unit() {
551            "".to_string()
552        } else {
553            format!(" -> {}", ret_ty.fmt_with_ctx(ctx))
554        };
555
556        // Body
557        let body = match &self.body {
558            Ok(body) => {
559                let body = body.fmt_with_ctx(ctx);
560                format!("\n{tab}{{\n{body}{tab}}}")
561            }
562            Err(Opaque) => String::new(),
563        };
564
565        // Put everything together
566        format!("{intro}{params}({args}){ret_ty}{preds}{body}",)
567    }
568}
569
570impl<C: AstFormatter> FmtWithCtx<C> for FunDeclRef {
571    fn fmt_with_ctx(&self, ctx: &C) -> String {
572        let id = ctx.format_object(self.id);
573        let generics = self.generics.fmt_with_ctx(ctx);
574        format!("{id}{generics}")
575    }
576}
577
578impl<C> FmtWithCtx<C> for GlobalDecl
579where
580    C: AstFormatter,
581    C: for<'a> SetLocals<'a>,
582    for<'a> <C as SetGenerics<'a>>::C: AstFormatter,
583    for<'a, 'b> <<C as SetGenerics<'a>>::C as SetLocals<'b>>::C: AstFormatter,
584    for<'a, 'b, 'c> <<C as SetGenerics<'a>>::C as SetLocals<'b>>::C: AstFormatter,
585{
586    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
587        let keyword = match self.global_kind {
588            GlobalKind::Static => "static",
589            GlobalKind::AnonConst | GlobalKind::NamedConst => "const",
590        };
591        let intro = self.item_meta.fmt_item_intro(ctx, tab, keyword);
592
593        // Update the context with the generics
594        let ctx = &ctx.set_generics(&self.generics);
595
596        // Translate the parameters and the trait clauses
597        let (params, preds) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "  ");
598        // Type
599        let ty = self.ty.fmt_with_ctx(ctx);
600        // Predicates
601        let eq_space = if !self.generics.has_predicates() {
602            " ".to_string()
603        } else {
604            "\n ".to_string()
605        };
606
607        // Decl name
608        let initializer = ctx.format_object(self.init);
609
610        // Put everything together
611        format!("{intro}{params}: {ty}{preds}{eq_space}= {initializer}()")
612    }
613}
614
615impl<C: AstFormatter> FmtWithCtx<C> for GlobalDeclRef {
616    fn fmt_with_ctx(&self, ctx: &C) -> String {
617        let id = ctx.format_object(self.id);
618        let generics = self.generics.fmt_with_ctx(ctx);
619        format!("{id}{generics}")
620    }
621}
622
623impl<C: AstFormatter> FmtWithCtx<C> for ImplElem {
624    fn fmt_with_ctx(&self, ctx: &C) -> String {
625        ctx.format_object(self)
626    }
627}
628
629impl ItemMeta {
630    /// Format the start of an item definition, up to the name.
631    pub fn fmt_item_intro<C>(&self, ctx: &C, tab: &str, keyword: &str) -> String
632    where
633        C: AstFormatter,
634    {
635        let name = self.name.fmt_with_ctx(ctx);
636        let vis = if self.attr_info.public { "pub " } else { "" };
637        let lang_item = self
638            .lang_item
639            .as_ref()
640            .map(|id| format!("{tab}#[lang_item(\"{id}\")]\n"))
641            .unwrap_or_default();
642        format!("{lang_item}{tab}{vis}{keyword} {name}")
643    }
644}
645
646impl<C: AstFormatter> FmtWithCtx<C> for LiteralTy {
647    fn fmt_with_ctx(&self, _ctx: &C) -> String {
648        match self {
649            LiteralTy::Integer(ty) => ty.to_string(),
650            LiteralTy::Float(ty) => ty.to_string(),
651            LiteralTy::Char => "char".to_owned(),
652            LiteralTy::Bool => "bool".to_owned(),
653        }
654    }
655}
656
657impl<C: AstFormatter> FmtWithCtx<C> for Name {
658    fn fmt_with_ctx(&self, ctx: &C) -> String {
659        let name = self
660            .name
661            .iter()
662            .map(|x| x.fmt_with_ctx(ctx))
663            .collect::<Vec<String>>();
664        name.join("::")
665    }
666}
667
668impl<C: AstFormatter> FmtWithCtx<C> for NullOp {
669    fn fmt_with_ctx(&self, _ctx: &C) -> String {
670        match self {
671            NullOp::SizeOf => "size_of".to_string(),
672            NullOp::AlignOf => "align_of".to_string(),
673            NullOp::OffsetOf(_) => "offset_of(?)".to_string(),
674            NullOp::UbChecks => "ub_checks".to_string(),
675        }
676    }
677}
678
679impl<C: AstFormatter> FmtWithCtx<C> for Operand {
680    fn fmt_with_ctx(&self, ctx: &C) -> String {
681        match self {
682            Operand::Copy(p) => format!("copy ({})", p.fmt_with_ctx(ctx)),
683            Operand::Move(p) => format!("move ({})", p.fmt_with_ctx(ctx)),
684            Operand::Const(c) => format!("const ({})", c.fmt_with_ctx(ctx)),
685        }
686    }
687}
688
689impl<C: AstFormatter, T, U> FmtWithCtx<C> for OutlivesPred<T, U>
690where
691    T: FmtWithCtx<C>,
692    U: FmtWithCtx<C>,
693{
694    fn fmt_with_ctx(&self, ctx: &C) -> String {
695        format!(
696            "{} : {}",
697            self.0.fmt_with_ctx(ctx),
698            self.1.fmt_with_ctx(ctx)
699        )
700    }
701}
702
703impl<C: AstFormatter> FmtWithCtx<C> for PathElem {
704    fn fmt_with_ctx(&self, ctx: &C) -> String {
705        match self {
706            PathElem::Ident(s, d) => {
707                let d = if d.is_zero() {
708                    "".to_string()
709                } else {
710                    format!("#{}", d)
711                };
712                format!("{s}{d}")
713            }
714            PathElem::Impl(impl_elem, d) => {
715                let impl_elem = impl_elem.fmt_with_ctx(ctx);
716                let d = if d.is_zero() {
717                    "".to_string()
718                } else {
719                    format!("#{}", d)
720                };
721                format!("{impl_elem}{d}")
722            }
723        }
724    }
725}
726
727impl<C: AstFormatter> FmtWithCtx<C> for Place {
728    fn fmt_with_ctx(&self, ctx: &C) -> String {
729        match &self.kind {
730            PlaceKind::Local(var_id) => ctx.format_object(*var_id),
731            PlaceKind::Projection(subplace, projection) => {
732                let sub = subplace.fmt_with_ctx(ctx);
733                match projection {
734                    ProjectionElem::Deref => {
735                        format!("*({sub})")
736                    }
737                    ProjectionElem::Field(proj_kind, field_id) => match proj_kind {
738                        FieldProjKind::Adt(adt_id, opt_variant_id) => {
739                            let field_name =
740                                ctx.format_object((*adt_id, *opt_variant_id, *field_id));
741                            let downcast = match opt_variant_id {
742                                None => "".to_string(),
743                                Some(variant_id) => format!(" as variant @{variant_id}"),
744                            };
745                            format!("({sub}{downcast}).{field_name}")
746                        }
747                        FieldProjKind::Tuple(_) => {
748                            format!("({sub}).{field_id}")
749                        }
750                        FieldProjKind::ClosureState => {
751                            format!("({sub}).@closure_state_field_{field_id}")
752                        }
753                    },
754                    ProjectionElem::Index {
755                        offset,
756                        from_end: true,
757                        ..
758                    } => format!("({sub})[-{}]", offset.fmt_with_ctx(ctx)),
759                    ProjectionElem::Index {
760                        offset,
761                        from_end: false,
762                        ..
763                    } => format!("({sub})[{}]", offset.fmt_with_ctx(ctx)),
764                    ProjectionElem::Subslice {
765                        from,
766                        to,
767                        from_end: true,
768                        ..
769                    } => format!(
770                        "({sub})[{}..-{}]",
771                        from.fmt_with_ctx(ctx),
772                        to.fmt_with_ctx(ctx)
773                    ),
774                    ProjectionElem::Subslice {
775                        from,
776                        to,
777                        from_end: false,
778                        ..
779                    } => format!(
780                        "({sub})[{}..{}]",
781                        from.fmt_with_ctx(ctx),
782                        to.fmt_with_ctx(ctx)
783                    ),
784                }
785            }
786        }
787    }
788}
789
790impl<C: AstFormatter> FmtWithCtx<C> for PolyTraitDeclRef {
791    fn fmt_with_ctx(&self, ctx: &C) -> String {
792        self.fmt_as_for(ctx)
793    }
794}
795
796impl<C: AstFormatter> FmtWithCtx<C> for RawConstantExpr {
797    fn fmt_with_ctx(&self, ctx: &C) -> String {
798        match self {
799            RawConstantExpr::Literal(c) => c.to_string(),
800            RawConstantExpr::Adt(variant_id, values) => {
801                // It is a bit annoying: in order to properly format the value,
802                // we need the type (which contains the type def id).
803                // Anyway, the printing utilities are mostly for debugging.
804                let variant_id = match variant_id {
805                    Some(id) => format!("Some({id})"),
806                    None => "None".to_string(),
807                };
808                let values: Vec<String> = values.iter().map(|v| v.fmt_with_ctx(ctx)).collect();
809                format!("ConstAdt {} [{}]", variant_id, values.join(", "))
810            }
811            RawConstantExpr::Array(values) => {
812                let values = values.iter().map(|v| v.fmt_with_ctx(ctx)).format(", ");
813                format!("[{}]", values)
814            }
815            RawConstantExpr::Global(global_ref) => global_ref.fmt_with_ctx(ctx),
816            RawConstantExpr::TraitConst(trait_ref, name) => {
817                format!("{}::{name}", trait_ref.fmt_with_ctx(ctx),)
818            }
819            RawConstantExpr::Ref(cv) => {
820                format!("&{}", cv.fmt_with_ctx(ctx))
821            }
822            RawConstantExpr::MutPtr(cv) => {
823                format!("&raw mut {}", cv.fmt_with_ctx(ctx))
824            }
825            RawConstantExpr::Var(id) => format!("{}", ctx.format_object(*id)),
826            RawConstantExpr::FnPtr(f) => {
827                format!("{}", f.fmt_with_ctx(ctx))
828            }
829            RawConstantExpr::RawMemory(bytes) => format!("RawMemory({bytes:?})"),
830            RawConstantExpr::Opaque(cause) => format!("Opaque({cause})"),
831        }
832    }
833}
834
835impl<C: AstFormatter> FmtWithCtx<C> for Region {
836    fn fmt_with_ctx(&self, ctx: &C) -> String {
837        match self {
838            Region::Static => "'static".to_string(),
839            Region::Var(var) => ctx.format_object(*var),
840            Region::Erased => "'_".to_string(),
841        }
842    }
843}
844
845impl Region {
846    pub fn fmt_without_ctx(&self) -> String {
847        match self {
848            Region::Static => "'static".to_string(),
849            Region::Var(var) => format!("'_{var}"),
850            Region::Erased => "'_".to_string(),
851        }
852    }
853}
854
855impl<T> RegionBinder<T> {
856    /// Format the parameters and contents of this binder and returns the resulting strings.
857    fn fmt_split<'a, C>(&'a self, ctx: &'a C) -> (String, String)
858    where
859        C: AstFormatter,
860        T: FmtWithCtx<<C as PushBinder<'a>>::C>,
861    {
862        let ctx = &ctx.push_bound_regions(&self.regions);
863        (
864            self.regions.iter().map(|r| ctx.format_object(r)).join(", "),
865            self.skip_binder.fmt_with_ctx(ctx),
866        )
867    }
868
869    /// Formats the binder as `for<params> value`.
870    fn fmt_as_for<'a, C>(&'a self, ctx: &'a C) -> String
871    where
872        C: AstFormatter,
873        T: FmtWithCtx<<C as PushBinder<'a>>::C>,
874    {
875        let (regions, value) = self.fmt_split(ctx);
876        let regions = if regions.is_empty() {
877            "".to_string()
878        } else {
879            format!("for<{regions}> ",)
880        };
881        format!("{regions}{value}",)
882    }
883}
884
885impl<C: AstFormatter> FmtWithCtx<C> for RegionVar {
886    fn fmt_with_ctx(&self, ctx: &C) -> String {
887        ctx.format_object(self)
888    }
889}
890
891impl<C: AstFormatter> FmtWithCtx<C> for Rvalue {
892    fn fmt_with_ctx(&self, ctx: &C) -> String {
893        match self {
894            Rvalue::Use(x) => x.fmt_with_ctx(ctx),
895            Rvalue::Ref(place, borrow_kind) => {
896                let borrow_kind = match borrow_kind {
897                    BorrowKind::Shared => "&",
898                    BorrowKind::Mut => "&mut ",
899                    BorrowKind::TwoPhaseMut => "&two-phase-mut ",
900                    BorrowKind::UniqueImmutable => "&uniq ",
901                    BorrowKind::Shallow => "&shallow ",
902                };
903                format!("{borrow_kind}{}", place.fmt_with_ctx(ctx))
904            }
905            Rvalue::RawPtr(place, mutability) => {
906                let ptr_kind = match mutability {
907                    RefKind::Shared => "&raw const ",
908                    RefKind::Mut => "&raw mut ",
909                };
910                format!("{ptr_kind}{}", place.fmt_with_ctx(ctx))
911            }
912
913            Rvalue::BinaryOp(binop, x, y) => {
914                format!("{} {} {}", x.fmt_with_ctx(ctx), binop, y.fmt_with_ctx(ctx))
915            }
916            Rvalue::UnaryOp(unop, x) => {
917                format!("{}({})", unop.fmt_with_ctx(ctx), x.fmt_with_ctx(ctx))
918            }
919            Rvalue::NullaryOp(op, ty) => {
920                format!("{}<{}>", op.fmt_with_ctx(ctx), ty.fmt_with_ctx(ctx))
921            }
922            Rvalue::Discriminant(p, _) => {
923                format!("@discriminant({})", p.fmt_with_ctx(ctx),)
924            }
925            Rvalue::Aggregate(kind, ops) => {
926                let ops_s: Vec<String> = ops.iter().map(|op| op.fmt_with_ctx(ctx)).collect();
927                match kind {
928                    AggregateKind::Adt(def_id, variant_id, field_id, _) => {
929                        match def_id {
930                            TypeId::Tuple => format!("({})", ops_s.join(", ")),
931                            TypeId::Builtin(_) => unreachable!(),
932                            TypeId::Adt(def_id) => {
933                                // Format every field
934                                let mut fields = vec![];
935                                for (i, op) in ops.iter().enumerate() {
936                                    let field_id = match *field_id {
937                                        None => FieldId::new(i),
938                                        Some(field_id) => {
939                                            assert_eq!(i, 0); // there should be only one operand
940                                            field_id
941                                        }
942                                    };
943                                    let field_name =
944                                        ctx.format_object((*def_id, *variant_id, field_id));
945                                    fields.push(format!(
946                                        "{}: {}",
947                                        field_name,
948                                        op.fmt_with_ctx(ctx)
949                                    ));
950                                }
951
952                                let variant = match variant_id {
953                                    None => ctx.format_object(*def_id),
954                                    Some(variant_id) => ctx.format_object((*def_id, *variant_id)),
955                                };
956                                format!("{} {{ {} }}", variant, fields.join(", "))
957                            }
958                        }
959                    }
960                    AggregateKind::Array(..) => {
961                        format!("[{}]", ops_s.join(", "))
962                    }
963                    AggregateKind::Closure(fn_id, generics) => {
964                        format!(
965                            "{{{}{}}} {{{}}}",
966                            ctx.format_object(*fn_id),
967                            generics.fmt_with_ctx(ctx),
968                            ops_s.join(", ")
969                        )
970                    }
971                    AggregateKind::RawPtr(_, rmut) => {
972                        let mutability = match rmut {
973                            RefKind::Shared => "const",
974                            RefKind::Mut => "mut ",
975                        };
976                        format!("*{} ({})", mutability, ops_s.join(", "))
977                    }
978                }
979            }
980            Rvalue::Global(global_ref) => global_ref.fmt_with_ctx(ctx),
981            Rvalue::GlobalRef(global_ref, RefKind::Shared) => {
982                format!("&{}", global_ref.fmt_with_ctx(ctx))
983            }
984            Rvalue::GlobalRef(global_ref, RefKind::Mut) => {
985                format!("&raw mut {}", global_ref.fmt_with_ctx(ctx))
986            }
987            Rvalue::Len(place, ..) => format!("len({})", place.fmt_with_ctx(ctx)),
988            Rvalue::Repeat(op, _ty, cg) => {
989                format!("[{}; {}]", op.fmt_with_ctx(ctx), cg.fmt_with_ctx(ctx))
990            }
991            Rvalue::ShallowInitBox(op, ty) => {
992                format!(
993                    "shallow_init_box::<{}>({})",
994                    ty.fmt_with_ctx(ctx),
995                    op.fmt_with_ctx(ctx)
996                )
997            }
998        }
999    }
1000}
1001
1002impl<C: AstFormatter> FmtWithCtx<C> for ullbc::Statement {
1003    fn fmt_with_ctx(&self, ctx: &C) -> String {
1004        // By default use a tab.
1005        self.fmt_with_ctx_and_indent(TAB_INCR, ctx)
1006    }
1007
1008    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
1009        use ullbc::RawStatement;
1010        let mut out = String::new();
1011        for line in &self.comments_before {
1012            let _ = writeln!(&mut out, "{tab}// {line}");
1013        }
1014        let _ = match &self.content {
1015            RawStatement::Assign(place, rvalue) => write!(
1016                &mut out,
1017                "{tab}{} := {}",
1018                place.fmt_with_ctx(ctx),
1019                rvalue.fmt_with_ctx(ctx),
1020            ),
1021            RawStatement::SetDiscriminant(place, variant_id) => write!(
1022                &mut out,
1023                "{tab}@discriminant({}) := {}",
1024                place.fmt_with_ctx(ctx),
1025                variant_id
1026            ),
1027            RawStatement::StorageLive(var_id) => {
1028                write!(
1029                    &mut out,
1030                    "{tab}storage_live({})",
1031                    ctx.format_object(*var_id)
1032                )
1033            }
1034            RawStatement::StorageDead(var_id) => {
1035                write!(
1036                    &mut out,
1037                    "{tab}storage_dead({})",
1038                    ctx.format_object(*var_id)
1039                )
1040            }
1041            RawStatement::Deinit(place) => {
1042                write!(&mut out, "{tab}deinit({})", place.fmt_with_ctx(ctx))
1043            }
1044            RawStatement::Drop(place) => {
1045                write!(&mut out, "{tab}drop {}", place.fmt_with_ctx(ctx))
1046            }
1047            RawStatement::Assert(assert) => write!(&mut out, "{tab}{}", assert.fmt_with_ctx(ctx)),
1048            RawStatement::Nop => write!(&mut out, "{tab}nop"),
1049            RawStatement::Error(s) => write!(&mut out, "{tab}@Error({})", s),
1050        };
1051        out
1052    }
1053}
1054
1055impl<C: AstFormatter> FmtWithCtx<C> for llbc::Statement {
1056    fn fmt_with_ctx(&self, ctx: &C) -> String {
1057        // By default use a tab.
1058        self.fmt_with_ctx_and_indent(TAB_INCR, ctx)
1059    }
1060
1061    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
1062        use llbc::RawStatement;
1063        let mut out = String::new();
1064        for line in &self.comments_before {
1065            let _ = writeln!(&mut out, "{tab}// {line}");
1066        }
1067        let _ = match &self.content {
1068            RawStatement::Assign(place, rvalue) => write!(
1069                &mut out,
1070                "{}{} := {}",
1071                tab,
1072                place.fmt_with_ctx(ctx),
1073                rvalue.fmt_with_ctx(ctx),
1074            ),
1075            RawStatement::SetDiscriminant(place, variant_id) => write!(
1076                &mut out,
1077                "{}@discriminant({}) := {}",
1078                tab,
1079                place.fmt_with_ctx(ctx),
1080                variant_id
1081            ),
1082            RawStatement::StorageLive(var_id) => {
1083                write!(
1084                    &mut out,
1085                    "{tab}storage_live({})",
1086                    ctx.format_object(*var_id)
1087                )
1088            }
1089            RawStatement::StorageDead(var_id) => {
1090                write!(
1091                    &mut out,
1092                    "{tab}storage_dead({})",
1093                    ctx.format_object(*var_id)
1094                )
1095            }
1096            RawStatement::Deinit(place) => {
1097                write!(&mut out, "{tab}deinit({})", place.fmt_with_ctx(ctx))
1098            }
1099            RawStatement::Drop(place) => {
1100                write!(&mut out, "{tab}drop {}", place.fmt_with_ctx(ctx))
1101            }
1102            RawStatement::Assert(assert) => {
1103                write!(&mut out, "{tab}{}", assert.fmt_with_ctx(ctx),)
1104            }
1105            RawStatement::Call(call) => {
1106                let (call_s, _) = fmt_call(ctx, call);
1107                write!(&mut out, "{tab}{} := {call_s}", call.dest.fmt_with_ctx(ctx),)
1108            }
1109            RawStatement::Abort(kind) => {
1110                write!(&mut out, "{}", kind.fmt_with_ctx_and_indent(tab, ctx))
1111            }
1112            RawStatement::Return => write!(&mut out, "{tab}return"),
1113            RawStatement::Break(index) => write!(&mut out, "{tab}break {index}"),
1114            RawStatement::Continue(index) => write!(&mut out, "{tab}continue {index}"),
1115            RawStatement::Nop => write!(&mut out, "{tab}nop"),
1116            RawStatement::Switch(switch) => match switch {
1117                Switch::If(discr, true_st, false_st) => {
1118                    let inner_tab = format!("{tab}{TAB_INCR}");
1119                    write!(
1120                        &mut out,
1121                        "{tab}if {} {{\n{}{tab}}}\n{tab}else {{\n{}{tab}}}",
1122                        discr.fmt_with_ctx(ctx),
1123                        true_st.fmt_with_ctx_and_indent(&inner_tab, ctx),
1124                        false_st.fmt_with_ctx_and_indent(&inner_tab, ctx),
1125                    )
1126                }
1127                Switch::SwitchInt(discr, _ty, maps, otherwise) => {
1128                    let inner_tab1 = format!("{tab}{TAB_INCR}");
1129                    let inner_tab2 = format!("{inner_tab1}{TAB_INCR}");
1130                    let mut maps: Vec<String> = maps
1131                        .iter()
1132                        .map(|(pvl, st)| {
1133                            // Note that there may be several pattern values
1134                            let pvl: Vec<String> = pvl.iter().map(|v| v.to_string()).collect();
1135                            format!(
1136                                "{inner_tab1}{} => {{\n{}{inner_tab1}}},\n",
1137                                pvl.join(" | "),
1138                                st.fmt_with_ctx_and_indent(&inner_tab2, ctx),
1139                            )
1140                        })
1141                        .collect();
1142                    maps.push(format!(
1143                        "{inner_tab1}_ => {{\n{}{inner_tab1}}},\n",
1144                        otherwise.fmt_with_ctx_and_indent(&inner_tab2, ctx),
1145                    ));
1146
1147                    write!(
1148                        &mut out,
1149                        "{tab}switch {} {{\n{}{tab}}}",
1150                        discr.fmt_with_ctx(ctx),
1151                        maps.iter().format(""),
1152                    )
1153                }
1154                Switch::Match(discr, maps, otherwise) => {
1155                    let inner_tab1 = format!("{tab}{TAB_INCR}");
1156                    let inner_tab2 = format!("{inner_tab1}{TAB_INCR}");
1157                    let discr_type: Option<TypeDeclId> = discr
1158                        .ty
1159                        .kind()
1160                        .as_adt()
1161                        .and_then(|(x, _)| x.as_adt())
1162                        .copied();
1163                    let mut maps: Vec<String> = maps
1164                        .iter()
1165                        .map(|(cases, st)| {
1166                            // Note that there may be several pattern values
1167                            let cases: Vec<String> = cases
1168                                .iter()
1169                                .map(|v| match discr_type {
1170                                    Some(type_id) => ctx.format_object((type_id, *v)),
1171                                    None => v.to_pretty_string(),
1172                                })
1173                                .collect();
1174                            format!(
1175                                "{inner_tab1}{} => {{\n{}{inner_tab1}}},\n",
1176                                cases.join(" | "),
1177                                st.fmt_with_ctx_and_indent(&inner_tab2, ctx),
1178                            )
1179                        })
1180                        .collect();
1181                    if let Some(otherwise) = otherwise {
1182                        maps.push(format!(
1183                            "{inner_tab1}_ => {{\n{}{inner_tab1}}},\n",
1184                            otherwise.fmt_with_ctx_and_indent(&inner_tab2, ctx),
1185                        ));
1186                    };
1187
1188                    write!(
1189                        &mut out,
1190                        "{tab}match {} {{\n{}{tab}}}",
1191                        discr.fmt_with_ctx(ctx),
1192                        maps.iter().format(""),
1193                    )
1194                }
1195            },
1196            RawStatement::Loop(body) => {
1197                let inner_tab = format!("{tab}{TAB_INCR}");
1198                write!(
1199                    &mut out,
1200                    "{tab}loop {{\n{}{tab}}}",
1201                    body.fmt_with_ctx_and_indent(&inner_tab, ctx),
1202                )
1203            }
1204            RawStatement::Error(s) => write!(&mut out, "{tab}@ERROR({})", s),
1205        };
1206        out
1207    }
1208}
1209
1210impl<C: AstFormatter> FmtWithCtx<C> for Terminator {
1211    fn fmt_with_ctx(&self, ctx: &C) -> String {
1212        // By default use a tab.
1213        self.fmt_with_ctx_and_indent(TAB_INCR, ctx)
1214    }
1215
1216    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
1217        let mut out = String::new();
1218        for line in &self.comments_before {
1219            let _ = writeln!(&mut out, "{tab}// {line}");
1220        }
1221        let _ = match &self.content {
1222            RawTerminator::Goto { target } => write!(&mut out, "{tab}goto bb{target}"),
1223            RawTerminator::Switch { discr, targets } => match targets {
1224                SwitchTargets::If(true_block, false_block) => write!(
1225                    &mut out,
1226                    "{tab}if {} -> bb{} else -> bb{}",
1227                    discr.fmt_with_ctx(ctx),
1228                    true_block,
1229                    false_block
1230                ),
1231                SwitchTargets::SwitchInt(_ty, maps, otherwise) => {
1232                    let mut maps: Vec<String> = maps
1233                        .iter()
1234                        .map(|(v, bid)| format!("{}: bb{}", v.to_string(), bid))
1235                        .collect();
1236                    maps.push(format!("otherwise: bb{otherwise}"));
1237                    let maps = maps.join(", ");
1238
1239                    write!(
1240                        &mut out,
1241                        "{tab}switch {} -> {}",
1242                        discr.fmt_with_ctx(ctx),
1243                        maps
1244                    )
1245                }
1246            },
1247            RawTerminator::Call { call, target } => {
1248                let (call_s, _) = fmt_call(ctx, call);
1249                write!(
1250                    &mut out,
1251                    "{tab}{} := {call_s} -> bb{target}",
1252                    call.dest.fmt_with_ctx(ctx)
1253                )
1254            }
1255            RawTerminator::Abort(kind) => write!(&mut out, "{tab}{}", kind.fmt_with_ctx(ctx)),
1256            RawTerminator::Return => write!(&mut out, "{tab}return"),
1257        };
1258        out
1259    }
1260}
1261
1262impl<C: AstFormatter> FmtWithCtx<C> for TraitClause {
1263    fn fmt_with_ctx(&self, ctx: &C) -> String {
1264        let clause_id = self.clause_id.to_pretty_string();
1265        let trait_ = self.trait_.fmt_with_ctx(ctx);
1266        format!("[{clause_id}]: {trait_}")
1267    }
1268}
1269
1270impl<C: AstFormatter> FmtWithCtx<C> for TraitDecl {
1271    fn fmt_with_ctx(&self, ctx: &C) -> String {
1272        let intro = self.item_meta.fmt_item_intro(ctx, "", "trait");
1273
1274        // Update the context
1275        let ctx = &ctx.set_generics(&self.generics);
1276
1277        let (generics, clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "");
1278
1279        let items = {
1280            let items = self
1281                .parent_clauses
1282                .iter()
1283                .map(|c| {
1284                    format!(
1285                        "{TAB_INCR}parent_clause{} : {}\n",
1286                        c.clause_id,
1287                        c.fmt_with_ctx(ctx)
1288                    )
1289                })
1290                .chain(self.type_clauses.iter().map(|(name, clauses)| {
1291                    clauses
1292                        .iter()
1293                        .map(|c| {
1294                            format!(
1295                                "{TAB_INCR}item_clause_{name}_{} : {}\n",
1296                                c.clause_id.to_string(),
1297                                c.fmt_with_ctx(ctx)
1298                            )
1299                        })
1300                        .collect()
1301                }))
1302                .chain(self.consts.iter().map(|(name, ty)| {
1303                    let ty = ty.fmt_with_ctx(ctx);
1304                    format!("{TAB_INCR}const {name} : {ty}\n")
1305                }))
1306                .chain(
1307                    self.types
1308                        .iter()
1309                        .map(|name| format!("{TAB_INCR}type {name}\n")),
1310                )
1311                .chain(self.methods().map(|(name, bound_fn)| {
1312                    let (params, fn_ref) = bound_fn.fmt_split(ctx);
1313                    format!("{TAB_INCR}fn {name}{params} = {fn_ref}\n",)
1314                }))
1315                .collect::<Vec<String>>();
1316            if items.is_empty() {
1317                "".to_string()
1318            } else {
1319                format!("\n{{\n{}}}", items.join(""))
1320            }
1321        };
1322
1323        format!("{intro}{generics}{clauses}{items}")
1324    }
1325}
1326
1327impl<C: AstFormatter> FmtWithCtx<C> for TraitDeclRef {
1328    fn fmt_with_ctx(&self, ctx: &C) -> String {
1329        let trait_id = ctx.format_object(self.trait_id);
1330        let generics = self.generics.fmt_with_ctx(ctx);
1331        format!("{trait_id}{generics}")
1332    }
1333}
1334
1335impl<C: AstFormatter> FmtWithCtx<C> for TraitImpl {
1336    fn fmt_with_ctx(&self, ctx: &C) -> String {
1337        let intro = self.item_meta.fmt_item_intro(ctx, "", "impl");
1338
1339        // Update the context
1340        let ctx = &ctx.set_generics(&self.generics);
1341
1342        let (generics, clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "");
1343
1344        let items = {
1345            let items = self
1346                .parent_trait_refs
1347                .iter()
1348                .enumerate()
1349                .map(|(i, clause)| {
1350                    let i = TraitClauseId::new(i);
1351                    format!(
1352                        "{TAB_INCR}parent_clause{i} = {}\n",
1353                        clause.fmt_with_ctx(ctx)
1354                    )
1355                })
1356                .chain(self.type_clauses.iter().map(|(name, clauses)| {
1357                    clauses
1358                        .iter()
1359                        .enumerate()
1360                        .map(|(i, c)| {
1361                            let i = TraitClauseId::new(i);
1362                            format!(
1363                                "{TAB_INCR}item_clause_{name}_{i} = {}\n",
1364                                c.fmt_with_ctx(ctx)
1365                            )
1366                        })
1367                        .collect()
1368                }))
1369                .chain(self.consts.iter().map(|(name, global)| {
1370                    format!("{TAB_INCR}const {name} = {}\n", global.fmt_with_ctx(ctx))
1371                }))
1372                .chain(self.types.iter().map(|(name, ty)| {
1373                    format!("{TAB_INCR}type {name} = {}\n", ty.fmt_with_ctx(ctx),)
1374                }))
1375                .chain(self.methods().map(|(name, bound_fn)| {
1376                    let (params, fn_ref) = bound_fn.fmt_split(ctx);
1377                    format!("{TAB_INCR}fn {name}{params} = {fn_ref}\n",)
1378                }))
1379                .collect::<Vec<String>>();
1380            if items.is_empty() {
1381                "".to_string()
1382            } else {
1383                format!("\n{{\n{}}}", items.join(""))
1384            }
1385        };
1386
1387        let impl_trait = self.impl_trait.fmt_with_ctx(ctx);
1388        format!("{intro}{generics} : {impl_trait}{clauses}{items}")
1389    }
1390}
1391
1392impl<C: AstFormatter> FmtWithCtx<C> for TraitRefKind {
1393    fn fmt_with_ctx(&self, ctx: &C) -> String {
1394        match self {
1395            TraitRefKind::SelfId => "Self".to_string(),
1396            TraitRefKind::ParentClause(id, _decl_id, clause_id) => {
1397                let id = id.fmt_with_ctx(ctx);
1398                format!("{id}::parent_clause{clause_id}")
1399            }
1400            TraitRefKind::ItemClause(id, _decl_id, type_name, clause_id) => {
1401                let id = id.fmt_with_ctx(ctx);
1402                // Using on purpose [to_pretty_string] instead of [format_object]:
1403                // the clause is local to the associated type, so it should not
1404                // be referenced in the current context.
1405                let clause = clause_id.to_pretty_string();
1406                format!("({id}::{type_name}::[{clause}])")
1407            }
1408            TraitRefKind::TraitImpl(id, args) => {
1409                let impl_ = ctx.format_object(*id);
1410                let args = args.fmt_with_ctx(ctx);
1411                format!("{impl_}{args}")
1412            }
1413            TraitRefKind::Clause(id) => ctx.format_object(*id),
1414            TraitRefKind::BuiltinOrAuto {
1415                trait_decl_ref: tr,
1416                types,
1417                ..
1418            } => {
1419                let tr = tr.fmt_with_ctx(ctx);
1420                let types = if types.is_empty() {
1421                    String::new()
1422                } else {
1423                    let types = types
1424                        .iter()
1425                        .map(|(name, ty)| {
1426                            let ty = ty.fmt_with_ctx(ctx);
1427                            format!("{name}  = {ty}")
1428                        })
1429                        .join(", ");
1430                    format!(" where {types}")
1431                };
1432                format!("{tr}{types}")
1433            }
1434            TraitRefKind::Dyn(tr) => tr.fmt_with_ctx(ctx),
1435            TraitRefKind::Unknown(msg) => format!("UNKNOWN({msg})"),
1436        }
1437    }
1438}
1439
1440impl<C: AstFormatter> FmtWithCtx<C> for TraitRef {
1441    fn fmt_with_ctx(&self, ctx: &C) -> String {
1442        self.kind.fmt_with_ctx(ctx)
1443    }
1444}
1445
1446impl<C: AstFormatter> FmtWithCtx<C> for TraitTypeConstraint {
1447    fn fmt_with_ctx(&self, ctx: &C) -> String {
1448        let trait_ref = self.trait_ref.fmt_with_ctx(ctx);
1449        let ty = self.ty.fmt_with_ctx(ctx);
1450        format!("{}::{} = {}", trait_ref, self.type_name, ty)
1451    }
1452}
1453
1454impl<C: AstFormatter> FmtWithCtx<C> for Ty {
1455    fn fmt_with_ctx(&self, ctx: &C) -> String {
1456        match self.kind() {
1457            TyKind::Adt(id, generics) => {
1458                let adt_ident = id.fmt_with_ctx(ctx);
1459
1460                if id.is_tuple() {
1461                    assert!(generics.trait_refs.is_empty());
1462                    let generics = generics.fmt_with_ctx_no_brackets(ctx);
1463                    format!("({generics})")
1464                } else {
1465                    let generics = generics.fmt_with_ctx(ctx);
1466                    format!("{adt_ident}{generics}")
1467                }
1468            }
1469            TyKind::Closure { fun_id, .. } => ctx.format_object(*fun_id),
1470            TyKind::TypeVar(id) => ctx.format_object(*id),
1471            TyKind::Literal(kind) => kind.to_string(),
1472            TyKind::Never => "!".to_string(),
1473            TyKind::Ref(r, ty, kind) => match kind {
1474                RefKind::Mut => {
1475                    format!("&{} mut ({})", r.fmt_with_ctx(ctx), ty.fmt_with_ctx(ctx))
1476                }
1477                RefKind::Shared => {
1478                    format!("&{} ({})", r.fmt_with_ctx(ctx), ty.fmt_with_ctx(ctx))
1479                }
1480            },
1481            TyKind::RawPtr(ty, kind) => match kind {
1482                RefKind::Shared => format!("*const {}", ty.fmt_with_ctx(ctx)),
1483                RefKind::Mut => format!("*mut {}", ty.fmt_with_ctx(ctx)),
1484            },
1485            TyKind::TraitType(trait_ref, name) => {
1486                format!("{}::{name}", trait_ref.fmt_with_ctx(ctx),)
1487            }
1488            TyKind::DynTrait(pred) => format!("dyn ({})", pred.with_ctx(ctx)),
1489            TyKind::Arrow(io) => {
1490                // Update the bound regions
1491                let ctx = &ctx.push_bound_regions(&io.regions);
1492
1493                let regions = if io.regions.is_empty() {
1494                    "".to_string()
1495                } else {
1496                    format!(
1497                        "<{}>",
1498                        io.regions.iter().map(|r| ctx.format_object(r)).join(", ")
1499                    )
1500                };
1501                let (inputs, output) = &io.skip_binder;
1502                let inputs = inputs
1503                    .iter()
1504                    .map(|x| x.fmt_with_ctx(ctx))
1505                    .collect::<Vec<String>>()
1506                    .join(", ");
1507                if output.is_unit() {
1508                    format!("fn{regions}({inputs})")
1509                } else {
1510                    let output = output.fmt_with_ctx(ctx);
1511                    format!("fn{regions}({inputs}) -> {output}")
1512                }
1513            }
1514            TyKind::Error(msg) => format!("type_error(\"{msg}\")"),
1515        }
1516    }
1517}
1518
1519impl<C: AstFormatter> FmtWithCtx<C> for TypeDecl {
1520    fn fmt_with_ctx(&self, ctx: &C) -> String {
1521        let keyword = match &self.kind {
1522            TypeDeclKind::Struct(..) => "struct",
1523            TypeDeclKind::Union(..) => "union",
1524            TypeDeclKind::Enum(..) => "enum",
1525            TypeDeclKind::Alias(..) => "type",
1526            TypeDeclKind::Opaque | TypeDeclKind::Error(..) => "opaque type",
1527        };
1528        let intro = self.item_meta.fmt_item_intro(ctx, "", keyword);
1529
1530        let ctx = &ctx.set_generics(&self.generics);
1531        let (params, preds) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "  ");
1532        // Predicates
1533        let nl_or_space = if !self.generics.has_predicates() {
1534            " ".to_string()
1535        } else {
1536            "\n ".to_string()
1537        };
1538
1539        let contents = match &self.kind {
1540            TypeDeclKind::Struct(fields) => {
1541                if !fields.is_empty() {
1542                    let fields = fields
1543                        .iter()
1544                        .map(|f| format!("\n  {},", f.fmt_with_ctx(ctx)))
1545                        .format("");
1546                    format!("{nl_or_space}=\n{{{fields}\n}}")
1547                } else {
1548                    format!("{nl_or_space}= {{}}")
1549                }
1550            }
1551            TypeDeclKind::Union(fields) => {
1552                let fields = fields
1553                    .iter()
1554                    .map(|f| format!("\n  {},", f.fmt_with_ctx(ctx)))
1555                    .format("");
1556                format!("{nl_or_space}=\n{{{fields}\n}}")
1557            }
1558            TypeDeclKind::Enum(variants) => {
1559                let variants = variants
1560                    .iter()
1561                    .map(|v| format!("|  {}", v.fmt_with_ctx(ctx)))
1562                    .format("\n");
1563                format!("{nl_or_space}=\n{variants}\n")
1564            }
1565            TypeDeclKind::Alias(ty) => format!(" = {}", ty.fmt_with_ctx(ctx)),
1566            TypeDeclKind::Opaque => format!(""),
1567            TypeDeclKind::Error(msg) => format!(" = ERROR({msg})"),
1568        };
1569        format!("{intro}{params}{preds}{contents}")
1570    }
1571}
1572
1573impl<C: AstFormatter> FmtWithCtx<C> for TypeId {
1574    fn fmt_with_ctx(&self, ctx: &C) -> String {
1575        match self {
1576            TypeId::Tuple => "".to_string(),
1577            TypeId::Adt(def_id) => ctx.format_object(*def_id),
1578            TypeId::Builtin(aty) => aty.get_name().fmt_with_ctx(ctx),
1579        }
1580    }
1581}
1582
1583impl<C: AstFormatter> FmtWithCtx<C> for TypeVar {
1584    fn fmt_with_ctx(&self, _ctx: &C) -> String {
1585        self.name.to_string()
1586    }
1587}
1588
1589impl<C: AstFormatter> FmtWithCtx<C> for UnOp {
1590    fn fmt_with_ctx(&self, ctx: &C) -> String {
1591        match self {
1592            UnOp::Not => "~".to_string(),
1593            UnOp::Neg => "-".to_string(),
1594            UnOp::PtrMetadata => "ptr_metadata".to_string(),
1595            UnOp::Cast(kind) => kind.fmt_with_ctx(ctx),
1596            UnOp::ArrayToSlice(..) => "array_to_slice".to_string(),
1597        }
1598    }
1599}
1600
1601impl<C: AstFormatter> FmtWithCtx<C> for Variant {
1602    fn fmt_with_ctx(&self, ctx: &C) -> String {
1603        let fields: Vec<String> = self.fields.iter().map(|f| f.fmt_with_ctx(ctx)).collect();
1604        let fields = fields.join(", ");
1605        format!("{}({})", self.name, fields)
1606    }
1607}
1608
1609impl std::fmt::Display for AnyTransId {
1610    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1611        let s = match self {
1612            AnyTransId::Type(x) => x.to_pretty_string(),
1613            AnyTransId::Fun(x) => x.to_pretty_string(),
1614            AnyTransId::Global(x) => x.to_pretty_string(),
1615            AnyTransId::TraitDecl(x) => x.to_pretty_string(),
1616            AnyTransId::TraitImpl(x) => x.to_pretty_string(),
1617        };
1618        f.write_str(&s)
1619    }
1620}
1621
1622impl std::fmt::Display for BinOp {
1623    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1624        match self {
1625            BinOp::BitXor => write!(f, "^"),
1626            BinOp::BitAnd => write!(f, "&"),
1627            BinOp::BitOr => write!(f, "|"),
1628            BinOp::Eq => write!(f, "=="),
1629            BinOp::Lt => write!(f, "<"),
1630            BinOp::Le => write!(f, "<="),
1631            BinOp::Ne => write!(f, "!="),
1632            BinOp::Ge => write!(f, ">="),
1633            BinOp::Gt => write!(f, ">"),
1634            BinOp::Div => write!(f, "/"),
1635            BinOp::Rem => write!(f, "%"),
1636            BinOp::Add => write!(f, "+"),
1637            BinOp::Sub => write!(f, "-"),
1638            BinOp::Mul => write!(f, "*"),
1639            BinOp::WrappingAdd => write!(f, "wrapping.+"),
1640            BinOp::WrappingSub => write!(f, "wrapping.-"),
1641            BinOp::WrappingMul => write!(f, "wrapping.*"),
1642            BinOp::CheckedAdd => write!(f, "checked.+"),
1643            BinOp::CheckedSub => write!(f, "checked.-"),
1644            BinOp::CheckedMul => write!(f, "checked.*"),
1645            BinOp::Shl => write!(f, "<<"),
1646            BinOp::Shr => write!(f, ">>"),
1647            BinOp::Cmp => write!(f, "cmp"),
1648            BinOp::Offset => write!(f, "offset"),
1649        }
1650    }
1651}
1652
1653impl std::fmt::Display for BorrowKind {
1654    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1655        // Reuse the derived `Debug` impl to get the variant name.
1656        write!(f, "{self:?}")
1657    }
1658}
1659
1660impl std::fmt::Display for BuiltinFunId {
1661    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1662        let name = match *self {
1663            BuiltinFunId::BoxNew => "BoxNew",
1664            BuiltinFunId::ArrayToSliceShared => "ArrayToSliceShared",
1665            BuiltinFunId::ArrayToSliceMut => "ArrayToSliceMut",
1666            BuiltinFunId::ArrayRepeat => "ArrayRepeat",
1667            BuiltinFunId::Index(BuiltinIndexOp {
1668                is_array,
1669                mutability,
1670                is_range,
1671            }) => {
1672                let ty = if is_array { "Array" } else { "Slice" };
1673                let op = if is_range { "SubSlice" } else { "Index" };
1674                let mutability = mutability.variant_name();
1675                &format!("{ty}{op}{mutability}")
1676            }
1677            BuiltinFunId::PtrFromParts(mutability) => {
1678                let mutability = mutability.variant_name();
1679                &format!("PtrFromParts{mutability}")
1680            }
1681        };
1682        f.write_str(name)
1683    }
1684}
1685
1686impl std::fmt::Display for DeBruijnId {
1687    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1688        write!(f, "{}", self.index)
1689    }
1690}
1691
1692impl<Id> Display for DeBruijnVar<Id>
1693where
1694    Id: Display,
1695{
1696    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1697        match self {
1698            Self::Bound(dbid, varid) => write!(f, "{dbid}_{varid}"),
1699            Self::Free(varid) => write!(f, "{varid}"),
1700        }
1701    }
1702}
1703
1704impl std::fmt::Display for ConstantExpr {
1705    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1706        write!(f, "{}", self.fmt_with_ctx(&FmtCtx::new()))
1707    }
1708}
1709
1710impl std::fmt::Display for FileName {
1711    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1712        match self {
1713            FileName::Virtual(path_buf) | FileName::Local(path_buf) => {
1714                write!(f, "{}", path_buf.display())
1715            }
1716            FileName::NotReal(name) => write!(f, "{}", name),
1717        }
1718    }
1719}
1720
1721impl std::fmt::Display for FloatTy {
1722    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1723        match self {
1724            FloatTy::F16 => write!(f, "f16"),
1725            FloatTy::F32 => write!(f, "f32"),
1726            FloatTy::F64 => write!(f, "f64"),
1727            FloatTy::F128 => write!(f, "f128"),
1728        }
1729    }
1730}
1731
1732impl std::fmt::Display for IntegerTy {
1733    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1734        match self {
1735            IntegerTy::Isize => write!(f, "isize"),
1736            IntegerTy::I8 => write!(f, "i8"),
1737            IntegerTy::I16 => write!(f, "i16"),
1738            IntegerTy::I32 => write!(f, "i32"),
1739            IntegerTy::I64 => write!(f, "i64"),
1740            IntegerTy::I128 => write!(f, "i128"),
1741            IntegerTy::Usize => write!(f, "usize"),
1742            IntegerTy::U8 => write!(f, "u8"),
1743            IntegerTy::U16 => write!(f, "u16"),
1744            IntegerTy::U32 => write!(f, "u32"),
1745            IntegerTy::U64 => write!(f, "u64"),
1746            IntegerTy::U128 => write!(f, "u128"),
1747        }
1748    }
1749}
1750
1751impl std::fmt::Display for GenericParams {
1752    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1753        write!(f, "{}", self.fmt_with_ctx_single_line(&FmtCtx::new()))
1754    }
1755}
1756
1757impl std::fmt::Display for Literal {
1758    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1759        match self {
1760            Literal::Scalar(v) => write!(f, "{v}"),
1761            Literal::Float(v) => write!(f, "{v}"),
1762            Literal::Bool(v) => write!(f, "{v}"),
1763            Literal::Char(v) => write!(f, "{v}"),
1764            Literal::Str(v) => write!(f, "\"{}\"", v.replace("\\", "\\\\").replace("\n", "\\n")),
1765            Literal::ByteStr(v) => write!(f, "{v:?}"),
1766        }
1767    }
1768}
1769
1770impl std::fmt::Display for Loc {
1771    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1772        write!(f, "{}:{}", self.line, self.col)
1773    }
1774}
1775
1776impl std::fmt::Display for RawAttribute {
1777    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1778        write!(f, "{}", self.path)?;
1779        if let Some(args) = &self.args {
1780            write!(f, "({args})")?;
1781        }
1782        Ok(())
1783    }
1784}
1785
1786impl std::fmt::Display for ScalarValue {
1787    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1788        match self {
1789            ScalarValue::Isize(v) => write!(f, "{v} : isize"),
1790            ScalarValue::I8(v) => write!(f, "{v} : i8"),
1791            ScalarValue::I16(v) => write!(f, "{v} : i16"),
1792            ScalarValue::I32(v) => write!(f, "{v} : i32"),
1793            ScalarValue::I64(v) => write!(f, "{v} : i64"),
1794            ScalarValue::I128(v) => write!(f, "{v} : i128"),
1795            ScalarValue::Usize(v) => write!(f, "{v} : usize"),
1796            ScalarValue::U8(v) => write!(f, "{v} : u8"),
1797            ScalarValue::U16(v) => write!(f, "{v} : u16"),
1798            ScalarValue::U32(v) => write!(f, "{v} : u32"),
1799            ScalarValue::U64(v) => write!(f, "{v} : u64"),
1800            ScalarValue::U128(v) => write!(f, "{v} : u128"),
1801        }
1802    }
1803}
1804
1805impl std::fmt::Display for FloatValue {
1806    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1807        let v = &self.value;
1808        match self.ty {
1809            FloatTy::F16 => write!(f, "{v} : f16"),
1810            FloatTy::F32 => write!(f, "{v} : f32"),
1811            FloatTy::F64 => write!(f, "{v} : f64"),
1812            FloatTy::F128 => write!(f, "{v} : f128"),
1813        }
1814    }
1815}
1816
1817impl std::fmt::Display for TraitItemName {
1818    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1819        write!(f, "{}", self.0)
1820    }
1821}
1822
1823impl std::fmt::Display for TypeVar {
1824    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1825        write!(f, "{}", self.name)
1826    }
1827}
1828
1829impl std::string::ToString for Local {
1830    fn to_string(&self) -> String {
1831        let id = self.index.to_pretty_string();
1832        match &self.name {
1833            // We display both the variable name and its id because some
1834            // variables may have the same name (in different scopes)
1835            Some(name) => format!("{name}{id}"),
1836            None => id,
1837        }
1838    }
1839}
1840
1841macro_rules! impl_display_via_ctx {
1842    ($ty:ty) => {
1843        impl Display for $ty {
1844            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1845                f.write_str(&self.fmt_with_ctx(&FmtCtx::new()))
1846            }
1847        }
1848    };
1849}
1850macro_rules! impl_debug_via_display {
1851    ($ty:ty) => {
1852        impl Debug for $ty {
1853            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1854                <_ as Display>::fmt(self, f)
1855            }
1856        }
1857    };
1858}
1859
1860impl_display_via_ctx!(Field);
1861impl_display_via_ctx!(GenericArgs);
1862impl_display_via_ctx!(LiteralTy);
1863impl_display_via_ctx!(Operand);
1864impl_display_via_ctx!(Place);
1865impl_display_via_ctx!(Rvalue);
1866impl_display_via_ctx!(Variant);
1867impl_debug_via_display!(GenericArgs);
1868impl_debug_via_display!(GenericParams);
1869
1870/// Format a function call.
1871/// We return the pair: (function call, comment)
1872pub fn fmt_call<C>(ctx: &C, call: &Call) -> (String, Option<String>)
1873where
1874    C: AstFormatter,
1875{
1876    let args: Vec<String> = call.args.iter().map(|x| x.fmt_with_ctx(ctx)).collect();
1877    let args = args.join(", ");
1878    let f = call.func.fmt_with_ctx(ctx);
1879    (format!("{f}({args})"), None)
1880}
1881
1882pub(crate) fn fmt_body_blocks_with_ctx<C>(
1883    body: &Vector<BlockId, BlockData>,
1884    tab: &str,
1885    ctx: &C,
1886) -> String
1887where
1888    C: AstFormatter,
1889{
1890    let block_tab = format!("{tab}{TAB_INCR}");
1891    let mut blocks: Vec<String> = Vec::new();
1892    for (bid, block) in body.iter_indexed_values() {
1893        blocks.push(
1894            format!(
1895                "{tab}bb{}: {{\n{}\n{tab}}}\n",
1896                bid.index(),
1897                block.fmt_with_ctx_and_indent(&block_tab, ctx),
1898            )
1899            .to_string(),
1900        );
1901    }
1902    blocks.join("\n")
1903}
charon_lib/pretty/fmt_with_ctx.rs

charon_lib/pretty/
fmt_with_ctx.rs
