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 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) => {
443                w!(cx, f, "discr({:?}, {:?})", adt_def.did(), ^place)
444            }
445            TyKind::Constr(pred, ty) => {
446                if cx.hide_refinements {
447                    w!(cx, f, "{:?}", ty)
448                } else {
449                    w!(cx, f, "{{ {:?} | {:?} }}", ty, pred)
450                }
451            }
452            TyKind::Param(param_ty) => w!(cx, f, "{}", ^param_ty),
453            TyKind::Downcast(adt, .., variant_idx, fields) => {
454                // base-name
455                w!(cx, f, "{:?}", adt.did())?;
456                // variant-name: if it is not a struct
457                if !adt.is_struct() {
458                    w!(cx, f, "::{}", ^adt.variant(*variant_idx).name)?;
459                }
460                // fields: use curly-braces + names for structs, otherwise use parens
461                if adt.is_struct() {
462                    let field_binds = iter::zip(&adt.variant(*variant_idx).fields, fields)
463                        .map(|(field_def, value)| FieldBind { name: field_def.name, value });
464                    w!(cx, f, " {{ {:?} }}", join!(", ", field_binds))?;
465                } else if !fields.is_empty() {
466                    w!(cx, f, "({:?})", join!(", ", fields))?;
467                }
468                Ok(())
469            }
470            TyKind::Blocked(ty) => w!(cx, f, "†{:?}", ty),
471            TyKind::Infer(ty_vid) => {
472                w!(cx, f, "{ty_vid:?}")
473            }
474        }
475    }
476
477    fn default_cx(tcx: TyCtxt) -> PrettyCx {
478        PrettyCx::default(tcx).kvar_args(KVarArgs::Hide)
479    }
480}
481
482impl Pretty for PtrKind {
483    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
484        match self {
485            PtrKind::Mut(re) => {
486                w!(cx, f, "mut")?;
487                if !cx.hide_regions {
488                    w!(cx, f, "[{:?}]", re)?;
489                }
490                Ok(())
491            }
492            PtrKind::Box => w!(cx, f, "box"),
493        }
494    }
495}
496
497impl Pretty for List<Ty> {
498    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
499        if let [ty] = &self[..] {
500            w!(cx, f, "({:?},)", ty)
501        } else {
502            w!(cx, f, "({:?})", join!(", ", self))
503        }
504    }
505}
506
507impl Pretty for ExistentialPredicate {
508    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
509        match self {
510            ExistentialPredicate::Trait(trait_ref) => w!(cx, f, "{:?}", trait_ref),
511            ExistentialPredicate::Projection(proj) => w!(cx, f, "({:?})", proj),
512            ExistentialPredicate::AutoTrait(def_id) => w!(cx, f, "{:?}", def_id),
513        }
514    }
515}
516
517impl Pretty for ExistentialTraitRef {
518    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
519        w!(cx, f, "{:?}", self.def_id)?;
520        if !self.args.is_empty() {
521            w!(cx, f, "<{:?}>", join!(", ", &self.args))?;
522        }
523        Ok(())
524    }
525}
526
527impl Pretty for ExistentialProjection {
528    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
529        w!(cx, f, "{:?}", self.def_id)?;
530        if !self.args.is_empty() {
531            w!(cx, f, "<{:?}>", join!(", ", &self.args))?;
532        }
533        w!(cx, f, " = {:?}", &self.term)
534    }
535}
536
537impl Pretty for BaseTy {
538    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
539        match self {
540            BaseTy::Int(int_ty) => w!(cx, f, "{}", ^int_ty.name_str()),
541            BaseTy::Uint(uint_ty) => w!(cx, f, "{}", ^uint_ty.name_str()),
542            BaseTy::Bool => w!(cx, f, "bool"),
543            BaseTy::Str => w!(cx, f, "str"),
544            BaseTy::Char => w!(cx, f, "char"),
545            BaseTy::Adt(adt_def, args) => {
546                w!(cx, f, "{:?}", adt_def.did())?;
547                let args = args
548                    .iter()
549                    .filter(|arg| !cx.hide_regions || !matches!(arg, GenericArg::Lifetime(_)))
550                    .collect_vec();
551                if !args.is_empty() {
552                    w!(cx, f, "<{:?}>", join!(", ", args))?;
553                }
554                Ok(())
555            }
556            BaseTy::FnDef(def_id, args) => {
557                w!(cx, f, "FnDef({:?}[{:?}])", def_id, join!(", ", args))
558            }
559            BaseTy::Param(param) => w!(cx, f, "{}", ^param),
560            BaseTy::Float(float_ty) => w!(cx, f, "{}", ^float_ty.name_str()),
561            BaseTy::Slice(ty) => w!(cx, f, "[{:?}]", ty),
562            BaseTy::RawPtr(ty, Mutability::Mut) => w!(cx, f, "*mut {:?}", ty),
563            BaseTy::RawPtr(ty, Mutability::Not) => w!(cx, f, "*const {:?}", ty),
564            BaseTy::RawPtrMetadata(ty) => {
565                w!(cx, f, "*raw {:?}", ty)
566            }
567            BaseTy::Ref(re, ty, mutbl) => {
568                w!(cx, f, "&")?;
569                if !cx.hide_regions {
570                    w!(cx, f, "{:?} ", re)?;
571                }
572                w!(cx, f, "{}{:?}",  ^mutbl.prefix_str(), ty)
573            }
574            BaseTy::FnPtr(poly_fn_sig) => {
575                w!(cx, f, "{:?}", poly_fn_sig)
576            }
577            BaseTy::Tuple(tys) => {
578                if let [ty] = &tys[..] {
579                    w!(cx, f, "({:?},)", ty)
580                } else {
581                    w!(cx, f, "({:?})", join!(", ", tys))
582                }
583            }
584            BaseTy::Alias(kind, alias_ty) => fmt_alias_ty(cx, f, *kind, alias_ty),
585            BaseTy::Array(ty, c) => w!(cx, f, "[{:?}; {:?}]", ty, ^c),
586            BaseTy::Never => w!(cx, f, "!"),
587            BaseTy::Closure(did, args, _) => {
588                w!(cx, f, "{:?}<{:?}>", did, args)
589            }
590            BaseTy::Coroutine(did, resume_ty, upvars) => {
591                w!(cx, f, "Coroutine({:?}, {:?})", did, resume_ty)?;
592                if !upvars.is_empty() {
593                    w!(cx, f, "<{:?}>", join!(", ", upvars))?;
594                }
595                Ok(())
596            }
597            BaseTy::Dynamic(preds, re) => {
598                w!(cx, f, "dyn {:?} + {:?}", join!(" + ", preds), re)
599            }
600            BaseTy::Infer(ty_vid) => {
601                w!(cx, f, "{ty_vid:?}")
602            }
603            BaseTy::Foreign(def_id) => {
604                w!(cx, f, "{:?}", def_id)
605            }
606        }
607    }
608}
609
610fn fmt_alias_ty(
611    cx: &PrettyCx,
612    f: &mut fmt::Formatter<'_>,
613    kind: AliasKind,
614    alias_ty: &AliasTy,
615) -> fmt::Result {
616    match kind {
617        AliasKind::Free => {
618            w!(cx, f, "{:?}", alias_ty.def_id)?;
619            if !alias_ty.args.is_empty() {
620                w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
621            }
622        }
623        AliasKind::Projection => {
624            let assoc_name = cx.tcx().item_name(alias_ty.def_id);
625            let trait_ref = cx.tcx().parent(alias_ty.def_id);
626            let trait_generic_count = cx.tcx().generics_of(trait_ref).count() - 1;
627
628            let [self_ty, args @ ..] = &alias_ty.args[..] else {
629                return w!(cx, f, "<alias_ty>");
630            };
631
632            w!(cx, f, "<{:?} as {:?}", self_ty, trait_ref)?;
633
634            let trait_generics = &args[..trait_generic_count];
635            if !trait_generics.is_empty() {
636                w!(cx, f, "<{:?}>", join!(", ", trait_generics))?;
637            }
638            w!(cx, f, ">::{}", ^assoc_name)?;
639
640            let assoc_generics = &args[trait_generic_count..];
641            if !assoc_generics.is_empty() {
642                w!(cx, f, "<{:?}>", join!(", ", assoc_generics))?;
643            }
644        }
645        AliasKind::Opaque => {
646            w!(cx, f, "{:?}", alias_ty.def_id)?;
647            if !alias_ty.args.is_empty() {
648                w!(cx, f, "<{:?}>", join!(", ", &alias_ty.args))?;
649            }
650            if !alias_ty.refine_args.is_empty() {
651                w!(cx, f, "⟨{:?}⟩", join!(", ", &alias_ty.refine_args))?;
652            }
653        }
654    }
655    Ok(())
656}
657
658impl Pretty for ValTree {
659    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
660        match self {
661            ValTree::Leaf(v) => w!(cx, f, "Leaf({v:?})"),
662            ValTree::Branch(children) => {
663                w!(cx, f, "Branch([{:?}])", join!(", ", children))
664            }
665        }
666    }
667}
668impl Pretty for UnevaluatedConst {
669    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
670        w!(cx, f, "UnevaluatedConst({:?}[...])", self.def)
671    }
672}
673
674impl Pretty for Const {
675    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
676        match &self.kind {
677            ConstKind::Param(p) => w!(cx, f, "{}", ^p.name.as_str()),
678            ConstKind::Value(_, v) => w!(cx, f, "{v:?}"),
679            ConstKind::Infer(infer_const) => w!(cx, f, "{:?}", ^infer_const),
680            ConstKind::Unevaluated(uneval_const) => w!(cx, f, "{:?}", uneval_const),
681        }
682    }
683}
684
685impl Pretty for GenericArg {
686    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
687        match self {
688            GenericArg::Ty(ty) => w!(cx, f, "{:?}", ty),
689            GenericArg::Base(ctor) => w!(cx, f, "{:?}", ctor.to_ty()),
690            GenericArg::Lifetime(re) => w!(cx, f, "{:?}", re),
691            GenericArg::Const(c) => w!(cx, f, "{:?}", c),
692        }
693    }
694}
695
696impl Pretty for VariantSig {
697    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
698        w!(cx, f, "({:?}) => {:?}", join!(", ", self.fields()), &self.idx)
699    }
700}
701
702impl Pretty for Region {
703    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
704        w!(cx, f, "{}", ^region_to_string(*self))
705    }
706}
707
708impl Pretty for DebruijnIndex {
709    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
710        w!(cx, f, "^{}", ^self.as_usize())
711    }
712}
713
714impl_debug_with_default_cx!(
715    Ensures,
716    Sort,
717    Ty => "ty",
718    BaseTy,
719    FnSig,
720    GenericArg => "generic_arg",
721    VariantSig,
722    PtrKind,
723    FuncSort,
724    SortCtor,
725    SubsetTy,
726    BvSize,
727    ExistentialPredicate,
728);
729
730impl PrettyNested for SubsetTy {
731    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
732        let bty_d = self.bty.fmt_nested(cx)?;
733        let idx_d = IdxFmt(self.idx.clone()).fmt_nested(cx)?;
734        if self.pred.is_trivially_true() || matches!(self.pred.kind(), ExprKind::KVar(..)) {
735            let text = format!("{}[{}]", bty_d.text, idx_d.text);
736            let children = float_children(vec![bty_d.children, idx_d.children]);
737            Ok(NestedString { text, children, key: None })
738        } else {
739            let pred_d = self.pred.fmt_nested(cx)?;
740            let text = format!("{{ {}[{}] | {} }}", bty_d.text, idx_d.text, pred_d.text);
741            let children = float_children(vec![bty_d.children, idx_d.children, pred_d.children]);
742            Ok(NestedString { text, children, key: None })
743        }
744    }
745}
746
747impl PrettyNested for GenericArg {
748    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
749        match self {
750            GenericArg::Ty(ty) => ty.fmt_nested(cx),
751            GenericArg::Base(ctor) => {
752                // if ctor is of the form `λb. bty[b]`, just print the `bty`
753                let inner = ctor.as_ref().skip_binder();
754                if ctor.vars().len() == 1 && inner.pred.is_trivially_true() && inner.idx.is_nu() {
755                    inner.bty.fmt_nested(cx)
756                } else {
757                    nested_with_bound_vars(cx, "λ", ctor.vars(), None, |prefix| {
758                        let ctor_d = ctor.skip_binder_ref().fmt_nested(cx)?;
759                        let text = format!("{}{}", prefix, ctor_d.text);
760                        Ok(NestedString { text, children: ctor_d.children, key: None })
761                    })
762                }
763            }
764            GenericArg::Lifetime(..) | GenericArg::Const(..) => debug_nested(cx, self),
765        }
766    }
767}
768
769impl PrettyNested for BaseTy {
770    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
771        match self {
772            BaseTy::Int(..)
773            | BaseTy::Uint(..)
774            | BaseTy::Bool
775            | BaseTy::Str
776            | BaseTy::Char
777            | BaseTy::Float(..)
778            | BaseTy::Param(..)
779            | BaseTy::Never
780            | BaseTy::FnPtr(..)
781            | BaseTy::FnDef(..)
782            | BaseTy::Alias(..)
783            | BaseTy::Closure(..)
784            | BaseTy::Coroutine(..)
785            | BaseTy::Dynamic(..)
786            | BaseTy::Infer(..)
787            | BaseTy::Foreign(..) => {
788                let text = format_cx!(cx, "{:?}", self);
789                Ok(NestedString { text, children: None, key: None })
790            }
791            BaseTy::Slice(ty) => {
792                let ty_d = ty.fmt_nested(cx)?;
793                let text = format!("[{}]", ty_d.text);
794                Ok(NestedString { text, children: ty_d.children, key: None })
795            }
796            BaseTy::Array(ty, c) => {
797                let ty_d = ty.fmt_nested(cx)?;
798                let text = format_cx!(cx, "[{:?}; {:?}]", ty_d.text, c);
799                Ok(NestedString { text, children: ty_d.children, key: None })
800            }
801            BaseTy::RawPtr(ty, Mutability::Mut) => {
802                let ty_d = ty.fmt_nested(cx)?;
803                let text = format!("*mut {}", ty_d.text);
804                Ok(NestedString { text, children: ty_d.children, key: None })
805            }
806            BaseTy::RawPtr(ty, Mutability::Not) => {
807                let ty_d = ty.fmt_nested(cx)?;
808                let text = format!("*const {}", ty_d.text);
809                Ok(NestedString { text, children: ty_d.children, key: None })
810            }
811            BaseTy::RawPtrMetadata(ty) => {
812                let ty_d = ty.fmt_nested(cx)?;
813                let text = format!("*raw {}", ty_d.text);
814                Ok(NestedString { text, children: ty_d.children, key: None })
815            }
816            BaseTy::Ref(_, ty, mutbl) => {
817                let ty_d = ty.fmt_nested(cx)?;
818                let prefix = mutbl.prefix_str();
819                let text = if prefix.is_empty() {
820                    format!("&{}", ty_d.text)
821                } else {
822                    format!("&{} {}", prefix, ty_d.text)
823                };
824                Ok(NestedString { text, children: ty_d.children, key: None })
825            }
826            BaseTy::Tuple(tys) => {
827                let mut texts = vec![];
828                let mut kidss = vec![];
829                for ty in tys {
830                    let ty_d = ty.fmt_nested(cx)?;
831                    texts.push(ty_d.text);
832                    kidss.push(ty_d.children);
833                }
834                let text = if let [text] = &texts[..] {
835                    format!("({text},)")
836                } else {
837                    format!("({})", texts.join(", "))
838                };
839                let children = float_children(kidss);
840                Ok(NestedString { text, children, key: None })
841            }
842            BaseTy::Adt(adt_def, args) => {
843                let mut texts = vec![];
844                let mut kidss = vec![];
845                for arg in args {
846                    let arg_d = arg.fmt_nested(cx)?;
847                    texts.push(arg_d.text);
848                    kidss.push(arg_d.children);
849                }
850                let args_str = if !args.is_empty() {
851                    format!("<{}>", texts.join(", "))
852                } else {
853                    String::new()
854                };
855                let text = format_cx!(cx, "{:?}{:?}", adt_def.did(), args_str);
856                let children = float_children(kidss);
857                Ok(NestedString { text, children, key: None })
858            }
859        }
860    }
861}
862
863pub fn nested_with_bound_vars(
864    cx: &PrettyCx,
865    left: &str,
866    vars: &[BoundVariableKind],
867    right: Option<String>,
868    f: impl FnOnce(String) -> Result<NestedString, fmt::Error>,
869) -> Result<NestedString, fmt::Error> {
870    let mut buffer = String::new();
871    cx.with_bound_vars(vars, || {
872        if !vars.is_empty() {
873            let right = right.unwrap_or(". ".to_string());
874            cx.fmt_bound_vars(false, left, vars, &right, &mut buffer)?;
875        }
876        f(buffer)
877    })
878}
879
880impl PrettyNested for Ty {
881    fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
882        match self.kind() {
883            TyKind::Indexed(bty, idx) => {
884                let bty_d = bty.fmt_nested(cx)?;
885                let idx_d = IdxFmt(idx.clone()).fmt_nested(cx)?;
886                let text = if idx_d.text.is_empty() {
887                    bty_d.text
888                } else {
889                    format!("{}[{}]", bty_d.text, idx_d.text)
890                };
891                let children = float_children(vec![bty_d.children, idx_d.children]);
892                Ok(NestedString { text, children, key: None })
893            }
894            TyKind::Exists(ty_ctor) => {
895                // TODO: remove redundant vars; see Ty
896                // if ctor is of the form `∃b. bty[b]`, just print the `bty`
897                if ty_ctor.vars().len() == 1
898                    && let TyKind::Indexed(bty, idx) = ty_ctor.skip_binder_ref().kind()
899                    && idx.is_nu()
900                {
901                    bty.fmt_nested(cx)
902                } else {
903                    nested_with_bound_vars(cx, "∃", ty_ctor.vars(), None, |exi_str| {
904                        let ty_ctor_d = ty_ctor.skip_binder_ref().fmt_nested(cx)?;
905                        let text = format!("{}{}", exi_str, ty_ctor_d.text);
906                        Ok(NestedString { text, children: ty_ctor_d.children, key: None })
907                    })
908                }
909            }
910            TyKind::Constr(expr, ty) => {
911                let expr_d = expr.fmt_nested(cx)?;
912                let ty_d = ty.fmt_nested(cx)?;
913                let text = format!("{{ {} | {} }}", ty_d.text, expr_d.text);
914                let children = float_children(vec![expr_d.children, ty_d.children]);
915                Ok(NestedString { text, children, key: None })
916            }
917            TyKind::StrgRef(re, loc, ty) => {
918                let ty_d = ty.fmt_nested(cx)?;
919                let text = format!("&{:?} strg <{:?}: {}>", re, loc, ty_d.text);
920                Ok(NestedString { text, children: ty_d.children, key: None })
921            }
922            TyKind::Blocked(ty) => {
923                let ty_d = ty.fmt_nested(cx)?;
924                let text = format!("†{}", ty_d.text);
925                Ok(NestedString { text, children: ty_d.children, key: None })
926            }
927            TyKind::Downcast(adt, .., variant_idx, fields) => {
928                let is_struct = adt.is_struct();
929                let mut text = format_cx!(cx, "{:?}", adt.did());
930                if !is_struct {
931                    text.push_str(&format!("::{}", adt.variant(*variant_idx).name));
932                }
933                if is_struct {
934                    text.push_str("{..}");
935                } else {
936                    text.push_str("(..)");
937                }
938                let keys: Vec<String> = if is_struct {
939                    adt.variant(*variant_idx)
940                        .fields
941                        .iter()
942                        .map(|f| f.name.to_string())
943                        .collect()
944                } else {
945                    (0..fields.len()).map(|i| format!("{i}")).collect()
946                };
947                let mut children = vec![];
948                for (key, field) in keys.into_iter().zip(fields) {
949                    let field_d = field.fmt_nested(cx)?;
950                    children.push(NestedString { key: Some(key), ..field_d });
951                }
952                Ok(NestedString { text, children: Some(children), key: None })
953            }
954            TyKind::Param(..)
955            | TyKind::Uninit
956            | TyKind::Ptr(..)
957            | TyKind::Discr(..)
958            | TyKind::Infer(..) => {
959                let text = format!("{self:?}");
960                Ok(NestedString { text, children: None, key: None })
961            }
962        }
963    }
964}
flux_middle/rty/pretty.rs

flux_middle/rty/
pretty.rs
