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 {
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::Call(call) => {
1022                let (call_s, _) = fmt_call(ctx, call);
1023                write!(&mut out, "{tab}{} := {call_s}", call.dest.fmt_with_ctx(ctx))
1024            }
1025            RawStatement::SetDiscriminant(place, variant_id) => write!(
1026                &mut out,
1027                "{tab}@discriminant({}) := {}",
1028                place.fmt_with_ctx(ctx),
1029                variant_id
1030            ),
1031            RawStatement::StorageLive(var_id) => {
1032                write!(
1033                    &mut out,
1034                    "{tab}storage_live({})",
1035                    ctx.format_object(*var_id)
1036                )
1037            }
1038            RawStatement::StorageDead(var_id) => {
1039                write!(
1040                    &mut out,
1041                    "{tab}storage_dead({})",
1042                    ctx.format_object(*var_id)
1043                )
1044            }
1045            RawStatement::Deinit(place) => {
1046                write!(&mut out, "{tab}deinit({})", place.fmt_with_ctx(ctx))
1047            }
1048            RawStatement::Drop(place) => {
1049                write!(&mut out, "{tab}drop {}", place.fmt_with_ctx(ctx))
1050            }
1051            RawStatement::Assert(assert) => write!(&mut out, "{tab}{}", assert.fmt_with_ctx(ctx)),
1052            RawStatement::Nop => write!(&mut out, "{tab}nop"),
1053            RawStatement::Error(s) => write!(&mut out, "{tab}@Error({})", s),
1054        };
1055        out
1056    }
1057}
1058
1059impl<C: AstFormatter> FmtWithCtx<C> for llbc::Statement {
1060    fn fmt_with_ctx(&self, ctx: &C) -> String {
1061        // By default use a tab.
1062        self.fmt_with_ctx_and_indent(TAB_INCR, ctx)
1063    }
1064
1065    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
1066        use llbc::RawStatement;
1067        let mut out = String::new();
1068        for line in &self.comments_before {
1069            let _ = writeln!(&mut out, "{tab}// {line}");
1070        }
1071        let _ = match &self.content {
1072            RawStatement::Assign(place, rvalue) => write!(
1073                &mut out,
1074                "{}{} := {}",
1075                tab,
1076                place.fmt_with_ctx(ctx),
1077                rvalue.fmt_with_ctx(ctx),
1078            ),
1079            RawStatement::SetDiscriminant(place, variant_id) => write!(
1080                &mut out,
1081                "{}@discriminant({}) := {}",
1082                tab,
1083                place.fmt_with_ctx(ctx),
1084                variant_id
1085            ),
1086            RawStatement::StorageLive(var_id) => {
1087                write!(
1088                    &mut out,
1089                    "{tab}storage_live({})",
1090                    ctx.format_object(*var_id)
1091                )
1092            }
1093            RawStatement::StorageDead(var_id) => {
1094                write!(
1095                    &mut out,
1096                    "{tab}storage_dead({})",
1097                    ctx.format_object(*var_id)
1098                )
1099            }
1100            RawStatement::Deinit(place) => {
1101                write!(&mut out, "{tab}deinit({})", place.fmt_with_ctx(ctx))
1102            }
1103            RawStatement::Drop(place) => {
1104                write!(&mut out, "{tab}drop {}", place.fmt_with_ctx(ctx))
1105            }
1106            RawStatement::Assert(assert) => {
1107                write!(&mut out, "{tab}{}", assert.fmt_with_ctx(ctx),)
1108            }
1109            RawStatement::Call(call) => {
1110                let (call_s, _) = fmt_call(ctx, call);
1111                write!(&mut out, "{tab}{} := {call_s}", call.dest.fmt_with_ctx(ctx),)
1112            }
1113            RawStatement::Abort(kind) => {
1114                write!(&mut out, "{}", kind.fmt_with_ctx_and_indent(tab, ctx))
1115            }
1116            RawStatement::Return => write!(&mut out, "{tab}return"),
1117            RawStatement::Break(index) => write!(&mut out, "{tab}break {index}"),
1118            RawStatement::Continue(index) => write!(&mut out, "{tab}continue {index}"),
1119            RawStatement::Nop => write!(&mut out, "{tab}nop"),
1120            RawStatement::Switch(switch) => match switch {
1121                Switch::If(discr, true_st, false_st) => {
1122                    let inner_tab = format!("{tab}{TAB_INCR}");
1123                    write!(
1124                        &mut out,
1125                        "{tab}if {} {{\n{}{tab}}}\n{tab}else {{\n{}{tab}}}",
1126                        discr.fmt_with_ctx(ctx),
1127                        true_st.fmt_with_ctx_and_indent(&inner_tab, ctx),
1128                        false_st.fmt_with_ctx_and_indent(&inner_tab, ctx),
1129                    )
1130                }
1131                Switch::SwitchInt(discr, _ty, maps, otherwise) => {
1132                    let inner_tab1 = format!("{tab}{TAB_INCR}");
1133                    let inner_tab2 = format!("{inner_tab1}{TAB_INCR}");
1134                    let mut maps: Vec<String> = maps
1135                        .iter()
1136                        .map(|(pvl, st)| {
1137                            // Note that there may be several pattern values
1138                            let pvl: Vec<String> = pvl.iter().map(|v| v.to_string()).collect();
1139                            format!(
1140                                "{inner_tab1}{} => {{\n{}{inner_tab1}}},\n",
1141                                pvl.join(" | "),
1142                                st.fmt_with_ctx_and_indent(&inner_tab2, ctx),
1143                            )
1144                        })
1145                        .collect();
1146                    maps.push(format!(
1147                        "{inner_tab1}_ => {{\n{}{inner_tab1}}},\n",
1148                        otherwise.fmt_with_ctx_and_indent(&inner_tab2, ctx),
1149                    ));
1150
1151                    write!(
1152                        &mut out,
1153                        "{tab}switch {} {{\n{}{tab}}}",
1154                        discr.fmt_with_ctx(ctx),
1155                        maps.iter().format(""),
1156                    )
1157                }
1158                Switch::Match(discr, maps, otherwise) => {
1159                    let inner_tab1 = format!("{tab}{TAB_INCR}");
1160                    let inner_tab2 = format!("{inner_tab1}{TAB_INCR}");
1161                    let mut maps: Vec<String> = maps
1162                        .iter()
1163                        .map(|(pvl, st)| {
1164                            // Note that there may be several pattern values
1165                            let pvl: Vec<String> = pvl.iter().map(|v| v.to_string()).collect();
1166                            format!(
1167                                "{inner_tab1}{} => {{\n{}{inner_tab1}}},\n",
1168                                pvl.join(" | "),
1169                                st.fmt_with_ctx_and_indent(&inner_tab2, ctx),
1170                            )
1171                        })
1172                        .collect();
1173                    if let Some(otherwise) = otherwise {
1174                        maps.push(format!(
1175                            "{inner_tab1}_ => {{\n{}{inner_tab1}}},\n",
1176                            otherwise.fmt_with_ctx_and_indent(&inner_tab2, ctx),
1177                        ));
1178                    };
1179
1180                    write!(
1181                        &mut out,
1182                        "{tab}match {} {{\n{}{tab}}}",
1183                        discr.fmt_with_ctx(ctx),
1184                        maps.iter().format(""),
1185                    )
1186                }
1187            },
1188            RawStatement::Loop(body) => {
1189                let inner_tab = format!("{tab}{TAB_INCR}");
1190                write!(
1191                    &mut out,
1192                    "{tab}loop {{\n{}{tab}}}",
1193                    body.fmt_with_ctx_and_indent(&inner_tab, ctx),
1194                )
1195            }
1196            RawStatement::Error(s) => write!(&mut out, "{tab}@ERROR({})", s),
1197        };
1198        out
1199    }
1200}
1201
1202impl<C: AstFormatter> FmtWithCtx<C> for Terminator {
1203    fn fmt_with_ctx(&self, ctx: &C) -> String {
1204        // By default use a tab.
1205        self.fmt_with_ctx_and_indent(TAB_INCR, ctx)
1206    }
1207
1208    fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
1209        let mut out = String::new();
1210        for line in &self.comments_before {
1211            let _ = writeln!(&mut out, "{tab}// {line}");
1212        }
1213        let _ = match &self.content {
1214            RawTerminator::Goto { target } => write!(&mut out, "{tab}goto bb{target}"),
1215            RawTerminator::Switch { discr, targets } => match targets {
1216                SwitchTargets::If(true_block, false_block) => write!(
1217                    &mut out,
1218                    "{tab}if {} -> bb{} else -> bb{}",
1219                    discr.fmt_with_ctx(ctx),
1220                    true_block,
1221                    false_block
1222                ),
1223                SwitchTargets::SwitchInt(_ty, maps, otherwise) => {
1224                    let mut maps: Vec<String> = maps
1225                        .iter()
1226                        .map(|(v, bid)| format!("{}: bb{}", v.to_string(), bid))
1227                        .collect();
1228                    maps.push(format!("otherwise: bb{otherwise}"));
1229                    let maps = maps.join(", ");
1230
1231                    write!(
1232                        &mut out,
1233                        "{tab}switch {} -> {}",
1234                        discr.fmt_with_ctx(ctx),
1235                        maps
1236                    )
1237                }
1238            },
1239            RawTerminator::Abort(kind) => write!(&mut out, "{tab}{}", kind.fmt_with_ctx(ctx)),
1240            RawTerminator::Return => write!(&mut out, "{tab}return"),
1241        };
1242        out
1243    }
1244}
1245
1246impl<C: AstFormatter> FmtWithCtx<C> for TraitClause {
1247    fn fmt_with_ctx(&self, ctx: &C) -> String {
1248        let clause_id = self.clause_id.to_pretty_string();
1249        let trait_ = self.trait_.fmt_with_ctx(ctx);
1250        format!("[{clause_id}]: {trait_}")
1251    }
1252}
1253
1254impl<C: AstFormatter> FmtWithCtx<C> for TraitDecl {
1255    fn fmt_with_ctx(&self, ctx: &C) -> String {
1256        let intro = self.item_meta.fmt_item_intro(ctx, "", "trait");
1257
1258        // Update the context
1259        let ctx = &ctx.set_generics(&self.generics);
1260
1261        let (generics, clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "");
1262
1263        let items = {
1264            let items = self
1265                .parent_clauses
1266                .iter()
1267                .map(|c| {
1268                    format!(
1269                        "{TAB_INCR}parent_clause{} : {}\n",
1270                        c.clause_id,
1271                        c.fmt_with_ctx(ctx)
1272                    )
1273                })
1274                .chain(self.type_clauses.iter().map(|(name, clauses)| {
1275                    clauses
1276                        .iter()
1277                        .map(|c| {
1278                            format!(
1279                                "{TAB_INCR}item_clause_{name}_{} : {}\n",
1280                                c.clause_id.to_string(),
1281                                c.fmt_with_ctx(ctx)
1282                            )
1283                        })
1284                        .collect()
1285                }))
1286                .chain(self.consts.iter().map(|(name, ty)| {
1287                    let ty = ty.fmt_with_ctx(ctx);
1288                    format!("{TAB_INCR}const {name} : {ty}\n")
1289                }))
1290                .chain(
1291                    self.types
1292                        .iter()
1293                        .map(|name| format!("{TAB_INCR}type {name}\n")),
1294                )
1295                .chain(self.methods().map(|(name, bound_fn)| {
1296                    let (params, fn_ref) = bound_fn.fmt_split(ctx);
1297                    format!("{TAB_INCR}fn {name}{params} = {fn_ref}\n",)
1298                }))
1299                .collect::<Vec<String>>();
1300            if items.is_empty() {
1301                "".to_string()
1302            } else {
1303                format!("\n{{\n{}}}", items.join(""))
1304            }
1305        };
1306
1307        format!("{intro}{generics}{clauses}{items}")
1308    }
1309}
1310
1311impl<C: AstFormatter> FmtWithCtx<C> for TraitDeclRef {
1312    fn fmt_with_ctx(&self, ctx: &C) -> String {
1313        let trait_id = ctx.format_object(self.trait_id);
1314        let generics = self.generics.fmt_with_ctx(ctx);
1315        format!("{trait_id}{generics}")
1316    }
1317}
1318
1319impl<C: AstFormatter> FmtWithCtx<C> for TraitImpl {
1320    fn fmt_with_ctx(&self, ctx: &C) -> String {
1321        let intro = self.item_meta.fmt_item_intro(ctx, "", "impl");
1322
1323        // Update the context
1324        let ctx = &ctx.set_generics(&self.generics);
1325
1326        let (generics, clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "");
1327
1328        let items = {
1329            let items = self
1330                .parent_trait_refs
1331                .iter()
1332                .enumerate()
1333                .map(|(i, clause)| {
1334                    let i = TraitClauseId::new(i);
1335                    format!(
1336                        "{TAB_INCR}parent_clause{i} = {}\n",
1337                        clause.fmt_with_ctx(ctx)
1338                    )
1339                })
1340                .chain(self.type_clauses.iter().map(|(name, clauses)| {
1341                    clauses
1342                        .iter()
1343                        .enumerate()
1344                        .map(|(i, c)| {
1345                            let i = TraitClauseId::new(i);
1346                            format!(
1347                                "{TAB_INCR}item_clause_{name}_{i} = {}\n",
1348                                c.fmt_with_ctx(ctx)
1349                            )
1350                        })
1351                        .collect()
1352                }))
1353                .chain(self.consts.iter().map(|(name, global)| {
1354                    format!("{TAB_INCR}const {name} = {}\n", global.fmt_with_ctx(ctx))
1355                }))
1356                .chain(self.types.iter().map(|(name, ty)| {
1357                    format!("{TAB_INCR}type {name} = {}\n", ty.fmt_with_ctx(ctx),)
1358                }))
1359                .chain(self.methods().map(|(name, bound_fn)| {
1360                    let (params, fn_ref) = bound_fn.fmt_split(ctx);
1361                    format!("{TAB_INCR}fn {name}{params} = {fn_ref}\n",)
1362                }))
1363                .collect::<Vec<String>>();
1364            if items.is_empty() {
1365                "".to_string()
1366            } else {
1367                format!("\n{{\n{}}}", items.join(""))
1368            }
1369        };
1370
1371        let impl_trait = self.impl_trait.fmt_with_ctx(ctx);
1372        format!("{intro}{generics} : {impl_trait}{clauses}{items}")
1373    }
1374}
1375
1376impl<C: AstFormatter> FmtWithCtx<C> for TraitRefKind {
1377    fn fmt_with_ctx(&self, ctx: &C) -> String {
1378        match self {
1379            TraitRefKind::SelfId => "Self".to_string(),
1380            TraitRefKind::ParentClause(id, _decl_id, clause_id) => {
1381                let id = id.fmt_with_ctx(ctx);
1382                format!("{id}::parent_clause{clause_id}")
1383            }
1384            TraitRefKind::ItemClause(id, _decl_id, type_name, clause_id) => {
1385                let id = id.fmt_with_ctx(ctx);
1386                // Using on purpose [to_pretty_string] instead of [format_object]:
1387                // the clause is local to the associated type, so it should not
1388                // be referenced in the current context.
1389                let clause = clause_id.to_pretty_string();
1390                format!("({id}::{type_name}::[{clause}])")
1391            }
1392            TraitRefKind::TraitImpl(id, args) => {
1393                let impl_ = ctx.format_object(*id);
1394                let args = args.fmt_with_ctx(ctx);
1395                format!("{impl_}{args}")
1396            }
1397            TraitRefKind::Clause(id) => ctx.format_object(*id),
1398            TraitRefKind::BuiltinOrAuto {
1399                trait_decl_ref: tr,
1400                types,
1401                ..
1402            } => {
1403                let tr = tr.fmt_with_ctx(ctx);
1404                let types = if types.is_empty() {
1405                    String::new()
1406                } else {
1407                    let types = types
1408                        .iter()
1409                        .map(|(name, ty)| {
1410                            let ty = ty.fmt_with_ctx(ctx);
1411                            format!("{name}  = {ty}")
1412                        })
1413                        .join(", ");
1414                    format!(" where {types}")
1415                };
1416                format!("{tr}{types}")
1417            }
1418            TraitRefKind::Dyn(tr) => tr.fmt_with_ctx(ctx),
1419            TraitRefKind::Unknown(msg) => format!("UNKNOWN({msg})"),
1420        }
1421    }
1422}
1423
1424impl<C: AstFormatter> FmtWithCtx<C> for TraitRef {
1425    fn fmt_with_ctx(&self, ctx: &C) -> String {
1426        self.kind.fmt_with_ctx(ctx)
1427    }
1428}
1429
1430impl<C: AstFormatter> FmtWithCtx<C> for TraitTypeConstraint {
1431    fn fmt_with_ctx(&self, ctx: &C) -> String {
1432        let trait_ref = self.trait_ref.fmt_with_ctx(ctx);
1433        let ty = self.ty.fmt_with_ctx(ctx);
1434        format!("{}::{} = {}", trait_ref, self.type_name, ty)
1435    }
1436}
1437
1438impl<C: AstFormatter> FmtWithCtx<C> for Ty {
1439    fn fmt_with_ctx(&self, ctx: &C) -> String {
1440        match self.kind() {
1441            TyKind::Adt(id, generics) => {
1442                let adt_ident = id.fmt_with_ctx(ctx);
1443
1444                if id.is_tuple() {
1445                    assert!(generics.trait_refs.is_empty());
1446                    let generics = generics.fmt_with_ctx_no_brackets(ctx);
1447                    format!("({generics})")
1448                } else {
1449                    let generics = generics.fmt_with_ctx(ctx);
1450                    format!("{adt_ident}{generics}")
1451                }
1452            }
1453            TyKind::TypeVar(id) => ctx.format_object(*id),
1454            TyKind::Literal(kind) => kind.to_string(),
1455            TyKind::Never => "!".to_string(),
1456            TyKind::Ref(r, ty, kind) => match kind {
1457                RefKind::Mut => {
1458                    format!("&{} mut ({})", r.fmt_with_ctx(ctx), ty.fmt_with_ctx(ctx))
1459                }
1460                RefKind::Shared => {
1461                    format!("&{} ({})", r.fmt_with_ctx(ctx), ty.fmt_with_ctx(ctx))
1462                }
1463            },
1464            TyKind::RawPtr(ty, kind) => match kind {
1465                RefKind::Shared => format!("*const {}", ty.fmt_with_ctx(ctx)),
1466                RefKind::Mut => format!("*mut {}", ty.fmt_with_ctx(ctx)),
1467            },
1468            TyKind::TraitType(trait_ref, name) => {
1469                format!("{}::{name}", trait_ref.fmt_with_ctx(ctx),)
1470            }
1471            TyKind::DynTrait(pred) => format!("dyn ({})", pred.with_ctx(ctx)),
1472            TyKind::Arrow(io) => {
1473                // Update the bound regions
1474                let ctx = &ctx.push_bound_regions(&io.regions);
1475
1476                let regions = if io.regions.is_empty() {
1477                    "".to_string()
1478                } else {
1479                    format!(
1480                        "<{}>",
1481                        io.regions.iter().map(|r| ctx.format_object(r)).join(", ")
1482                    )
1483                };
1484                let (inputs, output) = &io.skip_binder;
1485                let inputs = inputs
1486                    .iter()
1487                    .map(|x| x.fmt_with_ctx(ctx))
1488                    .collect::<Vec<String>>()
1489                    .join(", ");
1490                if output.is_unit() {
1491                    format!("fn{regions}({inputs})")
1492                } else {
1493                    let output = output.fmt_with_ctx(ctx);
1494                    format!("fn{regions}({inputs}) -> {output}")
1495                }
1496            }
1497            TyKind::Error(msg) => format!("type_error(\"{msg}\")"),
1498        }
1499    }
1500}
1501
1502impl<C: AstFormatter> FmtWithCtx<C> for TypeDecl {
1503    fn fmt_with_ctx(&self, ctx: &C) -> String {
1504        let keyword = match &self.kind {
1505            TypeDeclKind::Struct(..) => "struct",
1506            TypeDeclKind::Union(..) => "union",
1507            TypeDeclKind::Enum(..) => "enum",
1508            TypeDeclKind::Alias(..) => "type",
1509            TypeDeclKind::Opaque | TypeDeclKind::Error(..) => "opaque type",
1510        };
1511        let intro = self.item_meta.fmt_item_intro(ctx, "", keyword);
1512
1513        let ctx = &ctx.set_generics(&self.generics);
1514        let (params, preds) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "  ");
1515        // Predicates
1516        let nl_or_space = if !self.generics.has_predicates() {
1517            " ".to_string()
1518        } else {
1519            "\n ".to_string()
1520        };
1521
1522        let contents = match &self.kind {
1523            TypeDeclKind::Struct(fields) => {
1524                if !fields.is_empty() {
1525                    let fields = fields
1526                        .iter()
1527                        .map(|f| format!("\n  {},", f.fmt_with_ctx(ctx)))
1528                        .format("");
1529                    format!("{nl_or_space}=\n{{{fields}\n}}")
1530                } else {
1531                    format!("{nl_or_space}= {{}}")
1532                }
1533            }
1534            TypeDeclKind::Union(fields) => {
1535                let fields = fields
1536                    .iter()
1537                    .map(|f| format!("\n  {},", f.fmt_with_ctx(ctx)))
1538                    .format("");
1539                format!("{nl_or_space}=\n{{{fields}\n}}")
1540            }
1541            TypeDeclKind::Enum(variants) => {
1542                let variants = variants
1543                    .iter()
1544                    .map(|v| format!("|  {}", v.fmt_with_ctx(ctx)))
1545                    .format("\n");
1546                format!("{nl_or_space}=\n{variants}\n")
1547            }
1548            TypeDeclKind::Alias(ty) => format!(" = {}", ty.fmt_with_ctx(ctx)),
1549            TypeDeclKind::Opaque => format!(""),
1550            TypeDeclKind::Error(msg) => format!(" = ERROR({msg})"),
1551        };
1552        format!("{intro}{params}{preds}{contents}")
1553    }
1554}
1555
1556impl<C: AstFormatter> FmtWithCtx<C> for TypeId {
1557    fn fmt_with_ctx(&self, ctx: &C) -> String {
1558        match self {
1559            TypeId::Tuple => "".to_string(),
1560            TypeId::Adt(def_id) => ctx.format_object(*def_id),
1561            TypeId::Builtin(aty) => aty.get_name().fmt_with_ctx(ctx),
1562        }
1563    }
1564}
1565
1566impl<C: AstFormatter> FmtWithCtx<C> for TypeVar {
1567    fn fmt_with_ctx(&self, _ctx: &C) -> String {
1568        self.name.to_string()
1569    }
1570}
1571
1572impl<C: AstFormatter> FmtWithCtx<C> for UnOp {
1573    fn fmt_with_ctx(&self, ctx: &C) -> String {
1574        match self {
1575            UnOp::Not => "~".to_string(),
1576            UnOp::Neg => "-".to_string(),
1577            UnOp::PtrMetadata => "ptr_metadata".to_string(),
1578            UnOp::Cast(kind) => kind.fmt_with_ctx(ctx),
1579            UnOp::ArrayToSlice(..) => "array_to_slice".to_string(),
1580        }
1581    }
1582}
1583
1584impl<C: AstFormatter> FmtWithCtx<C> for Variant {
1585    fn fmt_with_ctx(&self, ctx: &C) -> String {
1586        let fields: Vec<String> = self.fields.iter().map(|f| f.fmt_with_ctx(ctx)).collect();
1587        let fields = fields.join(", ");
1588        format!("{}({})", self.name, fields)
1589    }
1590}
1591
1592impl std::fmt::Display for AnyTransId {
1593    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1594        let s = match self {
1595            AnyTransId::Type(x) => x.to_pretty_string(),
1596            AnyTransId::Fun(x) => x.to_pretty_string(),
1597            AnyTransId::Global(x) => x.to_pretty_string(),
1598            AnyTransId::TraitDecl(x) => x.to_pretty_string(),
1599            AnyTransId::TraitImpl(x) => x.to_pretty_string(),
1600        };
1601        f.write_str(&s)
1602    }
1603}
1604
1605impl std::fmt::Display for BinOp {
1606    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1607        match self {
1608            BinOp::BitXor => write!(f, "^"),
1609            BinOp::BitAnd => write!(f, "&"),
1610            BinOp::BitOr => write!(f, "|"),
1611            BinOp::Eq => write!(f, "=="),
1612            BinOp::Lt => write!(f, "<"),
1613            BinOp::Le => write!(f, "<="),
1614            BinOp::Ne => write!(f, "!="),
1615            BinOp::Ge => write!(f, ">="),
1616            BinOp::Gt => write!(f, ">"),
1617            BinOp::Div => write!(f, "/"),
1618            BinOp::Rem => write!(f, "%"),
1619            BinOp::Add => write!(f, "+"),
1620            BinOp::Sub => write!(f, "-"),
1621            BinOp::Mul => write!(f, "*"),
1622            BinOp::CheckedAdd => write!(f, "checked.+"),
1623            BinOp::CheckedSub => write!(f, "checked.-"),
1624            BinOp::CheckedMul => write!(f, "checked.*"),
1625            BinOp::Shl => write!(f, "<<"),
1626            BinOp::Shr => write!(f, ">>"),
1627            BinOp::Cmp => write!(f, "cmp"),
1628            BinOp::Offset => write!(f, "offset"),
1629        }
1630    }
1631}
1632
1633impl std::fmt::Display for BorrowKind {
1634    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1635        // Reuse the derived `Debug` impl to get the variant name.
1636        write!(f, "{self:?}")
1637    }
1638}
1639
1640impl std::fmt::Display for BuiltinFunId {
1641    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1642        let name = match *self {
1643            BuiltinFunId::BoxNew => "BoxNew",
1644            BuiltinFunId::ArrayToSliceShared => "ArrayToSliceShared",
1645            BuiltinFunId::ArrayToSliceMut => "ArrayToSliceMut",
1646            BuiltinFunId::ArrayRepeat => "ArrayRepeat",
1647            BuiltinFunId::Index(BuiltinIndexOp {
1648                is_array,
1649                mutability,
1650                is_range,
1651            }) => {
1652                let ty = if is_array { "Array" } else { "Slice" };
1653                let op = if is_range { "SubSlice" } else { "Index" };
1654                let mutability = mutability.variant_name();
1655                &format!("{ty}{op}{mutability}")
1656            }
1657            BuiltinFunId::PtrFromParts(mutability) => {
1658                let mutability = mutability.variant_name();
1659                &format!("PtrFromParts{mutability}")
1660            }
1661        };
1662        f.write_str(name)
1663    }
1664}
1665
1666impl std::fmt::Display for DeBruijnId {
1667    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1668        write!(f, "{}", self.index)
1669    }
1670}
1671
1672impl<Id> Display for DeBruijnVar<Id>
1673where
1674    Id: Display,
1675{
1676    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1677        match self {
1678            Self::Bound(dbid, varid) => write!(f, "{dbid}_{varid}"),
1679            Self::Free(varid) => write!(f, "{varid}"),
1680        }
1681    }
1682}
1683
1684impl std::fmt::Display for ConstantExpr {
1685    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1686        write!(f, "{}", self.fmt_with_ctx(&FmtCtx::new()))
1687    }
1688}
1689
1690impl std::fmt::Display for FileName {
1691    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1692        match self {
1693            FileName::Virtual(path_buf) | FileName::Local(path_buf) => {
1694                write!(f, "{}", path_buf.display())
1695            }
1696            FileName::NotReal(name) => write!(f, "{}", name),
1697        }
1698    }
1699}
1700
1701impl std::fmt::Display for FloatTy {
1702    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1703        match self {
1704            FloatTy::F16 => write!(f, "f16"),
1705            FloatTy::F32 => write!(f, "f32"),
1706            FloatTy::F64 => write!(f, "f64"),
1707            FloatTy::F128 => write!(f, "f128"),
1708        }
1709    }
1710}
1711
1712impl std::fmt::Display for IntegerTy {
1713    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1714        match self {
1715            IntegerTy::Isize => write!(f, "isize"),
1716            IntegerTy::I8 => write!(f, "i8"),
1717            IntegerTy::I16 => write!(f, "i16"),
1718            IntegerTy::I32 => write!(f, "i32"),
1719            IntegerTy::I64 => write!(f, "i64"),
1720            IntegerTy::I128 => write!(f, "i128"),
1721            IntegerTy::Usize => write!(f, "usize"),
1722            IntegerTy::U8 => write!(f, "u8"),
1723            IntegerTy::U16 => write!(f, "u16"),
1724            IntegerTy::U32 => write!(f, "u32"),
1725            IntegerTy::U64 => write!(f, "u64"),
1726            IntegerTy::U128 => write!(f, "u128"),
1727        }
1728    }
1729}
1730
1731impl std::fmt::Display for GenericParams {
1732    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1733        write!(f, "{}", self.fmt_with_ctx_single_line(&FmtCtx::new()))
1734    }
1735}
1736
1737impl std::fmt::Display for Literal {
1738    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1739        match self {
1740            Literal::Scalar(v) => write!(f, "{v}"),
1741            Literal::Float(v) => write!(f, "{v}"),
1742            Literal::Bool(v) => write!(f, "{v}"),
1743            Literal::Char(v) => write!(f, "{v}"),
1744            Literal::Str(v) => write!(f, "\"{}\"", v.replace("\\", "\\\\").replace("\n", "\\n")),
1745            Literal::ByteStr(v) => write!(f, "{v:?}"),
1746        }
1747    }
1748}
1749
1750impl std::fmt::Display for Loc {
1751    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1752        write!(f, "{}:{}", self.line, self.col)
1753    }
1754}
1755
1756impl std::fmt::Display for RawAttribute {
1757    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1758        write!(f, "{}", self.path)?;
1759        if let Some(args) = &self.args {
1760            write!(f, "({args})")?;
1761        }
1762        Ok(())
1763    }
1764}
1765
1766impl std::fmt::Display for ScalarValue {
1767    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1768        match self {
1769            ScalarValue::Isize(v) => write!(f, "{v} : isize"),
1770            ScalarValue::I8(v) => write!(f, "{v} : i8"),
1771            ScalarValue::I16(v) => write!(f, "{v} : i16"),
1772            ScalarValue::I32(v) => write!(f, "{v} : i32"),
1773            ScalarValue::I64(v) => write!(f, "{v} : i64"),
1774            ScalarValue::I128(v) => write!(f, "{v} : i128"),
1775            ScalarValue::Usize(v) => write!(f, "{v} : usize"),
1776            ScalarValue::U8(v) => write!(f, "{v} : u8"),
1777            ScalarValue::U16(v) => write!(f, "{v} : u16"),
1778            ScalarValue::U32(v) => write!(f, "{v} : u32"),
1779            ScalarValue::U64(v) => write!(f, "{v} : u64"),
1780            ScalarValue::U128(v) => write!(f, "{v} : u128"),
1781        }
1782    }
1783}
1784
1785impl std::fmt::Display for FloatValue {
1786    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1787        let v = &self.value;
1788        match self.ty {
1789            FloatTy::F16 => write!(f, "{v} : f16"),
1790            FloatTy::F32 => write!(f, "{v} : f32"),
1791            FloatTy::F64 => write!(f, "{v} : f64"),
1792            FloatTy::F128 => write!(f, "{v} : f128"),
1793        }
1794    }
1795}
1796
1797impl std::fmt::Display for TraitItemName {
1798    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
1799        write!(f, "{}", self.0)
1800    }
1801}
1802
1803impl std::fmt::Display for TypeVar {
1804    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1805        write!(f, "{}", self.name)
1806    }
1807}
1808
1809impl std::string::ToString for Local {
1810    fn to_string(&self) -> String {
1811        let id = self.index.to_pretty_string();
1812        match &self.name {
1813            // We display both the variable name and its id because some
1814            // variables may have the same name (in different scopes)
1815            Some(name) => format!("{name}{id}"),
1816            None => id,
1817        }
1818    }
1819}
1820
1821macro_rules! impl_display_via_ctx {
1822    ($ty:ty) => {
1823        impl Display for $ty {
1824            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1825                f.write_str(&self.fmt_with_ctx(&FmtCtx::new()))
1826            }
1827        }
1828    };
1829}
1830macro_rules! impl_debug_via_display {
1831    ($ty:ty) => {
1832        impl Debug for $ty {
1833            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1834                <_ as Display>::fmt(self, f)
1835            }
1836        }
1837    };
1838}
1839
1840impl_display_via_ctx!(Field);
1841impl_display_via_ctx!(GenericArgs);
1842impl_display_via_ctx!(LiteralTy);
1843impl_display_via_ctx!(Operand);
1844impl_display_via_ctx!(Place);
1845impl_display_via_ctx!(Rvalue);
1846impl_display_via_ctx!(Variant);
1847impl_debug_via_display!(GenericArgs);
1848impl_debug_via_display!(GenericParams);
1849
1850/// Format a function call.
1851/// We return the pair: (function call, comment)
1852pub fn fmt_call<C>(ctx: &C, call: &Call) -> (String, Option<String>)
1853where
1854    C: AstFormatter,
1855{
1856    let args: Vec<String> = call.args.iter().map(|x| x.fmt_with_ctx(ctx)).collect();
1857    let args = args.join(", ");
1858    let f = call.func.fmt_with_ctx(ctx);
1859    (format!("{f}({args})"), None)
1860}
1861
1862pub(crate) fn fmt_body_blocks_with_ctx<C>(
1863    body: &Vector<BlockId, BlockData>,
1864    tab: &str,
1865    ctx: &C,
1866) -> String
1867where
1868    C: AstFormatter,
1869{
1870    let block_tab = format!("{tab}{TAB_INCR}");
1871    let mut blocks: Vec<String> = Vec::new();
1872    for (bid, block) in body.iter_indexed_values() {
1873        blocks.push(
1874            format!(
1875                "{tab}bb{}: {{\n{}\n{tab}}}\n",
1876                bid.index(),
1877                block.fmt_with_ctx_and_indent(&block_tab, ctx),
1878            )
1879            .to_string(),
1880        );
1881    }
1882    blocks.join("\n")
1883}
charon_lib/pretty/fmt_with_ctx.rs

charon_lib/pretty/
fmt_with_ctx.rs
