flux_middle/rty/
pretty.rs

1use std::{fmt, iter};
2
3use expr::{FieldBind, pretty::aggregate_nested};
4use rustc_data_structures::snapshot_map::SnapshotMap;
5use rustc_type_ir::DebruijnIndex;
6use ty::{UnevaluatedConst, ValTree, region_to_string};
7
8use super::*;
9use crate::pretty::*;
10
11impl Pretty for ClauseKind {
12    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
13        match self {
14            ClauseKind::Trait(pred) => w!(cx, f, "Trait ({:?})", ^pred),
15            ClauseKind::Projection(pred) => w!(cx, f, "Projection ({:?})", ^pred),
16            ClauseKind::RegionOutlives(pred) => {
17                w!(cx, f, "Outlives ({:?}, {:?})", &pred.0, &pred.1)
18            }
19            ClauseKind::TypeOutlives(pred) => w!(cx, f, "Outlives ({:?}, {:?})", &pred.0, &pred.1),
20            ClauseKind::ConstArgHasType(c, ty) => w!(cx, f, "ConstArgHasType ({:?}, {:?})", c, ty),
21        }
22    }
23}
24
25impl Pretty for BoundRegionKind {
26    fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
27        match self {
28            BoundRegionKind::Anon => w!(cx, f, "'<annon>"),
29            BoundRegionKind::Named(_, sym) => w!(cx, f, "{sym}"),
30            BoundRegionKind::ClosureEnv => w!(cx, f, "'<env>"),
31        }
32    }
33}
34
35impl<T> Pretty for Binder<T>
36where
37    T: Pretty,
38{
39    default fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
40        cx.with_bound_vars(self.vars(), || {
41            if !self.vars().is_empty() {
42                cx.fmt_bound_vars(true, "for<", self.vars(), "> ", f)?;
43            }
44            w!(cx, f, "{:?}", self.skip_binder_ref())
45        })
46    }
47}
48
49impl<T: Pretty> std::fmt::Debug for Binder<T> {
50    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
51        pprint_with_default_cx(f, self, None)
52    }
53}
54
55impl Pretty for PolyFnSig {
56    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
57        let vars = self.vars();
58        cx.with_bound_vars(vars, || {
59            if !vars.is_empty() {
60                cx.fmt_bound_vars(true, "for<", vars, "> ", f)?;
61            }
62            w!(cx, f, "{:?}", self.skip_binder_ref())
63        })
64    }
65}
66
67impl Pretty for SortCtor {
68    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
69        match self {
70            SortCtor::Set => w!(cx, f, "Set"),
71            SortCtor::Map => w!(cx, f, "Map"),
72            SortCtor::User { name, .. } => w!(cx, f, "{}", ^name),
73            SortCtor::Adt(adt_sort_def) => {
74                w!(cx, f, "{:?}", adt_sort_def.did())
75            }
76        }
77    }
78}
79
80impl Pretty for SortInfer {
81    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
82        match self {
83            SortInfer::SortVar(svid) => w!(cx, f, "{:?}", ^svid),
84            SortInfer::NumVar(nvid) => w!(cx, f, "{:?}", ^nvid),
85        }
86    }
87}
88
89impl Pretty for Sort {
90    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
91        match self {
92            Sort::Bool => w!(cx, f, "bool"),
93            Sort::Int => w!(cx, f, "int"),
94            Sort::Real => w!(cx, f, "real"),
95            Sort::Str => w!(cx, f, "str"),
96            Sort::Char => w!(cx, f, "char"),
97            Sort::BitVec(size) => w!(cx, f, "bitvec<{:?}>", size),
98            Sort::Loc => w!(cx, f, "loc"),
99            Sort::Var(n) => w!(cx, f, "@{}", ^n.index()),
100            Sort::Func(sort) => w!(cx, f, "{:?}", sort),
101            Sort::Tuple(sorts) => {
102                if let [sort] = &sorts[..] {
103                    w!(cx, f, "({:?},)", sort)
104                } else {
105                    w!(cx, f, "({:?})", join!(", ", sorts))
106                }
107            }
108            Sort::Alias(kind, alias_ty) => {
109                fmt_alias_ty(cx, f, *kind, alias_ty)?;
110                w!(cx, f, "::sort")
111            }
112            Sort::App(ctor, sorts) => {
113                if sorts.is_empty() {
114                    w!(cx, f, "{:?}", ctor)
115                } else {
116                    w!(cx, f, "{:?}<{:?}>", ctor, join!(", ", sorts))
117                }
118            }
119            Sort::Param(param_ty) => w!(cx, f, "{}::sort", ^param_ty),
120            Sort::Infer(svar) => w!(cx, f, "{:?}", svar),
121            Sort::Err => w!(cx, f, "err"),
122        }
123    }
124
125    fn default_cx(tcx: TyCtxt) -> PrettyCx {
126        PrettyCx::default(tcx).hide_refinements(true)
127    }
128}
129
130impl Pretty for SortArg {
131    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
132        match self {
133            SortArg::Sort(sort) => w!(cx, f, "{:?}", sort),
134            SortArg::BvSize(size) => w!(cx, f, "{:?}", size),
135        }
136    }
137}
138
139impl Pretty for BvSize {
140    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
141        match self {
142            BvSize::Fixed(size) => w!(cx, f, "{}", ^size),
143            BvSize::Param(param) => w!(cx, f, "{:?}", ^param),
144            BvSize::Infer(size_vid) => w!(cx, f, "{:?}", ^size_vid),
145        }
146    }
147}
148
149impl Pretty for FuncSort {
150    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
151        match self.inputs() {
152            [input] => {
153                w!(cx, f, "{:?} -> {:?}", input, self.output())
154            }
155            inputs => {
156                w!(cx, f,
157                   "({}) -> {:?}",
158                   ^inputs
159                       .iter()
160                       .format_with(", ", |s, f| f(&format_args_cx!(cx, "{:?}", s))),
161                   self.output()
162                )
163            }
164        }
165    }
166}
167
168impl Pretty for PolyFuncSort {
169    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
170        if self.params.is_empty() {
171            w!(cx, f, "{:?}", &self.fsort)
172        } else {
173            w!(cx, f, "for<{}> {:?}", ^self.params.len(), &self.fsort)
174        }
175    }
176}
177
178impl Pretty for FnSig {
179    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
180        if !self.requires.is_empty() {
181            w!(cx, f, "[{:?}] ", join!(", ", &self.requires))?;
182        }
183        w!(cx, f, "fn({:?}) -> {:?}", join!(", ", &self.inputs), &self.output)?;
184
185        Ok(())
186    }
187}
188
189impl Pretty for Binder<FnOutput> {
190    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
191        let vars = self.vars();
192        cx.with_bound_vars(vars, || {
193            if !vars.is_empty() {
194                cx.fmt_bound_vars(true, "exists<", vars, "> ", f)?;
195            }
196            w!(cx, f, "{:?}", self.skip_binder_ref())
197        })
198    }
199}
200
201impl Pretty for FnOutput {
202    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
203        w!(cx, f, "{:?}", &self.ret)?;
204        if !self.ensures.is_empty() {
205            w!(cx, f, "; [{:?}]", join!(", ", &self.ensures))?;
206        }
207        Ok(())
208    }
209}
210
211impl Pretty for Ensures {
212    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
213        match self {
214            Ensures::Type(loc, ty) => w!(cx, f, "{:?}: {:?}", ^loc, ty),
215            Ensures::Pred(e) => w!(cx, f, "{:?}", e),
216        }
217    }
218}
219
220impl Pretty for SubsetTy {
221    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
222        if self.pred.is_trivially_true() {
223            w!(cx, f, "{:?}[{:?}]", &self.bty, &self.idx)
224        } else {
225            w!(cx, f, "{{ {:?}[{:?}] | {:?} }}", &self.bty, &self.idx, &self.pred)
226        }
227    }
228}
229
230// This is a trick to avoid pretty printing `S [S { x: 10, y: 20}]`
231// and instead just print `S[{x: 10, y: 20}]` for struct-valued indices.
232struct IdxFmt(Expr);
233
234impl PrettyNested for IdxFmt {
235    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
236        let kind = self.0.kind();
237        match kind {
238            ExprKind::Ctor(ctor, flds) => aggregate_nested(cx, ctor, flds, false),
239            ExprKind::Tuple(flds) if flds.is_empty() => {
240                Ok(NestedString { text: String::new(), key: None, children: None })
241            }
242            _ => self.0.fmt_nested(cx),
243        }
244    }
245}
246
247impl Pretty for IdxFmt {
248    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
249        let e = if cx.simplify_exprs {
250            self.0.simplify(&SnapshotMap::default())
251        } else {
252            self.0.clone()
253        };
254        if let ExprKind::Ctor(ctor, flds) = e.kind()
255            && let Some(adt_sort_def) = cx.adt_sort_def_of(ctor.def_id())
256            && let Some(variant) = adt_sort_def.opt_struct_variant()
257        {
258            let fields = iter::zip(variant.field_names(), flds)
259                .map(|(name, value)| FieldBind { name: *name, value: value.clone() })
260                .collect_vec();
261            w!(cx, f, "{{ {:?} }}", join!(", ", fields))
262        } else {
263            w!(cx, f, "{:?}", e)
264        }
265    }
266}
267
268impl Pretty for Ty {
269    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
270        match self.kind() {
271            TyKind::Indexed(bty, idx) => {
272                if cx.hide_refinements {
273                    w!(cx, f, "{:?}", bty)?;
274                    return Ok(());
275                }
276                if idx.is_unit() {
277                    w!(cx, f, "{:?}", bty)?;
278                } else {
279                    w!(cx, f, "{:?}[{:?}]", parens!(bty, !bty.is_atom()), IdxFmt(idx.clone()))?;
280                }
281                Ok(())
282            }
283            TyKind::Exists(ty_ctor) => {
284                let vars = ty_ctor.vars();
285                cx.with_bound_vars(vars, || {
286                    if cx.hide_refinements {
287                        w!(cx, f, "{:?}", ty_ctor.skip_binder_ref())
288                    } else {
289                        cx.fmt_bound_vars(false, "∃", vars, ". ", f)?;
290                        w!(cx, f, "{:?}", ty_ctor.skip_binder_ref())
291                    }
292                })
293            }
294            TyKind::Uninit => w!(cx, f, "uninit"),
295            TyKind::StrgRef(re, loc, ty) => w!(cx, f, "&{:?} strg <{:?}: {:?}>", re, loc, ty),
296            TyKind::Ptr(pk, loc) => w!(cx, f, "ptr({:?}, {:?})", pk, loc),
297            TyKind::Discr(adt_def, place) => w!(cx, f, "discr({:?}, {:?})", adt_def.did(), ^place),
298            TyKind::Constr(pred, ty) => {
299                if cx.hide_refinements {
300                    w!(cx, f, "{:?}", ty)
301                } else {
302                    w!(cx, f, "{{ {:?} | {:?} }}", ty, pred)
303                }
304            }
305            TyKind::Param(param_ty) => w!(cx, f, "{}", ^param_ty),
306            TyKind::Downcast(adt, .., variant_idx, fields) => {
307                // base-name
308                w!(cx, f, "{:?}", adt.did())?;
309                // variant-name: if it is not a struct
310                if !adt.is_struct() {
311                    w!(cx, f, "::{}", ^adt.variant(*variant_idx).name)?;
312                }
313                // fields: use curly-braces + names for structs, otherwise use parens
314                if adt.is_struct() {
315                    let field_binds = iter::zip(&adt.variant(*variant_idx).fields, fields)
316                        .map(|(field_def, value)| FieldBind { name: field_def.name, value });
317                    w!(cx, f, " {{ {:?} }}", join!(", ", field_binds))?;
318                } else if !fields.is_empty() {
319                    w!(cx, f, "({:?})", join!(", ", fields))?;
320                }
321                Ok(())
322            }
323            TyKind::Blocked(ty) => w!(cx, f, "†{:?}", ty),
324            TyKind::Infer(ty_vid) => {
325                w!(cx, f, "{ty_vid:?}")
326            }
327        }
328    }
329
330    fn default_cx(tcx: TyCtxt) -> PrettyCx {
331        PrettyCx::default(tcx).kvar_args(KVarArgs::Hide)
332    }
333}
334
335impl Pretty for PtrKind {
336    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
337        match self {
338            PtrKind::Mut(re) => {
339                w!(cx, f, "mut")?;
340                if !cx.hide_regions {
341                    w!(cx, f, "[{:?}]", re)?;
342                }
343                Ok(())
344            }
345            PtrKind::Box => w!(cx, f, "box"),
346        }
347    }
348}
349
350impl Pretty for List<Ty> {
351    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
352        if let [ty] = &self[..] {
353            w!(cx, f, "({:?},)", ty)
354        } else {
355            w!(cx, f, "({:?})", join!(", ", self))
356        }
357    }
358}
359
360impl Pretty for ExistentialPredicate {
361    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
362        match self {
363            ExistentialPredicate::Trait(trait_ref) => w!(cx, f, "{:?}", trait_ref),
364            ExistentialPredicate::Projection(proj) => w!(cx, f, "({:?})", proj),
365            ExistentialPredicate::AutoTrait(def_id) => w!(cx, f, "{:?}", def_id),
366        }
367    }
368}
369
370impl Pretty for ExistentialTraitRef {
371    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
372        w!(cx, f, "{:?}", self.def_id)?;
373        if !self.args.is_empty() {
374            w!(cx, f, "<{:?}>", join!(", ", &self.args))?;
375        }
376        Ok(())
377    }
378}
379
380impl Pretty for ExistentialProjection {
381    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
382        w!(cx, f, "{:?}", self.def_id)?;
383        if !self.args.is_empty() {
384            w!(cx, f, "<{:?}>", join!(", ", &self.args))?;
385        }
386        w!(cx, f, " = {:?}", &self.term)
387    }
388}
389
390impl Pretty for BaseTy {
391    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
392        match self {
393            BaseTy::Int(int_ty) => w!(cx, f, "{}", ^int_ty.name_str()),
394            BaseTy::Uint(uint_ty) => w!(cx, f, "{}", ^uint_ty.name_str()),
395            BaseTy::Bool => w!(cx, f, "bool"),
396            BaseTy::Str => w!(cx, f, "str"),
397            BaseTy::Char => w!(cx, f, "char"),
398            BaseTy::Adt(adt_def, args) => {
399                w!(cx, f, "{:?}", adt_def.did())?;
400                let args = args
401                    .iter()
402                    .filter(|arg| !cx.hide_regions || !matches!(arg, GenericArg::Lifetime(_)))
403                    .collect_vec();
404                if !args.is_empty() {
405                    w!(cx, f, "<{:?}>", join!(", ", args))?;
406                }
407                Ok(())
408            }
409            BaseTy::FnDef(def_id, args) => {
410                w!(cx, f, "FnDef({:?}[{:?}])", def_id, join!(", ", args))
411            }
412            BaseTy::Param(param) => w!(cx, f, "{}", ^param),
413            BaseTy::Float(float_ty) => w!(cx, f, "{}", ^float_ty.name_str()),
414            BaseTy::Slice(ty) => w!(cx, f, "[{:?}]", ty),
415            BaseTy::RawPtr(ty, Mutability::Mut) => w!(cx, f, "*mut {:?}", ty),
416            BaseTy::RawPtr(ty, Mutability::Not) => w!(cx, f, "*const {:?}", ty),
417            BaseTy::RawPtrMetadata(ty) => {
418                w!(cx, f, "*raw {:?}", ty)
419            }
420            BaseTy::Ref(re, ty, mutbl) => {
421                w!(cx, f, "&")?;
422                if !cx.hide_regions {
423                    w!(cx, f, "{:?} ", re)?;
424                }
425                w!(cx, f, "{}{:?}",  ^mutbl.prefix_str(), ty)
426            }
427            BaseTy::FnPtr(poly_fn_sig) => {
428                w!(cx, f, "{:?}", poly_fn_sig)
429            }
430            BaseTy::Tuple(tys) => {
431                if let [ty] = &tys[..] {
432                    w!(cx, f, "({:?},)", ty)
433                } else {
434                    w!(cx, f, "({:?})", join!(", ", tys))
435                }
436            }
437            BaseTy::Alias(kind, alias_ty) => fmt_alias_ty(cx, f, *kind, alias_ty),
438            BaseTy::Array(ty, c) => w!(cx, f, "[{:?}; {:?}]", ty, ^c),
439            BaseTy::Never => w!(cx, f, "!"),
440            BaseTy::Closure(did, args, _) => {
441                w!(cx, f, "{:?}<{:?}>", did, args)
442            }
443            BaseTy::Coroutine(did, resume_ty, upvars) => {
444                w!(cx, f, "Coroutine({:?}, {:?})", did, resume_ty)?;
445                if !upvars.is_empty() {
446                    w!(cx, f, "<{:?}>", join!(", ", upvars))?;
447                }
448                Ok(())
449            }
450            BaseTy::Dynamic(preds, re) => {
451                w!(cx, f, "dyn {:?} + {:?}", join!(" + ", preds), re)
452            }
453            BaseTy::Infer(ty_vid) => {
454                w!(cx, f, "{ty_vid:?}")
455            }
456            BaseTy::Foreign(def_id) => {
457                w!(cx, f, "{:?}", def_id)
458            }
459        }
460    }
461}
462
463fn fmt_alias_ty(
464    cx: &PrettyCx,
465    f: &mut fmt::Formatter<'_>,
466    kind: AliasKind,
467    alias_ty: &AliasTy,
468) -> fmt::Result {
469    match kind {
470        AliasKind::Weak => {
471            w!(cx, f, "{:?}", alias_ty.def_id)?;
472            if !alias_ty.args.is_empty() {
473                w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
474            }
475        }
476        AliasKind::Projection => {
477            let assoc_name = cx.tcx().item_name(alias_ty.def_id);
478            let trait_ref = cx.tcx().parent(alias_ty.def_id);
479            let trait_generic_count = cx.tcx().generics_of(trait_ref).count() - 1;
480
481            let [self_ty, args @ ..] = &alias_ty.args[..] else {
482                return w!(cx, f, "<alias_ty>");
483            };
484
485            w!(cx, f, "<{:?} as {:?}", self_ty, trait_ref)?;
486
487            let trait_generics = &args[..trait_generic_count];
488            if !trait_generics.is_empty() {
489                w!(cx, f, "<{:?}>", join!(", ", trait_generics))?;
490            }
491            w!(cx, f, ">::{}", ^assoc_name)?;
492
493            let assoc_generics = &args[trait_generic_count..];
494            if !assoc_generics.is_empty() {
495                w!(cx, f, "<{:?}>", join!(", ", assoc_generics))?;
496            }
497        }
498        AliasKind::Opaque => {
499            w!(cx, f, "{:?}", alias_ty.def_id)?;
500            if !alias_ty.args.is_empty() {
501                w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
502            }
503            if !alias_ty.refine_args.is_empty() {
504                w!(cx, f, "⟨{:?}⟩", join!(", ", &alias_ty.refine_args))?;
505            }
506        }
507    }
508    Ok(())
509}
510
511impl Pretty for ValTree {
512    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
513        match self {
514            ValTree::Leaf(v) => w!(cx, f, "Leaf({v:?})"),
515            ValTree::Branch(children) => {
516                w!(cx, f, "Branch([{:?}])", join!(", ", children))
517            }
518        }
519    }
520}
521impl Pretty for UnevaluatedConst {
522    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
523        w!(cx, f, "UnevaluatedConst({:?}[...])", self.def)
524    }
525}
526
527impl Pretty for Const {
528    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
529        match &self.kind {
530            ConstKind::Param(p) => w!(cx, f, "{}", ^p.name.as_str()),
531            ConstKind::Value(_, v) => w!(cx, f, "{v:?}"),
532            ConstKind::Infer(infer_const) => w!(cx, f, "{:?}", ^infer_const),
533            ConstKind::Unevaluated(uneval_const) => w!(cx, f, "{:?}", uneval_const),
534        }
535    }
536}
537
538impl Pretty for GenericArg {
539    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
540        match self {
541            GenericArg::Ty(ty) => w!(cx, f, "{:?}", ty),
542            GenericArg::Base(ctor) => {
543                cx.with_bound_vars(ctor.vars(), || {
544                    if !cx.hide_refinements {
545                        cx.fmt_bound_vars(false, "λ", ctor.vars(), ". ", f)?;
546                    }
547                    w!(cx, f, "{:?}", ctor.skip_binder_ref())
548                })
549            }
550            GenericArg::Lifetime(re) => w!(cx, f, "{:?}", re),
551            GenericArg::Const(c) => w!(cx, f, "{:?}", c),
552        }
553    }
554}
555
556impl Pretty for VariantSig {
557    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
558        w!(cx, f, "({:?}) => {:?}", join!(", ", self.fields()), &self.idx)
559    }
560}
561
562impl Pretty for Region {
563    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
564        w!(cx, f, "{}", ^region_to_string(*self))
565    }
566}
567
568impl Pretty for DebruijnIndex {
569    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
570        w!(cx, f, "^{}", ^self.as_usize())
571    }
572}
573
574impl_debug_with_default_cx!(
575    Ensures,
576    Sort,
577    Ty => "ty",
578    BaseTy,
579    FnSig,
580    GenericArg => "generic_arg",
581    VariantSig,
582    PtrKind,
583    FuncSort,
584    SortCtor,
585    SubsetTy,
586    BvSize,
587    ExistentialPredicate,
588);
589
590impl PrettyNested for SubsetTy {
591    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
592        let bty_d = self.bty.fmt_nested(cx)?;
593        let idx_d = IdxFmt(self.idx.clone()).fmt_nested(cx)?;
594        if self.pred.is_trivially_true() {
595            let text = format!("{}[{}]", bty_d.text, idx_d.text);
596            let children = float_children(vec![bty_d.children, idx_d.children]);
597            Ok(NestedString { text, children, key: None })
598        } else {
599            let pred_d = self.pred.fmt_nested(cx)?;
600            let text = format!("{{ {}[{}] | {} }}", bty_d.text, idx_d.text, pred_d.text);
601            let children = float_children(vec![bty_d.children, idx_d.children, pred_d.children]);
602            Ok(NestedString { text, children, key: None })
603        }
604    }
605}
606
607impl PrettyNested for GenericArg {
608    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
609        match self {
610            GenericArg::Ty(ty) => ty.fmt_nested(cx),
611            GenericArg::Base(ctor) => {
612                nested_with_bound_vars(cx, "λ", ctor.vars(), None, |prefix| {
613                    let ctor_d = ctor.skip_binder_ref().fmt_nested(cx)?;
614                    let text = format!("{}{}", prefix, ctor_d.text);
615                    Ok(NestedString { text, children: ctor_d.children, key: None })
616                })
617            }
618            GenericArg::Lifetime(..) | GenericArg::Const(..) => debug_nested(cx, self),
619        }
620    }
621}
622
623impl PrettyNested for BaseTy {
624    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
625        match self {
626            BaseTy::Int(..)
627            | BaseTy::Uint(..)
628            | BaseTy::Bool
629            | BaseTy::Str
630            | BaseTy::Char
631            | BaseTy::Float(..)
632            | BaseTy::Param(..)
633            | BaseTy::Never
634            | BaseTy::FnPtr(..)
635            | BaseTy::FnDef(..)
636            | BaseTy::Alias(..)
637            | BaseTy::Closure(..)
638            | BaseTy::Coroutine(..)
639            | BaseTy::Dynamic(..)
640            | BaseTy::Infer(..)
641            | BaseTy::Foreign(..) => {
642                let text = format_cx!(cx, "{:?}", self);
643                Ok(NestedString { text, children: None, key: None })
644            }
645            BaseTy::Slice(ty) => {
646                let ty_d = ty.fmt_nested(cx)?;
647                let text = format!("[{}]", ty_d.text);
648                Ok(NestedString { text, children: ty_d.children, key: None })
649            }
650            BaseTy::Array(ty, c) => {
651                let ty_d = ty.fmt_nested(cx)?;
652                let text = format_cx!(cx, "[{:?}; {:?}]", ty_d.text, c);
653                Ok(NestedString { text, children: ty_d.children, key: None })
654            }
655            BaseTy::RawPtr(ty, Mutability::Mut) => {
656                let ty_d = ty.fmt_nested(cx)?;
657                let text = format!("*mut {}", ty_d.text);
658                Ok(NestedString { text, children: ty_d.children, key: None })
659            }
660            BaseTy::RawPtr(ty, Mutability::Not) => {
661                let ty_d = ty.fmt_nested(cx)?;
662                let text = format!("*const {}", ty_d.text);
663                Ok(NestedString { text, children: ty_d.children, key: None })
664            }
665            BaseTy::RawPtrMetadata(ty) => {
666                let ty_d = ty.fmt_nested(cx)?;
667                let text = format!("*raw {}", ty_d.text);
668                Ok(NestedString { text, children: ty_d.children, key: None })
669            }
670            BaseTy::Ref(_, ty, mutbl) => {
671                let ty_d = ty.fmt_nested(cx)?;
672                let text = format!("&{} {}", mutbl.prefix_str(), ty_d.text);
673                Ok(NestedString { text, children: ty_d.children, key: None })
674            }
675            BaseTy::Tuple(tys) => {
676                let mut texts = vec![];
677                let mut kidss = vec![];
678                for ty in tys {
679                    let ty_d = ty.fmt_nested(cx)?;
680                    texts.push(ty_d.text);
681                    kidss.push(ty_d.children);
682                }
683                let text = if let [text] = &texts[..] {
684                    format!("({},)", text)
685                } else {
686                    format!("({})", texts.join(", "))
687                };
688                let children = float_children(kidss);
689                Ok(NestedString { text, children, key: None })
690            }
691            BaseTy::Adt(adt_def, args) => {
692                let mut texts = vec![];
693                let mut kidss = vec![];
694                for arg in args {
695                    let arg_d = arg.fmt_nested(cx)?;
696                    texts.push(arg_d.text);
697                    kidss.push(arg_d.children);
698                }
699                let args_str = if !args.is_empty() {
700                    format!("<{}>", texts.join(", "))
701                } else {
702                    String::new()
703                };
704                let text = format_cx!(cx, "{:?}{:?}", adt_def.did(), args_str);
705                let children = float_children(kidss);
706                Ok(NestedString { text, children, key: None })
707            }
708        }
709    }
710}
711
712pub fn nested_with_bound_vars(
713    cx: &PrettyCx,
714    left: &str,
715    vars: &[BoundVariableKind],
716    right: Option<String>,
717    f: impl FnOnce(String) -> Result<NestedString, fmt::Error>,
718) -> Result<NestedString, fmt::Error> {
719    let mut buffer = String::new();
720    cx.with_bound_vars(vars, || {
721        if !vars.is_empty() {
722            let right = right.unwrap_or(". ".to_string());
723            cx.fmt_bound_vars(false, left, vars, &right, &mut buffer)?;
724        }
725        f(buffer)
726    })
727}
728
729impl PrettyNested for Ty {
730    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
731        match self.kind() {
732            TyKind::Indexed(bty, idx) => {
733                let bty_d = bty.fmt_nested(cx)?;
734                let idx_d = IdxFmt(idx.clone()).fmt_nested(cx)?;
735                let text = if idx_d.text.is_empty() {
736                    bty_d.text
737                } else {
738                    format!("{}[{}]", bty_d.text, idx_d.text)
739                };
740                let children = float_children(vec![bty_d.children, idx_d.children]);
741                Ok(NestedString { text, children, key: None })
742            }
743            TyKind::Exists(ty_ctor) => {
744                nested_with_bound_vars(cx, "∃", ty_ctor.vars(), None, |exi_str| {
745                    let ty_ctor_d = ty_ctor.skip_binder_ref().fmt_nested(cx)?;
746                    let text = format!("{}{}", exi_str, ty_ctor_d.text);
747                    Ok(NestedString { text, children: ty_ctor_d.children, key: None })
748                })
749            }
750            TyKind::Constr(expr, ty) => {
751                let expr_d = expr.fmt_nested(cx)?;
752                let ty_d = ty.fmt_nested(cx)?;
753                let text = format!("{{ {} | {} }}", ty_d.text, expr_d.text);
754                let children = float_children(vec![expr_d.children, ty_d.children]);
755                Ok(NestedString { text, children, key: None })
756            }
757            TyKind::StrgRef(re, loc, ty) => {
758                let ty_d = ty.fmt_nested(cx)?;
759                let text = format!("&{:?} strg <{:?}: {}>", re, loc, ty_d.text);
760                Ok(NestedString { text, children: ty_d.children, key: None })
761            }
762            TyKind::Blocked(ty) => {
763                let ty_d = ty.fmt_nested(cx)?;
764                let text = format!("†{}", ty_d.text);
765                Ok(NestedString { text, children: ty_d.children, key: None })
766            }
767            TyKind::Downcast(adt, .., variant_idx, fields) => {
768                let is_struct = adt.is_struct();
769                let mut text = format_cx!(cx, "{:?}", adt.did());
770                if !is_struct {
771                    text.push_str(&format!("::{}", adt.variant(*variant_idx).name));
772                }
773                if is_struct {
774                    text.push_str("{..}");
775                } else {
776                    text.push_str("(..)");
777                }
778                let keys: Vec<String> = if is_struct {
779                    adt.variant(*variant_idx)
780                        .fields
781                        .iter()
782                        .map(|f| f.name.to_string())
783                        .collect()
784                } else {
785                    (0..fields.len()).map(|i| format!("{}", i)).collect()
786                };
787                let mut children = vec![];
788                for (key, field) in keys.into_iter().zip(fields) {
789                    let field_d = field.fmt_nested(cx)?;
790                    children.push(NestedString { key: Some(key), ..field_d });
791                }
792                Ok(NestedString { text, children: Some(children), key: None })
793            }
794            TyKind::Param(..)
795            | TyKind::Uninit
796            | TyKind::Ptr(..)
797            | TyKind::Discr(..)
798            | TyKind::Infer(..) => {
799                let text = format!("{:?}", self);
800                Ok(NestedString { text, children: None, key: None })
801            }
802        }
803    }
804}