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

flux_middle/rty/
pretty.rs
