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

flux_middle/rty/
pretty.rs
