flux_middle/rty/
pretty.rs

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            // First format the body, adding a dectorator (@ or #) to vars in indexes that we can.
75            w!(cx, f_body, "{:?}", binder.skip_binder_ref())
76        },
77        |(), bound_var_layer, body| {
78            // Then remove any vars that we added a decorator to.
79            //
80            // As well as any vars that we are removing because they are redundant.
81
82            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(def_id) => w!(cx, f, "{}", ^def_id.name()),
130            SortCtor::Adt(adt_sort_def) => {
131                w!(cx, f, "{:?}", adt_sort_def.did())
132            }
133        }
134    }
135}
136
137impl Pretty for Sort {
138    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
139        match self {
140            Sort::Bool => w!(cx, f, "bool"),
141            Sort::Int => w!(cx, f, "int"),
142            Sort::Real => w!(cx, f, "real"),
143            Sort::Str => w!(cx, f, "str"),
144            Sort::Char => w!(cx, f, "char"),
145            Sort::BitVec(size) => w!(cx, f, "bitvec<{:?}>", size),
146            Sort::Loc => w!(cx, f, "loc"),
147            Sort::Var(n) => w!(cx, f, "@{}", ^n.index()),
148            Sort::Func(sort) => w!(cx, f, "{:?}", sort),
149            Sort::Tuple(sorts) => {
150                if let [sort] = &sorts[..] {
151                    w!(cx, f, "({:?},)", sort)
152                } else {
153                    w!(cx, f, "({:?})", join!(", ", sorts))
154                }
155            }
156            Sort::Alias(kind, alias_ty) => {
157                fmt_alias_ty(cx, f, *kind, alias_ty)?;
158                w!(cx, f, "::sort")
159            }
160            Sort::App(ctor, sorts) => {
161                if sorts.is_empty() {
162                    w!(cx, f, "{:?}", ctor)
163                } else {
164                    w!(cx, f, "{:?}<{:?}>", ctor, join!(", ", sorts))
165                }
166            }
167            Sort::Param(param_ty) => w!(cx, f, "{}::sort", ^param_ty),
168            Sort::Infer(svar) => w!(cx, f, "{:?}", ^svar),
169            Sort::Err => w!(cx, f, "err"),
170        }
171    }
172
173    fn default_cx(tcx: TyCtxt) -> PrettyCx {
174        PrettyCx::default(tcx).hide_refinements(true)
175    }
176}
177
178impl Pretty for SortArg {
179    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
180        match self {
181            SortArg::Sort(sort) => w!(cx, f, "{:?}", sort),
182            SortArg::BvSize(size) => w!(cx, f, "{:?}", size),
183        }
184    }
185}
186
187impl Pretty for BvSize {
188    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
189        match self {
190            BvSize::Fixed(size) => w!(cx, f, "{}", ^size),
191            BvSize::Param(param) => w!(cx, f, "{:?}", ^param),
192            BvSize::Infer(size_vid) => w!(cx, f, "{:?}", ^size_vid),
193        }
194    }
195}
196
197impl Pretty for FuncSort {
198    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
199        match self.inputs() {
200            [input] => {
201                w!(cx, f, "{:?} -> {:?}", input, self.output())
202            }
203            inputs => {
204                w!(cx, f,
205                   "({}) -> {:?}",
206                   ^inputs
207                       .iter()
208                       .format_with(", ", |s, f| f(&format_args_cx!(cx, "{:?}", s))),
209                   self.output()
210                )
211            }
212        }
213    }
214}
215
216impl Pretty for PolyFuncSort {
217    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
218        if self.params.is_empty() {
219            w!(cx, f, "{:?}", &self.fsort)
220        } else {
221            w!(cx, f, "for<{}> {:?}", ^self.params.len(), &self.fsort)
222        }
223    }
224}
225
226impl Pretty for FnSig {
227    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
228        w!(
229            cx,
230            f,
231            "fn({:?}) -> {:?}",
232            join!(", ", self.inputs.iter().map(|input| input.shallow_canonicalize())),
233            &self.output
234        )?;
235        if !self.requires.is_empty() {
236            w!(cx, f, " requires {:?}", join!(" ∧ ", &self.requires))?;
237        }
238        Ok(())
239    }
240}
241
242impl Pretty for Binder<FnOutput> {
243    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
244        format_fn_root_binder(self, cx, FnRootLayerType::FnRet, "exists", f)
245    }
246}
247
248impl Pretty for FnOutput {
249    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
250        w!(cx, f, "{:?}", &self.ret.shallow_canonicalize())?;
251        if !self.ensures.is_empty() {
252            w!(cx, f, " ensures {:?}", join!(" ∧ ", &self.ensures))?;
253        }
254        Ok(())
255    }
256}
257
258impl Pretty for Ensures {
259    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
260        match self {
261            Ensures::Type(loc, ty) => w!(cx, f, "{:?}: {:?}", ^loc, ty),
262            Ensures::Pred(e) => w!(cx, f, "{:?}", e),
263        }
264    }
265}
266
267impl Pretty for SubsetTy {
268    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
269        w!(cx, f, "{:?}", &self.to_ty())
270    }
271}
272
273// This is a trick to avoid pretty printing `S [S { x: 10, y: 20}]`
274// and instead just print `S[{x: 10, y: 20}]` for struct-valued indices.
275struct IdxFmt(Expr);
276
277impl PrettyNested for IdxFmt {
278    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
279        let kind = self.0.kind();
280        match kind {
281            ExprKind::Ctor(ctor, flds) => aggregate_nested(cx, ctor, flds, false),
282            ExprKind::Tuple(flds) if flds.is_empty() => {
283                Ok(NestedString { text: String::new(), key: None, children: None })
284            }
285            _ => self.0.fmt_nested(cx),
286        }
287    }
288}
289
290impl Pretty for IdxFmt {
291    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
292        let e = if cx.simplify_exprs {
293            self.0.simplify(&SnapshotMap::default())
294        } else {
295            self.0.clone()
296        };
297        let mut buf = String::new();
298        match e.kind() {
299            ExprKind::Ctor(ctor, flds)
300                if let Some(adt_sort_def) = cx.adt_sort_def_of(ctor.def_id())
301                    && let Some(variant) = adt_sort_def.opt_struct_variant() =>
302            {
303                let fields = iter::zip(variant.field_names(), flds)
304                    .map(|(name, value)| FieldBind { name: *name, value: value.clone() })
305                    .collect_vec();
306                // Check if _all_ the fields are vars
307                if let Some(var_fields) = fields
308                    .iter()
309                    .map(|field| {
310                        if let ExprKind::Var(Var::Bound(debruijn, BoundReft { var, .. })) =
311                            field.value.kind()
312                        {
313                            Some((*debruijn, *var, field.value.clone()))
314                        } else {
315                            None
316                        }
317                    })
318                    .collect::<Option<Vec<_>>>()
319                {
320                    // If they are all meant to be removed, we can elide the entire index.
321                    if var_fields.iter().all(|(debruijn, var, _e)| {
322                        cx.bvar_env
323                            .should_remove_var(*debruijn, *var)
324                            .unwrap_or(false)
325                    }) {
326                        var_fields.iter().for_each(|(debruijn, var, _e)| {
327                            cx.bvar_env.mark_var_as_removed(*debruijn, *var);
328                        });
329                        // We write nothing here: we can erase the index
330                        // If we can't remove all of the vars, we can still elide the
331                        // constructor names and do our normal thing of adding @ and #
332                        //
333                        // NOTE: this is heavily copied from the var case below.
334                    } else {
335                        let mut fields = var_fields.into_iter().map(|(debruijn, var, e)| {
336                            if let Some((seen, layer_type)) =
337                                cx.bvar_env.check_if_seen_fn_root_bvar(debruijn, var)
338                                && !seen
339                            {
340                                match layer_type {
341                                    FnRootLayerType::FnArgs => {
342                                        format_cx!(cx, "@{:?}", e)
343                                    }
344                                    FnRootLayerType::FnRet => {
345                                        format_cx!(cx, "#{:?}", e)
346                                    }
347                                }
348                            } else {
349                                format_cx!(cx, "{:?}", e)
350                            }
351                        });
352                        buf.write_str(&fields.join(", "))?;
353                    }
354                } else {
355                    buf.write_str(&format_cx!(cx, "{{ {:?} }}", join!(", ", fields)))?;
356                }
357            }
358            // The first time we encounter a var in an index position where it
359            // can introduce an existential (at the function root level), we put
360            // a marker in front of it depending on where the var is.
361            //
362            // * If it's in the argument position, we use @
363            // * If it's in the return position, we use #
364            //
365            // This does not take priority over removing variables, which
366            // we check to do first.
367            //
368            // TODO: handle more complicated cases such as structs.
369            ExprKind::Var(Var::Bound(debruijn, BoundReft { var, .. })) => {
370                if cx
371                    .bvar_env
372                    .should_remove_var(*debruijn, *var)
373                    .unwrap_or(false)
374                {
375                    cx.bvar_env.mark_var_as_removed(*debruijn, *var);
376                    // don't write anything
377                } else {
378                    if let Some((seen, layer_type)) =
379                        cx.bvar_env.check_if_seen_fn_root_bvar(*debruijn, *var)
380                        && !seen
381                    {
382                        match layer_type {
383                            FnRootLayerType::FnArgs => {
384                                buf.write_str("@")?;
385                            }
386                            FnRootLayerType::FnRet => {
387                                buf.write_str("#")?;
388                            }
389                        }
390                    }
391                    buf.write_str(&format_cx!(cx, "{:?}", e))?;
392                }
393            }
394            ExprKind::Var(Var::EarlyParam(ep)) => {
395                if let Some(param) = cx.earlyparam_env.borrow_mut().as_mut()
396                    && param.insert(*ep)
397                {
398                    // FIXME: handle adding # for early params in output position
399                    buf.write_str(&format_cx!(cx, "@{:?}", e))?;
400                } else {
401                    buf.write_str(&format_cx!(cx, "{:?}", e))?;
402                }
403            }
404            _ => {
405                buf.write_str(&format_cx!(cx, "{:?}", e))?;
406            }
407        }
408        if !buf.is_empty() { write!(f, "[{}]", buf) } else { Ok(()) }
409    }
410}
411
412impl Pretty for Ty {
413    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
414        match self.kind() {
415            TyKind::Indexed(bty, idx) => {
416                if cx.hide_refinements {
417                    w!(cx, f, "{:?}", bty)?;
418                    return Ok(());
419                }
420                if idx.is_unit() {
421                    w!(cx, f, "{:?}", bty)?;
422                } else {
423                    w!(cx, f, "{:?}[{:?}]", parens!(bty, !bty.is_atom()), IdxFmt(idx.clone()))?;
424                }
425                Ok(())
426            }
427            TyKind::Exists(_ty_ctor) => {
428                w!(cx, f, "{:?}", self.shallow_canonicalize())
429            }
430            TyKind::Uninit => w!(cx, f, "uninit"),
431            TyKind::StrgRef(re, loc, ty) => w!(cx, f, "&{:?} strg <{:?}: {:?}>", re, loc, ty),
432            TyKind::Ptr(pk, loc) => w!(cx, f, "ptr({:?}, {:?})", pk, loc),
433            TyKind::Discr(adt_def, place) => {
434                w!(cx, f, "discr({:?}, {:?})", adt_def.did(), ^place)
435            }
436            TyKind::Constr(pred, ty) => {
437                if cx.hide_refinements {
438                    w!(cx, f, "{:?}", ty)
439                } else {
440                    w!(cx, f, "{{ {:?} | {:?} }}", ty, pred)
441                }
442            }
443            TyKind::Param(param_ty) => w!(cx, f, "{}", ^param_ty),
444            TyKind::Downcast(adt, .., variant_idx, fields) => {
445                // base-name
446                w!(cx, f, "{:?}", adt.did())?;
447                // variant-name: if it is not a struct
448                if !adt.is_struct() {
449                    w!(cx, f, "::{}", ^adt.variant(*variant_idx).name)?;
450                }
451                // fields: use curly-braces + names for structs, otherwise use parens
452                if adt.is_struct() {
453                    let field_binds = iter::zip(&adt.variant(*variant_idx).fields, fields)
454                        .map(|(field_def, value)| FieldBind { name: field_def.name, value });
455                    w!(cx, f, " {{ {:?} }}", join!(", ", field_binds))?;
456                } else if !fields.is_empty() {
457                    w!(cx, f, "({:?})", join!(", ", fields))?;
458                }
459                Ok(())
460            }
461            TyKind::Blocked(ty) => w!(cx, f, "†{:?}", ty),
462            TyKind::Infer(ty_vid) => {
463                w!(cx, f, "{ty_vid:?}")
464            }
465        }
466    }
467
468    fn default_cx(tcx: TyCtxt) -> PrettyCx {
469        PrettyCx::default(tcx).kvar_args(KVarArgs::Hide)
470    }
471}
472
473impl Pretty for PtrKind {
474    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
475        match self {
476            PtrKind::Mut(re) => {
477                w!(cx, f, "mut")?;
478                if !cx.hide_regions {
479                    w!(cx, f, "[{:?}]", re)?;
480                }
481                Ok(())
482            }
483            PtrKind::Box => w!(cx, f, "box"),
484        }
485    }
486}
487
488impl Pretty for List<Ty> {
489    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
490        if let [ty] = &self[..] {
491            w!(cx, f, "({:?},)", ty)
492        } else {
493            w!(cx, f, "({:?})", join!(", ", self))
494        }
495    }
496}
497
498impl Pretty for ExistentialPredicate {
499    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
500        match self {
501            ExistentialPredicate::Trait(trait_ref) => w!(cx, f, "{:?}", trait_ref),
502            ExistentialPredicate::Projection(proj) => w!(cx, f, "({:?})", proj),
503            ExistentialPredicate::AutoTrait(def_id) => w!(cx, f, "{:?}", def_id),
504        }
505    }
506}
507
508impl Pretty for ExistentialTraitRef {
509    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
510        w!(cx, f, "{:?}", self.def_id)?;
511        if !self.args.is_empty() {
512            w!(cx, f, "<{:?}>", join!(", ", &self.args))?;
513        }
514        Ok(())
515    }
516}
517
518impl Pretty for ExistentialProjection {
519    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
520        w!(cx, f, "{:?}", self.def_id)?;
521        if !self.args.is_empty() {
522            w!(cx, f, "<{:?}>", join!(", ", &self.args))?;
523        }
524        w!(cx, f, " = {:?}", &self.term)
525    }
526}
527
528impl Pretty for BaseTy {
529    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
530        match self {
531            BaseTy::Int(int_ty) => w!(cx, f, "{}", ^int_ty.name_str()),
532            BaseTy::Uint(uint_ty) => w!(cx, f, "{}", ^uint_ty.name_str()),
533            BaseTy::Bool => w!(cx, f, "bool"),
534            BaseTy::Str => w!(cx, f, "str"),
535            BaseTy::Char => w!(cx, f, "char"),
536            BaseTy::Adt(adt_def, args) => {
537                w!(cx, f, "{:?}", adt_def.did())?;
538                let args = args
539                    .iter()
540                    .filter(|arg| !cx.hide_regions || !matches!(arg, GenericArg::Lifetime(_)))
541                    .collect_vec();
542                if !args.is_empty() {
543                    w!(cx, f, "<{:?}>", join!(", ", args))?;
544                }
545                Ok(())
546            }
547            BaseTy::FnDef(def_id, args) => {
548                w!(cx, f, "FnDef({:?}[{:?}])", def_id, join!(", ", args))
549            }
550            BaseTy::Param(param) => w!(cx, f, "{}", ^param),
551            BaseTy::Float(float_ty) => w!(cx, f, "{}", ^float_ty.name_str()),
552            BaseTy::Slice(ty) => w!(cx, f, "[{:?}]", ty),
553            BaseTy::RawPtr(ty, Mutability::Mut) => w!(cx, f, "*mut {:?}", ty),
554            BaseTy::RawPtr(ty, Mutability::Not) => w!(cx, f, "*const {:?}", ty),
555            BaseTy::RawPtrMetadata(ty) => {
556                w!(cx, f, "*raw {:?}", ty)
557            }
558            BaseTy::Ref(re, ty, mutbl) => {
559                w!(cx, f, "&")?;
560                if !cx.hide_regions {
561                    w!(cx, f, "{:?} ", re)?;
562                }
563                w!(cx, f, "{}{:?}",  ^mutbl.prefix_str(), ty)
564            }
565            BaseTy::FnPtr(poly_fn_sig) => {
566                w!(cx, f, "{:?}", poly_fn_sig)
567            }
568            BaseTy::Tuple(tys) => {
569                if let [ty] = &tys[..] {
570                    w!(cx, f, "({:?},)", ty)
571                } else {
572                    w!(cx, f, "({:?})", join!(", ", tys))
573                }
574            }
575            BaseTy::Alias(kind, alias_ty) => fmt_alias_ty(cx, f, *kind, alias_ty),
576            BaseTy::Array(ty, c) => w!(cx, f, "[{:?}; {:?}]", ty, ^c),
577            BaseTy::Never => w!(cx, f, "!"),
578            BaseTy::Closure(did, args, _) => {
579                w!(cx, f, "{:?}<{:?}>", did, args)
580            }
581            BaseTy::Coroutine(did, resume_ty, upvars) => {
582                w!(cx, f, "Coroutine({:?}, {:?})", did, resume_ty)?;
583                if !upvars.is_empty() {
584                    w!(cx, f, "<{:?}>", join!(", ", upvars))?;
585                }
586                Ok(())
587            }
588            BaseTy::Dynamic(preds, re) => {
589                w!(cx, f, "dyn {:?} + {:?}", join!(" + ", preds), re)
590            }
591            BaseTy::Infer(ty_vid) => {
592                w!(cx, f, "{ty_vid:?}")
593            }
594            BaseTy::Foreign(def_id) => {
595                w!(cx, f, "{:?}", def_id)
596            }
597        }
598    }
599}
600
601fn fmt_alias_ty(
602    cx: &PrettyCx,
603    f: &mut fmt::Formatter<'_>,
604    kind: AliasKind,
605    alias_ty: &AliasTy,
606) -> fmt::Result {
607    match kind {
608        AliasKind::Free => {
609            w!(cx, f, "{:?}", alias_ty.def_id)?;
610            if !alias_ty.args.is_empty() {
611                w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
612            }
613        }
614        AliasKind::Projection => {
615            let assoc_name = cx.tcx().item_name(alias_ty.def_id);
616            let trait_ref = cx.tcx().parent(alias_ty.def_id);
617            let trait_generic_count = cx.tcx().generics_of(trait_ref).count() - 1;
618
619            let [self_ty, args @ ..] = &alias_ty.args[..] else {
620                return w!(cx, f, "<alias_ty>");
621            };
622
623            w!(cx, f, "<{:?} as {:?}", self_ty, trait_ref)?;
624
625            let trait_generics = &args[..trait_generic_count];
626            if !trait_generics.is_empty() {
627                w!(cx, f, "<{:?}>", join!(", ", trait_generics))?;
628            }
629            w!(cx, f, ">::{}", ^assoc_name)?;
630
631            let assoc_generics = &args[trait_generic_count..];
632            if !assoc_generics.is_empty() {
633                w!(cx, f, "<{:?}>", join!(", ", assoc_generics))?;
634            }
635        }
636        AliasKind::Opaque => {
637            w!(cx, f, "{:?}", alias_ty.def_id)?;
638            if !alias_ty.args.is_empty() {
639                w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
640            }
641            if !alias_ty.refine_args.is_empty() {
642                w!(cx, f, "⟨{:?}⟩", join!(", ", &alias_ty.refine_args))?;
643            }
644        }
645    }
646    Ok(())
647}
648
649impl Pretty for ValTree {
650    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
651        match self {
652            ValTree::Leaf(v) => w!(cx, f, "Leaf({v:?})"),
653            ValTree::Branch(children) => {
654                w!(cx, f, "Branch([{:?}])", join!(", ", children))
655            }
656        }
657    }
658}
659impl Pretty for UnevaluatedConst {
660    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
661        w!(cx, f, "UnevaluatedConst({:?}[...])", self.def)
662    }
663}
664
665impl Pretty for Const {
666    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
667        match &self.kind {
668            ConstKind::Param(p) => w!(cx, f, "{}", ^p.name.as_str()),
669            ConstKind::Value(_, v) => w!(cx, f, "{v:?}"),
670            ConstKind::Infer(infer_const) => w!(cx, f, "{:?}", ^infer_const),
671            ConstKind::Unevaluated(uneval_const) => w!(cx, f, "{:?}", uneval_const),
672        }
673    }
674}
675
676impl Pretty for GenericArg {
677    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
678        match self {
679            GenericArg::Ty(ty) => w!(cx, f, "{:?}", ty),
680            GenericArg::Base(ctor) => w!(cx, f, "{:?}", ctor.to_ty()),
681            GenericArg::Lifetime(re) => w!(cx, f, "{:?}", re),
682            GenericArg::Const(c) => w!(cx, f, "{:?}", c),
683        }
684    }
685}
686
687impl Pretty for VariantSig {
688    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
689        w!(cx, f, "({:?}) => {:?}", join!(", ", self.fields()), &self.idx)
690    }
691}
692
693impl Pretty for Region {
694    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
695        w!(cx, f, "{}", ^region_to_string(*self))
696    }
697}
698
699impl Pretty for DebruijnIndex {
700    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
701        w!(cx, f, "^{}", ^self.as_usize())
702    }
703}
704
705impl_debug_with_default_cx!(
706    Ensures,
707    Sort,
708    Ty => "ty",
709    BaseTy,
710    FnSig,
711    GenericArg => "generic_arg",
712    VariantSig,
713    PtrKind,
714    FuncSort,
715    SortCtor,
716    SubsetTy,
717    BvSize,
718    ExistentialPredicate,
719);
720
721impl PrettyNested for SubsetTy {
722    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
723        let bty_d = self.bty.fmt_nested(cx)?;
724        let idx_d = IdxFmt(self.idx.clone()).fmt_nested(cx)?;
725        if self.pred.is_trivially_true() || matches!(self.pred.kind(), ExprKind::KVar(..)) {
726            let text = format!("{}[{}]", bty_d.text, idx_d.text);
727            let children = float_children(vec![bty_d.children, idx_d.children]);
728            Ok(NestedString { text, children, key: None })
729        } else {
730            let pred_d = self.pred.fmt_nested(cx)?;
731            let text = format!("{{ {}[{}] | {} }}", bty_d.text, idx_d.text, pred_d.text);
732            let children = float_children(vec![bty_d.children, idx_d.children, pred_d.children]);
733            Ok(NestedString { text, children, key: None })
734        }
735    }
736}
737
738impl PrettyNested for GenericArg {
739    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
740        match self {
741            GenericArg::Ty(ty) => ty.fmt_nested(cx),
742            GenericArg::Base(ctor) => {
743                // if ctor is of the form `λb. bty[b]`, just print the `bty`
744                let inner = ctor.as_ref().skip_binder();
745                if ctor.vars().len() == 1 && inner.pred.is_trivially_true() && inner.idx.is_nu() {
746                    inner.bty.fmt_nested(cx)
747                } else {
748                    nested_with_bound_vars(cx, "λ", ctor.vars(), None, |prefix| {
749                        let ctor_d = ctor.skip_binder_ref().fmt_nested(cx)?;
750                        let text = format!("{}{}", prefix, ctor_d.text);
751                        Ok(NestedString { text, children: ctor_d.children, key: None })
752                    })
753                }
754            }
755            GenericArg::Lifetime(..) | GenericArg::Const(..) => debug_nested(cx, self),
756        }
757    }
758}
759
760impl PrettyNested for BaseTy {
761    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
762        match self {
763            BaseTy::Int(..)
764            | BaseTy::Uint(..)
765            | BaseTy::Bool
766            | BaseTy::Str
767            | BaseTy::Char
768            | BaseTy::Float(..)
769            | BaseTy::Param(..)
770            | BaseTy::Never
771            | BaseTy::FnPtr(..)
772            | BaseTy::FnDef(..)
773            | BaseTy::Alias(..)
774            | BaseTy::Closure(..)
775            | BaseTy::Coroutine(..)
776            | BaseTy::Dynamic(..)
777            | BaseTy::Infer(..)
778            | BaseTy::Foreign(..) => {
779                let text = format_cx!(cx, "{:?}", self);
780                Ok(NestedString { text, children: None, key: None })
781            }
782            BaseTy::Slice(ty) => {
783                let ty_d = ty.fmt_nested(cx)?;
784                let text = format!("[{}]", ty_d.text);
785                Ok(NestedString { text, children: ty_d.children, key: None })
786            }
787            BaseTy::Array(ty, c) => {
788                let ty_d = ty.fmt_nested(cx)?;
789                let text = format_cx!(cx, "[{:?}; {:?}]", ty_d.text, c);
790                Ok(NestedString { text, children: ty_d.children, key: None })
791            }
792            BaseTy::RawPtr(ty, Mutability::Mut) => {
793                let ty_d = ty.fmt_nested(cx)?;
794                let text = format!("*mut {}", ty_d.text);
795                Ok(NestedString { text, children: ty_d.children, key: None })
796            }
797            BaseTy::RawPtr(ty, Mutability::Not) => {
798                let ty_d = ty.fmt_nested(cx)?;
799                let text = format!("*const {}", ty_d.text);
800                Ok(NestedString { text, children: ty_d.children, key: None })
801            }
802            BaseTy::RawPtrMetadata(ty) => {
803                let ty_d = ty.fmt_nested(cx)?;
804                let text = format!("*raw {}", ty_d.text);
805                Ok(NestedString { text, children: ty_d.children, key: None })
806            }
807            BaseTy::Ref(_, ty, mutbl) => {
808                let ty_d = ty.fmt_nested(cx)?;
809                let prefix = mutbl.prefix_str();
810                let text = if prefix.is_empty() {
811                    format!("&{}", ty_d.text)
812                } else {
813                    format!("&{} {}", prefix, ty_d.text)
814                };
815                Ok(NestedString { text, children: ty_d.children, key: None })
816            }
817            BaseTy::Tuple(tys) => {
818                let mut texts = vec![];
819                let mut kidss = vec![];
820                for ty in tys {
821                    let ty_d = ty.fmt_nested(cx)?;
822                    texts.push(ty_d.text);
823                    kidss.push(ty_d.children);
824                }
825                let text = if let [text] = &texts[..] {
826                    format!("({text},)")
827                } else {
828                    format!("({})", texts.join(", "))
829                };
830                let children = float_children(kidss);
831                Ok(NestedString { text, children, key: None })
832            }
833            BaseTy::Adt(adt_def, args) => {
834                let mut texts = vec![];
835                let mut kidss = vec![];
836                for arg in args {
837                    let arg_d = arg.fmt_nested(cx)?;
838                    texts.push(arg_d.text);
839                    kidss.push(arg_d.children);
840                }
841                let args_str = if !args.is_empty() {
842                    format!("<{}>", texts.join(", "))
843                } else {
844                    String::new()
845                };
846                let text = format_cx!(cx, "{:?}{:?}", adt_def.did(), args_str);
847                let children = float_children(kidss);
848                Ok(NestedString { text, children, key: None })
849            }
850        }
851    }
852}
853
854pub fn nested_with_bound_vars(
855    cx: &PrettyCx,
856    left: &str,
857    vars: &[BoundVariableKind],
858    right: Option<String>,
859    f: impl FnOnce(String) -> Result<NestedString, fmt::Error>,
860) -> Result<NestedString, fmt::Error> {
861    let mut buffer = String::new();
862    cx.with_bound_vars(vars, || {
863        if !vars.is_empty() {
864            let right = right.unwrap_or(". ".to_string());
865            cx.fmt_bound_vars(false, left, vars, &right, &mut buffer)?;
866        }
867        f(buffer)
868    })
869}
870
871impl PrettyNested for Ty {
872    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
873        match self.kind() {
874            TyKind::Indexed(bty, idx) => {
875                let bty_d = bty.fmt_nested(cx)?;
876                let idx_d = IdxFmt(idx.clone()).fmt_nested(cx)?;
877                let text = if idx_d.text.is_empty() {
878                    bty_d.text
879                } else {
880                    format!("{}[{}]", bty_d.text, idx_d.text)
881                };
882                let children = float_children(vec![bty_d.children, idx_d.children]);
883                Ok(NestedString { text, children, key: None })
884            }
885            TyKind::Exists(ty_ctor) => {
886                // TODO: remove redundant vars; see Ty
887                // if ctor is of the form `∃b. bty[b]`, just print the `bty`
888                if ty_ctor.vars().len() == 1
889                    && let TyKind::Indexed(bty, idx) = ty_ctor.skip_binder_ref().kind()
890                    && idx.is_nu()
891                {
892                    bty.fmt_nested(cx)
893                } else {
894                    nested_with_bound_vars(cx, "∃", ty_ctor.vars(), None, |exi_str| {
895                        let ty_ctor_d = ty_ctor.skip_binder_ref().fmt_nested(cx)?;
896                        let text = format!("{}{}", exi_str, ty_ctor_d.text);
897                        Ok(NestedString { text, children: ty_ctor_d.children, key: None })
898                    })
899                }
900            }
901            TyKind::Constr(expr, ty) => {
902                let expr_d = expr.fmt_nested(cx)?;
903                let ty_d = ty.fmt_nested(cx)?;
904                let text = format!("{{ {} | {} }}", ty_d.text, expr_d.text);
905                let children = float_children(vec![expr_d.children, ty_d.children]);
906                Ok(NestedString { text, children, key: None })
907            }
908            TyKind::StrgRef(re, loc, ty) => {
909                let ty_d = ty.fmt_nested(cx)?;
910                let text = format!("&{:?} strg <{:?}: {}>", re, loc, ty_d.text);
911                Ok(NestedString { text, children: ty_d.children, key: None })
912            }
913            TyKind::Blocked(ty) => {
914                let ty_d = ty.fmt_nested(cx)?;
915                let text = format!("†{}", ty_d.text);
916                Ok(NestedString { text, children: ty_d.children, key: None })
917            }
918            TyKind::Downcast(adt, .., variant_idx, fields) => {
919                let is_struct = adt.is_struct();
920                let mut text = format_cx!(cx, "{:?}", adt.did());
921                if !is_struct {
922                    text.push_str(&format!("::{}", adt.variant(*variant_idx).name));
923                }
924                if is_struct {
925                    text.push_str("{..}");
926                } else {
927                    text.push_str("(..)");
928                }
929                let keys: Vec<String> = if is_struct {
930                    adt.variant(*variant_idx)
931                        .fields
932                        .iter()
933                        .map(|f| f.name.to_string())
934                        .collect()
935                } else {
936                    (0..fields.len()).map(|i| format!("{i}")).collect()
937                };
938                let mut children = vec![];
939                for (key, field) in keys.into_iter().zip(fields) {
940                    let field_d = field.fmt_nested(cx)?;
941                    children.push(NestedString { key: Some(key), ..field_d });
942                }
943                Ok(NestedString { text, children: Some(children), key: None })
944            }
945            TyKind::Param(..)
946            | TyKind::Uninit
947            | TyKind::Ptr(..)
948            | TyKind::Discr(..)
949            | TyKind::Infer(..) => {
950                let text = format!("{self:?}");
951                Ok(NestedString { text, children: None, key: None })
952            }
953        }
954    }
955}
flux_middle/rty/pretty.rs

flux_middle/rty/
pretty.rs
