1use std::{
2 fmt::{self, Write},
3 iter,
4};
5
6use expr::{FieldBind, pretty::aggregate_nested};
7use rustc_data_structures::snapshot_map::SnapshotMap;
8use rustc_type_ir::DebruijnIndex;
9use ty::{UnevaluatedConst, ValTree, region_to_string};
10
11use super::{fold::TypeVisitable, *};
12use crate::pretty::*;
13
14impl Pretty for ClauseKind {
15 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
16 match self {
17 ClauseKind::Trait(pred) => w!(cx, f, "Trait ({:?})", ^pred),
18 ClauseKind::Projection(pred) => w!(cx, f, "Projection ({:?})", ^pred),
19 ClauseKind::RegionOutlives(pred) => {
20 w!(cx, f, "Outlives ({:?}, {:?})", &pred.0, &pred.1)
21 }
22 ClauseKind::TypeOutlives(pred) => w!(cx, f, "Outlives ({:?}, {:?})", &pred.0, &pred.1),
23 ClauseKind::ConstArgHasType(c, ty) => w!(cx, f, "ConstArgHasType ({:?}, {:?})", c, ty),
24 }
25 }
26}
27
28impl Pretty for BoundRegionKind {
29 fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
30 match self {
31 BoundRegionKind::Anon => w!(cx, f, "'<annon>"),
32 BoundRegionKind::NamedAnon(sym) => w!(cx, f, "'{sym}"),
33 BoundRegionKind::Named(def_id) => w!(cx, f, "'{def_id:?}"),
34 BoundRegionKind::ClosureEnv => w!(cx, f, "'<env>"),
35 }
36 }
37}
38
39impl<T> Pretty for Binder<T>
40where
41 T: Pretty,
42{
43 default fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
44 cx.with_bound_vars(self.vars(), || {
45 if !self.vars().is_empty() {
46 cx.fmt_bound_vars(true, "for<", self.vars(), "> ", f)?;
47 }
48 w!(cx, f, "{:?}", self.skip_binder_ref())
49 })
50 }
51}
52
53impl<T: Pretty> std::fmt::Debug for Binder<T> {
54 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
55 pprint_with_default_cx(f, self, None)
56 }
57}
58
59fn format_fn_root_binder<T: Pretty + TypeVisitable>(
60 binder: &Binder<T>,
61 cx: &PrettyCx,
62 fn_root_layer_type: FnRootLayerType,
63 binder_name: &str,
64 f: &mut fmt::Formatter<'_>,
65) -> fmt::Result {
66 let vars = binder.vars();
67 let redundant_bvars = binder.skip_binder_ref().redundant_bvars();
68
69 cx.with_bound_vars_removable(
70 vars,
71 redundant_bvars,
72 Some(fn_root_layer_type),
73 |f_body| {
74 w!(cx, f_body, "{:?}", binder.skip_binder_ref())
76 },
77 |(), bound_var_layer, body| {
78 let BoundVarLayer {
83 successfully_removed_vars,
84 layer_map: BoundVarLayerMap::FnRootLayerMap(fn_root_layer),
85 ..
86 } = bound_var_layer
87 else {
88 unreachable!()
89 };
90 let filtered_vars = vars
91 .into_iter()
92 .enumerate()
93 .filter_map(|(idx, var)| {
94 let not_removed =
95 !successfully_removed_vars.contains(&BoundVar::from_usize(idx));
96 let refine_var = matches!(var, BoundVariableKind::Refine(..));
97 let not_seen = !fn_root_layer.seen_vars.contains(&BoundVar::from_usize(idx));
98 if not_removed && refine_var && not_seen { Some(var.clone()) } else { None }
99 })
100 .collect_vec();
101 if filtered_vars.is_empty() {
102 write!(f, "{}", body)
103 } else {
104 let left = format!("{binder_name}<");
105 let right = format!("> {}", body);
106 cx.fmt_bound_vars(true, &left, &filtered_vars, &right, f)
107 }
108 },
109 )
110}
111
112impl<T: Pretty> Pretty for EarlyBinder<T> {
113 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
114 cx.with_early_params(|| self.skip_binder_ref().fmt(cx, f))
115 }
116}
117
118impl Pretty for PolyFnSig {
119 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
120 format_fn_root_binder(self, cx, FnRootLayerType::FnArgs, "for", f)
121 }
122}
123
124impl Pretty for SortCtor {
125 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
126 match self {
127 SortCtor::Set => w!(cx, f, "Set"),
128 SortCtor::Map => w!(cx, f, "Map"),
129 SortCtor::User { name, .. } => w!(cx, f, "{}", ^name),
130 SortCtor::Adt(adt_sort_def) => {
131 w!(cx, f, "{:?}", adt_sort_def.did())
132 }
133 }
134 }
135}
136
137impl Pretty for SortInfer {
138 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
139 match self {
140 SortInfer::SortVar(svid) => w!(cx, f, "{:?}", ^svid),
141 SortInfer::NumVar(nvid) => w!(cx, f, "{:?}", ^nvid),
142 }
143 }
144}
145
146impl Pretty for Sort {
147 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
148 match self {
149 Sort::Bool => w!(cx, f, "bool"),
150 Sort::Int => w!(cx, f, "int"),
151 Sort::Real => w!(cx, f, "real"),
152 Sort::Str => w!(cx, f, "str"),
153 Sort::Char => w!(cx, f, "char"),
154 Sort::BitVec(size) => w!(cx, f, "bitvec<{:?}>", size),
155 Sort::Loc => w!(cx, f, "loc"),
156 Sort::Var(n) => w!(cx, f, "@{}", ^n.index()),
157 Sort::Func(sort) => w!(cx, f, "{:?}", sort),
158 Sort::Tuple(sorts) => {
159 if let [sort] = &sorts[..] {
160 w!(cx, f, "({:?},)", sort)
161 } else {
162 w!(cx, f, "({:?})", join!(", ", sorts))
163 }
164 }
165 Sort::Alias(kind, alias_ty) => {
166 fmt_alias_ty(cx, f, *kind, alias_ty)?;
167 w!(cx, f, "::sort")
168 }
169 Sort::App(ctor, sorts) => {
170 if sorts.is_empty() {
171 w!(cx, f, "{:?}", ctor)
172 } else {
173 w!(cx, f, "{:?}<{:?}>", ctor, join!(", ", sorts))
174 }
175 }
176 Sort::Param(param_ty) => w!(cx, f, "{}::sort", ^param_ty),
177 Sort::Infer(svar) => w!(cx, f, "{:?}", svar),
178 Sort::Err => w!(cx, f, "err"),
179 }
180 }
181
182 fn default_cx(tcx: TyCtxt) -> PrettyCx {
183 PrettyCx::default(tcx).hide_refinements(true)
184 }
185}
186
187impl Pretty for SortArg {
188 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
189 match self {
190 SortArg::Sort(sort) => w!(cx, f, "{:?}", sort),
191 SortArg::BvSize(size) => w!(cx, f, "{:?}", size),
192 }
193 }
194}
195
196impl Pretty for BvSize {
197 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
198 match self {
199 BvSize::Fixed(size) => w!(cx, f, "{}", ^size),
200 BvSize::Param(param) => w!(cx, f, "{:?}", ^param),
201 BvSize::Infer(size_vid) => w!(cx, f, "{:?}", ^size_vid),
202 }
203 }
204}
205
206impl Pretty for FuncSort {
207 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
208 match self.inputs() {
209 [input] => {
210 w!(cx, f, "{:?} -> {:?}", input, self.output())
211 }
212 inputs => {
213 w!(cx, f,
214 "({}) -> {:?}",
215 ^inputs
216 .iter()
217 .format_with(", ", |s, f| f(&format_args_cx!(cx, "{:?}", s))),
218 self.output()
219 )
220 }
221 }
222 }
223}
224
225impl Pretty for PolyFuncSort {
226 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
227 if self.params.is_empty() {
228 w!(cx, f, "{:?}", &self.fsort)
229 } else {
230 w!(cx, f, "for<{}> {:?}", ^self.params.len(), &self.fsort)
231 }
232 }
233}
234
235impl Pretty for FnSig {
236 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
237 w!(
238 cx,
239 f,
240 "fn({:?}) -> {:?}",
241 join!(", ", self.inputs.iter().map(|input| input.shallow_canonicalize())),
242 &self.output
243 )?;
244 if !self.requires.is_empty() {
245 w!(cx, f, " requires {:?}", join!(" ∧ ", &self.requires))?;
246 }
247 Ok(())
248 }
249}
250
251impl Pretty for Binder<FnOutput> {
252 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
253 format_fn_root_binder(self, cx, FnRootLayerType::FnRet, "exists", f)
254 }
255}
256
257impl Pretty for FnOutput {
258 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
259 w!(cx, f, "{:?}", &self.ret.shallow_canonicalize())?;
260 if !self.ensures.is_empty() {
261 w!(cx, f, " ensures {:?}", join!(" ∧ ", &self.ensures))?;
262 }
263 Ok(())
264 }
265}
266
267impl Pretty for Ensures {
268 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
269 match self {
270 Ensures::Type(loc, ty) => w!(cx, f, "{:?}: {:?}", ^loc, ty),
271 Ensures::Pred(e) => w!(cx, f, "{:?}", e),
272 }
273 }
274}
275
276impl Pretty for SubsetTy {
277 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
278 w!(cx, f, "{:?}", &self.to_ty())
279 }
280}
281
282struct IdxFmt(Expr);
285
286impl PrettyNested for IdxFmt {
287 fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
288 let kind = self.0.kind();
289 match kind {
290 ExprKind::Ctor(ctor, flds) => aggregate_nested(cx, ctor, flds, false),
291 ExprKind::Tuple(flds) if flds.is_empty() => {
292 Ok(NestedString { text: String::new(), key: None, children: None })
293 }
294 _ => self.0.fmt_nested(cx),
295 }
296 }
297}
298
299impl Pretty for IdxFmt {
300 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
301 let e = if cx.simplify_exprs {
302 self.0.simplify(&SnapshotMap::default())
303 } else {
304 self.0.clone()
305 };
306 let mut buf = String::new();
307 match e.kind() {
308 ExprKind::Ctor(ctor, flds)
309 if let Some(adt_sort_def) = cx.adt_sort_def_of(ctor.def_id())
310 && let Some(variant) = adt_sort_def.opt_struct_variant() =>
311 {
312 let fields = iter::zip(variant.field_names(), flds)
313 .map(|(name, value)| FieldBind { name: *name, value: value.clone() })
314 .collect_vec();
315 if let Some(var_fields) = fields
317 .iter()
318 .map(|field| {
319 if let ExprKind::Var(Var::Bound(debruijn, BoundReft { var, .. })) =
320 field.value.kind()
321 {
322 Some((*debruijn, *var, field.value.clone()))
323 } else {
324 None
325 }
326 })
327 .collect::<Option<Vec<_>>>()
328 {
329 if var_fields.iter().all(|(debruijn, var, _e)| {
331 cx.bvar_env
332 .should_remove_var(*debruijn, *var)
333 .unwrap_or(false)
334 }) {
335 var_fields.iter().for_each(|(debruijn, var, _e)| {
336 cx.bvar_env.mark_var_as_removed(*debruijn, *var);
337 });
338 } else {
344 let mut fields = var_fields.into_iter().map(|(debruijn, var, e)| {
345 if let Some((seen, layer_type)) =
346 cx.bvar_env.check_if_seen_fn_root_bvar(debruijn, var)
347 && !seen
348 {
349 match layer_type {
350 FnRootLayerType::FnArgs => {
351 format_cx!(cx, "@{:?}", e)
352 }
353 FnRootLayerType::FnRet => {
354 format_cx!(cx, "#{:?}", e)
355 }
356 }
357 } else {
358 format_cx!(cx, "{:?}", e)
359 }
360 });
361 buf.write_str(&fields.join(", "))?;
362 }
363 } else {
364 buf.write_str(&format_cx!(cx, "{{ {:?} }}", join!(", ", fields)))?;
365 }
366 }
367 ExprKind::Var(Var::Bound(debruijn, BoundReft { var, .. })) => {
379 if cx
380 .bvar_env
381 .should_remove_var(*debruijn, *var)
382 .unwrap_or(false)
383 {
384 cx.bvar_env.mark_var_as_removed(*debruijn, *var);
385 } else {
387 if let Some((seen, layer_type)) =
388 cx.bvar_env.check_if_seen_fn_root_bvar(*debruijn, *var)
389 && !seen
390 {
391 match layer_type {
392 FnRootLayerType::FnArgs => {
393 buf.write_str("@")?;
394 }
395 FnRootLayerType::FnRet => {
396 buf.write_str("#")?;
397 }
398 }
399 }
400 buf.write_str(&format_cx!(cx, "{:?}", e))?;
401 }
402 }
403 ExprKind::Var(Var::EarlyParam(ep)) => {
404 if let Some(param) = cx.earlyparam_env.borrow_mut().as_mut()
405 && param.insert(*ep)
406 {
407 buf.write_str(&format_cx!(cx, "@{:?}", e))?;
409 } else {
410 buf.write_str(&format_cx!(cx, "{:?}", e))?;
411 }
412 }
413 _ => {
414 buf.write_str(&format_cx!(cx, "{:?}", e))?;
415 }
416 }
417 if !buf.is_empty() { write!(f, "[{}]", buf) } else { Ok(()) }
418 }
419}
420
421impl Pretty for Ty {
422 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
423 match self.kind() {
424 TyKind::Indexed(bty, idx) => {
425 if cx.hide_refinements {
426 w!(cx, f, "{:?}", bty)?;
427 return Ok(());
428 }
429 if idx.is_unit() {
430 w!(cx, f, "{:?}", bty)?;
431 } else {
432 w!(cx, f, "{:?}[{:?}]", parens!(bty, !bty.is_atom()), IdxFmt(idx.clone()))?;
433 }
434 Ok(())
435 }
436 TyKind::Exists(_ty_ctor) => {
437 w!(cx, f, "{:?}", self.shallow_canonicalize())
438 }
439 TyKind::Uninit => w!(cx, f, "uninit"),
440 TyKind::StrgRef(re, loc, ty) => w!(cx, f, "&{:?} strg <{:?}: {:?}>", re, loc, ty),
441 TyKind::Ptr(pk, loc) => w!(cx, f, "ptr({:?}, {:?})", pk, loc),
442 TyKind::Discr(adt_def, place) => {
443 w!(cx, f, "discr({:?}, {:?})", adt_def.did(), ^place)
444 }
445 TyKind::Constr(pred, ty) => {
446 if cx.hide_refinements {
447 w!(cx, f, "{:?}", ty)
448 } else {
449 w!(cx, f, "{{ {:?} | {:?} }}", ty, pred)
450 }
451 }
452 TyKind::Param(param_ty) => w!(cx, f, "{}", ^param_ty),
453 TyKind::Downcast(adt, .., variant_idx, fields) => {
454 w!(cx, f, "{:?}", adt.did())?;
456 if !adt.is_struct() {
458 w!(cx, f, "::{}", ^adt.variant(*variant_idx).name)?;
459 }
460 if adt.is_struct() {
462 let field_binds = iter::zip(&adt.variant(*variant_idx).fields, fields)
463 .map(|(field_def, value)| FieldBind { name: field_def.name, value });
464 w!(cx, f, " {{ {:?} }}", join!(", ", field_binds))?;
465 } else if !fields.is_empty() {
466 w!(cx, f, "({:?})", join!(", ", fields))?;
467 }
468 Ok(())
469 }
470 TyKind::Blocked(ty) => w!(cx, f, "†{:?}", ty),
471 TyKind::Infer(ty_vid) => {
472 w!(cx, f, "{ty_vid:?}")
473 }
474 }
475 }
476
477 fn default_cx(tcx: TyCtxt) -> PrettyCx {
478 PrettyCx::default(tcx).kvar_args(KVarArgs::Hide)
479 }
480}
481
482impl Pretty for PtrKind {
483 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
484 match self {
485 PtrKind::Mut(re) => {
486 w!(cx, f, "mut")?;
487 if !cx.hide_regions {
488 w!(cx, f, "[{:?}]", re)?;
489 }
490 Ok(())
491 }
492 PtrKind::Box => w!(cx, f, "box"),
493 }
494 }
495}
496
497impl Pretty for List<Ty> {
498 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
499 if let [ty] = &self[..] {
500 w!(cx, f, "({:?},)", ty)
501 } else {
502 w!(cx, f, "({:?})", join!(", ", self))
503 }
504 }
505}
506
507impl Pretty for ExistentialPredicate {
508 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
509 match self {
510 ExistentialPredicate::Trait(trait_ref) => w!(cx, f, "{:?}", trait_ref),
511 ExistentialPredicate::Projection(proj) => w!(cx, f, "({:?})", proj),
512 ExistentialPredicate::AutoTrait(def_id) => w!(cx, f, "{:?}", def_id),
513 }
514 }
515}
516
517impl Pretty for ExistentialTraitRef {
518 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
519 w!(cx, f, "{:?}", self.def_id)?;
520 if !self.args.is_empty() {
521 w!(cx, f, "<{:?}>", join!(", ", &self.args))?;
522 }
523 Ok(())
524 }
525}
526
527impl Pretty for ExistentialProjection {
528 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
529 w!(cx, f, "{:?}", self.def_id)?;
530 if !self.args.is_empty() {
531 w!(cx, f, "<{:?}>", join!(", ", &self.args))?;
532 }
533 w!(cx, f, " = {:?}", &self.term)
534 }
535}
536
537impl Pretty for BaseTy {
538 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
539 match self {
540 BaseTy::Int(int_ty) => w!(cx, f, "{}", ^int_ty.name_str()),
541 BaseTy::Uint(uint_ty) => w!(cx, f, "{}", ^uint_ty.name_str()),
542 BaseTy::Bool => w!(cx, f, "bool"),
543 BaseTy::Str => w!(cx, f, "str"),
544 BaseTy::Char => w!(cx, f, "char"),
545 BaseTy::Adt(adt_def, args) => {
546 w!(cx, f, "{:?}", adt_def.did())?;
547 let args = args
548 .iter()
549 .filter(|arg| !cx.hide_regions || !matches!(arg, GenericArg::Lifetime(_)))
550 .collect_vec();
551 if !args.is_empty() {
552 w!(cx, f, "<{:?}>", join!(", ", args))?;
553 }
554 Ok(())
555 }
556 BaseTy::FnDef(def_id, args) => {
557 w!(cx, f, "FnDef({:?}[{:?}])", def_id, join!(", ", args))
558 }
559 BaseTy::Param(param) => w!(cx, f, "{}", ^param),
560 BaseTy::Float(float_ty) => w!(cx, f, "{}", ^float_ty.name_str()),
561 BaseTy::Slice(ty) => w!(cx, f, "[{:?}]", ty),
562 BaseTy::RawPtr(ty, Mutability::Mut) => w!(cx, f, "*mut {:?}", ty),
563 BaseTy::RawPtr(ty, Mutability::Not) => w!(cx, f, "*const {:?}", ty),
564 BaseTy::RawPtrMetadata(ty) => {
565 w!(cx, f, "*raw {:?}", ty)
566 }
567 BaseTy::Ref(re, ty, mutbl) => {
568 w!(cx, f, "&")?;
569 if !cx.hide_regions {
570 w!(cx, f, "{:?} ", re)?;
571 }
572 w!(cx, f, "{}{:?}", ^mutbl.prefix_str(), ty)
573 }
574 BaseTy::FnPtr(poly_fn_sig) => {
575 w!(cx, f, "{:?}", poly_fn_sig)
576 }
577 BaseTy::Tuple(tys) => {
578 if let [ty] = &tys[..] {
579 w!(cx, f, "({:?},)", ty)
580 } else {
581 w!(cx, f, "({:?})", join!(", ", tys))
582 }
583 }
584 BaseTy::Alias(kind, alias_ty) => fmt_alias_ty(cx, f, *kind, alias_ty),
585 BaseTy::Array(ty, c) => w!(cx, f, "[{:?}; {:?}]", ty, ^c),
586 BaseTy::Never => w!(cx, f, "!"),
587 BaseTy::Closure(did, args, _) => {
588 w!(cx, f, "{:?}<{:?}>", did, args)
589 }
590 BaseTy::Coroutine(did, resume_ty, upvars) => {
591 w!(cx, f, "Coroutine({:?}, {:?})", did, resume_ty)?;
592 if !upvars.is_empty() {
593 w!(cx, f, "<{:?}>", join!(", ", upvars))?;
594 }
595 Ok(())
596 }
597 BaseTy::Dynamic(preds, re) => {
598 w!(cx, f, "dyn {:?} + {:?}", join!(" + ", preds), re)
599 }
600 BaseTy::Infer(ty_vid) => {
601 w!(cx, f, "{ty_vid:?}")
602 }
603 BaseTy::Foreign(def_id) => {
604 w!(cx, f, "{:?}", def_id)
605 }
606 }
607 }
608}
609
610fn fmt_alias_ty(
611 cx: &PrettyCx,
612 f: &mut fmt::Formatter<'_>,
613 kind: AliasKind,
614 alias_ty: &AliasTy,
615) -> fmt::Result {
616 match kind {
617 AliasKind::Free => {
618 w!(cx, f, "{:?}", alias_ty.def_id)?;
619 if !alias_ty.args.is_empty() {
620 w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
621 }
622 }
623 AliasKind::Projection => {
624 let assoc_name = cx.tcx().item_name(alias_ty.def_id);
625 let trait_ref = cx.tcx().parent(alias_ty.def_id);
626 let trait_generic_count = cx.tcx().generics_of(trait_ref).count() - 1;
627
628 let [self_ty, args @ ..] = &alias_ty.args[..] else {
629 return w!(cx, f, "<alias_ty>");
630 };
631
632 w!(cx, f, "<{:?} as {:?}", self_ty, trait_ref)?;
633
634 let trait_generics = &args[..trait_generic_count];
635 if !trait_generics.is_empty() {
636 w!(cx, f, "<{:?}>", join!(", ", trait_generics))?;
637 }
638 w!(cx, f, ">::{}", ^assoc_name)?;
639
640 let assoc_generics = &args[trait_generic_count..];
641 if !assoc_generics.is_empty() {
642 w!(cx, f, "<{:?}>", join!(", ", assoc_generics))?;
643 }
644 }
645 AliasKind::Opaque => {
646 w!(cx, f, "{:?}", alias_ty.def_id)?;
647 if !alias_ty.args.is_empty() {
648 w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
649 }
650 if !alias_ty.refine_args.is_empty() {
651 w!(cx, f, "⟨{:?}⟩", join!(", ", &alias_ty.refine_args))?;
652 }
653 }
654 }
655 Ok(())
656}
657
658impl Pretty for ValTree {
659 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
660 match self {
661 ValTree::Leaf(v) => w!(cx, f, "Leaf({v:?})"),
662 ValTree::Branch(children) => {
663 w!(cx, f, "Branch([{:?}])", join!(", ", children))
664 }
665 }
666 }
667}
668impl Pretty for UnevaluatedConst {
669 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
670 w!(cx, f, "UnevaluatedConst({:?}[...])", self.def)
671 }
672}
673
674impl Pretty for Const {
675 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
676 match &self.kind {
677 ConstKind::Param(p) => w!(cx, f, "{}", ^p.name.as_str()),
678 ConstKind::Value(_, v) => w!(cx, f, "{v:?}"),
679 ConstKind::Infer(infer_const) => w!(cx, f, "{:?}", ^infer_const),
680 ConstKind::Unevaluated(uneval_const) => w!(cx, f, "{:?}", uneval_const),
681 }
682 }
683}
684
685impl Pretty for GenericArg {
686 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
687 match self {
688 GenericArg::Ty(ty) => w!(cx, f, "{:?}", ty),
689 GenericArg::Base(ctor) => w!(cx, f, "{:?}", ctor.to_ty()),
690 GenericArg::Lifetime(re) => w!(cx, f, "{:?}", re),
691 GenericArg::Const(c) => w!(cx, f, "{:?}", c),
692 }
693 }
694}
695
696impl Pretty for VariantSig {
697 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
698 w!(cx, f, "({:?}) => {:?}", join!(", ", self.fields()), &self.idx)
699 }
700}
701
702impl Pretty for Region {
703 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
704 w!(cx, f, "{}", ^region_to_string(*self))
705 }
706}
707
708impl Pretty for DebruijnIndex {
709 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
710 w!(cx, f, "^{}", ^self.as_usize())
711 }
712}
713
714impl_debug_with_default_cx!(
715 Ensures,
716 Sort,
717 Ty => "ty",
718 BaseTy,
719 FnSig,
720 GenericArg => "generic_arg",
721 VariantSig,
722 PtrKind,
723 FuncSort,
724 SortCtor,
725 SubsetTy,
726 BvSize,
727 ExistentialPredicate,
728);
729
730impl PrettyNested for SubsetTy {
731 fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
732 let bty_d = self.bty.fmt_nested(cx)?;
733 let idx_d = IdxFmt(self.idx.clone()).fmt_nested(cx)?;
734 if self.pred.is_trivially_true() || matches!(self.pred.kind(), ExprKind::KVar(..)) {
735 let text = format!("{}[{}]", bty_d.text, idx_d.text);
736 let children = float_children(vec![bty_d.children, idx_d.children]);
737 Ok(NestedString { text, children, key: None })
738 } else {
739 let pred_d = self.pred.fmt_nested(cx)?;
740 let text = format!("{{ {}[{}] | {} }}", bty_d.text, idx_d.text, pred_d.text);
741 let children = float_children(vec![bty_d.children, idx_d.children, pred_d.children]);
742 Ok(NestedString { text, children, key: None })
743 }
744 }
745}
746
747impl PrettyNested for GenericArg {
748 fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
749 match self {
750 GenericArg::Ty(ty) => ty.fmt_nested(cx),
751 GenericArg::Base(ctor) => {
752 let inner = ctor.as_ref().skip_binder();
754 if ctor.vars().len() == 1 && inner.pred.is_trivially_true() && inner.idx.is_nu() {
755 inner.bty.fmt_nested(cx)
756 } else {
757 nested_with_bound_vars(cx, "λ", ctor.vars(), None, |prefix| {
758 let ctor_d = ctor.skip_binder_ref().fmt_nested(cx)?;
759 let text = format!("{}{}", prefix, ctor_d.text);
760 Ok(NestedString { text, children: ctor_d.children, key: None })
761 })
762 }
763 }
764 GenericArg::Lifetime(..) | GenericArg::Const(..) => debug_nested(cx, self),
765 }
766 }
767}
768
769impl PrettyNested for BaseTy {
770 fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
771 match self {
772 BaseTy::Int(..)
773 | BaseTy::Uint(..)
774 | BaseTy::Bool
775 | BaseTy::Str
776 | BaseTy::Char
777 | BaseTy::Float(..)
778 | BaseTy::Param(..)
779 | BaseTy::Never
780 | BaseTy::FnPtr(..)
781 | BaseTy::FnDef(..)
782 | BaseTy::Alias(..)
783 | BaseTy::Closure(..)
784 | BaseTy::Coroutine(..)
785 | BaseTy::Dynamic(..)
786 | BaseTy::Infer(..)
787 | BaseTy::Foreign(..) => {
788 let text = format_cx!(cx, "{:?}", self);
789 Ok(NestedString { text, children: None, key: None })
790 }
791 BaseTy::Slice(ty) => {
792 let ty_d = ty.fmt_nested(cx)?;
793 let text = format!("[{}]", ty_d.text);
794 Ok(NestedString { text, children: ty_d.children, key: None })
795 }
796 BaseTy::Array(ty, c) => {
797 let ty_d = ty.fmt_nested(cx)?;
798 let text = format_cx!(cx, "[{:?}; {:?}]", ty_d.text, c);
799 Ok(NestedString { text, children: ty_d.children, key: None })
800 }
801 BaseTy::RawPtr(ty, Mutability::Mut) => {
802 let ty_d = ty.fmt_nested(cx)?;
803 let text = format!("*mut {}", ty_d.text);
804 Ok(NestedString { text, children: ty_d.children, key: None })
805 }
806 BaseTy::RawPtr(ty, Mutability::Not) => {
807 let ty_d = ty.fmt_nested(cx)?;
808 let text = format!("*const {}", ty_d.text);
809 Ok(NestedString { text, children: ty_d.children, key: None })
810 }
811 BaseTy::RawPtrMetadata(ty) => {
812 let ty_d = ty.fmt_nested(cx)?;
813 let text = format!("*raw {}", ty_d.text);
814 Ok(NestedString { text, children: ty_d.children, key: None })
815 }
816 BaseTy::Ref(_, ty, mutbl) => {
817 let ty_d = ty.fmt_nested(cx)?;
818 let prefix = mutbl.prefix_str();
819 let text = if prefix.is_empty() {
820 format!("&{}", ty_d.text)
821 } else {
822 format!("&{} {}", prefix, ty_d.text)
823 };
824 Ok(NestedString { text, children: ty_d.children, key: None })
825 }
826 BaseTy::Tuple(tys) => {
827 let mut texts = vec![];
828 let mut kidss = vec![];
829 for ty in tys {
830 let ty_d = ty.fmt_nested(cx)?;
831 texts.push(ty_d.text);
832 kidss.push(ty_d.children);
833 }
834 let text = if let [text] = &texts[..] {
835 format!("({text},)")
836 } else {
837 format!("({})", texts.join(", "))
838 };
839 let children = float_children(kidss);
840 Ok(NestedString { text, children, key: None })
841 }
842 BaseTy::Adt(adt_def, args) => {
843 let mut texts = vec![];
844 let mut kidss = vec![];
845 for arg in args {
846 let arg_d = arg.fmt_nested(cx)?;
847 texts.push(arg_d.text);
848 kidss.push(arg_d.children);
849 }
850 let args_str = if !args.is_empty() {
851 format!("<{}>", texts.join(", "))
852 } else {
853 String::new()
854 };
855 let text = format_cx!(cx, "{:?}{:?}", adt_def.did(), args_str);
856 let children = float_children(kidss);
857 Ok(NestedString { text, children, key: None })
858 }
859 }
860 }
861}
862
863pub fn nested_with_bound_vars(
864 cx: &PrettyCx,
865 left: &str,
866 vars: &[BoundVariableKind],
867 right: Option<String>,
868 f: impl FnOnce(String) -> Result<NestedString, fmt::Error>,
869) -> Result<NestedString, fmt::Error> {
870 let mut buffer = String::new();
871 cx.with_bound_vars(vars, || {
872 if !vars.is_empty() {
873 let right = right.unwrap_or(". ".to_string());
874 cx.fmt_bound_vars(false, left, vars, &right, &mut buffer)?;
875 }
876 f(buffer)
877 })
878}
879
880impl PrettyNested for Ty {
881 fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
882 match self.kind() {
883 TyKind::Indexed(bty, idx) => {
884 let bty_d = bty.fmt_nested(cx)?;
885 let idx_d = IdxFmt(idx.clone()).fmt_nested(cx)?;
886 let text = if idx_d.text.is_empty() {
887 bty_d.text
888 } else {
889 format!("{}[{}]", bty_d.text, idx_d.text)
890 };
891 let children = float_children(vec![bty_d.children, idx_d.children]);
892 Ok(NestedString { text, children, key: None })
893 }
894 TyKind::Exists(ty_ctor) => {
895 if ty_ctor.vars().len() == 1
898 && let TyKind::Indexed(bty, idx) = ty_ctor.skip_binder_ref().kind()
899 && idx.is_nu()
900 {
901 bty.fmt_nested(cx)
902 } else {
903 nested_with_bound_vars(cx, "∃", ty_ctor.vars(), None, |exi_str| {
904 let ty_ctor_d = ty_ctor.skip_binder_ref().fmt_nested(cx)?;
905 let text = format!("{}{}", exi_str, ty_ctor_d.text);
906 Ok(NestedString { text, children: ty_ctor_d.children, key: None })
907 })
908 }
909 }
910 TyKind::Constr(expr, ty) => {
911 let expr_d = expr.fmt_nested(cx)?;
912 let ty_d = ty.fmt_nested(cx)?;
913 let text = format!("{{ {} | {} }}", ty_d.text, expr_d.text);
914 let children = float_children(vec![expr_d.children, ty_d.children]);
915 Ok(NestedString { text, children, key: None })
916 }
917 TyKind::StrgRef(re, loc, ty) => {
918 let ty_d = ty.fmt_nested(cx)?;
919 let text = format!("&{:?} strg <{:?}: {}>", re, loc, ty_d.text);
920 Ok(NestedString { text, children: ty_d.children, key: None })
921 }
922 TyKind::Blocked(ty) => {
923 let ty_d = ty.fmt_nested(cx)?;
924 let text = format!("†{}", ty_d.text);
925 Ok(NestedString { text, children: ty_d.children, key: None })
926 }
927 TyKind::Downcast(adt, .., variant_idx, fields) => {
928 let is_struct = adt.is_struct();
929 let mut text = format_cx!(cx, "{:?}", adt.did());
930 if !is_struct {
931 text.push_str(&format!("::{}", adt.variant(*variant_idx).name));
932 }
933 if is_struct {
934 text.push_str("{..}");
935 } else {
936 text.push_str("(..)");
937 }
938 let keys: Vec<String> = if is_struct {
939 adt.variant(*variant_idx)
940 .fields
941 .iter()
942 .map(|f| f.name.to_string())
943 .collect()
944 } else {
945 (0..fields.len()).map(|i| format!("{i}")).collect()
946 };
947 let mut children = vec![];
948 for (key, field) in keys.into_iter().zip(fields) {
949 let field_d = field.fmt_nested(cx)?;
950 children.push(NestedString { key: Some(key), ..field_d });
951 }
952 Ok(NestedString { text, children: Some(children), key: None })
953 }
954 TyKind::Param(..)
955 | TyKind::Uninit
956 | TyKind::Ptr(..)
957 | TyKind::Discr(..)
958 | TyKind::Infer(..) => {
959 let text = format!("{self:?}");
960 Ok(NestedString { text, children: None, key: None })
961 }
962 }
963 }
964}