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            BaseTy::Pat => todo!(),
599        }
600    }
601}
602
603fn fmt_alias_ty(
604    cx: &PrettyCx,
605    f: &mut fmt::Formatter<'_>,
606    kind: AliasKind,
607    alias_ty: &AliasTy,
608) -> fmt::Result {
609    match kind {
610        AliasKind::Free => {
611            w!(cx, f, "{:?}", alias_ty.def_id)?;
612            if !alias_ty.args.is_empty() {
613                w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
614            }
615        }
616        AliasKind::Projection => {
617            let assoc_name = cx.tcx().item_name(alias_ty.def_id);
618            let trait_ref = cx.tcx().parent(alias_ty.def_id);
619            let trait_generic_count = cx.tcx().generics_of(trait_ref).count() - 1;
620
621            let [self_ty, args @ ..] = &alias_ty.args[..] else {
622                return w!(cx, f, "<alias_ty>");
623            };
624
625            w!(cx, f, "<{:?} as {:?}", self_ty, trait_ref)?;
626
627            let trait_generics = &args[..trait_generic_count];
628            if !trait_generics.is_empty() {
629                w!(cx, f, "<{:?}>", join!(", ", trait_generics))?;
630            }
631            w!(cx, f, ">::{}", ^assoc_name)?;
632
633            let assoc_generics = &args[trait_generic_count..];
634            if !assoc_generics.is_empty() {
635                w!(cx, f, "<{:?}>", join!(", ", assoc_generics))?;
636            }
637        }
638        AliasKind::Opaque => {
639            w!(cx, f, "{:?}", alias_ty.def_id)?;
640            if !alias_ty.args.is_empty() {
641                w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
642            }
643            if !alias_ty.refine_args.is_empty() {
644                w!(cx, f, "⟨{:?}⟩", join!(", ", &alias_ty.refine_args))?;
645            }
646        }
647    }
648    Ok(())
649}
650
651impl Pretty for ValTree {
652    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
653        match self {
654            ValTree::Leaf(v) => w!(cx, f, "Leaf({v:?})"),
655            ValTree::Branch(children) => {
656                w!(cx, f, "Branch([{:?}])", join!(", ", children))
657            }
658        }
659    }
660}
661impl Pretty for UnevaluatedConst {
662    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
663        w!(cx, f, "UnevaluatedConst({:?}[...])", self.def)
664    }
665}
666
667impl Pretty for Const {
668    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
669        match &self.kind {
670            ConstKind::Param(p) => w!(cx, f, "{}", ^p.name.as_str()),
671            ConstKind::Value(_, v) => w!(cx, f, "{v:?}"),
672            ConstKind::Infer(infer_const) => w!(cx, f, "{:?}", ^infer_const),
673            ConstKind::Unevaluated(uneval_const) => w!(cx, f, "{:?}", uneval_const),
674        }
675    }
676}
677
678impl Pretty for GenericArg {
679    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
680        match self {
681            GenericArg::Ty(ty) => w!(cx, f, "{:?}", ty),
682            GenericArg::Base(ctor) => w!(cx, f, "{:?}", ctor.to_ty()),
683            GenericArg::Lifetime(re) => w!(cx, f, "{:?}", re),
684            GenericArg::Const(c) => w!(cx, f, "{:?}", c),
685        }
686    }
687}
688
689impl Pretty for VariantSig {
690    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
691        w!(cx, f, "({:?}) => {:?}", join!(", ", self.fields()), &self.idx)
692    }
693}
694
695impl Pretty for Region {
696    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
697        w!(cx, f, "{}", ^region_to_string(*self))
698    }
699}
700
701impl Pretty for DebruijnIndex {
702    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
703        w!(cx, f, "^{}", ^self.as_usize())
704    }
705}
706
707impl_debug_with_default_cx!(
708    Ensures,
709    Sort,
710    Ty => "ty",
711    BaseTy,
712    FnSig,
713    GenericArg => "generic_arg",
714    VariantSig,
715    PtrKind,
716    FuncSort,
717    SortCtor,
718    SubsetTy,
719    BvSize,
720    ExistentialPredicate,
721);
722
723impl PrettyNested for SubsetTy {
724    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
725        let bty_d = self.bty.fmt_nested(cx)?;
726        let idx_d = IdxFmt(self.idx.clone()).fmt_nested(cx)?;
727        if self.pred.is_trivially_true() || matches!(self.pred.kind(), ExprKind::KVar(..)) {
728            let text = format!("{}[{}]", bty_d.text, idx_d.text);
729            let children = float_children(vec![bty_d.children, idx_d.children]);
730            Ok(NestedString { text, children, key: None })
731        } else {
732            let pred_d = self.pred.fmt_nested(cx)?;
733            let text = format!("{{ {}[{}] | {} }}", bty_d.text, idx_d.text, pred_d.text);
734            let children = float_children(vec![bty_d.children, idx_d.children, pred_d.children]);
735            Ok(NestedString { text, children, key: None })
736        }
737    }
738}
739
740impl PrettyNested for GenericArg {
741    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
742        match self {
743            GenericArg::Ty(ty) => ty.fmt_nested(cx),
744            GenericArg::Base(ctor) => {
745                // if ctor is of the form `λb. bty[b]`, just print the `bty`
746                let inner = ctor.as_ref().skip_binder();
747                if ctor.vars().len() == 1 && inner.pred.is_trivially_true() && inner.idx.is_nu() {
748                    inner.bty.fmt_nested(cx)
749                } else {
750                    cx.nested_with_bound_vars("λ", ctor.vars(), None, |prefix| {
751                        let ctor_d = ctor.skip_binder_ref().fmt_nested(cx)?;
752                        let text = format!("{}{}", prefix, ctor_d.text);
753                        Ok(NestedString { text, children: ctor_d.children, key: None })
754                    })
755                }
756            }
757            GenericArg::Lifetime(..) | GenericArg::Const(..) => debug_nested(cx, self),
758        }
759    }
760}
761
762impl PrettyNested for BaseTy {
763    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
764        match self {
765            BaseTy::Int(..)
766            | BaseTy::Uint(..)
767            | BaseTy::Bool
768            | BaseTy::Str
769            | BaseTy::Char
770            | BaseTy::Float(..)
771            | BaseTy::Param(..)
772            | BaseTy::Never
773            | BaseTy::FnPtr(..)
774            | BaseTy::FnDef(..)
775            | BaseTy::Alias(..)
776            | BaseTy::Closure(..)
777            | BaseTy::Coroutine(..)
778            | BaseTy::Dynamic(..)
779            | BaseTy::Infer(..)
780            | BaseTy::Foreign(..) => {
781                let text = format_cx!(cx, "{:?}", self);
782                Ok(NestedString { text, children: None, key: None })
783            }
784            BaseTy::Slice(ty) => {
785                let ty_d = ty.fmt_nested(cx)?;
786                let text = format!("[{}]", ty_d.text);
787                Ok(NestedString { text, children: ty_d.children, key: None })
788            }
789            BaseTy::Array(ty, c) => {
790                let ty_d = ty.fmt_nested(cx)?;
791                let text = format_cx!(cx, "[{:?}; {:?}]", ty_d.text, c);
792                Ok(NestedString { text, children: ty_d.children, key: None })
793            }
794            BaseTy::RawPtr(ty, Mutability::Mut) => {
795                let ty_d = ty.fmt_nested(cx)?;
796                let text = format!("*mut {}", ty_d.text);
797                Ok(NestedString { text, children: ty_d.children, key: None })
798            }
799            BaseTy::RawPtr(ty, Mutability::Not) => {
800                let ty_d = ty.fmt_nested(cx)?;
801                let text = format!("*const {}", ty_d.text);
802                Ok(NestedString { text, children: ty_d.children, key: None })
803            }
804            BaseTy::RawPtrMetadata(ty) => {
805                let ty_d = ty.fmt_nested(cx)?;
806                let text = format!("*raw {}", ty_d.text);
807                Ok(NestedString { text, children: ty_d.children, key: None })
808            }
809            BaseTy::Ref(_, ty, mutbl) => {
810                let ty_d = ty.fmt_nested(cx)?;
811                let prefix = mutbl.prefix_str();
812                let text = if prefix.is_empty() {
813                    format!("&{}", ty_d.text)
814                } else {
815                    format!("&{} {}", prefix, ty_d.text)
816                };
817                Ok(NestedString { text, children: ty_d.children, key: None })
818            }
819            BaseTy::Tuple(tys) => {
820                let mut texts = vec![];
821                let mut kidss = vec![];
822                for ty in tys {
823                    let ty_d = ty.fmt_nested(cx)?;
824                    texts.push(ty_d.text);
825                    kidss.push(ty_d.children);
826                }
827                let text = if let [text] = &texts[..] {
828                    format!("({text},)")
829                } else {
830                    format!("({})", texts.join(", "))
831                };
832                let children = float_children(kidss);
833                Ok(NestedString { text, children, key: None })
834            }
835            BaseTy::Adt(adt_def, args) => {
836                let mut texts = vec![];
837                let mut kidss = vec![];
838                for arg in args {
839                    let arg_d = arg.fmt_nested(cx)?;
840                    texts.push(arg_d.text);
841                    kidss.push(arg_d.children);
842                }
843                let args_str = if !args.is_empty() {
844                    format!("<{}>", texts.join(", "))
845                } else {
846                    String::new()
847                };
848                let text = format_cx!(cx, "{:?}{:?}", adt_def.did(), args_str);
849                let children = float_children(kidss);
850                Ok(NestedString { text, children, key: None })
851            }
852            BaseTy::Pat => todo!(),
853        }
854    }
855}
856
857impl PrettyNested for Ty {
858    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
859        match self.kind() {
860            TyKind::Indexed(bty, idx) => {
861                let bty_d = bty.fmt_nested(cx)?;
862                let idx_d = IdxFmt(idx.clone()).fmt_nested(cx)?;
863                let text = if idx_d.text.is_empty() {
864                    bty_d.text
865                } else {
866                    format!("{}[{}]", bty_d.text, idx_d.text)
867                };
868                let children = float_children(vec![bty_d.children, idx_d.children]);
869                Ok(NestedString { text, children, key: None })
870            }
871            TyKind::Exists(ty_ctor) => {
872                // TODO: remove redundant vars; see Ty
873                // if ctor is of the form `∃b. bty[b]`, just print the `bty`
874                if ty_ctor.vars().len() == 1
875                    && let TyKind::Indexed(bty, idx) = ty_ctor.skip_binder_ref().kind()
876                    && idx.is_nu()
877                {
878                    bty.fmt_nested(cx)
879                } else {
880                    cx.nested_with_bound_vars("∃", ty_ctor.vars(), None, |exi_str| {
881                        let ty_ctor_d = ty_ctor.skip_binder_ref().fmt_nested(cx)?;
882                        let text = format!("{}{}", exi_str, ty_ctor_d.text);
883                        Ok(NestedString { text, children: ty_ctor_d.children, key: None })
884                    })
885                }
886            }
887            TyKind::Constr(expr, ty) => {
888                let expr_d = expr.fmt_nested(cx)?;
889                let ty_d = ty.fmt_nested(cx)?;
890                let text = format!("{{ {} | {} }}", ty_d.text, expr_d.text);
891                let children = float_children(vec![expr_d.children, ty_d.children]);
892                Ok(NestedString { text, children, key: None })
893            }
894            TyKind::StrgRef(re, loc, ty) => {
895                let ty_d = ty.fmt_nested(cx)?;
896                let text = format!("&{:?} strg <{:?}: {}>", re, loc, ty_d.text);
897                Ok(NestedString { text, children: ty_d.children, key: None })
898            }
899            TyKind::Blocked(ty) => {
900                let ty_d = ty.fmt_nested(cx)?;
901                let text = format!("†{}", ty_d.text);
902                Ok(NestedString { text, children: ty_d.children, key: None })
903            }
904            TyKind::Downcast(adt, .., variant_idx, fields) => {
905                let is_struct = adt.is_struct();
906                let mut text = format_cx!(cx, "{:?}", adt.did());
907                if !is_struct {
908                    text.push_str(&format!("::{}", adt.variant(*variant_idx).name));
909                }
910                if is_struct {
911                    text.push_str("{..}");
912                } else {
913                    text.push_str("(..)");
914                }
915                let keys: Vec<String> = if is_struct {
916                    adt.variant(*variant_idx)
917                        .fields
918                        .iter()
919                        .map(|f| f.name.to_string())
920                        .collect()
921                } else {
922                    (0..fields.len()).map(|i| format!("{i}")).collect()
923                };
924                let mut children = vec![];
925                for (key, field) in keys.into_iter().zip(fields) {
926                    let field_d = field.fmt_nested(cx)?;
927                    children.push(NestedString { key: Some(key), ..field_d });
928                }
929                Ok(NestedString { text, children: Some(children), key: None })
930            }
931            TyKind::Param(..)
932            | TyKind::Uninit
933            | TyKind::Ptr(..)
934            | TyKind::Discr(..)
935            | TyKind::Infer(..) => {
936                let text = format!("{self:?}");
937                Ok(NestedString { text, children: None, key: None })
938            }
939        }
940    }
941}
flux_middle/rty/pretty.rs

flux_middle/rty/
pretty.rs
